From f771dea78b01bd4fff123a372ed3311186bd43ad Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 14 Sep 2025 13:19:50 -0700 Subject: [PATCH] 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 | 12 ++++--- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- src/Lean/Expr.lean | 17 +++++++++- tests/lean/run/5475.lean | 2 +- tests/lean/run/6373.lean | 50 ++++++++++++++++++++++++++++++ tests/lean/run/funind_proof.lean | 4 +-- 6 files changed, 78 insertions(+), 9 deletions(-) create mode 100644 tests/lean/run/6373.lean diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 050581e1b6..648ed62c64 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index c5aa567070..201b09b3da 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/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 _ => diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 838b8f1524..c2b34bd068 100644 --- a/src/Lean/Expr.lean +++ b/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`, diff --git a/tests/lean/run/5475.lean b/tests/lean/run/5475.lean index a194038a7e..47ea0cf417 100644 --- a/tests/lean/run/5475.lean +++ b/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 --- diff --git a/tests/lean/run/6373.lean b/tests/lean/run/6373.lean new file mode 100644 index 0000000000..b8230d8f0e --- /dev/null +++ b/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) diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean index faf7c41daa..1948df974a 100644 --- a/tests/lean/run/funind_proof.lean +++ b/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, *]