typeclass inference failure

Stream: lean4

[Kevin Buzzard]

import Mathlib.LinearAlgebra.TensorProduct
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.LinearAlgebra.Quotient

open TensorProduct

variable (k α A : Type*) [CommRing k] [AddCommGroup A]
  [Module k A] (S : Submodule k (A ⊗[k] (α →₀ k)))

set_option trace.Meta.synthInstance true in
#check (A ⊗[k] (α →₀ k)) ⧸ S -- fails to synthesise HasQuotient instance

noncomputable instance : AddCommGroup (A ⊗[k] (α →₀ k)) := inferInstance -- shortcut

#check (A ⊗[k] (α →₀ k)) ⧸ S -- now works fine

The relevant instance trace is

[Meta.synthInstance] ❌ HasQuotient (A ⊗[k] (α →₀ k)) (Submodule k (A ⊗[k] (α →₀ k))) ▼
  [] new goal HasQuotient _tc.0 (Submodule k (A ⊗[k] (α →₀ k))) ▶
  [] ❌ apply @Submodule.hasQuotient to HasQuotient ?m.2747 (Submodule k (A ⊗[k] (α →₀ k))) ▼
    [tryResolve] ❌ HasQuotient ?m.2747 (Submodule k (A ⊗[k] (α →₀ k))) ≟ HasQuotient ?m.2752 (Submodule ?m.2751 ?m.2752) ▼
      [] ✅ Ring k ▶
      [] ❌ AddCommGroup (A ⊗[k] (α →₀ k)) ▼
        [] new goal AddCommGroup (A ⊗[k] (α →₀ k)) ▶
        [] ❌ apply inst✝¹ to AddCommGroup (A ⊗[k] (α →₀ k)) ▶
        [] ❌ apply @TensorProduct.addCommGroup to AddCommGroup (A ⊗[k] (α →₀ k)) ▼
          [tryResolve] ❌ AddCommGroup (A ⊗[k] (α →₀ k)) ≟ AddCommGroup (?m.2830 ⊗[?m.2828] ?m.2831) ▼
            [] ❌ AddCommGroup (α →₀ k) ▼
              [] new goal AddCommGroup (α →₀ k) ▶
              [] ❌ apply inst✝¹ to AddCommGroup (α →₀ k) ▶
              [] ❌ apply @Finsupp.addCommGroup to AddCommGroup (α →₀ k) ▼
                [tryResolve] ❌ AddCommGroup (α →₀ k) ≟ AddCommGroup (?m.2851 →₀ ?m.2852)

and the last line is the inexplicable failure. Is it something to do with computability?

[Matthew Ballard]

It isn’t computability because the #check still works if you remove the noncomputable attribute. You only get an error about not generating IR

[Matthew Ballard]

Something isn’t being unfolded

[Matthew Ballard]

At some point it reaches

AddMonoid.toAddSemigroup =?= TensorProduct.addSemigroup A (α →₀ k)

What is supposed to happen:

[Meta.isDefEq] ✅ AddMonoid.toAddSemigroup =?= TensorProduct.addSemigroup A (α →₀ k) ▼
  [] ✅ TensorProduct.addSemigroup A (α →₀ k) =?= TensorProduct.addSemigroup A (α →₀ k) ▼
    [] ✅ A =?= A
    [] ✅ α →₀ k =?= α →₀ k
    [] ✅ k =?= k
    [] ✅ CommRing.toCommSemiring =?= CommRing.toCommSemiring
    [] ✅ AddCommGroup.toAddCommMonoid =?= AddCommGroup.toAddCommMonoid
    [] ✅ AddCommGroup.toAddCommMonlean=?= Finsupp.addCommMonoid ▶
    [] ✅ inst✝ =?= inst✝
    [] ✅ Finsupp.module α k =?= Finsupp.module α k

What actually does

