fix: rw ... at h unknown fvar bug (#2728)

src/Lean/Elab/Tactic/Rewrite.lean

@@ -19,13 +19,15 @@ def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) :
     replaceMainGoal (mvarId' :: r.mvarIds)
 
 def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) :
-    TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
+    TacticM Unit := withMainContext do
+  -- Note: we cannot execute `replaceLocalDecl` inside `Term.withSynthesize`.
+  -- See issues #2711 and #2727.
+  let rwResult ← Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
     let localDecl ← fvarId.getDecl
-    let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
-    let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
-    replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
+    (← getMainGoal).rewrite localDecl.type e symm (config := config)
+  let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
+  replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
 
 def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
   let lbrak := rwRulesSeqStx[0]

src/Lean/Meta/Tactic/Replace.lean

@@ -92,6 +92,10 @@ where
   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`.
+
+  Note: `replaceLocalDecl` should not be used when unassigned pending mvars might be present in
+  `typeNew`, as these may later be synthesized to fvars which occur after `fvarId` (by e.g.
+  `Term.withSynthesize` or `Term.synthesizeSyntheticMVars`) .
   -/
 abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   replaceLocalDeclCore mvarId fvarId typeNew eqProof

tests/lean/rwWithSynthesizeBug.lean

@@ -0,0 +1,46 @@
+/-!
+# Ensure that `rw ... at h` does not create unknown free variables (issue #2711)
+
+## Context
+
+`rw ... at h` elaborates its rules with postponed metavariables, which, prior to this test, were
+synthesized after the bulk of the tactic has taken place by `Term.withSynthesize`. Specifically,
+these mvars were synthesized after `replaceLocalDecl` has executed.
+
+`replaceLocalDecl` needs to be sure it's not inserting the new, rewritten hypothesis before any
+fvars which the type of that hypothesis now depends on. For example, if the type of `h` got
+rewritten to `f i` where `i` was a local declaration occurring after `h`, `replaceLocalDecl` should
+insert the rewritten `h` after `i`.
+
+To ensure this, it traverses the type looking for fvars to find the latest-occurring one. However,
+the pending mvars it might encounter in the type have not even been assigned yet, and so
+`replaceLocalDecl` will not find any fvars when it traverses over them. `Term.withSynthesize` might
+nevertheless assign these mvars to later-occurring fvars afterwards. As such, the type of the
+rewritten hypothesis might become ill-formed at the place `replaceLocalDecl` inserts it once the
+pending mvars are assigned, as it might now include unknown `FVarId`s (the `FVarId`s following the
+insertion spot will have been changed by the insertion).
+
+This test reflects the choice to synthesize the pending mvars before `replaceLocalDecl` is
+executed, thus avoiding this issue.
+-/
+
+class Bar (α) where a : α
+
+def f {α} [Bar α] (a : α) := a
+
+def w (_ : α) : Prop := True
+
+theorem foo {a : α} [Bar α] : w a = w (f a) := rfl
+
+set_option pp.explicit true in
+example : True := by
+  have h : w 5 := trivial
+  let inst : Bar Nat := ⟨0⟩
+  rw [foo] at h
+  -- Previous goal state:
+  /-
+  h✝ : @w Nat 5
+  h : @w Nat (@f Nat _uniq.158 5)
+  inst : Bar Nat := @Bar.mk Nat 0
+  ⊢ True
+  -/

tests/lean/rwWithSynthesizeBug.lean.expected.out

@@ -0,0 +1,4 @@
+rwWithSynthesizeBug.lean:36:18-39:15: error: unsolved goals
+inst : Bar Nat := @Bar.mk Nat 0
+h : @w Nat (@f Nat inst 5)
+⊢ True