typeclass inference can go haywire

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean's type class inference system sometimes tries and fails to solve the same problem 384 or more times consecutively in the middle of a proof.

Steps to Reproduce

NOTE: Far simpler examples are further down the thread.

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 AddSemigroup (G : Type u) extends Add G where
  add_assoc : ∀ a b c : G, a + b + c = a + (b + c)

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

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class AddCommSemigroup (G : Type u) extends AddSemigroup G where
  add_comm : ∀ a b : G, a + b = b + a

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 AddZeroClass (M : Type u) extends Zero M, Add M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

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

class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where

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

structure Units (α : Type u) [Monoid α] where
  val : α
  inv : α
  val_inv : val * inv = 1
  inv_val : inv * val = 1

postfix:1024 "ˣ" => Units

class Inv (α : Type u) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

instance [Monoid α] : Inv αˣ :=
  ⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩

instance [Monoid α] : CoeHead αˣ α :=
  ⟨Units.val⟩

def divp [Monoid α] (a : α) (u : Units α) : α :=
  a * (u⁻¹ : αˣ)

infixl:70 " /ₚ " => divp

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

class LeftCancelSemigroup (G : Type u) extends Semigroup G where
  mul_left_cancel : ∀ a b c : G, a * b = a * c → b = c

class LeftCancelMonoid (M : Type u) extends LeftCancelSemigroup M, Monoid M

class RightCancelSemigroup (G : Type u) extends Semigroup G where
  mul_right_cancel : ∀ a b c : G, a * b = c * b → a = c

class RightCancelMonoid (M : Type u) extends RightCancelSemigroup M, Monoid M

class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  sub a b := a + -b
  sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl

class AddGroup (A : Type u) extends SubNegMonoid A where
  add_left_neg : ∀ a : A, -a + a = 0

class AddMonoidWithOne (R : Type u) extends AddMonoid R, One R where

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

class AddGroupWithOne (R : Type u) extends AddMonoidWithOne R, AddGroup R where

class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G

class Distrib (R : Type _) extends Mul R, Add R where
  protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α

class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α

class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

class CommRing (α : Type u) extends Ring α, CommMonoid α

