fix: over-specialized backward rules in vcgen's spec rule cache (#14431)

This PR fixes `vcgen` failing with `Failed to apply rule` when the same
equality spec matches two different programs within one run, e.g. the
equations of a recursive function registered via `vcgen [f]`: the cached
backward rule was specialized to the first matched program and could not
be applied to the next one.

The rule built from an equality spec unified the equation's LHS with the
goal's program, baking the first program's arguments and dictionaries
into a rule that is cached per spec theorem, `WP` instance and excess
argument count. Rule construction now treats equality specs like `⊑ wp`
specs: it pins only what the cache key determines, namely the monad, the
value and predicate types and the `WP` instance, and leaves the
equation's remaining variables, including instance binders, as schematic
rule parameters that applying the rule binds against the concrete goal
program. Dictionary projections this substitution exposes in the premise
program are reduced by the existing head-reduction step before the next
spec lookup, which also makes the construction-time dictionary synthesis
and projection reduction unnecessary.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean

@@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
 public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
-import Lean.Meta.WHNF
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.Internal.SpecAttr
@@ -269,45 +268,34 @@ Normalize an instantiated equality spec `lhs = rhs` (both of type `info.M α`) t
 
 The schematic `Q`/`E` make the postcondition and exception-postcondition VCs collapse in
 `mkSpecBackwardProof`, so the resulting rule rewrites a `wp lhs` goal to a `wp rhs` premise, matching
-the equational behaviour of a simp spec. Leftover dictionary metavariables (abstract-monad equations
-such as `Spec.UnfoldLift.get`) are synthesized first, and dictionary projections in `rhs` are reduced
-so the RHS exposes the actual operation (e.g. `MonadState.modifyGet`'s RHS `inst.modifyGet` reduces to
-`MonadStateOf.modifyGet`). Reducing, rather than folding the projection, is essential: folding would
-turn it back into the keyed head `MonadState.modifyGet` and the rewrite would loop.
+the equational behaviour of a simp spec. Only the monad, the value type and the `WP` instance are
+pinned from the goal, mirroring how `tryMkBackwardRuleFromSpec` treats `⊑ wp` specs; the equation's
+remaining variables, including instance binders, stay schematic and become rule parameters that
+applying the rule binds against the concrete goal program. Dictionary projections this substitution
+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) (xs : Array Expr) (eqPrf eqType : Expr) :
+private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
     OptionT MetaM (Expr × Expr) := do
-  let_expr Eq eqα lhs rhs := eqType
+  let_expr Eq eqα _lhs _rhs := eqType
     | throwError "simp spec is not an equation: {eqType}"
   -- Recover the value type `α` and confirm the equation is in the goal's monad. `α` is typed at the
   -- monad's domain sort so the equation's element type stays well-formed.
   let α ← mkFreshExprMVar (← inferType info.M).bindingDomain!
   guard <| ← isDefEqGuarded eqα (mkApp info.M α)
-  -- Pin the schematic instance and state metavariables by unifying the equation's LHS with the goal's
-  -- concrete program, so dictionary projections in `rhs` reduce against the real instance.
-  let _ ← show MetaM Bool from commitWhen <| isDefEqGuarded lhs info.prog
-  -- Synthesize leftover dictionary metavariables (e.g. for an abstract-monad lift equation, whose LHS
-  -- does not unify with a concrete program) so the projections in `rhs` reduce against instances.
-  for x in xs do
-    if x.isMVar && !(← x.mvarId!.isAssigned) then
-      try x.mvarId!.assign (← Meta.synthInstance (← Meta.inferType x))
-      catch _ => pure ()
-  -- Reduce dictionary projections to expose the actual operation VCGen continues on.
-  let rhs ← show MetaM Expr from Meta.transform rhs (pre := fun e => do
-    if let .proj .. := e then
-      if let some r ← withDefault <| Meta.reduceProj? e then return .done r
-    return .continue)
+  -- Reusing the goal's `WP` instance below pins the program and value types it is typed at. That
+  -- unification must happen at the current metavariable depth: `mkAppOptM` raises the depth, so the
+  -- equation's type metavariables are read-only there.
+  guard <| ← isDefEqGuarded (mkApp info.M α) info.Prog
   -- `post`/`epost` are schematic metavariables (their VCs collapse downstream).
   let post ← mkFreshExprMVar (userName := `Q) (← mkArrow α info.Pred)
   let epost ← mkFreshExprMVar (userName := `E) info.EPred
-  -- Cast to the reduced RHS so the resulting `wp` rewrites onto the exposed operation.
-  let eqPrf ← mkExpectedTypeHint eqPrf (← mkEq lhs rhs)
   -- Pin the monad and assertion instances from the goal's `wp` arguments. Inferring the monad from
   -- the equation type alone would leave `m β =?= info.M γ` as an underdetermined flex-rigid problem,
-  -- so non-monadic equations like `Option.getD.eq_1` would fail to unify. With `m` fixed, the value
-  -- type is inferred from the equation proof.
+  -- so non-monadic equations like `Option.getD.eq_1` would fail to unify.
   let specProof ← mkAppOptM ``Std.Internal.Do.wp_le_wp_of_eq <|
-    (info.args.extract 0 7).map some ++ #[none, none, some eqPrf, some post, some epost]
+    #[some (mkApp info.M α), some α] ++ (info.args.extract 2 7).map some
+      ++ #[none, none, some eqPrf, some post, some epost]
   return (specProof, ← instantiateMVars (← Meta.inferType specProof))
 
 /--
@@ -326,11 +314,11 @@ same way.
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
     (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
+  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) ←
-    if specType.isAppOfArity ``Eq 3 then eqSpecToWp? info xs specProof specType
+    if specType.isAppOfArity ``Eq 3 then eqSpecToWp? info specProof specType
     else pure (specProof, specType)
   let_expr PartialOrder.rel Pred' _cl' pre rhs := specType
     | throwError "target not a partial order ⊑ application {specType}"

tests/elab/vcgenSpecRuleCache.lean

@@ -0,0 +1,39 @@
+import Std.Tactic.Do
+import Std.Internal.Do
+
+/-!
+Regression test for `vcgen`'s spec backward-rule cache. The rule built from an equality spec must
+stay generic in the spec's value variables: the cache reuses the rule for every program matching
+the same spec theorem, so a rule specialized to the first matched program (e.g. `recf 3` below,
+whose unfolding produces the recursive call `recf 2` handled by the same equation) fails on the
+next one.
+-/
+
+set_option mvcgen.warning false
+
+def recf (n : Nat) : Id Nat :=
+  match n with | 0 => pure 1 | n + 1 => recf n
+
+def myid (a : Nat) : Id Nat :=
+  pure a
+
+def myid2 (a : α) : Id α :=
+  pure a
+
+section
+open Lean.Order Std.Internal.Do
+
+-- The same equation `recf.eq_2` matches both `recf 3` and the recursive call `recf 2`.
+example : ⦃ True ⦄ recf 3 ⦃ fun r => r > 0 ⦄ := by
+  vcgen [recf] with finish
+
+-- The same equation `myid.eq_1` matches two calls with different arguments.
+example : ⦃ True ⦄ (do let x ← myid 3; let y ← myid 5; pure (x + y) : Id Nat) ⦃ fun r => r > 0 ⦄ := by
+  vcgen [myid] with finish
+
+-- The same equation `myid2.eq_1` matches calls at two different value types.
+example :
+    ⦃ True ⦄ (do let x ← myid2 3; let y ← myid2 "st"; pure (x + y.length) : Id Nat)
+    ⦃ fun r => r > 0 ⦄ := by
+  vcgen [myid2] with finish
+end