Possible bug in typeclass search

Stream: lean4

[Michael Stoll]

I'm moving this here from this thread, as it is not a Mathlib-specific problem.

To save you having to follow the link, here is the #mwe I posted there:

class A (α : Type) where

class B (α : Type) where

class C (α : Type) where

class D (α : Type) where

instance test (α : Type) [B α] [C α] : A α where

instance B_nat : B Nat where

instance DtoB (α : Type) [D α] : B α where

set_option trace.Meta.synthInstance true

#synth A Nat

which produces the fully expanded trace

[Meta.synthInstance] ❌ A Nat ▼
  [] new goal A Nat ▼
    [instances] #[test]
  [] ✅ apply test to A Nat ▼
    [tryResolve] ✅ A Nat ≟ A Nat
    [] new goal B Nat ▼
      [instances] #[DtoB, B_nat]
  [] ✅ apply B_nat to B Nat ▼
    [tryResolve] ✅ B Nat ≟ B Nat
  [resume] propagating B Nat to subgoal B Nat of A Nat ▼
    [] size: 1
    [] no instances for C Nat ▼
      [instances] #[]
------------------------------------
  [] ✅ apply DtoB to B Nat ▼
    [tryResolve] ✅ B Nat ≟ B Nat
    [] no instances for D Nat ▼
      [instances] #[]

(separation added).

As you can see, after an instance for B Nat is found, but none for C Nat, the instance search for B Nat continues (even though an instance is already known and test cannot possibly be used due to the lack of an instance for C Nat) -- this is the part of the trace below the separating line.

It looks to me like this is a bug and that fixing it will likely speed up Mathlib by a fairly large amount (see the thread linked above).

[Sébastien Gouëzel]

I agree that this is a strange behavior, and that it could have a very high performance impact. @Sebastian Ullrich, do you have some thoughts on this?

[Sebastian Ullrich]

Sorry, I'm not familiar enough with the algorithm or implementation to give a quick assessment here

[Michael Stoll]

Who would be the right person to ping here?

[Joachim Breitner]

Just guessing here, but maybe in general using a different instance for B Nat might instantiate some mvars differently, so with one instance the C Nat will fail, but with another instance it will succeeds? That would justify to continue the search.

It may be nontrivial to notice that the instances in test’s type are independent enough so that it’s not worth going back?

[Sébastien Gouëzel]

The design of typeclasses in mathlib (and in general in Lean, if I understand correctly) is that all instances should be the same, so if one instance fails all the other ones should also fail. That's not an intrinsic property of the system, but rather of the way we use the system. With this in mind, going back to see if another instance will succeed is just a waste of time everywhere throughout mathlib, and probably a very costly one.

[Floris van Doorn]

