test: replaceLocalDecl instantiates mvars

tests/lean/replaceLocalDeclInstantiateMVars.lean

@@ -0,0 +1,82 @@
+import Lean
+
+/-!
+# Ensure `replaceLocalDecl` instantiates metavariables
+
+These tests ensure that `replaceLocalDecl` does not introduce unknown `FVarId`s by inserting a new
+local declaration too early.
+
+## 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`.
+
+However, if it encounters a metavariable during this traversal, it simply continues traversing,
+even if this metavariable is 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 (the
+`FVarId`s of the local declarations after the insertion are modified).
+-/
+
+/-!
+## Free variable in typeclass synthesis
+
+This test uses `rw ... at`, which employs `replaceLocalDecl` after `MVarId.rewrite`.
+`MVarId.rewrite` does not necessarily instantiate metavariables in its output (including instance
+metavariables).
+-/
+
+class Bar (α) where a : α
+
+def f {α} [Bar α] (a : α) := a
+
+def w (_ : Nat) : Prop := True
+
+theorem foo {α} [Bar α] (a : α) : a = f a := rfl
+
+set_option pp.explicit true in
+example : True := by
+  have h : w 5 := trivial
+  let inst : Bar Nat := ⟨0⟩
+  rw [foo 5] at h
+  /-
+  Previously, goal state was:
+
+  h✝: w 5
+  h: w (@f Nat _uniq.NNN 5)
+  inst: Bar Nat := @Bar.mk Nat 0
+  ⊢ True
+  -/
+
+/-! ## Direct test -/
+
+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 typeNewMVar ← mkFreshExprMVar none
+  let underlyingTypeNew ← inferType <|← mkEqRefl (Expr.fvar fvar₂)
+  typeNewMVar.mvarId!.assign underlyingTypeNew
+  let proof ← elabTerm proof underlyingTypeNew
+  let { mvarId .. } ← (← getMainGoal).replaceLocalDecl fvar₁ underlyingTypeNew 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
+  -/

tests/lean/replaceLocalDeclInstantiateMVars.lean.expected.out

@@ -0,0 +1,9 @@
+replaceLocalDeclInstantiateMVars.lean:43:18-46:17: error: unsolved goals
+h✝ : w 5
+inst : Bar Nat := @Bar.mk Nat 0
+h : w (@f Nat inst 5)
+⊢ True
+replaceLocalDeclInstantiateMVars.lean:72:18-75:44: error: unsolved goals
+h₂ : Nat
+h₁ : h₂ = h₂
+⊢ True