From 2a66006ca72e440fb651299909f018d85767fdab Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 21 Aug 2026 15:08:34 +0000
Subject: [PATCH 1/4] fix: canonicalize the WP instance of wp applications in
 vcgen

A monad may register a bespoke `WP` instance next to its `WPMonad`
instance. The goal's `wp` application then carries the registered
instance, while a backward rule built from a spec stated over
`[WPMonad m Pred EPred]` carries the blanket `WPMonad.toWP` route.
The two spellings are definitionally equal only at instance
transparency, so rule application failed with "No spec applicable".

`work` now canonicalizes the goal target with `Sym.canon`, and
`tryMkBackwardRuleFromSpec` canonicalizes the constructed rule, so
both sides carry the instance that `synthInstance` returns. The
instance guard synthesizes the spec's outstanding instance parameters
and compares the two concrete spellings at instance transparency.

The regression test registers bespoke `WP` instances for two custom
monads, one stating the `toWP` field by name and one via
`inferInstance`. The `Std.WP` interpretations stay
`instance_reducible` definitions: registering them as instances pins
the `outParam` assertion types during synthesis and breaks
lattice-generic contexts such as the section variables in
`tests/elab/vcgenFrames.lean`.
---
 src/Lean/Elab/Tactic/VCGen/Driver.lean        | 19 ++++
 .../Elab/Tactic/VCGen/RuleConstruction.lean   | 45 +++++++--
 tests/elab/vcgenBespokeWPInstance.lean        | 98 +++++++++++++++++++
 3 files changed, 156 insertions(+), 6 deletions(-)
 create mode 100644 tests/elab/vcgenBespokeWPInstance.lean

diff --git a/src/Lean/Elab/Tactic/VCGen/Driver.lean b/src/Lean/Elab/Tactic/VCGen/Driver.lean
index 3224c838f1c4..1c994b7165cb 100644
--- a/src/Lean/Elab/Tactic/VCGen/Driver.lean
+++ b/src/Lean/Elab/Tactic/VCGen/Driver.lean
@@ -10,6 +10,7 @@ public import Lean.Elab.Tactic.Meta
 public import Lean.Elab.Tactic.VCGen.Context
 public import Lean.Elab.Tactic.VCGen.Solve
 public import Lean.Meta.Sym.Grind
+import Lean.Meta.Sym.Canon
 
 open Lean Meta Elab Tactic Sym Sym.Internal Lean.Order
 open Lean.Elab.Tactic.Do.SpecAttr
@@ -93,8 +94,26 @@ private structure WorkItem where
   goal : Grind.Goal
   scope : Scope
 
+/--
+Canonicalize the goal target with `Sym.canon`, so instance arguments take their canonical,
+re-synthesized form. In particular, the `WP` instance of a `wp` application in the target becomes
+the instance that `synthInstance` returns, whichever way the goal spelled it (a registered bespoke
+`WP` instance or the blanket `WPMonad.toWP` route). Backward rules built from spec theorems are
+canonicalized the same way in `tryMkBackwardRuleFromSpec`, so rule application matches the target
+structurally.
+-/
+private def canonTarget (mvarId : MVarId) : SymM MVarId := do
+  let mvarDecl ← mvarId.getDecl
+  let type ← shareCommon (← Sym.canon mvarDecl.type)
+  if isSameExpr type mvarDecl.type then return mvarId
+  let mvarNew ← mkFreshExprMVarAt mvarDecl.lctx mvarDecl.localInstances type .syntheticOpaque
+    mvarDecl.userName
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+
 public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
+  let mvarId ← canonTarget mvarId
   let mut worklist : Array WorkItem := #[{ goal := { goal with mvarId }, scope }]
   while let some s := worklist.back? do
     worklist := worklist.pop
diff --git a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
index b1471e39c4c8..63951ea36b3e 100644
--- a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
+++ b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
@@ -12,6 +12,7 @@ public import Lean.Elab.Tactic.VCGen.Reduce
 public import Lean.Elab.Tactic.VCGen.SpecDB
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
+import Lean.Meta.Sym.Canon
 meta import Std.WP.Frame
 
 open Lean Meta Elab Tactic Sym
@@ -283,7 +284,7 @@ exposes in the premise program (e.g. for class projection unfold equations like
 `MonadState.modifyGet.eq_1`) are reduced by `wpHeadReduce?` before the next spec lookup.
 -/
 private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
-    OptionT MetaM (Expr × Expr) := do
+    OptionT SymM (Expr × Expr) := do
   let_expr Eq eqα _lhs _rhs := eqType
     | throwError "simp spec is not an equation: {eqType}"
   -- Unify the equation's type with the goal's program type. First-order approximation decomposes
@@ -301,6 +302,32 @@ private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
     (info.args.take 7).map some ++ #[none, none, some eqPrf, some post, some epost]
   return (specProof, ← instantiateMVars (← Meta.inferType specProof))
 