A related observation (which I also made in the mathlib thread:
In the Lean 3 community version, I believe we changed the order of search for arguments of instances, from left-to-right to right-to-left, i.e. when applying the instance test searching first for C α and only then for B α. The reason is that more constraining type-classes are generally the right-most typeclasses, so they will fail more quickly.

Was it a conscious decision in Lean 4 to do instance search from left-to-right?

[Matthew Ballard]

What is the performance cost (if any) in the synthesis step to trying the instance argument with the fewest available instances first?

[Michael Stoll]

If the behavior I observed is a consequence of a conscious design decision, maybe it would be possible to make it configurable (so that in Mathlib we could switch it off)?

[Michael Stoll]

Here is a variant:

class A where

class B where

class C where

class D where

class E where

instance test [B] [C] : A where

instance DtoB [D] : B where

instance EtoB [E] : B where

instance instB : B where

instance instE : E where

set_option trace.Meta.synthInstance true

#synth A

which gives

[Meta.synthInstance] ❌ A ▼
  [] new goal A ▼
    [instances] #[@test]
  [] ✅ apply @test to A ▼
    [tryResolve] ✅ A ≟ A
    [] new goal B ▼
      [instances] #[@DtoB, @EtoB, instB]
  [] ✅ apply instB to B ▼
    [tryResolve] ✅ B ≟ B
  [resume] propagating B to subgoal B of A ▼
    [] size: 1
    [] no instances for C ▼
      [instances] #[]
  [] ✅ apply @EtoB to B ▼
    [tryResolve] ✅ B ≟ B
    [] new goal E ▼
      [instances] #[instE]
  [] ✅ apply instE to E ▼
    [tryResolve] ✅ E ≟ E
  [resume] propagating E to subgoal E of B ▼
    [] size: 1
  [] ✅ apply @DtoB to B ▼
    [tryResolve] ✅ B ≟ B
    [] no instances for D ▼
      [instances] #[]

This shows that it even continues searching for B instances after it has found another one after backtracking. (Which explains the behavior we see in Mathlib, where the whole search tree is traversed in these cases).

[Michael Stoll]

I have made an issue: lean4#3996

[Yuyang Zhao]

I have observed many times that the same TC search seems to be attempted many times. But most of the examples are quite complex and difficult to make #mwe s. Maybe the examples in this thread are relevant.

[Michael Stoll]

Is there any chance one could set up a formal model of typeclass search and then use it to prove things about it?

[Mario Carneiro]

I think the original paper on the algorithm is most relevant to that: https://arxiv.org/abs/2001.04301 . In particular, it does quite a lot to avoid repeated searches for the same thing, so it would be good to determine whether lean4#3996 represents a bug in the algorithm or in the implementation

[Michael Stoll]

Another meaning of "tabled" :smile:

[Michael Stoll]

@Mario Carneiro @Sebastian Ullrich I've had a look at the paper and tried to follow the pseudocode to see what it is supposed to do in the following simple case:

class A
class B
class C
class D

instance test [B] [C] : A
instance DtoB [D] : B
instance instB : B

#synth A

but I had problems doing that, one reason being that there is no clear definition of the various data structures and another that it is not clear to me what happens if an instance like instB above is encountered that produces no subgoals: in line 20 the call to NewConsumerNode would receive an empty list of subgoals, but then the code is supposed to look at the first subgoal, which does not exist... Also it says "for each solution to g", but does not say how they are obtained. Can you help me understand what it is supposed to do?

BTW, if I interpret footnote 6

Note that the logics of Coq and Lean are so expressive that even for a given type
with no unification variables, different choices of instances may indeed cause different
downstream goals to succeed and fail; however, it is common practice in both systems
to ignore this possibility and to assume that instances are “morally canonical”.

correctly, then it supports my claim that it should be considered a bug when the algorithm or its implementation keeps looking for solutions to a typeclass search problem after it has already found one.

[Mario Carneiro]

it is not clear to me what happens if an instance like instB above is encountered that produces no subgoals: in line 20 the call to NewConsumerNode would receive an empty list of subgoals, but then the code is supposed to look at the first subgoal, which does not exist...

The actual code panics in this case, so I'm pretty sure it is handled elsewhere

[Michael Stoll]

Mario Carneiro said:

The actual code panics in this case, so I'm pretty sure it is handled elsewhere

I hope so; this is certainly a quite common situation!

[Michael Stoll]

Does this mean that the description of the algorithm in the paper is incomplete?

[Michael Stoll]

Here is an example where instance synthesis fails while it should succeed.

class A where

class B (n : Nat) where

class C where


instance test' [B 10] : A where

instance test [B 0] [C] : A where

instance foo {n : Nat} [B n.succ] : B n where

instance instB (n : Nat) : B n where

set_option trace.Meta.synthInstance true

#synth A

It gets stuck trying (and infinitely often failing) to establish A via test and never gets to trying test'.
@Sebastian Ullrich

[Kevin Buzzard]

Putting set_option synthInstance.maxHeartbeats 40 before the #synth stops VS code from crashing and produces a finite trace.

[Michael Stoll]

A fix has just been merged. Now I'm eager to see its effect on Mathlib!

[Kevin Buzzard]

Are you eager enough to learn how to see this effect yourself today? :-)

[Michael Stoll]

