class HOp (α β γ) where hOp : α → β → γ

class LOp (α β) where lOp : α → β → β

class Op (α) where op : α → α → α

@[default_instance]
instance inst1 [LOp α β] : HOp α β β := ⟨LOp.lOp⟩

instance inst2 [Op α] : LOp α α := ⟨Op.op⟩

infix:75 " ⋆ " => HOp.hOp

section Test
variable (α) [LOp Nat α]
variable (x y z : α) (m n : Nat)

example : n ⋆ x = z := sorry -- TC works

example : 1 ⋆ x = z := sorry -- TC works

attribute [default_instance] inst2

example : n ⋆ x = z := sorry -- TC works

example : 1 ⋆ x = z := sorry -- TC fails

end Test