unifying ⦃x y⦄ with {x y}

Stream: lean4

[Kevin Buzzard]

Unification is a bit less powerful here in Lean 4 than in Lean 3:

variable {α : Type}

def Symmetric (r : α → α → Prop) := ∀ ⦃x y⦄, r x y → r y x

example (r : α → α → Prop) (hr : Symmetric r): ∀ {x y}, r x y → r y x := hr -- works in Lean 3, fails in Lean 4
example (r : α → α → Prop) (hr : Symmetric r): ∀ {x y}, r x y → r y x := λ foo => hr foo -- works in Lean 4

I don't know what the desired behaviour is (i.e. whether this should work or not), but the reason it's autoport-breaking is that in core Lean 4 we have Equivalence defined with {x y} fields and in Mathlib4 we have Symmetric defined with ⦃x y⦄. I don't have any objections to putting in all the lambdas of course.

[Mario Carneiro]

cc: @Leonardo de Moura

[Mario Carneiro]

I'm torn on whether this should work. The only reason it works in lean 3 is because it doesn't do auto-implicits in the first place; if you wrote \lam _ _, hr then it wouldn't work in lean 3 either. I think @hr will work in this case

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/equivalence.20relations.20are.20symmetric/near/308132822 is also related

[Leonardo de Moura]

@Mario Carneiro Yes, the issue is due to the new implicit lambda feature in Lean 4. @hr is a good workaround.
The binder notation ⦃x y⦄ is very Lean-specific, and does not work well with the implicit lambda feature.
It would be great to collect many examples that are triggering this problem. We should discuss this issue in the next dev meeting.