From 4ce04776b66d121005bb67539e850f9c9ae98dde Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 27 Jan 2026 11:05:20 +0100 Subject: [PATCH] fix: do not assign synthetic opaque MVars in mspec (#12184) This PR ensures that the `mspec` tactic does not assign synthetic opaque MVars occurring in the goal, just like the `apply` tactic. --- src/Lean/Elab/Tactic/Do/Spec.lean | 2 +- .../lean/run/mspecNoAssignSyntheticOpaque.lean | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/mspecNoAssignSyntheticOpaque.lean diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 33ec89f7be..f4a88fc621 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -199,7 +199,7 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag let_expr f@Triple m ps instWP α prog P Q := specTy | liftMetaM <| throwError "target not a Triple application {specTy}" let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog - unless (← withAssignableSyntheticOpaque <| isDefEqGuarded wp wp') do + unless (← isDefEqGuarded wp wp') do Term.throwTypeMismatchError none wp wp' spec -- Try synthesizing synthetic MVars. We don't have the convenience of `TermElabM`, hence diff --git a/tests/lean/run/mspecNoAssignSyntheticOpaque.lean b/tests/lean/run/mspecNoAssignSyntheticOpaque.lean new file mode 100644 index 0000000000..c0ce5b1b2c --- /dev/null +++ b/tests/lean/run/mspecNoAssignSyntheticOpaque.lean @@ -0,0 +1,17 @@ +import Lean + +open Std.Do + +set_option mvcgen.warning false + +theorem set_spec : ⦃⌜True⌝⦄ set (m := StateM Nat) 42 ⦃⇓_ s => ⌜s = 42⌝⦄ := by + mvcgen + +example : True := by + have : ⦃⌜True⌝⦄ set (m := StateM Nat) (?n : Nat) ⦃⇓_ s => ⌜s = 42⌝⦄ := by + -- apply set_spec -- this fails, so `mspec` below should fail, too + mintro _ + fail_if_success mspec set_spec + have : ?n = 42 := by rfl + mspec set_spec + trivial