fix: hygiene for goals generated by mvcgen

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -92,17 +92,17 @@ def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
   | _ => k
 
 def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
+  goal.freshenLCtxUserNamesSinceIdx (← read).initialCtxSize
   let ty ← goal.getType
   if ty.isAppOf ``Std.Do.Invariant then
     modify fun s => { s with invariants := s.invariants.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }
 
 def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := do
-  withFreshUserNamesSinceIdx (← read).initialCtxSize do
-    let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
-    addSubGoalAsVC m.mvarId!
-    return m
+  let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
+  addSubGoalAsVC m.mvarId!
+  return m
 
 def liftSimpM (x : SimpM α) : VCGenM α := do
   let ctx ← read

src/Lean/Meta/Basic.lean

@@ -1968,14 +1968,14 @@ def withErasedFVars [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId)
 /--
 Ensures that the user names of all local declarations after index `idx` have a macro scope.
 -/
-def withFreshUserNamesSinceIdx [MonadLCtx n] [MonadLiftT MetaM n] (idx : Nat) (k : n α) : n α := do
-  let mut lctx ← getLCtx
+private def freshenUserNamesSinceIdx [MonadLiftT MetaM n] (lctx : LocalContext) (idx : Nat) : n LocalContext := do
+  let mut lctx := lctx
   for i in [idx:lctx.numIndices] do
     let some decl := lctx.decls[i]! | continue
     let n := decl.userName
     if !n.hasMacroScopes then
       lctx := lctx.setUserName decl.fvarId (← liftMetaM <| mkFreshUserName n)
-  withLCtx' lctx k
+  return lctx
 
 private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
   let mvarDecl ← mvarId.getDecl
@@ -2013,6 +2013,14 @@ def withoutModifyingMCtx : n α → n α :=
     finally
       modify fun s => { s with cache, mctx }
 
+/--
+Ensures that the user names of all local declarations after index `idx` have a macro scope.
+-/
+def _root_.Lean.MVarId.freshenLCtxUserNamesSinceIdx [MonadMCtx n] [MonadLiftT MetaM n] (mvarId : MVarId) (idx : Nat) : n Unit := do
+  let some decl := (← getMCtx).findDecl? mvarId | liftMetaM <| throwError m!"unknown metavariable {mvarId.name}"
+  let lctx ← freshenUserNamesSinceIdx decl.lctx idx
+  modifyMCtx fun mctx => { mctx with decls := mctx.decls.insert mvarId { decl with lctx } }
+
 @[inline] private def approxDefEqImp (x : MetaM α) : MetaM α :=
   withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true}) x