Missing named arg error reported late

Stream: lean4

[James Gallicchio]

For code like this:

def test : Nat → String → Nat := λ i _ => i

#check test (foo := 5) "hi"

I would expect this to error at foo := 5 saying that test doesn't have a parameter foo. But instead it gives a type error at "hi" because it doesn't match the type of the first arg.

This is kind of confusing -- I just had an example where I thought an argument of some function was named (it wasn't) and I had a confusing type error on a different parameter; the "fix" was to pass the named parameter unnamed

[Leonardo de Moura]

Pushed the following improvement https://github.com/leanprover/lean4/commit/40c8db7494adccfbc9fb35920b91b65dc1b6df3f
The commit also improves the error position for argument type mismatches. Here is the new test.

def boo (x : Nat) (y : Nat) := x + y
def bla (x : Nat) := boo x

#check bla (y := 2) 5     -- Ok
#check bla (y := 5) "hi"  -- 1 error at "hi"
#check bla (z := 5) "hi"  -- 2 errors at `(z := 5)` and "hi"
#check bla (z := 5) 2     -- 1 errors at `(z := 5)`