`rw` inserts rewritten hypothesis that forward-references fvar

[datokrat]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

rw [lemma] at hyp can leave hyp with a type that references a free variable which no longer exists in the local context, in the form of a literal _fvar.n. Subsequent tactics that recurse into that subterm, e.g. another rw that must match against ?c[?i], then fail with varying error messages because of the fvar., because the unifier aborts on the dangling fvar.

Context

Discovered while working on the getElemV refactor of Init.Data.String.Basic. See commit Slice.Pos.next_le_of_lt in https://github.com/leanprover/lean4/blob/2fd80bb88ea0c3c2400b7539baa92ec341f200f1/src/Init/Data/String/Basic.lean.

Steps to Reproduce

Observe the error in

theorem getElem_eq_sorry (b : ByteArray) (i : Nat) (hi : i < b.size) :
    b[i] = sorry :=
  sorry

/-- error: unknown free variable `_fvar.478` -/
#guard_msgs in
example (b : ByteArray) (i : Nat) (hi : i < b.size)
    (P : UInt8 → Prop) (hyp : P (b[i]'hi)) : True := by
  have h₂ : i < (b.extract 0 b.size).size := by simp; omega
  rw [show b[i]'hi = b[0 + i]'(by omega) by simp] at hyp
  rw [← ByteArray.getElem_extract] at hyp
  rotate_left
  · exact h₂
  · -- hyp is now `P (getElem (b.extract 0 b.size) i _fvar.478)`
    rw [getElem_eq_sorry] at hyp
    trivial

Expected behavior: No error, proof should succeed.

Actual behavior:

hyp's type contains an invalid _fvar.n as bounds proof. Reason: It is supposed to refer to h₂, but h₂ comes after hyp in the local context, so it can't be referenced.

Error message is shown. In the real-world example, the error message was "could not find pattern" and it took me a long time to figure out what is the problem. However, I wasn't able to create a small reproducer for that error message. Arguably, the invalid fvar is the root cause.

Versions

Lean 4.31.0-nightly-2026-04-15
Target: x86_64-unknown-linux-gnu

Additional Information

Look at the tactic state at the second bulleet point (the state with rewritten hyp):

b : ByteArray
i : Nat
hi : i < b.size
P : UInt8 → Prop
hyp✝ : P b[0 + i]
hyp : P (b.extract 0 b.size)[i]
h₂ : i < (b.extract 0 b.size).size
⊢ True

The problem is that the new, rewritten hyp variable is added to the local context before h₂, so the reference to it goes stale.

The bu probably comes from replaceLocalDeclCore in src/Lean/Meta/Tactic/Replace.lean. The current implementation uses:

let (_, localDecl') ← findMaxFVar (← instantiateMVars typeNew) |>.run localDecl
let result ← mvarId.assertAfter localDecl'.fvarId localDecl.userName typeNew typeNewPr

findMaxFVar only walks FVar nodes in typeNew. It does not consider the local contexts of unassigned metavariables that appear in typeNew. But those mvars have local contexts that may reference later fvars. Their eventual solutions can therefore literally reference
those fvars. When assertAfter reverts and re-introduces the later fvars, the earlier variable (in our case the rewritten hyp) refers to a later variable (h₂). This is already bad in and of it self. Additionally the fvarIds after the new hyp change, but the side-condition mvar still lives in the old context. Its eventual solution refers to the old fvarId, and that stale reference gets spliced into the new hypothesis's type.

With caution, let me show a present Claude prototyped in src/Lean/Meta/Tactic/Replace.lean: After computing localDecl' via findMaxFVar, walk every unassigned mvar remaining in typeNew and push localDecl' past any of the mvar's local-context fvars that are still in the main goal's local context:

let typeNewInst ← instantiateMVars typeNew
let (_, localDecl') ← findMaxFVar typeNewInst |>.run localDecl
let lctx ← getLCtx
let mvars ← getMVars typeNewInst
let mut localDecl' := localDecl'
for m in mvars do
  unless ← m.isAssigned do
    let mLCtx := (← m.getDecl).lctx
    for ldecl' in mLCtx do
      if let some ldecl := lctx.find? ldecl'.fvarId then
        if ldecl.index > localDecl'.index then
          localDecl' := ldecl
let result ← mvarId.assertAfter localDecl'.fvarId localDecl.userName typeNew typeNewPr

This makes assertAfter insert after the fvars the unassigned metavariables in typeNew could potentially refer to.

I manually verified that this fixes the reproducer and it seems correct to me, but I wonder whether there's a more efficient way to get the highest fvar index in an unassigned metavariable's local context other than iterating all of them.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.