From 291e95e3c577dda38ea149939734f3426d426c89 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Tue, 24 Oct 2023 19:26:09 -0400
Subject: [PATCH] fix: add `instantiateMVars` to `replaceLocalDecl` (#2712)

* fix: `instantiateMVars` in `replaceLocalDecl`
* docs: update `replaceLocalDecl`
* test: `replaceLocalDecl` instantiates mvars
---
 src/Lean/Meta/Tactic/Replace.lean             | 21 ++++--
 .../replaceLocalDeclInstantiateMVars.lean     | 64 +++++++++++++++++++
 ...ocalDeclInstantiateMVars.lean.expected.out |  4 ++
 3 files changed, 82 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/replaceLocalDeclInstantiateMVars.lean
 create mode 100644 tests/lean/replaceLocalDeclInstantiateMVars.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
index 1089cd630b..99b279b9eb 100644
--- a/src/Lean/Meta/Tactic/Replace.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -62,9 +62,12 @@ private def replaceLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (typeNew :
   mvarId.withContext do
     let localDecl ← fvarId.getDecl
     let typeNewPr ← mkEqMP eqProof (mkFVar fvarId)
-    -- `typeNew` may contain variables that occur after `fvarId`.
-    -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed at the position we are inserting it.
-    let (_, localDecl') ← findMaxFVar typeNew |>.run localDecl
+    /- `typeNew` may contain variables that occur after `fvarId`.
+        Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed at the
+        position we are inserting it.
+        We must `instantiateMVars` first to ensure that there is no mvar in `typeNew` which is
+        assigned to some later-occurring fvar. -/
+    let (_, localDecl') ← findMaxFVar (← instantiateMVars typeNew) |>.run localDecl
     let result ← mvarId.assertAfter localDecl'.fvarId localDecl.userName typeNew typeNewPr
     (do let mvarIdNew ← result.mvarId.clear fvarId
         pure { result with mvarId := mvarIdNew })
@@ -81,11 +84,15 @@ where
 
 /--
   Replace type of the local declaration with id `fvarId` with one with the same user-facing name, but with type `typeNew`.
-  This method assumes `eqProof` is a proof that type of `fvarId` is equal to `typeNew`.
-  This tactic actually adds a new declaration and (try to) clear the old one.
+  This method assumes `eqProof` is a proof that the type of `fvarId` is equal to `typeNew`.
+  This tactic actually adds a new declaration and (tries to) clear the old one.
   If the old one cannot be cleared, then at least its user-facing name becomes inaccessible.
-  Remark: the new declaration is added immediately after `fvarId`.
-  `typeNew` must be well-formed at `fvarId`, but `eqProof` may contain variables declared after `fvarId`. -/
+
+  The new local declaration is inserted at the soonest point after `fvarId` at which it is
+  well-formed. That is, if `typeNew` involves declarations which occur later than `fvarId` in the
+  local context, the new local declaration will be inserted immediately after the latest-occurring
+  one. Otherwise, it will be inserted immediately after `fvarId`.
+  -/
 abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   replaceLocalDeclCore mvarId fvarId typeNew eqProof
 
diff --git a/tests/lean/replaceLocalDeclInstantiateMVars.lean b/tests/lean/replaceLocalDeclInstantiateMVars.lean
new file mode 100644
index 0000000000..f44b34da81
--- /dev/null
+++ b/tests/lean/replaceLocalDeclInstantiateMVars.lean
@@ -0,0 +1,64 @@
+import Lean
+
+/-!
+# Ensure `replaceLocalDecl` instantiates metavariables
+
+These tests ensure that `replaceLocalDecl` is aware of `FVarId`s present in the assignments of
+metavariables present in the inserted declaration, and thus does not introduce unknown `FVarId`s by
+inserting a local declaration before it's well-formed.
+
+## Context
+
+`replaceLocalDecl mvarId fvarId typeNew eqProof` replaces `fvarId` with a new FVarId that has the
+same name but type `typeNew`. It does this by inserting a new local declaration with type `typeNew`
+and clearing the old one if possible.
+
+It makes sure that the new local declaration is inserted at the soonest point after `fvarId` at
+which `typeNew` is well-formed. It does this by traversing `typeNew` and finding the `FVarId` with
+the maximum index among all `FVarId`s occurring in `typeNew`.
+
+If `replaceLocalDecl` encounters a metavariable during this traversal, it simply continues
+traversing. Previously, it might have been the case that this metavariable we encountered was
+assigned to an expression which contains an `FVarId` occurring after `fvarId`. This can lead to
+`replaceLocalDecl` inserting a local declaration with a type which depends on `FVarId`s which come
+after it in the local context, thus creating unknown `FVarId`s. (Note that the `FVarId`s of the
+local declarations occurring after the insertion are modified, so the `FVarId` involved in the
+assignment may not even exist in the local context anymore.)
+
+We now attempt to prevent `replaceLocalDecl` from encountering assigned metavariables by
+calling `instantiateMVars` in `replaceLocalDecl` before traversal.
+
+Note that this is not a perfect solution to the overall problem; `Term.synthesizeSyntheticMVars`
+may introduce assignments to inaccessible `FVarId`s after `replaceLocalDecl` has run, in which case
+`instantiateMVars` is ineffective (as the metavariable has not even been assigned yet). See issue
+#2727.
+-/
+
+/-! ## Direct test of instantiated mvars -/
+
+open Lean Meta Elab Tactic in
+/-- Replace the type of `fvar₁` with `fvar₂ = fvar₂` where the expression `fvar₂ = fvar₂` is hidden
+under a metavariable assignment. Note that initially `fvar₁` must come before `fvar₂` in order to
+make sure `replaceLocalDecl` is behaving correctly. -/
+elab "replace " fvar₁:ident " with " fvar₂:ident " via " proof:term : tactic => withMainContext do
+  let fvar₁ ← getFVarId fvar₁
+  let fvar₂ ← getFVarId fvar₂
+  let underlyingTypeNew ← inferType <|← mkEqRefl (Expr.fvar fvar₂)
+  -- make a metavariable to use as the type in `replaceLocalDecl`; assign it to `underlyingTypeNew`
+  let typeNewMVar ← mkFreshExprMVar none
+  typeNewMVar.mvarId!.assign underlyingTypeNew
+  let proof ← elabTerm proof underlyingTypeNew
+  let { mvarId .. } ← (← getMainGoal).replaceLocalDecl fvar₁ typeNewMVar proof
+  replaceMainGoal [mvarId]
+
+example : True := by
+  have h₁ : True := trivial
+  have h₂ : Nat := 0
+  replace h₁ with h₂ via eq_true rfl |>.symm
+  /-
+  Previously, goal state was:
+
+  h₁: _uniq.NNNN = _uniq.NNNN
+  h₂: Nat
+  ⊢ True
+  -/
diff --git a/tests/lean/replaceLocalDeclInstantiateMVars.lean.expected.out b/tests/lean/replaceLocalDeclInstantiateMVars.lean.expected.out
new file mode 100644
index 0000000000..5ef4a105a0
--- /dev/null
+++ b/tests/lean/replaceLocalDeclInstantiateMVars.lean.expected.out
@@ -0,0 +1,4 @@
+replaceLocalDeclInstantiateMVars.lean:54:18-57:44: error: unsolved goals
+h₂ : Nat
+h₁ : h₂ = h₂
+⊢ True