Typeclass inference diamond

Stream: lean4

[Kyle Miller]

While experimenting with ways to deal with diamonds, and I ran across an example that's puzzling to me. I've reduced it (without changing the names) to try to isolate the behavior: while CommMonoid.mk is an instance, and it's able to construct an instance just fine when used directly, inferInstance in the same position is not able to.

class HasMulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a

class Semigroup (α : Type u) where
    [Mul : Mul α]
attribute [instance] Semigroup.mk Semigroup.Mul

class Monoid (α : Type u) where
    [Semigroup : Semigroup α]
attribute [instance] Monoid.mk Monoid.Semigroup

class CommSemigroup (α : Type u) where
    [Semigroup : Semigroup α]
    [HasMulComm : HasMulComm α]
attribute [instance] CommSemigroup.mk CommSemigroup.Semigroup CommSemigroup.HasMulComm

class CommMonoid (α : Type u) where
    [Monoid : Monoid α]
    [HasMulComm : HasMulComm α]
attribute [instance] CommMonoid.mk CommMonoid.Monoid CommMonoid.HasMulComm

variables {β : Type u} [CommSemigroup β]
example : Monoid β := inferInstance
example : Semigroup β := inferInstance
example : CommMonoid β := CommMonoid.mk -- ok
example : CommMonoid β := inferInstance -- not ok

/- ok: -/
example : (CommMonoid.mk : CommMonoid β).HasMulComm = (inferInstanceAs (CommSemigroup β)).HasMulComm := rfl

[Kyle Miller]

Is it expected for there to be a difference between the last two examples? (Tested on both stable and nightly.)

class HasMulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a

class A (α : Type u) where
    [Mul : Mul α]
attribute [instance] A.mk A.Mul

class B (α : Type u) where
    [Mul : Mul α]
    [HasMulComm : HasMulComm α]
attribute [instance] B.mk B.Mul B.HasMulComm

-- OK:
example [A α] [HasMulComm α] : B α := inferInstance

section
variables [A α] [HasMulComm α]

-- OK:
example : B α := by exact inferInstance

-- Not OK:
example : B α := inferInstance
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

end

[Leonardo de Moura]

Thanks. Pushed a fix and added your example to the test suite.
https://github.com/leanprover/lean4/commit/300fcc3321adbee229549a870787aec5f12b2d09

[Kyle Miller]

Here is a variation on this theme. I'm wondering why inferInstance fails but B.mk succeeds:

class HasMulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a

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

class B (α : Type u) extends A α, HasMulComm α
attribute [instance] B.mk

example [Mul α] : A α := inferInstance
example [Mul α] [HasMulComm α] : A α := inferInstance
example [B α] : A α := inferInstance

example [A α] [HasMulComm α] : B α := inferInstance
example [Mul α] [HasMulComm α] : B α := inferInstance -- fails
example [Mul α] [HasMulComm α] : B α := B.mk

If I'm reading the Meta.synthInstance trace correctly, for B.mk it finds an A instance first and then succeeds in finding the HasMulComm instance, but the inferInstance jumps straight to trying to find a HasMulComm.

[Leonardo de Moura]

Pushed a fix.
The issue looks similar to the previous one, but it was due to a completely different issue.