[] ❌ AddMonoid.toAddSemigroup =?= TensorProduct.addSemigroup A (α →₀ k) ▼
                          [] ❌ AddMonoid.toAddSemigroup =?= let src := AddCon.addMonoid (addConGen (TensorProduct.Eqv k A (α →₀ k)));
                              AddSemigroup.mk
                                (_ :
                                  ∀ (a b c : AddCon.Quotient (addConGen (TensorProduct.Eqv k A (α →₀ k)))),
                                    a + b + c = a + (b + c)) ▶

It looks like it’s having trouble filling a metavariable for R in the tensor product with k

[Matthew Ballard]

A trace class for the branching logic of unification would be nice

[Kevin Buzzard]

I came back to this today. I've stripped the example down to importing Algebra.Ring.Basic. It's a delicate minimisation problem -- you make one false move and suddenly it all magically works again. An empirical observation is that when it works, the trace looks like this:

[Meta.synthInstance] ✅ HasQuotient (TensorProduct k A (Finsupp α k)) (Submodule k (TensorProduct k A (Finsupp α k))) ▼
  [] new goal HasQuotient _tc.0 (Submodule k (TensorProduct k A (Finsupp α k))) ▶
  [] ✅ apply @Submodule.hasQuotient to HasQuotient (TensorProduct k A (Finsupp α k))
        (Submodule k (TensorProduct k A (Finsupp α k))) ▼
    [tryResolve] ✅ HasQuotient (TensorProduct k A (Finsupp α k))
          (Submodule k
            (TensorProduct k A
              (Finsupp α
                k))) ≟ HasQuotient (TensorProduct k A (Finsupp α k)) (Submodule k (TensorProduct k A (Finsupp α k)))

and the [tryResolve] for HasQuotient has no metavariables in. But when it's failing (like the example I post below), the trace looks like this:

[Meta.synthInstance] ❌ HasQuotient (TensorProduct k A (Finsupp α k)) (Submodule k (TensorProduct k A (Finsupp α k))) ▼
  [] new goal HasQuotient _tc.0 (Submodule k (TensorProduct k A (Finsupp α k))) ▶
  [] ❌ apply @Submodule.hasQuotient to HasQuotient ?m.6925 (Submodule k (TensorProduct k A (Finsupp α k))) ▼
    [tryResolve] ❌ HasQuotient ?m.6925 (Submodule k (TensorProduct k A (Finsupp α k))) ≟ HasQuotient ?m.6928 (Submodule ?m.6927 ?m.6928) ▶

i.e. there's a bunch of metavariables in [tryResolve].

I have no understanding of what encourages the metavariables to appear/disappear; I just try simplifying the problem a bit and sometimes it's metavariables, sometimes it isn't.

[Kevin Buzzard]

Mathlib-free! It's totally weird: one way to fix it is to change the definition of Ring so it extends the two things in the other order.

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

-- Note: no need to extend Zero mathematically, as it's in `AddCommGroup`, but if we
-- don't extend `Zero` then the problem goes away, and if we
-- extend `AddCommGroup` first and then `Zero` the problem also goes waway.
-- note: in mathlib this is what is happening (we extend two things both of which have a zero
-- in the definition of `Ring`)
class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type) where
  quotient' : B → Type

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := ⟨fun _ => M⟩

def TensorProduct (R : Type) [Zero R] (M : Type) (N : Type)
    [Zero M] [Zero N] [Module R M] [Module R N] : Type := Unit

instance TensorProduct.zero {R : Type} [Zero R] {M : Type}
    {N : Type} [Zero M] [Zero N] [Module R M]
    [Module R N] : Zero (TensorProduct R M N) :=
  ({ zero := .unit } : Zero Unit) -- or `sorry`

instance TensorProduct.addCommGroup {R : Type} [Zero R]
    {M : Type} {N : Type} [AddCommGroup M] [AddCommGroup N] [Module R M]
    [Module R N] : AddCommGroup (TensorProduct R M N) :=
  { TensorProduct.zero with }

