From 42ab5dfab0785fb0ea601950c078d6087dadd0f4 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 23 Apr 2025 20:29:10 -0700
Subject: [PATCH] fix: have `runTermElabM` reset local context when types of
 autobound implicits contain metavariables (#7952)

This PR makes two improvements to the local context when there are
autobound implicits in `variable`s. First, the local context no longer
has two copies of every variable (the local context is rebuilt if the
types of autobound implicits have metavariables). Second, these
metavariables get names using the same algorithm used by binders that
appear in declarations (with `mkForallFVars'` instead of
`mkForallFVars`).

This removes the last use of `Term.addAutoBoundImplicits'`, which
inherently has this variable duplication issue.
---
 src/Lean/Elab/Command.lean          | 12 ++++-
 tests/lean/run/autoboundIssues.lean | 82 +++++++++++++++++++++++++++++
 2 files changed, 92 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 41923ad3a0..aed9978afe 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -9,6 +9,7 @@ import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
 import Lean.Language.Basic
+import Lean.Meta.ForEachExpr
 
 namespace Lean.Elab.Command
 
@@ -719,9 +720,16 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
           -- So, we use `Core.resetMessageLog`.
           Core.resetMessageLog
-          let someType := mkSort levelZero
-          Term.addAutoBoundImplicits' xs someType fun xs _ =>
+          let xs ← Term.addAutoBoundImplicits xs none
+          if xs.all (·.isFVar) then
             Term.withoutAutoBoundImplicit <| elabFn xs
+          else
+            -- Abstract any mvars that appear in `xs` using `mkForallFVars` (the type `mkSort levelZero` is an arbitrary placeholder)
+            -- and then rebuild the local context from scratch.
+            -- Resetting prevents the local context from including the original fvars from `xs`.
+            let ctxType ← Meta.mkForallFVars' xs (mkSort levelZero)
+            Meta.withLCtx {} {} <| Meta.forallBoundedTelescope ctxType xs.size fun xs _ =>
+              Term.withoutAutoBoundImplicit <| elabFn xs
 
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
   liftCoreM x
diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean
index 95d1233f96..afcd15a3cc 100644
--- a/tests/lean/run/autoboundIssues.lean
+++ b/tests/lean/run/autoboundIssues.lean
@@ -1,10 +1,92 @@
+/-!
+# Regression tests for auto-bound implicits
+-/
+
+set_option pp.mvars false
+
+/-!
+Auto-bound implicit appears in dot notation in the type, for a variable that appears later.
+-/
 example : n.succ = 1 → n = 0 := by
   intros h; injection h
 
+/-!
+Auto-bound implicit appears in dot notation in a binder, for a variable that appears later.
+-/
 example (h : n.succ = 1) : n = 0 := by
   injection h
 
+/-!
+Auto-bound implicit appears as argument to notation that is postponed.
+The type of `σ` is specialized to `T` later.
+-/
 opaque T : Type
 opaque T.Pred : T → T → Prop
 
 example {ρ} (hρ : ρ.Pred σ) : T.Pred ρ ρ := sorry
+
+
+namespace TestRunTermElab
+/-!
+In the following tests, there is an auto-bound implicit whose type is a metavariable,
+which gets turned into an additional variable.
+-/
+
+def constUnit (a : A) : Type := Unit
+
+/-!
+The auto-bound implicit creates a new variable `A✝`, which comes from the argument name in `constUnit`.
+(This has been the case well before the creation of this test.)
+-/
+/--
+info: A✝ : Sort u_1
+a : A✝
+_x : constUnit a
+⊢ True
+-/
+#guard_msgs in
+example (_x : constUnit a) : True := by
+  trace_state
+  trivial
+
+variable (x : constUnit a)
+
+/-!
+The local context here used to be
+```
+a✝ : ?_
+x✝¹ : constUnit a✝
+x✝ : Sort ?_
+a : x✝
+x : constUnit a
+⊢ True
+```
+Note the duplication and `x✝` for the name of the metavariable-as-a-variable.
+The duplication was because `runTermElabM` wasn't resetting the local context.
+The poor variable name was due to using `mkForallFVars` instead of `mkForallFVars'`.
+-/
+/--
+info: A✝ : Sort _
+a : A✝
+x : constUnit a
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  trace_state
+  trivial
+
+/-!
+Checking that `#check` also has the improvement.
+-/
+/--
+info: 1 : Nat
+---
+info: A✝ : Sort _
+a : A✝
+x : constUnit a
+⊢ ?_
+-/
+#guard_msgs in #check (by trace_state; exact 1)
+
+end TestRunTermElab