+/--
+Decide whether the goal's `WP` instance `instWP` matches the spec's `instWP'`, assigning the spec's
+metavariables inside `instWP'` on success.
+
+The plain `isDefEq` handles the common case where both sides spell the instance the same way, e.g.
+both through the blanket `WPMonad.toWP` route; head congruence then assigns the spec's `WPMonad`
+metavariable. When the spellings differ (say, the goal carries a registered bespoke `WP` instance
+while the spec was stated through the blanket route), the heads mismatch and no reducibility
+setting can close the gap while the spec's `WPMonad` is still a metavariable. In that case, pin
+the spec's instance type against the goal's, synthesize the spec's outstanding instance parameters
+(`xs`/`bs` are the spec's telescope), and compare the two now-concrete spellings at instance
+transparency, the level at which `instance`-command definitions unfold.
+-/
+private def isDefEqInstWP (instWP instWP' : Expr) (xs : Array Expr) (bs : Array BinderInfo) :
+    MetaM Bool := do
+  if ← isDefEqGuarded instWP instWP' then return true
+  unless ← isDefEqGuarded (← Meta.inferType instWP') (← Meta.inferType instWP) do return false
+  for x in xs, b in bs do
+    if b == .instImplicit && !(← x.mvarId!.isAssigned) then
+      let ty ← instantiateMVars (← Meta.inferType x)
+      unless ty.hasExprMVar do
+        if let .some val ← trySynthInstance ty then
+          discard <| isDefEqGuarded x val
+  let instWP' ← instantiateMVars instWP'
+  withTransparency .instances <| isDefEqGuarded instWP instWP'
+
 /--
 Try to build a backward rule from a single spec theorem.
 
@@ -309,15 +336,20 @@ For a spec already in `⊑ wp` form (`pre ⊑ wp prog post epost`, where the lat
 `lhs = rhs` is first normalized to `wp rhs Q E ⊑ wp lhs Q E` via `eqSpecToWp?` and then handled the
 same way.
 
+The abstracted rule is canonicalized with `Sym.canon` before pattern extraction, so the instance
+arguments baked into its conclusion (e.g. the `WP` instance of the `wp` application) take the same
+canonical, re-synthesized form as the internalized goals the rule is applied to; see `canonTarget`
+in `VCGen.Driver`.
+
 - `info.Pred`: the goal's lattice type (e.g. `Nat → Prop`)
 - `info.instWP`: the `WPMonad` instance for the goal monad
 - `info.excessArgs`: free variables representing state args from
   `info.Pred = σ1 → ... → σn → Prop`
 -/
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
-    (stateArgNames : Array Name := #[]) : OptionT MetaM BackwardRule := do
+    (stateArgNames : Array Name := #[]) : OptionT SymM BackwardRule := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
-  let (_xs, _bs, specProof, specType) ← specThm.instantiate
+  let (xs, bs, specProof, specType) ← specThm.instantiate
   -- Equality specs (the simp side of `@[spec]`) are normalized to `⊑ wp` form, then handled like
   -- any ordinary `⊑ wp` spec.
   let (specProof, specType) ←
@@ -328,7 +360,7 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
   guard <| ← isDefEqGuarded info.Pred Pred'
   let_expr Std.WP.wp _Prog' _Value' _Pred' _EPred' _instAL' _instEAL' instWP' prog postSpec epostSpec := rhs
     | throwError "target not a wp application {rhs}"
-  guard <| ← isDefEqGuarded info.instWP instWP'
+  guard <| ← isDefEqInstWP info.instWP instWP' xs bs
   -- Use local excess-state binders so explicit post premises can be re-lifted to `⊑`.
   -- Name them positionally from `stateArgNames` (else `s`) so the rule's binders carry good names.
   let mut ss := #[]
@@ -338,7 +370,8 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
     ssTypes := ssTypes.push ty
     ss := ss.push <| ← mkFreshExprMVar (userName := stateArgNames[i]?.getD `s) ty
   let res ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
-  mkBackwardRuleFromExpr res.expr res.paramNames.toList
+  let expr ← Sym.canon res.expr
+  mkBackwardRuleFromExpr expr res.paramNames.toList
 
 /-! ## Split rules -/
 
@@ -444,7 +477,7 @@ condition `WP.Frames op prog F`, with the frame `F` left schematic and the weake
 frame. `analyzeFrameRule` records the positions of the schematic slots.
 -/
 public def mkFrameBackwardRule (fp : FrameProc) (info : WPApp) :
-    MetaM FrameBackwardRule := do
+    SymM FrameBackwardRule := do
   -- Pin the program and the operator, leaving everything else schematic;
   -- `tryMkBackwardRuleFromSpec` turns the unassigned metavariables into rule parameters.
   let op ← fp.mkOpAppM info
diff --git a/tests/elab/vcgenBespokeWPInstance.lean b/tests/elab/vcgenBespokeWPInstance.lean
new file mode 100644
index 000000000000..98e1b94e2142
--- /dev/null
+++ b/tests/elab/vcgenBespokeWPInstance.lean
@@ -0,0 +1,98 @@
+import Std.WP
+import Std.Tactic.Do
+
+/-!
+A monad may register a bespoke `WP` instance next to its `WPMonad` instance. The goal then
+carries the registered instance while a spec instantiated from `[WPMonad m …]` carries the
+blanket `WPMonad.toWP` route. Rule construction canonicalizes both spellings to the instance
+that `synthInstance` returns, so `Spec.bind` applies either way. `Identity` states the `toWP`
+field by name, `Identity2` via `inferInstance`.
+-/
+
+set_option experimental.vcgen true
+open Std.WP Lean.Order
+
+universe u
+variable {α : Type u}
+
+structure Identity (α : Type u) where
+  run : α
+
+instance : Monad Identity where
+  pure x := ⟨x⟩
+  bind x f := f x.run
+
+instance : LawfulMonad Identity :=
+  LawfulMonad.mk' Identity
+    (id_map := fun _ => rfl)
+    (pure_bind := fun _ _ => rfl)
+    (bind_assoc := fun _ _ _ => rfl)
+
+instance Identity.instWP : WP (Identity α) α Prop EStack⟨⟩ where
+  wpTrans x := ⟨fun post _ => post x.run⟩
+  wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run
+
+instance Identity.instWPMonad : WPMonad Identity Prop EStack⟨⟩ where
+  toWP _ := Identity.instWP
+  pure_le_wp_pure x post epost := PartialOrder.rel_refl
+  bind_le_wp_bind x f post epost := PartialOrder.rel_refl
+
+theorem Identity.of_run_eq_wp {x : α} {prog : Identity α}
+    (h : Identity.run prog = x) (P : α → Prop)
+    (hwp : wp prog P ()) : P x := by
+  simp_all [wp, WP.wpTrans, ← h]
+
+def rev (xs : List α) : Identity (List α) := do
+  let mut out := []
+  for x in xs do
+    out := x :: out
+  return out
+
+example {xs : List α} : (rev xs).run = xs.reverse := by
+  generalize h : (rev xs).run = x
+  apply Identity.of_run_eq_wp h
+  simp only [rev]
+  vcgen invariants
+  · fun pref _suff out => out = pref.reverse
+  with finish
+
+structure Identity2 (α : Type u) where
+  run : α
+
+instance : Monad Identity2 where
+  pure x := ⟨x⟩
+  bind x f := f x.run
+
+instance : LawfulMonad Identity2 :=
+  LawfulMonad.mk' Identity2
+    (id_map := fun _ => rfl)
+    (pure_bind := fun _ _ => rfl)
+    (bind_assoc := fun _ _ _ => rfl)
+
+instance Identity2.instWP : WP (Identity2 α) α Prop EStack⟨⟩ where
+  wpTrans x := ⟨fun post _ => post x.run⟩
+  wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run
+
+instance Identity2.instWPMonad : WPMonad Identity2 Prop EStack⟨⟩ where
+  toWP _ := inferInstance
+  pure_le_wp_pure x post epost := PartialOrder.rel_refl
+  bind_le_wp_bind x f post epost := PartialOrder.rel_refl
+
+theorem Identity2.of_run_eq_wp {x : α} {prog : Identity2 α}
+    (h : Identity2.run prog = x) (P : α → Prop)
+    (hwp : wp prog P ()) : P x := by
+  simp_all [wp, WP.wpTrans, ← h]
+
+def rev2 (xs : List α) : Identity2 (List α) := do
+  let mut out := []
+  for x in xs do
+    out := x :: out
+  return out
+
+example {xs : List α} : (rev2 xs).run = xs.reverse := by
+  generalize h : (rev2 xs).run = x
+  apply Identity2.of_run_eq_wp h
+  simp only [rev2]
+  vcgen invariants
+  · fun pref _suff out => out = pref.reverse
+  with finish

From c10d45194f561623499f7e3dd1eaa1087a31d1c2 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 21 Aug 2026 16:12:53 +0000
Subject: [PATCH 2/4] refactor: simplify canonTarget and the WP instance guard

`canonTarget` reuses `MVarId.replaceTargetDefEqFast` and drops the no-op check. The rule-construction instance guard compares the goal's `WP` instance against the spec's at default transparency (`withDefault <| isDefEqGuarded ...`), which suffices to match a bespoke goal instance against the spec's `WPMonad.toWP` spelling, replacing `isDefEqInstWP`.
---
 src/Lean/Elab/Tactic/VCGen/Driver.lean        | 16 ++--------
 .../Elab/Tactic/VCGen/RuleConstruction.lean   | 32 ++-----------------
 2 files changed, 6 insertions(+), 42 deletions(-)

diff --git a/src/Lean/Elab/Tactic/VCGen/Driver.lean b/src/Lean/Elab/Tactic/VCGen/Driver.lean
index 1c994b7165cb..78d16beb965a 100644
--- a/src/Lean/Elab/Tactic/VCGen/Driver.lean
+++ b/src/Lean/Elab/Tactic/VCGen/Driver.lean
@@ -95,21 +95,11 @@ private structure WorkItem where
   scope : Scope
 
 /--
-Canonicalize the goal target with `Sym.canon`, so instance arguments take their canonical,
-re-synthesized form. In particular, the `WP` instance of a `wp` application in the target becomes
-the instance that `synthInstance` returns, whichever way the goal spelled it (a registered bespoke
-`WP` instance or the blanket `WPMonad.toWP` route). Backward rules built from spec theorems are
-canonicalized the same way in `tryMkBackwardRuleFromSpec`, so rule application matches the target
-structurally.
+Canonicalizes the goal target with `Sym.canon`, so its instance arguments (e.g. the `WP`
+instance of a `wp` application) match the canonicalized rules from `tryMkBackwardRuleFromSpec`.
 -/
 private def canonTarget (mvarId : MVarId) : SymM MVarId := do
-  let mvarDecl ← mvarId.getDecl
-  let type ← shareCommon (← Sym.canon mvarDecl.type)
-  if isSameExpr type mvarDecl.type then return mvarId
-  let mvarNew ← mkFreshExprMVarAt mvarDecl.lctx mvarDecl.localInstances type .syntheticOpaque
-    mvarDecl.userName
-  mvarId.assign mvarNew
-  return mvarNew.mvarId!
+  mvarId.replaceTargetDefEqFast (← shareCommon (← Sym.canon (← mvarId.getType)))
 
 public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
diff --git a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
index 63951ea36b3e..b44f34e58d0d 100644
--- a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
+++ b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
@@ -302,32 +302,6 @@ private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
     (info.args.take 7).map some ++ #[none, none, some eqPrf, some post, some epost]
   return (specProof, ← instantiateMVars (← Meta.inferType specProof))
 
-/--
-Decide whether the goal's `WP` instance `instWP` matches the spec's `instWP'`, assigning the spec's
-metavariables inside `instWP'` on success.
-
-The plain `isDefEq` handles the common case where both sides spell the instance the same way, e.g.
-both through the blanket `WPMonad.toWP` route; head congruence then assigns the spec's `WPMonad`
-metavariable. When the spellings differ (say, the goal carries a registered bespoke `WP` instance
-while the spec was stated through the blanket route), the heads mismatch and no reducibility
-setting can close the gap while the spec's `WPMonad` is still a metavariable. In that case, pin
-the spec's instance type against the goal's, synthesize the spec's outstanding instance parameters
-(`xs`/`bs` are the spec's telescope), and compare the two now-concrete spellings at instance
-transparency, the level at which `instance`-command definitions unfold.
--/
-private def isDefEqInstWP (instWP instWP' : Expr) (xs : Array Expr) (bs : Array BinderInfo) :
-    MetaM Bool := do
-  if ← isDefEqGuarded instWP instWP' then return true
-  unless ← isDefEqGuarded (← Meta.inferType instWP') (← Meta.inferType instWP) do return false
-  for x in xs, b in bs do
-    if b == .instImplicit && !(← x.mvarId!.isAssigned) then
-      let ty ← instantiateMVars (← Meta.inferType x)
-      unless ty.hasExprMVar do
-        if let .some val ← trySynthInstance ty then
-          discard <| isDefEqGuarded x val
-  let instWP' ← instantiateMVars instWP'
-  withTransparency .instances <| isDefEqGuarded instWP instWP'
-
 /--
 Try to build a backward rule from a single spec theorem.
 
@@ -342,14 +316,14 @@ canonical, re-synthesized form as the internalized goals the rule is applied to;
 in `VCGen.Driver`.
 
 - `info.Pred`: the goal's lattice type (e.g. `Nat → Prop`)
-- `info.instWP`: the `WPMonad` instance for the goal monad
+- `info.instWP`: the `WP` instance of the goal's `wp` application
 - `info.excessArgs`: free variables representing state args from
   `info.Pred = σ1 → ... → σn → Prop`
 -/
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
     (stateArgNames : Array Name := #[]) : OptionT SymM BackwardRule := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
-  let (xs, bs, specProof, specType) ← specThm.instantiate
+  let (_xs, _bs, specProof, specType) ← specThm.instantiate
   -- Equality specs (the simp side of `@[spec]`) are normalized to `⊑ wp` form, then handled like
   -- any ordinary `⊑ wp` spec.
   let (specProof, specType) ←
@@ -360,7 +334,7 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
   guard <| ← isDefEqGuarded info.Pred Pred'
   let_expr Std.WP.wp _Prog' _Value' _Pred' _EPred' _instAL' _instEAL' instWP' prog postSpec epostSpec := rhs
     | throwError "target not a wp application {rhs}"
-  guard <| ← isDefEqInstWP info.instWP instWP' xs bs
+  guard <| ← withDefault <| isDefEqGuarded info.instWP instWP'
   -- Use local excess-state binders so explicit post premises can be re-lifted to `⊑`.
   -- Name them positionally from `stateArgNames` (else `s`) so the rule's binders carry good names.
   let mut ss := #[]

From ddd0a8b2cc654bacdd26030d7a8c35da1ca01a86 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 21 Aug 2026 18:16:43 +0200
Subject: [PATCH 3/4] Clean up comments in RuleConstruction.lean

Removed unnecessary explanation about canonicalization and instance arguments in the abstracted rule.
---
 src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
index b44f34e58d0d..c32a61e1ac5d 100644
--- a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
+++ b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
@@ -310,11 +310,6 @@ For a spec already in `⊑ wp` form (`pre ⊑ wp prog post epost`, where the lat
 `lhs = rhs` is first normalized to `wp rhs Q E ⊑ wp lhs Q E` via `eqSpecToWp?` and then handled the
 same way.
 
-The abstracted rule is canonicalized with `Sym.canon` before pattern extraction, so the instance
-arguments baked into its conclusion (e.g. the `WP` instance of the `wp` application) take the same
-canonical, re-synthesized form as the internalized goals the rule is applied to; see `canonTarget`
-in `VCGen.Driver`.
-
 - `info.Pred`: the goal's lattice type (e.g. `Nat → Prop`)
 - `info.instWP`: the `WP` instance of the goal's `wp` application
 - `info.excessArgs`: free variables representing state args from

From b93a53c5d31badeaf2c9f89c9d495b24f624f712 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 21 Aug 2026 17:08:08 +0000
Subject: [PATCH 4/4] refactor: drop wp canonicalization, register the WP
 interpretations as instances
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The default-transparency instance guard alone fixes spec application for goals with a registered `WP` instance: the rule conclusion pins the goal's own instance arguments, premises keep the spec's `WPMonad.toWP` spelling, and `synthPending` assigns the spec's `WPMonad` metavariable during the guard, so goals and rules stay consistent without canonicalizing either. `Sym.canon` on the constructed rule also rewrote tuple matchers into projections, which destroyed the binder names that `binderNameHint` consumption reads and broke `tests/elab/intrinsicVerification.lean` (also on CI).

The `WP` interpretations in `Std.WP.Monad.Instances` are proper instances now, with `toWP _ := inferInstance`, so the existing tests exercise the registered-instance path and the dedicated regression test is gone. The `Id`-monad theorems in `tests/elab/vcgenFrames.lean` state their assertions at `Prop`: a hypothesis `[WPMonad Id Pred EPred]` over a generic `Pred` denotes no real instance, and instance search, which ignores `outParam` positions during selection, resolves `WP (Id β) …` to the registered `Prop` instance regardless.
---
 src/Lean/Elab/Tactic/VCGen/Driver.lean        |  9 --
 .../Elab/Tactic/VCGen/RuleConstruction.lean   | 12 +--
 src/Std/WP/Monad/Instances.lean               | 32 +++---
 tests/elab/vcgenBespokeWPInstance.lean        | 98 -------------------
 tests/elab/vcgenFrames.lean                   | 35 +++----
 5 files changed, 34 insertions(+), 152 deletions(-)
 delete mode 100644 tests/elab/vcgenBespokeWPInstance.lean

diff --git a/src/Lean/Elab/Tactic/VCGen/Driver.lean b/src/Lean/Elab/Tactic/VCGen/Driver.lean
index 78d16beb965a..3224c838f1c4 100644
--- a/src/Lean/Elab/Tactic/VCGen/Driver.lean
+++ b/src/Lean/Elab/Tactic/VCGen/Driver.lean
@@ -10,7 +10,6 @@ public import Lean.Elab.Tactic.Meta
 public import Lean.Elab.Tactic.VCGen.Context
 public import Lean.Elab.Tactic.VCGen.Solve
 public import Lean.Meta.Sym.Grind
-import Lean.Meta.Sym.Canon
 
 open Lean Meta Elab Tactic Sym Sym.Internal Lean.Order
 open Lean.Elab.Tactic.Do.SpecAttr
@@ -94,16 +93,8 @@ private structure WorkItem where
   goal : Grind.Goal
   scope : Scope
 
-/--
-Canonicalizes the goal target with `Sym.canon`, so its instance arguments (e.g. the `WP`
-instance of a `wp` application) match the canonicalized rules from `tryMkBackwardRuleFromSpec`.
--/
-private def canonTarget (mvarId : MVarId) : SymM MVarId := do
-  mvarId.replaceTargetDefEqFast (← shareCommon (← Sym.canon (← mvarId.getType)))
-
 public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
-  let mvarId ← canonTarget mvarId
   let mut worklist : Array WorkItem := #[{ goal := { goal with mvarId }, scope }]
   while let some s := worklist.back? do
     worklist := worklist.pop
diff --git a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
index c32a61e1ac5d..b117d46c3e11 100644
--- a/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
+++ b/src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean
@@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.VCGen.Reduce
 public import Lean.Elab.Tactic.VCGen.SpecDB
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
-import Lean.Meta.Sym.Canon
 meta import Std.WP.Frame
 
 open Lean Meta Elab Tactic Sym
@@ -284,7 +283,7 @@ exposes in the premise program (e.g. for class projection unfold equations like
 `MonadState.modifyGet.eq_1`) are reduced by `wpHeadReduce?` before the next spec lookup.
 -/
 private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
-    OptionT SymM (Expr × Expr) := do
+    OptionT MetaM (Expr × Expr) := do
   let_expr Eq eqα _lhs _rhs := eqType
     | throwError "simp spec is not an equation: {eqType}"
   -- Unify the equation's type with the goal's program type. First-order approximation decomposes
@@ -316,7 +315,7 @@ same way.
   `info.Pred = σ1 → ... → σn → Prop`
 -/
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
-    (stateArgNames : Array Name := #[]) : OptionT SymM BackwardRule := do
+    (stateArgNames : Array Name := #[]) : OptionT MetaM BackwardRule := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
   let (_xs, _bs, specProof, specType) ← specThm.instantiate
   -- Equality specs (the simp side of `@[spec]`) are normalized to `⊑ wp` form, then handled like
@@ -329,6 +328,8 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
   guard <| ← isDefEqGuarded info.Pred Pred'
   let_expr Std.WP.wp _Prog' _Value' _Pred' _EPred' _instAL' _instEAL' instWP' prog postSpec epostSpec := rhs
     | throwError "target not a wp application {rhs}"
+  -- `withDefault`: the goal can carry a registered `WP` instance (e.g. `Id.wpInst`) while the
+  -- spec spells `WPMonad.toWP ?inst`; default transparency unfolds both after `?inst` synthesis.
   guard <| ← withDefault <| isDefEqGuarded info.instWP instWP'
   -- Use local excess-state binders so explicit post premises can be re-lifted to `⊑`.
   -- Name them positionally from `stateArgNames` (else `s`) so the rule's binders carry good names.
@@ -339,8 +340,7 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
     ssTypes := ssTypes.push ty
     ss := ss.push <| ← mkFreshExprMVar (userName := stateArgNames[i]?.getD `s) ty
   let res ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
-  let expr ← Sym.canon res.expr
-  mkBackwardRuleFromExpr expr res.paramNames.toList
+  mkBackwardRuleFromExpr res.expr res.paramNames.toList
 
 /-! ## Split rules -/
 
@@ -446,7 +446,7 @@ condition `WP.Frames op prog F`, with the frame `F` left schematic and the weake
 frame. `analyzeFrameRule` records the positions of the schematic slots.
 -/
 public def mkFrameBackwardRule (fp : FrameProc) (info : WPApp) :
-    SymM FrameBackwardRule := do
+    MetaM FrameBackwardRule := do
   -- Pin the program and the operator, leaving everything else schematic;
   -- `tryMkBackwardRuleFromSpec` turns the unassigned metavariables into rule parameters.
   let op ← fp.mkOpAppM info
diff --git a/src/Std/WP/Monad/Instances.lean b/src/Std/WP/Monad/Instances.lean
index 08fc776182e4..1092170c3a95 100644
--- a/src/Std/WP/Monad/Instances.lean
+++ b/src/Std/WP/Monad/Instances.lean
@@ -41,13 +41,13 @@ namespace Std.WP
 variable {m : Type u → Type z}
 
 /-- `Id`'s `WP` interpretation: `Prop` assertions and no exceptions. -/
-@[instance_reducible] def Id.wpInst {α : Type u} : WP (Id α) α Prop EStack⟨⟩ where
+instance Id.wpInst {α : Type u} : WP (Id α) α Prop EStack⟨⟩ where
   wpTrans x := ⟨fun post _epost => post x⟩
   wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x
 
 /-- `Id` is a WPMonad with `Prop` assertions and no exceptions. -/
 instance Id.instWPMonad : WPMonad Id.{u} Prop EStack⟨⟩ where
-  toWP _ := Id.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind _ _ _ _ := PartialOrder.rel_refl
 
@@ -86,7 +86,7 @@ instance {ε : Type u} {Pred : Type v} {EPred : Type w} {ε' : Type u}
 
 /-- `ExceptT`'s `WP` interpretation: lift the base interpretation by adding an exception
 postcondition layer. -/
-@[instance_reducible] def ExceptT.wpInst {Pred : Type v}
+instance ExceptT.wpInst {Pred : Type v}
   [Assertion Pred] [Assertion EPred] [WP (m (Except ε α)) (Except ε α) Pred EPred] :
     WP (ExceptT ε m α) α Pred ((ε → Pred) × EPred) where
   wpTrans x := PredTrans.pushExceptT (WP.wpTrans x.run)
@@ -103,7 +103,7 @@ postcondition layer. -/
 instance ExceptT.instWPMonad {Pred : Type v}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (ExceptT ε m) Pred ((ε → Pred) × EPred) where
-  toWP _ := ExceptT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost =>
     WPMonad.pure_le_wp_pure (m := m) (Except.ok x) (pushExcept post epost.fst) epost.snd
   bind_le_wp_bind x f := fun post epost => by
@@ -124,7 +124,7 @@ theorem ExceptT.wp_apply_eq {α ε Pred EPred}
 
 /-- `OptionT`'s `WP` interpretation: lift the base interpretation by adding a `Unit` exception
 postcondition layer. -/
-@[instance_reducible] def OptionT.wpInst {Pred : Type u}
+instance OptionT.wpInst {Pred : Type u}
   [Assertion Pred] [Assertion EPred] [WP (m (Option α)) (Option α) Pred EPred] :
     WP (OptionT m α) α Pred ((Unit → Pred) × EPred) where
   wpTrans x := PredTrans.pushOptionT (WP.wpTrans x.run)
@@ -140,7 +140,7 @@ postcondition layer. -/
 instance OptionT.instWPMonad {Pred : Type u}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (OptionT m) Pred ((Unit → Pred) × EPred) where
-  toWP _ := OptionT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost =>
     WPMonad.pure_le_wp_pure (m := m) (some x) (pushOption post epost.fst) epost.snd
   bind_le_wp_bind x f := fun post epost => by
@@ -160,7 +160,7 @@ theorem OptionT.wp_apply_eq {α : Type u} {Pred : Type u} {EPred}
     wp x post epost = wp x.run (pushOption post epost.fst) epost.snd := rfl
 
 /-- `StateT`'s `WP` interpretation: lift the base interpretation by adding a state argument. -/
-@[instance_reducible] def StateT.wpInst {EPred : Type v} {σ : Type u} {Pred : Type w}
+instance StateT.wpInst {EPred : Type v} {σ : Type u} {Pred : Type w}
   [Assertion Pred] [Assertion EPred] [WP (m (α × σ)) (α × σ) Pred EPred] :
     WP (StateT σ m α) α (σ → Pred) EPred where
   wpTrans x := pushArg (WP.wpTrans <| x.run ·)
@@ -174,7 +174,7 @@ theorem OptionT.wp_apply_eq {α : Type u} {Pred : Type u} {EPred}
 instance (priority := low) StateT.instWPMonad {EPred : Type v} {σ : Type u} {Pred : Type w}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (StateT σ m) (σ → Pred) EPred where
-  toWP _ := StateT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost s =>
     WPMonad.pure_le_wp_pure (m := m) (x, s) (fun p => post p.1 p.2) epost
   bind_le_wp_bind x f := fun post epost s => by
@@ -187,7 +187,7 @@ theorem StateT.wp_apply_eq {σ : Type u}
     wp x post epost s = wp (x.run s) (fun (a, s) => post a s) epost := rfl
 
 /-- `ReaderT`'s `WP` interpretation: lift the base interpretation by adding a reader argument. -/
-@[instance_reducible] def ReaderT.wpInst {Pred : Type v}
+instance ReaderT.wpInst {Pred : Type v}
   [Assertion Pred] [Assertion EPred] [WP (m α) α Pred EPred] :
     WP (ReaderT ρ m α) α (ρ → Pred) EPred where
   wpTrans x := ⟨fun post epost r => wp (x.run r) (fun a => post a r) epost⟩
@@ -201,7 +201,7 @@ theorem StateT.wp_apply_eq {σ : Type u}
 instance ReaderT.instWPMonad {Pred : Type v}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (ReaderT ρ m) (ρ → Pred) EPred where
-  toWP _ := ReaderT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost r =>
     WPMonad.pure_le_wp_pure (m := m) x (fun a => post a r) epost
   bind_le_wp_bind x f := fun post epost r => by
@@ -224,7 +224,7 @@ theorem ReaderT.wp_apply_eq {ρ : Type u}
 
 /-- `Option`'s `WP` interpretation: `Prop` assertions and a `Unit`-indexed exception
 postcondition. -/
-@[instance_reducible] def Option.wpInst {α : Type u} : WP (Option α) α Prop (Unit → Prop) where
+instance Option.wpInst {α : Type u} : WP (Option α) α Prop (Unit → Prop) where
   wpTrans x := ⟨fun post epost => pushOption post epost x⟩
   wp_trans_monotone x := fun post post' epost epost' hepost hpost => by
     cases x with
@@ -233,13 +233,13 @@ postcondition. -/
 
 /-- `Option` is a WPMonad with `Prop` assertions and a `Unit`-indexed exception postcondition. -/
 instance Option.instWPMonad : WPMonad Option.{u} Prop (Unit → Prop) where
-  toWP _ := Option.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost => by cases x <;> exact id
 
 /-- `Except ε`'s `WP` interpretation: `Prop` assertions and an `ε`-indexed exception
 postcondition. -/
-@[instance_reducible] def Except.wpInst {α : Type u} : WP (Except ε α) α Prop (ε → Prop) where
+instance Except.wpInst {α : Type u} : WP (Except ε α) α Prop (ε → Prop) where
   wpTrans x := ⟨fun post epost => pushExcept post epost x⟩
   wp_trans_monotone x := fun post post' epost epost' hepost hpost => by
     cases x with
@@ -248,12 +248,12 @@ postcondition. -/
 
 /-- `Except ε` is a WPMonad with `Prop` assertions and an `ε`-indexed exception postcondition. -/
 instance Except.instWPMonad : WPMonad (Except ε) Prop (ε → Prop) where
-  toWP _ := Except.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost => by cases x <;> exact id
 
 /-- `EStateM ε σ`'s `WP` interpretation combining state and exceptions. -/
-@[instance_reducible] def EStateM.wpInst {α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop) where
+instance EStateM.wpInst {α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop) where
   wpTrans x := ⟨fun post epost s => match x s with
     | .ok a s' => post a s'
     | .error el s' => epost el s'⟩
@@ -266,7 +266,7 @@ instance Except.instWPMonad : WPMonad (Except ε) Prop (ε → Prop) where
 
 /-- `EStateM ε σ` is a WPMonad combining state and exceptions. -/
 instance EStateM.instWPMonad : WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop) where
-  toWP _ := EStateM.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost s => PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost s => by
     simp only [WP.wp, WP.wpTrans, bind, EStateM.bind]
diff --git a/tests/elab/vcgenBespokeWPInstance.lean b/tests/elab/vcgenBespokeWPInstance.lean
deleted file mode 100644
index 98e1b94e2142..000000000000
--- a/tests/elab/vcgenBespokeWPInstance.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import Std.WP
-import Std.Tactic.Do
-
-/-!
-A monad may register a bespoke `WP` instance next to its `WPMonad` instance. The goal then
-carries the registered instance while a spec instantiated from `[WPMonad m …]` carries the
-blanket `WPMonad.toWP` route. Rule construction canonicalizes both spellings to the instance
-that `synthInstance` returns, so `Spec.bind` applies either way. `Identity` states the `toWP`
-field by name, `Identity2` via `inferInstance`.
--/
-
-set_option experimental.vcgen true
-open Std.WP Lean.Order
-
-universe u
-variable {α : Type u}
-
-structure Identity (α : Type u) where
-  run : α
-
-instance : Monad Identity where
-  pure x := ⟨x⟩
-  bind x f := f x.run
-
-instance : LawfulMonad Identity :=
-  LawfulMonad.mk' Identity
-    (id_map := fun _ => rfl)
-    (pure_bind := fun _ _ => rfl)
-    (bind_assoc := fun _ _ _ => rfl)
-
-instance Identity.instWP : WP (Identity α) α Prop EStack⟨⟩ where
-  wpTrans x := ⟨fun post _ => post x.run⟩
-  wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run
-
-instance Identity.instWPMonad : WPMonad Identity Prop EStack⟨⟩ where
-  toWP _ := Identity.instWP
-  pure_le_wp_pure x post epost := PartialOrder.rel_refl
-  bind_le_wp_bind x f post epost := PartialOrder.rel_refl
-
-theorem Identity.of_run_eq_wp {x : α} {prog : Identity α}
-    (h : Identity.run prog = x) (P : α → Prop)
-    (hwp : wp prog P ()) : P x := by
-  simp_all [wp, WP.wpTrans, ← h]
-
-def rev (xs : List α) : Identity (List α) := do
-  let mut out := []
-  for x in xs do
-    out := x :: out
-  return out
-
-example {xs : List α} : (rev xs).run = xs.reverse := by
-  generalize h : (rev xs).run = x
-  apply Identity.of_run_eq_wp h
-  simp only [rev]
-  vcgen invariants
-  · fun pref _suff out => out = pref.reverse
-  with finish
-
-structure Identity2 (α : Type u) where
-  run : α
-
-instance : Monad Identity2 where
-  pure x := ⟨x⟩
-  bind x f := f x.run
-
-instance : LawfulMonad Identity2 :=
-  LawfulMonad.mk' Identity2
-    (id_map := fun _ => rfl)
-    (pure_bind := fun _ _ => rfl)
-    (bind_assoc := fun _ _ _ => rfl)
-
-instance Identity2.instWP : WP (Identity2 α) α Prop EStack⟨⟩ where
-  wpTrans x := ⟨fun post _ => post x.run⟩
-  wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run
-
-instance Identity2.instWPMonad : WPMonad Identity2 Prop EStack⟨⟩ where
-  toWP _ := inferInstance
-  pure_le_wp_pure x post epost := PartialOrder.rel_refl
-  bind_le_wp_bind x f post epost := PartialOrder.rel_refl
-
-theorem Identity2.of_run_eq_wp {x : α} {prog : Identity2 α}
-    (h : Identity2.run prog = x) (P : α → Prop)
-    (hwp : wp prog P ()) : P x := by
-  simp_all [wp, WP.wpTrans, ← h]
-
-def rev2 (xs : List α) : Identity2 (List α) := do
-  let mut out := []
-  for x in xs do
-    out := x :: out
-  return out
-
-example {xs : List α} : (rev2 xs).run = xs.reverse := by
-  generalize h : (rev2 xs).run = x
-  apply Identity2.of_run_eq_wp h
-  simp only [rev2]
-  vcgen invariants
-  · fun pref _suff out => out = pref.reverse
-  with finish
diff --git a/tests/elab/vcgenFrames.lean b/tests/elab/vcgenFrames.lean
index a88a5059d128..9b6f65a0628f 100644
--- a/tests/elab/vcgenFrames.lean
+++ b/tests/elab/vcgenFrames.lean
@@ -60,24 +60,21 @@ theorem frames_mkFreshNat [Monad m] [Assertion Pred] [Assertion EPred]
 /-- `Id`-specialized `frames_mkFreshNat`. With the base monad ground, `grind` can derive a
 usable pattern, so registering it lets `finish` discharge the preservation VC. -/
 @[grind .]
-theorem frames_mkFreshNat_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred}
+theorem frames_mkFreshNat_Id {P : AppState → Prop}
     (h : ∀ s a, P { s with fst := a } = P s) :
     WP.Frames (· ⊓ ·) (mkFreshNat : StateT AppState Id Nat) P :=
   frames_mkFreshNat h
 
 /-- The frame recovers `s.2`, which the lossy spec dropped. The `fail_if_success` confirms the frame
 is doing the work: without it, `grind` cannot close the lost `s.2 = 7`. -/
-theorem recovers_snd [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
   vcgen frames | mkFreshNat => fun s => ⌜s.2 = 7⌝ with finish
 
 /-- Two calls, two alternatives: consume-once frames each `mkFreshNat` exactly once. -/
-theorem recovers_snd_pair [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd_pair :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshPair : StateT AppState Id (Nat × Nat))
     ⦃ fun p s => ⌜p.1 = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen [mkFreshPair] frames
@@ -110,15 +107,13 @@ theorem frames_mkFreshSnd [Monad m] [Assertion Pred] [Assertion EPred]
 
 /-- `Id`-specialized `frames_mkFreshSnd`, registered so `finish` discharges the preservation VC. -/
 @[grind .]
-theorem frames_mkFreshSnd_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred}
+theorem frames_mkFreshSnd_Id {P : AppState → Prop}
     (h : ∀ s a, P { s with snd := a } = P s) :
     WP.Frames (· ⊓ ·) (mkFreshSnd : StateT AppState Id Nat) P :=
   frames_mkFreshSnd h
 
 /-- Mirror of `recovers_snd`: frame the complementary (`fst`) footprint. -/
-theorem recovers_fst [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_fst :
     ⦃ fun s => ⌜s.1 = 5 ∧ s.2 = 0⌝ ⦄ (mkFreshSnd : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.1 = 5⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -133,8 +128,7 @@ def mkFreshMixed [Monad m] [MonadStateOf AppState m] : m (Nat × Nat) := do
 
 /-- `mkFreshNat` (writes `fst`) and `mkFreshSnd` (writes `snd`) are framed by different alternatives:
 each recovers the component the other op's lossy spec would drop. -/
-theorem recovers_both [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_both :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshMixed : StateT AppState Id (Nat × Nat))
     ⦃ fun p s => ⌜s.1 = 1 ∧ s.2 = 8⌝ ⦄ := by
   vcgen [mkFreshMixed] frames
@@ -168,16 +162,14 @@ theorem frames_addFst [Monad m] [Assertion Pred] [Assertion EPred]
 
 /-- `Id`-specialized `frames_addFst`, registered so `finish` discharges the preservation VC. -/
 @[grind .]
-theorem frames_addFst_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred} {k : Nat}
+theorem frames_addFst_Id {P : AppState → Prop} {k : Nat}
     (h : ∀ s a, P { s with fst := a } = P s) :
     WP.Frames (· ⊓ ·) (addFst k : StateT AppState Id Nat) P :=
   frames_addFst h
 
 /-- The frame `fun s => ⌜s.2 = j⌝` references the matched argument `j`, so `elabFrame` introduces
 `let j := k` and the assignment is recovered in the postcondition. -/
-theorem recovers_with_arg [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_with_arg :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = k⌝ ⦄ (addFst k : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = k⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -211,15 +203,13 @@ theorem frames_bumpSnd {σ : Type} [Monad m] [Assertion Pred] [Assertion EPred]
 /-- `Id`-specialized `frames_bumpSnd` over an abstract state `σ`, registered so `finish`
 discharges the preservation VC. -/
 @[grind .]
-theorem frames_bumpSnd_Id {σ : Type} [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : σ × Nat → Pred}
+theorem frames_bumpSnd_Id {σ : Type} {P : σ × Nat → Prop}
     (h : ∀ s a, P { s with snd := a } = P s) :
     WP.Frames (· ⊓ ·) (bumpSnd : StateT (σ × Nat) Id Nat) P :=
   frames_bumpSnd h
 
 /-- The frame recovers `s.1 = a` for an abstract `a : σ`, which the lossy spec dropped. -/
-theorem recovers_fst_poly {σ : Type} [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] {a : σ} :
+theorem recovers_fst_poly {σ : Type} {a : σ} :
     ⦃ fun s => ⌜s.1 = a ∧ s.2 = 0⌝ ⦄ (bumpSnd : StateT (σ × Nat) Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.1 = a⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -239,7 +229,7 @@ example [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred]
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen frames | mkFreshSnd => fun s => ⌜s.2 = 7⌝
 
-/-! ## The polymorphic frame lemmas instantiate at a concrete monad -/
+/-! ## The lemmas apply at the `StateM` alias -/
 
 example : ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateM AppState Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := recovers_snd
@@ -303,8 +293,7 @@ def selectiveFrameProc : FrameInferenceProc := fun i => do
 
 /-- `mkFreshNat_spec_guarded` is passed over; the clause still frames `s.2 = 7` when
 `mkFreshNat_spec_lossy` applies. -/
-theorem recovers_snd_second_candidate [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd_second_candidate :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen frames | mkFreshNat => fun s => ⌜s.2 = 7⌝ with finish