behavior of `(arg := sorry)` syntax

Stream: lean4

[Jireh Loreaux]

Guess which of the following succeeds. I find this behavior extremely counterintuitive.

theorem foo (n m : Nat) (h : m = n) : m = n := h

example (n m : Nat) (h' : m = n) : m = n :=
  foo (h := h')

example (n m : Nat) (h' : m = n) : m = n :=
  foo _ _ (h := h')

example (n m : Nat) (h' : m = n) : m = n :=
  foo _ _ h'

[Jireh Loreaux]

This behavior means that supplying arguments with the (arg := sorry) syntax makes the user think / guess which prior arguments can be inferred from the value of arg!

[Kyle Miller]

This seems related to issue lean4#1867, and I added your example. I'm not sure whether it's working as intended or not, but it feels like a bug to me.

[Jireh Loreaux]

Indeed, that appears to be the same thing. Thanks!