instance TensorProduct.module {R : Type} [Zero R] {M : Type}
    {N : Type} [Zero M] [Zero N] [Module R M]
    [Module R N] : Module R (TensorProduct R M N) :=
  { }

 -- if you remove `[Zero M]` then the problem goes away
def Finsupp (M : Type) [Zero M] := Unit

instance Finsupp.zero {G : Type} [Zero G] : Zero (Finsupp G) :=
sorry -- replacing with `{ zero := sorry}` makes the problem go away?!
      -- in the original example from mathlib there is no sorry at all

instance Finsupp.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Finsupp G) :=
  { Finsupp.zero with }

instance Finsupp.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Finsupp M) := { }

variable (k A : Type) [Ring k] [AddCommGroup A] [Module k A]

-- set_option trace.Meta.synthInstance true in
#synth HasQuotient (TensorProduct k A (Finsupp k)) (Submodule k (TensorProduct k A (Finsupp k))) -- fails

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Finsupp k) := inferInstance

-- and now the original `#synth` works fine
#synth HasQuotient (TensorProduct k A (Finsupp k)) (Submodule k (TensorProduct k A (Finsupp k)))

The trace looks like this:

[Meta.synthInstance] ❌ HasQuotient (TensorProduct k A (Finsupp k)) (Submodule k (TensorProduct k A (Finsupp k))) ▼
  [] new goal HasQuotient _tc.0 (Submodule k (TensorProduct k A (Finsupp k))) ▶
  [] ✅ apply @Submodule.hasQuotient to HasQuotient (TensorProduct k A (Finsupp k))
        (Submodule k (TensorProduct k A (Finsupp k))) ▶
  [] ❌ apply inst✝¹ to AddCommGroup (TensorProduct k A (Finsupp k)) ▶
  [] ❌ apply @TensorProduct.addCommGroup to AddCommGroup (TensorProduct k A (Finsupp k)) ▼
    [tryResolve] ❌ AddCommGroup (TensorProduct k A (Finsupp k)) ≟ AddCommGroup (TensorProduct ?m.1245 ?m.1247 ?m.1248) ▼
      [] ✅ AddCommGroup A ▶
      [] ❌ AddCommGroup (Finsupp k) ▼
        [] result <not-available> (cached)

With pp.all both the <not-available> instance and the instance found by typeclass inference in the shortcut are AddCommGroup (@Finsupp k (@Ring.toZero k inst✝²)) (so syntactically equal).

Vague conjecture: changing the definition of Ring in mathlib from

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

to

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

might fix this. But I have no idea what's going on. Hopefully the minimisation can make it easier for others to find out. The wall I hit is that I cannot see any more details about what tryResolve is doing and in particular why it's failing.

[Kevin Buzzard]

Indeed I have just confirmed that changing the definition of Ring in mathlib from

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

to

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

makes the original error at the top of this thread disappear.

This is ridiculously brittle. What are we supposed to be doing here? Are there guidelines for how we are supposed to build the algebra heirarchy? And are we not following them? @Sébastien Gouëzel you understood this at some point. Does my suggestion fit into your understanding of things or is this a new phenomenon?

[Kevin Buzzard]

Amelia (who found the original issue) points out that I can remove the tensor product from the mix:

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

-- switching the order makes the issue go away
class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type) where
  quotient' : B → Type

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := ⟨fun _ => M⟩

def Finsupp (M : Type) [Zero M] := Unit

instance Finsupp.zero {G : Type} [Zero G] : Zero (Finsupp G) :=
sorry -- replacing with `{ zero := sorry}` makes the problem go away?!
      -- in the original example from mathlib there is no sorry at all

instance Finsupp.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Finsupp G) :=
  { Finsupp.zero with }

instance Finsupp.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Finsupp M) := { }

variable (k : Type) [Ring k]

-- set_option trace.Meta.synthInstance true in
#synth HasQuotient (Finsupp (Finsupp k)) (Submodule k (Finsupp (Finsupp k))) -- fails

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Finsupp k) := inferInstance

