type class inference issues

Stream: general

[Floris van Doorn]

I have been struggling with type class inference lately. The two main issues are
(1) The error maximum class-instance resolution depth has been reached
(2) In some cases (which are hard to reproduce in minimal examples) I get incredibly long elaboration times (10-30 seconds for a single definition), and I suspect this is completely caused by type class inference (the eventual error I often get is that the type-class max depth is reached).

Problem 1 can be easily solved by setting the class.instance_max_depth option higher. Problem 2 makes this solution for problem 1 not that attractive, if type class inference then takes even longer.

I have some concrete and some open-ended questions:
Q.1 What does instance_max_depth exactly mean? Does it mean the depth/height of the search tree, or the total number of instances in the solution? For example, in the following example I have to set the depth to 125, with 124 it fails:

import ring_theory.algebra linear_algebra.tensor_product

variables {R : Type*} [comm_ring R]
variables {M : Type*} {N : Type*} [ring M] [ring N]
variables [algebra R M] [algebra R N]

local notation M ` ⊗[`:100 R `] ` N:100 := tensor_product R M N

namespace tensor_product
set_option class.instance_max_depth 125

protected def mul : M ⊗[R] N →ₗ[R] M ⊗[R] N →ₗ[R] M ⊗[R] N :=
begin
  refine tensor_product.lift ⟨λ m, ⟨λ n, _, _, _⟩, _, _⟩,
  all_goals { sorry }
end

Q.2 Does the option trace.class_instances show the complete trace or does Lean/VSCode truncate the trace somewhere? In traces where I get the max-depth reached error, the highest depth I can find is typically (11) or (12)
Q.3 In the trace, I see the same type class search over and over again (in a single definition). Is the caching of type class instances failing me, or is something else going on?
Q.4 What are type-class best practices? Do I want to add instances to short-circuit the type class inference? For example, in the example above, if I add the following local instances I don't have to increase the max depth at all:

protected def add_comm_group' : add_comm_group (M ⊗[R] N) := by apply_instance
protected def module' : module R (M ⊗[R] N) := by apply_instance
local attribute [instance, priority 2000] tensor_product.add_comm_group' tensor_product.module'
protected def lmap_add_comm_group : add_comm_group (M ⊗[R] N →ₗ[R] M ⊗[R] N) := by apply_instance
protected def lmap_module : module R (M ⊗[R] N →ₗ[R] M ⊗[R] N) := by apply_instance
local attribute [instance, priority 2000]
  tensor_product.lmap_add_comm_group tensor_product.lmap_module

Are there other tips/tricks to keep type-class inference happy/under control?

[Floris van Doorn]

PS: The reason for the example in Q.1 is that I'm surprised I would need to go to depth 100+.

[Floris van Doorn]

I just had another problem with type class inference.
I have an instance (with pp.all true):

_inst_3 : @is_ring_hom.{u_1 u_2} α β (@comm_ring.to_ring.{u_1} α _inst_1) (@comm_ring.to_ring.{u_2} β _inst_2) f

But the trace shows that this instance does not unify with its own type, even with pp.all true.

[class_instances] (0) ?x_9 : @is_ring_hom.{u_1 u_2} α β (@comm_ring.to_ring.{u_1} α _inst_1) (@comm_ring.to_ring.{u_2} β _inst_2) f := _inst_3
failed is_def_eq

The error occurs here:
https://github.com/fpvandoorn/formalabstracts/blob/is_ring_hom/src/ring_theory/basic.lean#L28

[Eric Rodriguez]

import algebra.order.ring

def foo (α) [has_lt α] [decidable_rel ((<) : α → α → Prop)] := 123

example {R} [linear_ordered_semiring R] := foo R --error

example {R} [h : linear_ordered_semiring R] :=
begin
  refine @foo R _ (show _, from _),
  exact (infer_instance : linear_order R).10,
end

what the hell is going on here?! it doesn't seem to be a diamond

[Eric Wieser]

(I never even considered that numeric dot notation supported double digits)

[Eric Wieser]

What's the error message?

[Eric Rodriguez]

it just cannot find the instance

[Eric Rodriguez]

it seens that linear_ordered_semiring.decidable_lt isn't an instance, but the linear_order version is and ther'es also clearly a linear_order instance, so it should be able to find it

[Anne Baanen]

If I enable trace.class_instances, then first of all it looks like linear_order.decidable_lt is not considered an instance. So I add that attribute and get the following trace:

[class_instances] (0) ?x_0 a b : decidable (a < b) := @linear_order.decidable_lt (?x_1 a b) (?x_2 a b) (?x_3 a b) (?x_4 a b)
failed is_def_eq
...

[Anne Baanen]

Looks like it's struggling with the problem:

@preorder.to_has_lt R
  (@partial_order.to_preorder R
     (@ordered_cancel_add_comm_monoid.to_partial_order R
        (@ordered_semiring.to_ordered_cancel_add_comm_monoid R (@linear_ordered_semiring.to_ordered_semiring R h)))) =?= @preorder.to_has_lt (?x_1 a b)
  (@partial_order.to_preorder (?x_1 a b)
     (@partial_order.mk (?x_1 a b) (@linear_order.le (?x_1 a b) (?x_2 a b)) (@linear_order.lt (?x_1 a b) (?x_2 a b)) _ _
        _
        _))

[Anne Baanen]

?x_2 a b should be inferred as the linear_order instance deriving from h : linear_ordered_semiring R, but apparently it's just being treated as opaque and never inferred.

[Anne Baanen]

Maybe this is the "pi instance bug" we've seen before with finsupp?