3.2. Bidirectional type checking🔗

There are two operations on expressions, written here in standard bidirectional notation:

Γ ⊢ e ⇒ A            -- "e synthesizes A"     (Synth.resolveStmtExpr)
Γ ⊢ e ⇐ A            -- "e checks against A"  (Check.resolveStmtExpr)

Synthesis returns a type inferred from the expression itself; checking verifies that the expression has a given expected type. Each construct picks a mode based on whether its type is determined locally (synth) or by context (check). The two judgments are connected by a single change-of-direction rule, subsumption:

\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}

The two judgments are implemented as Synth.resolveStmtExpr and Check.resolveStmtExpr:

def

Strata.Laurel.Resolution.Synth.resolveStmtExpr
  (exprMd : Strata.Laurel.StmtExprMd)
  (expected? : Option Strata.Laurel.HighTypeMd := none) :
  Strata.Laurel.ResolveM
    (Strata.Laurel.StmtExprMd × Strata.Laurel.HighTypeMd)
Strata.Laurel.Resolution.Synth.resolveStmtExpr
  (exprMd : Strata.Laurel.StmtExprMd)
  (expected? :
    Option Strata.Laurel.HighTypeMd :=
    none) :
  Strata.Laurel.ResolveM
    (Strata.Laurel.StmtExprMd ×
      Strata.Laurel.HighTypeMd)

Synth-mode resolution: resolve e and synthesize its HighType, written Γ ⊢ e ⇒ T. Each constructor with a synthesis rule delegates to its rule's helper. Statement-shaped constructs (While, Exit, Return, Assert, Assume, Var-Declare) synthesize TVoid.

Synthesis returns a type inferred from the expression itself; checking (Check.resolveStmtExpr) verifies that the expression has a given expected type. The two functions are mutually recursive, with termination on a lexicographic measure (exprMd, tag) — tag 2 for synth, 3 for check, helpers smaller — so that subsumption (which calls synth on the same expression) can decrease via Prod.Lex.right.

expected? is the type this expression is being checked against, when the caller has one. It is NOT a second checking mode: every rule below ignores it except the call rules, which need it to bind a type argument that the arguments alone leave undetermined (setEmpty<T>() fixes T from nowhere else), and the check-capable wrappers IfThenElse, Block, Old, OldGuarantee, OldRelies and ProveBy, which forward it to their value-producing children so a call nested in one sees the same slot a direct one would. Subsumption still happens in Check.resolveStmtExpr, which is the one place that verifies the synthesized type against expected — passing it here only sharpens inference, it never accepts anything extra.

def

Strata.Laurel.Resolution.Check.resolveStmtExpr
  (exprMd : Strata.Laurel.StmtExprMd)
  (expected : Strata.Laurel.HighTypeMd) :
  Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
Strata.Laurel.Resolution.Check.resolveStmtExpr
  (exprMd : Strata.Laurel.StmtExprMd)
  (expected : Strata.Laurel.HighTypeMd) :
  Strata.Laurel.ResolveM
    Strata.Laurel.StmtExprMd

Check-mode resolution (rule Sub at the boundary): resolve e and verify its type is a consistent subtype of expected, written Γ ⊢ e ⇐ T. Bidirectional rules for individual constructs push expected into subexpressions rather than bouncing through synthesis, which keeps error messages localized and lets the expected type propagate through nested control flow. Constructs with a dedicated Check.<construct> rule:

bindings — Var (.Declare …), Assign
control flow — Block, IfThenElse, While, Exit, Return
verification — Assert, Assume, Old, ProveBy
holes — Hole (typed and untyped)

Everything else falls back to subsumption — synthesize, then verify isConsistentSubtype actual expected.

The right principle for new call sites is: when the position has a known expected type (TBool for conditions, numeric for decreases, the declared output for a constant initializer or a functional body), use Check.resolveStmtExpr. When it doesn't, use resolveStmtExpr (a thin wrapper that calls Synth.resolveStmtExpr and discards the synthesized type, used at sites where typing is not enforced — verification annotations, modifies/reads clauses).