theorem divp_eq_iff_mul_eq [Monoid α] {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x := sorry

theorem divp_mul_eq_mul_divp {α : Type u} [CommMonoid α] (x y : α) (u : αˣ) :
    x /ₚ u * y = x * y /ₚ u := sorry

@[simp] theorem mul_right_eq_self {M : Type u} [inst : LeftCancelMonoid M] {a b : M} :
    a * b = a ↔ b = 1 := sorry

variable {R : Type _} [CommRing R] (a b : R) (u₁ u₂ : Rˣ) in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.Tactic.simp true in
example : a /ₚ u₁ = b /ₚ u₂ ↔ a * u₂ = b * u₁ := by
  simp [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp]
/-
...

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶
...
-/

The instance trace in this minimal example shows Lean trying and failing to solve LeftCancelMonoid R 384 times.

Expected behavior:

I would hope that Lean does not need to go up this blind alley.

Actual behavior: [What actually happens]

In this minimal example, Lean spends a lot of time trying and failing very quickly to solve LeftCancelMonoid R. In the mathlib example which this was minimised from, Lean tries to solve LeftCancelMonoid R over 500 times and each time it takes a lot longer to fail because in mathlib there are of course ways to prove that something is a left-cancel-monoid. Lean 4 takes about 0.001 seconds to fail each time in the mathlib example, contributing to a 0.5 second delay. Unfortunately it then tries to solve RightCancelMonoid R hundreds of times, and then CancelMonoidWithZero R hundreds of times (I could probably update the MWE to indicate this behaviour if you want to see the wild goose chase happening multiple times), meaning that the simp call takes so long to complete that Lean runs out of heartbeats.

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Lean (version 4.0.0-nightly-2023-01-16, commit 5349a08, Release)

Additional Information

Zulip discussion here.

[dwrensha]

This issue came up while I was porting field_simp. I have commented out one of the test cases because this issue makes it take too long: leanprover-community/mathlib4#1824

[kbuzzard]

We might be seeing this issue again in the mathlib port: leanprover-community/mathlib4#1979

Minimising would involve building the algebra heirarchy up to modules (which I can do if required); here is a version which depends on mathlib.

import Mathlib.Algebra.Module.Submodule.Basic

set_option profiler true
set_option synthInstance.maxHeartbeats 140000 -- default is 20000; five times that not enough here
set_option trace.Meta.synthInstance true

variables {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
{N : Submodule R M} (n : ℕ) in
#synth CoeT ℕ n (Module.End R N) -- takes 7 wall clock seconds

/-
...(chase the large number)
    [tryResolve] [7.199349s] ❌ Ring (Module.End R { x // x ∈ N }) ≟ Ring (Module.End ?m.527 ?m.528) ▼
      [] [0.115698s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.115001s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.118302s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.119675s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.113969s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.109342s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.110053s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.101198s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.108375s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.109773s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098758s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103855s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106827s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.109454s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.108562s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.109977s] ❌ AddCommGroup { x // x ∈ N } ▶
...
-/

There are 70 failures in total.

[rwbarton]

The issue also occurs with

example : a /ₚ u₁ = b /ₚ u₂ ↔ a * u₂ = b * u₁ := mul_right_eq_self

so it doesn't have to do with simp (except in the sense that simp is a place where we expect to have unification fail a lot of the time).
Unification is doing a lot of getting stuck and backtracking somehow, and each time it gets stuck it tries calling unstuckMVar to synthesize the instance (which doesn't help because it doesn't exist).

[kbuzzard]

I have minimised the example a lot more. Inspired by Reid's example of changing all the names from NonUnitalSemiring to A, I have now got this. Hope this helps!

class A1 (M : Type u) extends Mul M

class A2 (M : Type u) extends A1 M

class A3 (M : Type u) extends A2 M

class A4 (M : Type u) extends A3 M

class B1 (M : Type u) extends Mul M

class CommRing (M : Type u) extends B1 M, A4 M

-- given `CommRing R` there are two distinct routes to `Mul R`:
-- CommRing -> B1 -> Mul
-- CommRing -> A4 -> A3 -> A2 -> A1 -> Mul

-- random extra bad class plus theorem which causes all the trouble
class BadClass (M : Type u) extends A4 M
theorem mul_right_eq_self {M : Type u} [inst : BadClass M] {a b c : M} :
    a * b = a ↔ b = c := sorry

set_option trace.Meta.synthInstance true

variable {R : Type _} [i : CommRing R] (a b c : R)
example :
  -- use the two (defeq) multiplications to say a * b = c ↔ a * b = c
  (@HMul.hMul R R R
    (@instHMul R (@A1.toMul R (@A2.toA1 R (@A3.toA2 R (@A4.toA3 R (@CommRing.toA4 R i))))))
    a b) = c ↔
  (@HMul.hMul R R R
    (@instHMul R (@B1.toMul R (@CommRing.toB1 R i)))
    a b) = c := 
    -- ⊢ a * b = c ↔ a * b = c
    mul_right_eq_self

/-
[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶
...
490 times
-/

[rwbarton]

A couple of comments about Kevin's test case.

• It helps to add set_option trace.Meta.isDefEq true and set_option pp.all true for a fuller picture.
• The blowup is really exponential; adding a class A5 increases the count by a factor of 2. Some of my attempts to reduce the example further also resulted in lots of repeated attempts, but not with exponential behavior.
• The class BadClass with no instances isn't very realistic. More often, there will be some instances of BadClass that just don't apply to the problem we need to solve. This affects the elaboration process because now TC synthesis has to do some unification to see that the instance is not helpful. In Kevin's example, adding instance : BadClass Nat increases the number of synthInstance attemps by a factor of around 15.

There seem to be (at least) two issues here:

• The elaborator tries to synthesize BadClass R very early on (with or without the BadClass Nat instance), which fails of course. Intuitively, one would expect that this causes elaboration to stop immediately. Instead what happens is that the elaborator continues trying to unify the HMul.hMul in the theorem type with the one coming from the metavariable representing the (failed) synthesized instance.
• This latter unification takes exponentially long. One cause (which was also diagnosed by @gebner on Zulip) is that each field A2.toA1, A3.toA2 etc. can equivalently be represented by a primitive projection .1, and elaboration manages to hit all of the combinations. You can see this by searching for any pattern like .1.1).1 in the trace with isDefEq and pp.all. But also, it's not clear to me why the elaborator should be doing any backtracking here in the first place.

[kbuzzard]

Adam Topaz points out that even without the defeq diamond you can get a smaller amount of chaos:

class A1 (M : Type u) extends Mul M

class A2 (M : Type u) extends A1 M

class A3 (M : Type u) extends A2 M

class A4 (M : Type u) extends A3 M

class CommRing (M : Type u) extends A4 M

class BadClass (M : Type u) extends A4 M

theorem mul_right_eq_self {M : Type u} [inst : BadClass M] {a b c : M} :
    a * b = a ↔ b = c := sorry

set_option trace.Meta.synthInstance true

variable {R : Type _} [CommRing R] (a b c : R)
example : a * b = c ↔ a * b = c :=
    mul_right_eq_self

/-
[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶

[Meta.synthInstance] ❌ BadClass R ▶
...
54 times
-/

and adding instance : BadClass Nat := sorry bumps it up to a total of 780 failed BadClass R.

[gebner]

And here is a version that makes BadClass slow to synthesize.

class A1 (M : Type u) extends Mul M
class A2 (M : Type u) extends A1 M
class A3 (M : Type u) extends A2 M
class A4 (M : Type u) extends A3 M
class CommRing (M : Type u) extends A4 M

class BadClass (M : Type u) extends A4 M

theorem mul_right_eq_self {M : Type u} [inst : BadClass M] {a b c : M} :
    a * b = a ↔ b = c := sorry

macro "exponential" "blowup" n:num "from" a:ident "to" c:ident : command => do
  let bs ← (List.range n.getNat).mapM fun i =>
    Lean.mkIdent <$> Lean.Macro.addMacroScope (.mkSimple s!"B{i}")
  let mut cmds : Array Lean.Syntax.Command ←
    bs.toArray.mapM (`(class $(·) (M N : Type) : Type))
  for b1 in bs, b2 in bs.tail! do
    cmds := cmds ++ #[
      ← `(instance {M N} [$b1 (Option M) N] : $b2 M N where),
      ← `(instance {M N} [$b1 (Inhabited M) N] : $b2 M N where)]
  cmds := cmds ++ #[← `(command| instance {M N} [$a N] : $(bs.head!) M N where)]
  cmds := cmds ++ #[← `(command| instance {M} [$(bs.getLast!) M M] : $c M := sorry)]
  return ⟨Lean.mkNullNode cmds⟩

class BaseBadClass (N : Type) : Type
instance : BaseBadClass Nat where
exponential blowup 12 from BaseBadClass to BadClass

variable {R : Type} [CommRing R] (a b c : R)
example : a * b = c ↔ a * b = c :=
  mul_right_eq_self

[gebner]

From what I can tell, #2152 fixed all of the performance issues here. Unification still does a lot of typeclass queries, but they return instantly due to being cached now.