fix: avoid assigning mvar when Sym.intros produces no binders

This PR fixes a bug in `Sym.introCore.finalize` where the original metavariable
was unconditionally assigned via a delayed assignment, even when no binders were
introduced. As a result, `Sym.intros` would return `.failed` while the goal
metavariable had already been silently assigned, confusing downstream code that
relies on `isAssigned` (e.g. VC filters in `mvcgen'`).

The test and fix were suggested by Sebastian Graf.

Co-Authored-By: Sebastian Graf <sgraf1337@gmail.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Sym/Intro.lean

@@ -48,6 +48,8 @@ def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) : SymM (Array F
     assignDelayedMVar auxMVar.mvarId! fvars mvarId'
     mvarId.assign val
   let finalize (lctx : LocalContext) (localInsts : LocalInstances) (fvars : Array Expr) (type : Expr) : SymM (Array Expr × MVarId) := do
+    if fvars.isEmpty then
+      return (#[], mvarId)
     let type ← instantiateRevS type fvars
     let mvar' ← mkFreshExprMVarAt lctx localInsts type .syntheticOpaque mvarDecl.userName
     let mvarId' := mvar'.mvarId!

tests/elab/sym_intro_issue.lean

@@ -0,0 +1,38 @@
+/-
+MWE: `Sym.introCore` assigns the original mvar even when no binders are introduced.
+`Sym.intros` returns `.failed` but the mvar is secretly assigned.
+
+The bug is in `introCore.finalize`: it unconditionally creates an `auxMVar` with a
+delayed assignment and assigns the original mvar to it, even when `fvars` is empty
+(no binders were introduced). Then `intros` checks `fvars.isEmpty` and returns `.failed`,
+but the mvar is already assigned. Downstream code that checks `isAssigned` (e.g. VC filters
+in mvcgen') will wrongly think the goal is solved.
+
+Fix: guard `finalize` with `if fvars.isEmpty then return (#[], mvarId)`.
+-/
+import Lean
+
+-- Demonstrate the bug by calling `Sym.intros` on a non-forall goal.
+-- With the fix in `introCore.finalize`, this prints "GOOD".
+-- Without the fix, it prints "BUG".
+/--
+info: before intros: isAssigned=false
+intros returned .failed (as expected for non-forall target)
+after intros: isAssigned=false, isDelayedAssigned=false
+GOOD: mvar is still unassigned
+-/
+#guard_msgs in
+open Lean Meta Sym in
+#eval show MetaM Unit from do
+  let goal ← mkFreshExprMVar (mkConst ``False) .syntheticOpaque
+  let goalId := goal.mvarId!
+  IO.println s!"before intros: isAssigned={← goalId.isAssigned}"
+  let result ← Sym.SymM.run (Sym.intros goalId)
+  match result with
+  | .failed => IO.println "intros returned .failed (as expected for non-forall target)"
+  | .goal _ _ => IO.println "intros returned .goal (unexpected)"
+  IO.println s!"after intros: isAssigned={← goalId.isAssigned}, isDelayedAssigned={← goalId.isDelayedAssigned}"
+  if (← goalId.isAssigned) then
+    IO.println "BUG: mvar was assigned despite intros returning .failed"
+  else
+    IO.println "GOOD: mvar is still unassigned"