type class inference looping

Stream: lean4

[Kevin Buzzard]

@Heather Macbeth ran into an issue in the mathlib port with typeclass inference looping. I minimised it, and it's quite surprising: if you don't tell Lean alpha explicitly, by the time it's figured out you mean alpha it seems to have forgotten that alpha is a MonoidWithZero.

universe u v w

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀

class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ

instance instHSMul (M : Type _) (α : Type _) [SMul M α] : HSMul M α α where
  hSMul := SMul.smul

infixr:73 " • " => HSMul.hSMul

class MulAction (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
  protected one_smul : ∀ b : β, (1 : α) • b = b
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

variable (R M)

class MulActionWithZero [MonoidWithZero R] [Zero M] extends MulAction R M where
  smul_zero : ∀ r : R, r • (0 : M) = 0
  zero_smul : ∀ m : M, (0 : R) • m = 0

class SMulZeroClass (M A : Type _) [Zero A] extends SMul M A where
  smul_zero : ∀ a : M, a • (0 : A) = 0

class SMulWithZero [Zero R] [Zero M] extends SMulZeroClass R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0

instance (priority := 100) MulActionWithZero.toSMulWithZero [MonoidWithZero R] [Zero M] [m : MulActionWithZero R M] :
    SMulWithZero R M :=
  { m with }

variable {I : Type u}

variable {f : I → Type v}

namespace Pi

instance instZero [∀ i, Zero <| f i] : Zero (∀ i : I, f i) :=
  ⟨fun _ => 0⟩

variable {M}

instance instSMul [∀ i, SMul M <| f i] : SMul M (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

instance smulWithZero [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    -- already this is odd:
    -- smul_zero := fun a => funext fun i => SMulZeroClass.smul_zero a -- "failed to synthesize instance `SMulZeroClass α (f i)`"
    smul_zero := fun a => funext fun i => @SMulZeroClass.smul_zero  _ (f i) _ _ a -- needs the @
    zero_smul := fun _ => funext fun _ => SMulWithZero.zero_smul _ }

instance mulAction (α) {m : Monoid α} [∀ i, MulAction α <| f i] :
    @MulAction α (∀ i : I, f i) m where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ => MulAction.mul_smul _ _ _
  one_smul _ := funext fun _ => MulAction.one_smul _

set_option trace.Meta.synthInstance true

set_option maxHeartbeats 10000 -- consider turning trace.Meta.synthInstance to false if you
-- make this number much bigger

-- works fine
instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
  { Pi.mulAction α with
    smul_zero := Pi.smulWithZero.smul_zero
    zero_smul := Pi.smulWithZero.zero_smul }

-- also works
instance mulActionWithZero' (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
  { Pi.mulAction α, @Pi.smulWithZero _ _ α _ _ _ with }

-- but this seems to be looping
instance mulActionWithZero' (α) [MonoidWithZero α] [∀ i, Zero (f i)]
    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
  { Pi.mulAction α, Pi.smulWithZero with }


/-
Lean claims to not be able to find `MonoidWithZero α` even though it's explicitly given as an instance.

[Meta.synthInstance] 💥 (i : I) → SMulWithZero α (f i) ▼
  [] new goal (i : I) → SMulWithZero α (f i) ▶
  [] 💥 apply MulActionWithZero.toSMulWithZero to (i : I) → SMulWithZero α (f i) ▼
    [tryResolve] 💥 SMulWithZero α (f i) ≟ SMulWithZero (?m.15131 i) (?m.15132 i) ▼
      [] ❌ Zero α ▼
        [] new goal Zero α ▶
        [] ✅ apply @MonoidWithZero.toZero to Zero α ▼
          [tryResolve] ✅ Zero α ≟ Zero α
          [] no instances for MonoidWithZero α ▶
        [] ✅ apply @AddMonoid.toZero to Zero α ▶
        [] ✅ apply @MulZeroOneClass.toZero to Zero α ▶
        [] ✅ apply @MonoidWithZero.toMulZeroOneClass to MulZeroOneClass α ▶
        [] ✅ apply @AddZeroClass.toZero to Zero α ▶
        [] ✅ apply @AddMonoid.toAddZeroClass to AddZeroClass α ▶
        [] ✅ apply @SemigroupWithZero.toZero to Zero α ▶
        [] ✅ apply @MonoidWithZero.toSemigroupWithZero to SemigroupWithZero α ▶
        [] ✅ apply @MulZeroClass.toZero to Zero α ▶
        [] ✅ apply @MulZeroOneClass.toMulZeroClass to MulZeroClass α ▶
        [] ✅ apply @SemigroupWithZero.toMulZeroClass to MulZeroClass α ▶
        [] ✅ apply @Zero.ofOfNat0 to Zero α ▶
        [] ✅ apply @Zero.toOfNat0 to OfNat α 0 ▶
      [] ✅ I → MonoidWithZero α ▶
-/

[Heather Macbeth]

Thanks for bringing this to #lean4 Kevin. I think I've minimized it a bit more actually:

variable {α : Type}
variable {R : Type}

class Zip (α : Type) -- represents `Zero`

class SMul (R : Type) (α : Type) where
  smul : R → α → α

infixr:73 " • " => SMul.smul

class MulAction (R : Type) (β : Type) extends SMul R β

class SMulZeroClass (R α : Type) extends SMul R α where
  smul_zero : ∀ r : R, ∀ a : α, r • a = a

class MulActionWithZero (R α : Type) extends MulAction R α, SMulZeroClass R α

class SMulWithZero (R α : Type) [Zip R] [Zip α] extends SMulZeroClass R α

instance MulActionWithZero.toSMulWithZero (R M : Type)
    [Zip R] [Zip M] [m : MulActionWithZero R M] :
    SMulWithZero R M :=
  { m with }


namespace pi
variable {I : Type}
variable {f : I → Type}

instance instZero [∀ i, Zip (f i)] : Zip (∀ i : I, f i) := ⟨⟩

instance instSMul [∀ i, SMul R (f i)] : SMul R (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

instance smulWithZero (R) [Zip R] [∀ i, Zip (f i)] [∀ i, SMulWithZero R (f i)] :
    SMulWithZero R (∀ i, f i) :=
  { pi.instSMul with
    smul_zero := sorry }

instance mulAction (R) [∀ i, MulAction R (f i)] : MulAction R (∀ i : I, f i) where
  smul := (· • ·)

set_option trace.Meta.synthInstance true

set_option maxHeartbeats 10000 -- consider turning trace off if you make this much bigger

-- seems to be looping
instance mulActionWithZero (R) [Zip R] [∀ i, Zip (f i)] [∀ i, MulActionWithZero R (f i)] :
    MulActionWithZero R (∀ i, f i) :=
 { pi.mulAction _, pi.smulWithZero _ with }

end pi

[Heather Macbeth]

And I checked that the error doesn't appear for the corresponding code in Lean 3.

[Heather Macbeth]

But i'm not sure how to read the typeclass inference trace.

[Moritz Firsching]

I'm not entirely sure, but I think I have observed the same behavior when porting Mathlib/Data/Set/Intervals/Instances.lean
Data/Set/Intervals/Instances.lean#L342-L344
Here one also gets an deterministic time out and the structure of the instance is very similar

[Gabriel Ebner]

After taking a quick look, this slightly confusing behavior is due to nested TC resolution. If you enable the trace.Meta.isDefEq option, then you'll see that the failing type class inference happens during unification. The thing is, we only allow a single layer of nesting (so tc->defeq->tc is fine, but defeq->tc->defeq->tc is not). So if you have a type class instance that requires nested TC resolution during TC synthesis (like the one here), then it won't be found during unification (i.e., when trying to fill in the underscore here).

[Heather Macbeth]

Thanks for the information Gabriel. Do you know why this feature was supported in Lean 3 but not in Lean 4?

[Gabriel Ebner]

What I said is correct, but after some investigation it's not the issue here (although it might bite us in the future). From what I can tell, all we're missing here is a !. https://github.com/leanprover/lean4/commit/70a6c06eef060d8e14869e2848749287e5364742

[Kevin Buzzard]

Does this change have any effect on the examples at lean4#1986?

[Gabriel Ebner]

Not as far as I can tell.

[Kevin Buzzard]

docs4#Pi.mulAction has {m : Monoid α} a typeclass variable being inferred by unification. Presumably this is intentional? Is this related?

[Kevin Buzzard]

And does it change this?

import Mathlib.Algebra.SMulWithZero

universe u v

variable {I : Type u}

variable {f : I → Type v}

set_option trace.Meta.synthInstance true

instance Pi.smulWithZero (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
    SMulWithZero α (∀ i, f i) :=
  { Pi.instSMul with
    smul_zero := fun a => funext fun i => SMulZeroClass.smul_zero a -- fails with error
    /-
    failed to synthesize instance
    SMulZeroClass α (f i)
    -/
    zero_smul := sorry }

[Kevin Buzzard]

smul_zero := fun a => funext fun i => @SMulZeroClass.smul_zero α (f i) _ _ a -- works fine

[Kevin Buzzard]

I see this in the traces of Heather's example:

[Meta.isDefEq] 💥 ∀ (r : R) (a : (i : I) → f i), r • a = a =?= ∀ (r : R) (a : (i : I) → f i), r • a = a

Is this surprising?

[Gabriel Ebner]

The bomb in synthInstance usually means that TC synthesis aborted because it saw a metavariable. For example, you need to find an instance of Group (?G, ?H). Then we abort and try again later when ?G is filled in.

[Kevin Buzzard]

But the bomb in the above had no metavariables I think

[Sebastian Ullrich]

This is the example with the heartbeat timeout, right? As soon as the limit is reached, any further isDefEq/whnf/... will bomb out in 0 steps. synthInstance is the only subsystem with a per-invocation limit.

[Sebastian Ullrich]

But also, image.png

[Henrik Böving]

How are you getting these type hovers in emacs in the info view? @Sebastian Ullrich

[Sebastian Ullrich]

By using VS Code :)

[Henrik Böving]

/o\

[Henrik Böving]

So I am the last one left on emacs now huh.

[Sebastian Ullrich]

It's basically the only time I use VS Code. But I'm not holding my breath for widget support in Emacs either. I guess using an external web browser window as suggested before is the most realistic solution.

[Oliver Nash]

Are typeclass cycles allowed in Lean 4?

Yesterday I tried to promote docs#Module.free_of_finite_type_torsion_free' to an instance but I failed and I suspect this is because it forms a cycle with docs#Module.Free.noZeroSMulDivisors

I also tried to promote docs#isNoetherian_of_isNoetherianRing_of_finite to an instance and again I failed and suspect this is because of the cycle it forms with docs#Module.IsNoetherian.finite

I tried to see if I could understand based on reading https://arxiv.org/pdf/2001.04301.pdf but I got lazy and decided I'd just ask here instead.

[Scott Morrison]

Yes, cycles should not be a problem.

[Oliver Nash]

I claim #6548 is further evidence that cycles are still problematic in Lean 4. I admit this is a bit vague since any new instance of course creates new work for typeclass inference but I think it's worth trying to collect a few examples of cycle-creating instances that are notably costly.

[Sebastian Ullrich]

Multiple files were touched, more were probably affected indirectly; out of these, one regressed by ~200ms and another one exceeded a threshold with no idea how close it was before, as already pointed out by Kevin. That is not evidence.

[Chris Hughes]

In the file that broke in #6548, the lemma XYIdeal_eq₂ goes from 93846 heartbeats to 109609 after adding attribute [instance] CharP.charP_to_charZero. The theorem XYIdeal_neg_mul goes from 803202 to 828585 after adding the same instance. I don't know if count_heartbeats is the thing we should be using here. ring1 times out looking for a CharZero instance on F[X][X] that isn't there.

[Kevin Buzzard]

I don't know if that wild goose chase for the CharZero instance is counted by heartbeats? It would probably be synthInstance heartbeats I guess.

[Junyan Xu]

I hope this is some better evidence that cycles are still problematic: https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1691792488
diff to reproduce and profile

[Anne Baanen]

Here's another example of problematic cycles I ran into recently: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60by_cases.60.20trying.20to.20find.20a.20weird.20instance/near/374893214

[Jireh Loreaux]

I'm fairly certain the errors I'm encountering here on #7309 are also due to cycle problems. This PR introduces two TC cycles, and it seems the latter (for OrderedCommRing) is causing the problems. For commit 987689ab10908b46992444e7f5075359ccacfcfd on the relevant branch#j-loreaux/OrderedStarRing, one can do:

import Mathlib

-- without disabling this instance, the `inferInstance` call fails below.
-- if it's disabled, Lean finds the instance very quickly
attribute [-instance] StarOrderedRing.toOrderedCommRing

example {R : Type*} [CommRing R] (I : Ideal R) (f : Polynomial R) : True := by
  letI : CommSemiring (AdjoinRoot f ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.span {f}))
    (Ideal.map Polynomial.C I)) := inferInstance
    -- even with the instance above activated `CommRing.toCommSemiring` works.
  trivial

Note: it's getting caught up in isDefEq and it's the maxHeartbeats timing out (not synthInstance.maxHeartbeats). The TC cycles I added don't actually change the data fields, but I think the issue may be that Lean is doing a lot of unbundling / rebundling because of new style structures, and then it can't unify.