Fix SMT encoding for polymorphic Sequence preconditions (#1201)

Strata/DL/Lambda/Preconditions.lean

@@ -53,6 +53,42 @@ def substitutePrecondition
   let substitution := formals.zip actuals |>.map fun ((name, _), actual) => (name, actual)
   LExpr.substFvarsLifting precond substitution
 
+/--
+Derive a type substitution at a call site for instantiating a polymorphic
+precondition. Prefers concrete information from the arguments' types over the
+operator's type annotation, because the operator's annotation may still be the
+generic type when `PrecondElim` runs before type checking. Falls back to the
+operator annotation when arguments carry no type information.
+
+Returns `Subst.empty` for monomorphic functions or when no useful constraints
+are available; the resulting unsubstituted precondition will be handled
+downstream (the SMT encoder treats unresolved type variables as uninterpreted
+sorts, yielding `unknown` rather than failing).
+
+Note: this is structurally similar to `LFunc.computeTypeSubst` in `Factory.lean`,
+but with the priority *reversed*. `computeTypeSubst` prefers `.op` annotations
+because it is called after type inference, where the `.op` always carries the
+instantiated arrow type. Here we run before type checking, so the `.op` may
+still carry the generic type — argument types are the more reliable source.
+The two helpers cannot be unified by a flag without destabilising the
+`computeTypeSubst`-based proofs in `Semantics.lean` (e.g.
+`computeTypeSubst_of_opTypeSubst`).
+-/
+def callSiteTypeSubst (fn : LFunc T) (callee : LExpr T.mono)
+    (args : List (LExpr T.mono)) : Subst :=
+  if fn.typeArgs.isEmpty then Subst.empty
+  else
+    let argConstraints := (args.zip fn.inputs.values).filterMap
+      (fun (arg, formal) => arg.typeOf.map (·, formal))
+    let argSubst :=
+      if argConstraints.isEmpty then none
+      else match Constraints.unify argConstraints SubstInfo.empty with
+        | .ok substInfo => some substInfo.subst
+        | .error _ => none
+    match argSubst with
+    | some s => s
+    | none => fn.opTypeSubst callee |>.getD Subst.empty
+
 /--
 Collect all WF obligations from an expression by traversing it and finding
 all calls to functions with preconditions.
@@ -71,12 +107,19 @@ where
     -- A function call generates an obligation that the precondition is
     -- satisfied under the current assumptions
     let callObligations := match Factory.callOfLFunc F e with
-      | some (_op, args, func) =>
+      | some (op, args, func) =>
         if func.preconditions.isEmpty then []
         else
           let md := e.metadata
+          -- Resolve polymorphic type variables in the precondition with the
+          -- type substitution implied by this call site. Without this, a
+          -- precondition expression like `(~Sequence.length : (Sequence %a) → int) s`
+          -- would carry the formal type variable `%a` into the obligation,
+          -- which the SMT encoder cannot resolve (issue #1201).
+          let tySubst := callSiteTypeSubst func op args
           func.preconditions.map fun precond =>
             let substedPrecond := substitutePrecondition precond.expr func.inputs args
+            let substedPrecond := substedPrecond.applySubst tySubst
             { funcName := func.name.name
               obligation := wrapImplications implications substedPrecond
               callSiteMetadata := md

Strata/Languages/Core/SMTEncoder.lean

@@ -236,7 +236,15 @@ def LMonoTy.toSMTType (E: Env) (ty : LMonoTy) (ctx : SMT.Context) (useArrayTheor
   | .ftvar tyv => match ctx.tySubst.find? tyv with
                     | .some termTy =>
                       .ok (termTy, ctx)
-                    | _ => .error f!"Unimplemented encoding for type var {tyv}"
+                    | _ =>
+                      -- Unresolved type variable from a polymorphic precondition
+                      -- whose call-site type couldn't be inferred (e.g. inside a
+                      -- polymorphic function body, or with polymorphic args).
+                      -- Treat as a fresh uninterpreted sort so the obligation can
+                      -- still be encoded; the solver will report `unknown` rather
+                      -- than the encoder failing outright (issue #1201).
+                      let ctx := ctx.addSort { name := tyv, arity := 0 }
+                      .ok ((.constr tyv []), ctx)
 
 def LMonoTys.toSMTType (E: Env) (args : LMonoTys) (ctx : SMT.Context) (useArrayTheory : Bool := false) :
     Except Format ((List TermType) × SMT.Context) := do

StrataTest/DL/Lambda/PreconditionsTests.lean

@@ -105,4 +105,43 @@ info: [WFObligation(safeDiv, (∀ (bvar:int) ((~Bool.Implies : (arrow bool (arro
 #eval collectWFObligations testFactory
   esM[((λ (int): %0) ((~safeDiv a) b))]
 
+/-! ### Polymorphic preconditions: type substitution at call site
+
+A polymorphic function whose precondition mentions the type variable `%a`
+must have that variable substituted with the call site's instantiated type.
+Without this, downstream SMT encoding fails on unresolved type vars (issue #1201).
+-/
+
+-- A polymorphic function `polySel<a>(s : Sequence a) : a` whose precondition
+-- contains an operator annotated with the type variable `%a`. This mirrors
+-- `Sequence.select`'s `0 <= i && i < Sequence.length(s : Sequence %a)`
+-- bound check, which uses an annotated `Sequence.length` op.
+private def polySelFunc : LFunc TestParams :=
+  { name := "polySel"
+    typeArgs := ["a"]
+    inputs := [("s", mty[Sequence %a])]
+    output := mty[%a]
+    -- precondition: ((~lenOf : (Sequence %a) → int) s)
+    -- The op carries a `%a` annotation that must be substituted at the call site.
+    preconditions := [⟨esM[((~lenOf : (Sequence %a) → int) s)], ()⟩]
+  }
+
+private def polyFactory : Factory TestParams := .ofArray #[polySelFunc]
+
+-- Call site annotates the operator with the instantiated arrow type
+-- `Sequence int → int`. After value substitution alone, the op annotation
+-- `(~lenOf : (Sequence %a) → int)` would still carry `%a`; the fix must also
+-- apply the call-site type substitution `[%a → int]`.
+/-- info: [WFObligation(polySel, ((~lenOf : (arrow (Sequence int) int)) myseq), ())] -/
+#guard_msgs in
+#eval collectWFObligations polyFactory
+  esM[((~polySel : (Sequence int) → int) myseq)]
+
+-- Same expectation when the operator is unannotated: the argument-types
+-- fallback unifies `Sequence int` against `Sequence %a` to derive `[%a → int]`.
+/-- info: [WFObligation(polySel, ((~lenOf : (arrow (Sequence int) int)) (myseq : (Sequence int))), ())] -/
+#guard_msgs in
+#eval collectWFObligations polyFactory
+  esM[(~polySel (myseq : (Sequence int)))]
+
 end Lambda