fix: make sure app elaborator eta feature does not result in capturable variables (#10377)

This PR fixes an issue where the "eta feature" in the app elaborator,
which is invoked when positional arguments are skipped due to named
arguments, results in variables that can be captured by those named
arguments. Now the temporary local variables that implement this feature
get fresh names. The names used for the closed lambda expression still
use the original parameter names.

Closes #6373

src/Lean/Elab/App.lean

@@ -169,9 +169,11 @@ structure State where
     -- fun x => f x 5
     ```
     `etaArgs` stores the fresh free variables for implementing the eta-expansion.
+    Each pair records the name to use for the binding and the fvar for the argument.
+
     When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`.
   -/
-  etaArgs              : Array Expr   := #[]
+  etaArgs              : Array (Name × Expr)   := #[]
   /-- Metavariables that we need to set the error context using the application being built. -/
   toSetErrorCtx        : Array MVarId := #[]
   /-- Metavariables for the instance implicit arguments that have already been processed. -/
@@ -420,7 +422,8 @@ private def finalize : M Expr := do
   for mvarId in s.toSetErrorCtx do
     registerMVarErrorImplicitArgInfo mvarId ref e
   if !s.etaArgs.isEmpty then
-    e ← mkLambdaFVars s.etaArgs e
+    e ← mkLambdaFVars (s.etaArgs.map (·.2)) e
+    e := e.updateBinderNames (s.etaArgs.map (some <| ·.1)).toList
   /-
     Remark: we should not use `s.fType` as `eType` even when
     `s.etaArgs.isEmpty`. Reason: it may have been unfolded.
@@ -562,8 +565,9 @@ mutual
   private partial def addEtaArg (argName : Name) : M Expr := do
     let n    ← getBindingName
     let type ← getArgExpectedType
-    withLocalDeclD n type fun x => do
-      modify fun s => { s with etaArgs := s.etaArgs.push x }
+    -- Use a fresh name to ensure that the remaining arguments can't capture this parameter's name.
+    withLocalDeclD (← Core.mkFreshUserName n) type fun x => do
+      modify fun s => { s with etaArgs := s.etaArgs.push (n, x) }
       addNewArg argName x
       main
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -306,7 +306,7 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
 
 @[builtin_tactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx =>
   match stx with
-  | `(tactic| apply $e) => evalApplyLikeTactic (·.apply (term? := some m!"`{e}`")) e
+  | `(tactic| apply $t) => evalApplyLikeTactic (fun g e => g.apply e (term? := some m!"`{e}`")) t
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun _ =>

src/Lean/Expr.lean

@@ -1346,7 +1346,7 @@ def inferImplicit (e : Expr) (numParams : Nat) (considerRange : Bool) : Expr :=
   | e, _ => e
 
 /--
-Uses `newBinderInfos` to update the binder infos of the first `numParams` foralls.
+Uses `binderInfos?` to update the binder infos of the corresponding forall expressions.
 -/
 def updateForallBinderInfos (e : Expr) (binderInfos? : List (Option BinderInfo)) : Expr :=
   match e, binderInfos? with
@@ -1356,6 +1356,21 @@ def updateForallBinderInfos (e : Expr) (binderInfos? : List (Option BinderInfo))
     Expr.forallE n d b bi
   | e, _ => e
 
+/--
+Uses `binderNames?` to update the binder names of the corresponding lambda and forall expressions.
+-/
+def updateBinderNames (e : Expr) (binderNames? : List (Option Name)) : Expr :=
+  match e, binderNames? with
+  | Expr.forallE n d b bi, newN? :: binderNames? =>
+    let b := updateBinderNames b binderNames?
+    let n := newN?.getD n
+    Expr.forallE n d b bi
+  | Expr.lam n d b bi, newN? :: binderNames? =>
+    let b := updateBinderNames b binderNames?
+    let n := newN?.getD n
+    Expr.lam n d b bi
+  | e, _ => e
+
 /--
 Instantiates the loose bound variables in `e` using the `subst` array,
 where a loose `Expr.bvar i` at "binding depth" `d` is instantiated with `subst[i - d]` if `0 <= i - d < subst.size`,

tests/lean/run/5475.lean

@@ -12,7 +12,7 @@ Formerly, argument `x` appeared as `_fvar.123`
 def f {α β : Type} (x: α) (y: β) : α := x
 /--
 error: don't know how to synthesize implicit argument `α`
-  @f ?_ Nat x Nat.zero
+  @f ?_ Nat x✝ Nat.zero
 context:
 ⊢ Type
 ---

tests/lean/run/6373.lean

@@ -0,0 +1,50 @@
+/-!
+# Test for issue 6373, variable capture for app elaborator eta feature
+
+https://github.com/leanprover/lean4/issues/6373
+-/
+
+def sum3 (x y z : Nat) : Nat := x + y + z
+
+/-!
+The following two used to elaborate differently.
+Now in the second, we can see that the `x` in the `fun` (from the eta feature), does not shadow the `x` in the `let`.
+Note that in both, `y` can still be used as a named argument.
+-/
+/--
+info: fun x =>
+  (let w := 15;
+    fun x y => sum3 x y w)
+    x 3 : Nat → Nat
+-/
+#guard_msgs in
+#check (let w := 15; sum3 (z := w)) (y := 3)
+/--
+info: fun x =>
+  (let x := 15;
+    fun x_1 y => sum3 x_1 y x)
+    x 3 : Nat → Nat
+-/
+#guard_msgs in
+#check (let x := 15; sum3 (z := x)) (y := 3)
+
+/-!
+Verifying that each evaluates to the same value when evaluated at `0`.
+The second used to evaluate to `3` instead of `18`.
+-/
+/-- info: 18 -/
+#guard_msgs in
+#eval (let w := 15; sum3 (z := w)) (y := 3) <| 0
+/-- info: 18 -/
+#guard_msgs in
+#eval (let x := 15; sum3 (z := x)) (y := 3) <| 0
+
+/-!
+Same verification, but make sure that `0` can be passed as a named argument.
+-/
+/-- info: 18 -/
+#guard_msgs in
+#eval (let w := 15; sum3 (z := w)) (y := 3) (x := 0)
+/-- info: 18 -/
+#guard_msgs in
+#eval (let x := 15; sum3 (z := x)) (y := 3) (x := 0)

tests/lean/run/funind_proof.lean

@@ -41,7 +41,7 @@ info: Term.replaceConst.induct (a : String) (motive1 : Term → Prop) (motive2 :
 #check replaceConst.induct
 
 theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  apply replaceConst.induct
+  apply replaceConst.induct (a := a)
     (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es)
   case case1 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *]
@@ -58,7 +58,7 @@ theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceCon
     simp [replaceConstLst, numConstsLst, *]
 
 theorem numConsts_replaceConst' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  apply replaceConst.induct
+  apply replaceConst.induct (a := a)
     (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es)
   <;> intros <;> simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]