type class inference goes haywire

Stream: lean4

[Kevin Buzzard]

The following code (minimised from mathlib, sorry for as ever having to build up a chunk of the alegbra hierarchy)

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 Nontrivial (α : Type _) : Prop where
  exists_pair_ne : ∃ x y : α, x ≠ y

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ˣ)

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]

has a completely innocuous-looking trace until the simplifier decides to try applying the simp lemma mul_right_eq_self. At this point it then does this

(over 350 instances of `[Meta.synthInstance] ❌ LeftCancelMonoid R ▶` omitted)

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.synthInstance] ❌ LeftCancelMonoid R ▶

[Meta.Tactic.simp.unify] @mul_right_eq_self:1000, failed to unify
      ?a * ?b = ?a
    with
      a * u₂.val = b * u₁.val `

Unfolding some of the 384 failures to synthesize LeftCancelMonoid R indicates that they all seem to be

[Meta.synthInstance] ❌ LeftCancelMonoid R ▼
  [] no instances for LeftCancelMonoid R ▼
    [instances] #[]

Of course in the real world example in mathlib they are much more complicated, because there are instances for this class, and the failures take longer to happen, leading to timeouts. The mathlib4 thread discussing this is here. This is surely a bug?

[Kevin Buzzard]

I just chose a random file in mathlib, switched on instance tracing and found a lemma with a three-line proof involving simp which (correctly) synthesized CommSemigroup α 86 times. This was in the first file I looked at. No idea if it's related though.

[Gabriel Ebner]

On a high level, this is a similar issue as lean4#1986. We try to unify the HMul R R R instance in the lemma (derived from an unknown LeftCancelMonoid instance) with the HMul R R R instance in the goal (derived from the CommRing instance in the context).

[David Renshaw]

( lean4#1986 presumeably)

[Gabriel Ebner]

We try many things during unification, and many of them multiple times. For example I can see that we visit the subgoal Monoid.toMulOneClass =?= NonUnitalSemiring.toNonUnitalNonAssocSemiring at least three times (and then there's probably a subgoal in there that gets visited 3*3 times, etc.). And whenever we inevitably fail to unify these subgoals, we try to instantiate the missing LeftCancelMonoid instance using type class synthesis.

[Gabriel Ebner]

lean4#2003 doesn't solve this problem either, because projections on metavariables don't reduce. :sad:

[David Renshaw]

It looks to me like all those synthInstance calls are happening in a single isDefEq call here: https://github.com/leanprover/lean4/blob/a125a36bcc79a28963ed5786f94c5d97648a8f99/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L57

[David Renshaw]

with lhs as ?a * ?b = ?a
and e as a * u₂.val = b * u₁.val

[David Renshaw]

a lot more info shows up with
set_option trace.Meta.isDefEq true

[James Gallicchio]

would it be feasible to cache the unification results that happen in a single isDefEq check? or would the cost of that outweigh the savings

[Kevin Buzzard]

lean4#2055