# Zulip Chat Archive

## Stream: lean4

### Topic: Typeclass inference diamond

#### Kyle Miller (Jan 09 2021 at 06:02):

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 (Jan 10 2021 at 23:23):

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 (Jan 11 2021 at 14:46):

Thanks. Pushed a fix and added your example to the test suite.

https://github.com/leanprover/lean4/commit/300fcc3321adbee229549a870787aec5f12b2d09

#### Kyle Miller (Jan 13 2021 at 19:40):

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 (Jan 14 2021 at 02:50):

Pushed a fix.

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

Last updated: May 07 2021 at 12:15 UTC