-- and now the original `#synth` works fine
#synth HasQuotient (Finsupp (Finsupp k)) (Submodule k (Finsupp (Finsupp k))) -- works
/-
Failing trace:

[Meta.synthInstance] ❌ HasQuotient (Finsupp (Finsupp k)) (Submodule k (Finsupp (Finsupp k))) ▼
  [] new goal HasQuotient _tc.0 (Submodule k (Finsupp (Finsupp k))) ▶
  [] ❌ apply @Submodule.hasQuotient to HasQuotient ?m.639 (Submodule k (Finsupp (Finsupp k))) ▼
    [tryResolve] ❌ HasQuotient ?m.639 (Submodule k (Finsupp (Finsupp k))) ≟ HasQuotient ?m.642 (Submodule ?m.641 ?m.642) ▼
      [] ✅ Ring k ▶
      [] ❌ AddCommGroup (Finsupp (Finsupp k)) ▼
        [] new goal AddCommGroup (Finsupp (Finsupp k)) ▶
        [] ❌ apply @Finsupp.addCommGroup to AddCommGroup (Finsupp (Finsupp k)) ▼
          [tryResolve] ❌ AddCommGroup (Finsupp (Finsupp k)) ≟ AddCommGroup (Finsupp ?m.655) ▼
            [] ❌ AddCommGroup (Finsupp k) ▼
              [] new goal AddCommGroup (Finsupp k) ▶
              [] ❌ apply @Finsupp.addCommGroup to AddCommGroup (Finsupp k) ▼
                [tryResolve] ❌ AddCommGroup (Finsupp k) ≟ AddCommGroup (Finsupp ?m.659)
-/

Shall I open an issue?

[Matthew Ballard]

[stuckMVar] found stuck MVar ?m.644 : AddCommGroup (Finsupp (Finsupp k))

[Kevin Buzzard]

I don't know how you're doing that but I now have a sorry-free example -- is the error still the same?

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type) where
  quotient' : B → Type

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := ⟨fun _ => M⟩

def Synonym (M : Type) [Zero M] := M

instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨(Zero.zero : G)⟩

instance Synonym.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Synonym G) :=
  { Synonym.zero with }

instance Synonym.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Synonym M) := { }

variable (R : Type) [Ring R]

set_option trace.Meta.synthInstance true in
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Synonym R) := inferInstance

-- and now the original `#synth` works fine
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works

[Kevin Buzzard]

I opened lean4#3313 now I got rid of the sorry. I changed Finsupp to Synonym and made it a type synonym.

[Kevin Buzzard]

With set_option trace.Meta.isDefEq.stuckMVar true I also see some stuck metavariables, the one nearest to the problem being

...
                [tryResolve] ❌ AddCommGroup (Synonym R) ≟ AddCommGroup (Synonym ?m.667) ▼
                  [isDefEq.stuckMVar] found stuck MVar ?m.668 : AddCommGroup R

Here we have [Ring R] and class Ring (α : Type) extends Zero α, AddCommGroup α

[Matthew Ballard]

I am confused as to how we reach a branch of code. (Be warned: off the top of my head)

We have the following ToMessageData instance

instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩

Now in docs#Lean.Meta.synthInstance? there is the following branch of code

    match s.cache.synthInstance.find? (localInsts, type) with
    | some result =>
      trace[Meta.synthInstance] "result {result} (cached)"

Here (result: Option Expr) so how do I reach the message?

[] result <not-available> (cached)

What dumb thing am I doing here?
As far as I can tell, this is the only place (cached) occurs in a message and above is the only place that not-available occurs.

[Matthew Ballard]

Nevermind - the answer is in front of my face. The result is still an Option

[Matthew Ballard]

You can also "fix" this by making Synonym reducible. At some point, Lean wants to unify

[] ✅ Synonym (Synonym R) =?= Synonym R ▶