Not that eager (it is getting late, and I'm watching the Snooker World Championship...). :billiards:

[Michael Stoll]

Looking at NumberTheory.RamificationInertia on the nightly-testing branch (and after making two _s explicit, which had become very slow, cf. #12412), I see that most of the slow Subsingleton instances are gone (with one exception), but Module, AddCommMonoid and AddMonoidHomClass are still often slow.

Overall, it looks like typeclass inference only takes 50% of the time it took before lean4#4003.

[Jireh Loreaux]

Sorry, where did you get that 50% figure? I couldn't find it.

[Michael Stoll]

I put set_option profiler true at the beginning of the file and ran lake build on it. Then I compared the reported total time for "typeclass inference" with what I remembered from when experimenting with the file.
So you could not possibly find that figure somewhere...

[Jovan Gerbscheid]

The fix hasn't fixed every occurrence of the problem. In particular, what the fix does is make it so that every type class sub-goal (i.e. generator node) that does not have metavariables stops trying to find more than 1 solution. However, it is possible to have a sub-goal B with metavariables that would only every be useful for solving some other subgoal A that doesn't have metavariables. In this case it will still continue to try finding solutions to B even when A is already solved. Here is a minimal example:

class A
class B (α : outParam Type)
class C (n : Nat)
instance [C n] : C (n+1) where
instance : C 0 where
instance : A where
instance (priority := high) [B α] : A where
instance [A] [C 100000] : B Nat where

class D
instance [A] [Nonempty Empty] : D where

#synth D

But my guess would be that fixing this wouldn't give a significant speedup.

[Jovan Gerbscheid]

I also have a converse. The following minimized example of a type class resolution worked in version 4.7.0, but fails since the fix:

class MulComm (α : Type u) [Mul α] : Prop where

class Monoid (α : Type u) extends Mul α
attribute [instance] Monoid.mk

class CommSemigroup (α : Type u) extends Mul α, MulComm α

class CommMonoid (α : Type u) extends Monoid α, MulComm α
attribute [instance] CommMonoid.mk

variable (β : Type u) [CommSemigroup β] [Monoid β]

set_option pp.explicit true
set_option pp.proofs true
/-
@CommMonoid.mk β (@Monoid.mk β (@CommSemigroup.toMul β inst✝))
  (@CommMonoid.toMulComm β
    (@CommMonoid.mk β (@Monoid.mk β (@CommSemigroup.toMul β inst✝))
      (@CommMonoid.toMulComm β
        (@CommMonoid.mk β (@Monoid.mk β (@CommSemigroup.toMul β inst✝)) (@CommSemigroup.toMulComm β inst✝)))))
-/
#synth CommMonoid β

When removing the redundant extra instance [Monoid β], the resolution works. However the synthesized instance contains some duplication that should clearly not be there.

[Jovan Gerbscheid]

The culprit for this weird behaviour is the type class parameter in the class MulComm, because it causes the following dependent instance: CommMonoid.toMulComm.{u} {α : Type u} [self : CommMonoid α] : @MulComm α (@Monoid.toMul α (@CommMonoid.toMonoid α self)). When trying to use this instance, isDefEq needs to figure out the metavariable self, which requires a call to synthPending, which then starts synthesizing an instance of CommMonoid β all over again. This recursive loop happens two times, and the third time around it reaches the hard-coded recursion limit, at which point a different instance needs to be found. Then it finds @CommMonoid.mk β (@Monoid.mk β (@CommSemigroup.toMul β inst✝)) (@CommSemigroup.toMulComm β inst✝). But because of the two extra layers of recursion, we get two extra applications of

CommMonoid.mk β (@Monoid.mk β (@CommSemigroup.toMul β inst✝))
  (@CommMonoid.toMulComm β

I think the solution to this is now quite clear: tabled type class resolution caches all progress within a single synthInstance call. But recursive calls to synthInstance should be able to share the same table.

[Kim Morrison]

I'm confused by attribute [instance] (Comm)Monoid.mk. Those aren't realistic are they?

[Jovan Gerbscheid]

I encountered the example here: https://github.com/leanprover/lean4/blob/91244b2dd9d223006227648659203373f5a46b0b/tests/lean/run/KyleAlg.lean

[Jovan Gerbscheid]

It would be useful for something like this:

variable (α : Type) [CommSemigroup α] [Monoid α]
#synth CommMonoid α

But I didn't realize that these kinds of instances are not in Mathlib.

[Jovan Gerbscheid]

There is exactly one class in which the .mk constructor is marked with the instance attribute, namely

MonadError.mk {m : Type → Type} [toMonadExceptOf : MonadExceptOf Exception m] [toMonadRef : MonadRef m]
  [toAddErrorMessageContext : AddErrorMessageContext m] : MonadError m

The consequence is that when synthesizing MonadRef m, the first thing it tries to do is to synthesize MonadExceptOf Exception m:

import Mathlib

open Lean
set_option trace.Meta.synthInstance true
#synth MonadRef MetaM