Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When named arguments are inserted in a partial function application after other arguments that are not provided, the whole application is wrapped in a lambda that abstracts the missing arguments.

For example, given

def sum3 (x y z : Nat) : Nat := x + y + z

the following works:

/-- info: fun x y => sum3 x y 3 : Nat → Nat → Nat -/
#guard_msgs in
#check sum3 (z := 3)

This lambda uses the same name for its parameters as the missing ones. This means that it can itself be used with named arguments later. The function's type keeps the parameter names, even though the pretty printer doesn't show it when they don't occur bound in their scope:

/--
info: let f := fun x y => sum3 x y 3;
fun x => f x 2 : Nat → Nat
-/
#guard_msgs in
#check let f := sum3 (z := 3); f (y := 2)

/-- info: fun x => (fun x y => sum3 x y 3) x 2 : Nat → Nat -/
#guard_msgs in
#check (sum3 (z := 3)) (y := 2)

There's unfortunately a variable capture bug. The variables inserted for the arguments to be abstracted are called eta arguments in the elaborator. The comment on the code that inserts eta arguments states that they should be fresh names, but the elaborator actually inserts the function type's parameter name:

This is subject to variable capture if one of the arguments to be inserted refers to a bound variable with the same name as the argument.

Context

This came up when documenting function application syntax for the language reference.

Steps to Reproduce

1. Put the following in a blank Lean file:

   def sum3 (x y z : Nat) : Nat := x + y + z
   
   #check (let w := 15; sum3 (z := w)) (y := 3)
   
   #check (let x := 15; sum3 (z := x)) (y := 3)

2. The two expressions after #check are alpha equivalent in the source language, but their elaborations are not alpha equivalent, as can be seen both in the output of #check and by the fact that the let-binding of x in the second one has an unused variable warning.
3. Double-check that the two expressions are not equivalent by applying them to 0:

   #eval (let w := 15; sum3 (z := w)) (y := 3) <| 0
   
   #eval (let x := 15; sum3 (z := x)) (y := 3) <| 0

   The first evaluates to 18, the second to 3.

Expected behavior:

The two should have alpha-equivalent elaborations and be the same function. Or, alternatively, eta args just wouldn't be usable as named parameters to the resulting function (that is, do what the comment says and generate fresh names).

Actual behavior:

They two terms differ, because the value of z becomes 0 in the second case due to being captured by the inserted x argument.

Note
I think the elaborator could avoid the variable capture issue while still allowing the eta arguments to be inserted by name if it used a fresh name for the bound variable, but the parameter name in a type ascription. The inner set of eta args could be elaborated as

#check (let x := 15; show (x y : Nat) → Nat from fun freshx freshy => sum3 freshx freshy x) (y := 3)

though I'm not sure if there's other issues to worry about here. For some reason, only show works here - an ordinary type ascription still results in capture.

Versions

"4.16.0-nightly-2024-12-12"

Additional Information

None

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.