[Matthew Ballard]

Aha you have abused defeq

instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨(Zero.zero : G)⟩

forces Lean to unwrap Synonym to unify

[Matthew Ballard]

If you place AddCommGroup first then Lean doesn't have to take the path through Zero

[Kevin Buzzard]

Yeah I can fix this by making Synonymreducible, but I can't make Finsupp reducible (which is the application -- I was just minimising here), and yeah I can fix this by reordering the definition of Ring, but I am not sure I'm allowed to reorder the definition of Ring in mathlib either, because my impression was that we already thought hard about the definition of Ring (again this is an artifact of minimising) :-( .

How do I make that instance without abusing defeq? And does the failure still occur? It wouldn't surprise me if it did.

[Eric Wieser]

def Synonym.mk {M : Type} [Zero M] (m : M) : Synonym M := m is the fragile way to avoid the abuse

[Eric Wieser]

But it doesn't help here

[Eric Wieser]

Here's the repro with no defeq abuse at all (no def)

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type)

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := {}

structure Synonym (M : Type) [Zero M] where m : M

instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨.mk (Zero.zero : G)⟩

instance Synonym.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Synonym G) :=
  { Synonym.zero with }

instance Synonym.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Synonym M) := { }

variable (R : Type) [Ring R]

set_option trace.Meta.synthInstance true in
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Synonym R) := inferInstance

-- and now the original `#synth` works fine
#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works

[Kevin Buzzard]

Thanks!

[Eric Wieser]

Edited to simplify further

[Eric Wieser]

Even removing the outParam makes no difference

[Eric Wieser]

In fact, the first argument of HasQuotient is a distraction here

[Eric Wieser]

Here's a slightly simpler example:

set_option autoImplicit false

class Zero (α : Type) where
  zero : α

class AddCommGroup (α : Type) extends Zero α where

class Ring (α : Type) extends Zero α, AddCommGroup α

class Module (R : Type) (M : Type) [Zero R] [Zero M] where

instance (R : Type) [Zero R] : Module R R := ⟨⟩

structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where

class HasQuotient (A : outParam <| Type) (B : Type)

instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
  [Module R M]: HasQuotient M (Submodule R M) := {}

structure Synonym (M : Type) [Zero M] where m : M

instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨.mk (Zero.zero : G)⟩

instance Synonym.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Synonym G) :=
  { Synonym.zero with }

instance Synonym.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
    Module R (Synonym M) := { }

variable (R : Type) [Ring R]

class OhNo (B : Type)

instance ohno {R : Type} {M : Type} [Ring R] [AddCommGroup M] [Module R M] : OhNo (Submodule R M) := {}

-- `abbrev` makes no difference, but makes the trace shorter
abbrev S2 := Synonym (Synonym R)

def oh1 : OhNo (Submodule R (S2 R)) := @ohno _ _ _ _ _  -- fails
def oh2 : OhNo (Submodule R (S2 R)) := @ohno _ (S2 R) _ _ _ -- ok

-- the trace indicates that this is the instance which typeclass inference gives up on,
-- but it's easily found
noncomputable instance : AddCommGroup (Synonym R) := inferInstance

def oh3 : type_of% (oh2 R) := ohno  -- ok

Now it's a unification problem rather than a TC problem

[Eric Wieser]

My hunch is that this is a caching bug with the DiscrTree, and that somehow@Synonym R Ring.toZero and @Synonym R AddCommGroup.toZero end up at the same key despite being different types

[Matthew Ballard]

This seems like a strange decision

[] ❌ fun [Zero G] => { zero := { m := Zero.zero } } =?= fun [AddCommGroup G] => AddCommGroup.toZero ▼
          [] ❌ Zero G =?= AddCommGroup G ▼
            [] ❌ Zero =?= AddCommGroup

[Eric Wieser]

Which message is that trace from?

[Matthew Ballard]

oh1 with isDefEq trace.

