Lean doesn't try unfolding when it could #1892
Description
def OrderDual (α : Type u) : Type u := α
variable (α : Type u) [instLE : LE α] {a b : α}
instance : LE (OrderDual α) := ⟨fun x y : α => y ≤ x⟩
theorem foo : a ≤ b := sorry
example : a ≤ b := foo (OrderDual α) -- fails
-- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
-- instLEOrderDual
-- inferred
-- instLE
example : a ≤ b := @foo (OrderDual α) _ b a -- works
example : a ≤ b := (foo (OrderDual α) :) -- worksHere we have a goal @LE.le.{u} α instLE a b which we want to match against @LE.le.{u} (OrderDual.{u} α) (@instLEOrderDual.{u} α instLE) ?a ?b, which is possible by unfolding instLEOrderDual and then assigning ?a := b, ?b := a. However lean seems to latch on the solution ?a := a, ?b := b and then complains that the instance argument does not match.