Lemmas with `IsCommutative` etc. arguments require type annotations

class IsCommutative (op : α → α → α) where
  comm : op x y = op y x

class LeftUnit (α : Type u) extends Mul α

class Monoid (α : Type u) extends LeftUnit α

class CommMonoid (α : Type u) extends LeftUnit α where
  mul_comm {x y : α} : x * y = y * x

instance [CommMonoid α] : IsCommutative (α := α) (· * ·) where
  comm := CommMonoid.mul_comm

instance [CommMonoid α] : Monoid α where

theorem foo [Monoid α] [IsCommutative (α := α) (· * ·)] {x y : α} :
    x * y = z ↔ y * x = z := by
  rw [IsCommutative.comm (op := (· * ·))]
  exact Iff.rfl

instance : CommMonoid Nat where
  mul_comm := Nat.mul_comm _ _

set_option trace.Meta.synthInstance true
variable (a b c : Nat) (h : a * b = c)

#check foo -- ok
#check foo.1 -- failed to synthesize instance IsCommutative (NOT stuck!)
#check foo.1 h -- failed to synthesize instance IsCommutative (NOT stuck!)
def bar := foo.1 h -- failed to synthesize instance IsCommutative (NOT stuck!)
#check Iff.mp foo -- failed to synthesize instance IsCommutative (NOT stuck!)
#check Iff.mp foo h -- failed to synthesize instance IsCommutative (NOT stuck!)

The last five commands should all succeed. Mathlib has a lot of lemmas like foo (usually due to CovariantClass, so e.g. le_neg, abs_pos, etc.). (It's important that the instance [CommMonoid α] → Monoid α is not a subobject projection here, but this is super common in the algebraic hierarchy.)

What's happening here is that we ignore the stuck exception in nested TC problems. So Lean thinks that the only IsCommutative instance does not apply because it cannot unify Monoid.toLeftUnit =?= CommMonoid.toLeftUnit while the type is still a metavariable. And since we ignore the stuck exception, we never try again. cc @Kha

A workaround is to specify the type manually (surprising syntax btw):

#check foo (α := Nat).1 -- ok
#check foo (α := Nat).1 h -- ok
def bar := foo (α:= Nat).1 h -- ok

For comparison, all is well without the IsCommutative argument:

theorem foo' [Monoid α] {x y : α} : x * y = z ↔ x * y = z := .rfl
#check foo' -- ok
#check foo'.1 -- ok
#check foo'.1 h -- ok
def bar' := foo'.1 h -- ok

Start by reproducing the foo and foo' checks in the issue and comparing nested typeclass synthesis with and without the IsCommutative argument. Trace the stuck nested typeclass problem described in the report; done means all five unannotated commands succeed without the manual α annotation.