[Eric Wieser]

What's the full path?

[Eric Wieser]

(There are 7 traces in the sidebar for me, and I don't know which one to expand, or how to fully expand them)

[Matthew Ballard]

The cache in docs#Lean.Meta.synthInstance? seems to have a none for AddCommGroup (S2 R) before the inferInstance and then addCommGroup after

[Matthew Ballard]

Here is another (full) trace

[Meta.isDefEq] ❌ Submodule ?m.1034 ?m.1035 =?= Submodule R (S2 R) ▼
  [] ✅ ?m.1034 =?= R ▶
  [] ✅ ?m.1035 =?= S2 R ▶
  [] ❌ ?m.1038 =?= Synonym.module (Synonym R) ▼
    [] ?m.1038 [assignable] =?= Synonym.module (Synonym R) [nonassignable]
    [] ❌ Module R (S2 R) =?= Module R (Synonym (Synonym R)) ▼
      [] ✅ R =?= R
      [] ✅ S2 R =?= Synonym (Synonym R) ▶
      [] ✅ Ring R =?= Ring R
      [] ✅ Ring.toZero =?= Ring.toZero ▶
      [] ❌ AddCommGroup.toZero =?= Synonym.zero ▼
        [] ❌ AddCommGroup.toZero =?= { zero := { m := Zero.zero } } ▼
          [] ❌ ?m.1037.1 =?= { zero := { m := Zero.zero } } ▼
            [] ✅ Zero (S2 R) =?= Zero (Synonym (Synonym R)) ▶
            [] ❌ Zero.zero =?= { m := Zero.zero } ▼
              [] ❌ ?m.1037.1.1 =?= { m := Zero.zero } ▼
                [] ✅ S2 R =?= Synonym (Synonym R) ▶
                [] ❌ ?m.1037.1.1.m =?= Zero.zero ▼
                  [] ❌ ?m.1037.1.1.1 =?= Zero.zero ▼
                    [] ❌ ?m.1037.1.1.1 =?= Synonym.zero.1 ▼
                      [] ❌ ?m.1037.1.1.1 =?= { m := Zero.zero } ▼
                        [] ✅ Synonym R =?= Synonym R
                        [] ❌ ?m.1037.1.1.1.m =?= Zero.zero ▼
                          [] ❌ ?m.1037.1.1.1.1 =?= Zero.zero ▼
                            [] ❌ ?m.1037.1.1.1.1 =?= Ring.toZero.1 ▼
                              [onFailure] ❌ ?m.1037.1.1.1.1 =?= Ring.toZero.1 ▼
                                [stuckMVar] found stuck MVar ?m.1037 : AddCommGroup (S2 R)

[Matthew Ballard]

And

[Meta.isDefEq] ❌ @AddCommGroup.toZero =?= @Synonym.zero ▼
  [] ❌ @AddCommGroup.toZero =?= fun {G} [Zero G] => { zero := { m := Zero.zero } } ▼
    [] ❌ fun {G} [Zero G] => { zero := { m := Zero.zero } } =?= fun {α} => @AddCommGroup.toZero α ▼
      [] ✅ Type =?= Type
      [] ❌ fun [Zero G] => { zero := { m := Zero.zero } } =?= @AddCommGroup.toZero G ▼
        [] ❌ fun [Zero G] => { zero := { m := Zero.zero } } =?= fun [AddCommGroup G] => AddCommGroup.toZero ▼
          [] ❌ Zero G =?= AddCommGroup G ▼
            [] ❌ Zero =?= AddCommGroup
            [onFailure] ❌ Zero G =?= AddCommGroup G
            [onFailure] ❌ Zero G =?= AddCommGroup G

[Matthew Ballard]

Note that the instance added for AddCommGroup (Synonym R) is not Synonym.addCommGroup which is now found in oh3 but is instAddCommGroupSynonymToZero

[Matthew Ballard]

Why did we go from none to Synonym.addCommGroup in the cache?