Lemmas with `IsCommutative` etc. arguments require type annotations

[gebner]

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

[eric-wieser]

I think we might have had this problem in lean 3 too, it was not uncommon to have to add a type annotation to make dot notation work.

[gebner]

I've clarified the title of the issue. This is a different issue, and it's new in Lean 4 because we didn't have the stuck exception handling in Lean 3. This issue also appears without dot-notation:

#check Iff.mp foo -- fails
#check Iff.mp foo h -- fails