2.1. 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) :
  Strata.Laurel.ResolveM
    (Strata.Laurel.StmtExprMd × Strata.Laurel.HighTypeMd)
Strata.Laurel.Resolution.Synth.resolveStmtExpr
  (exprMd : Strata.Laurel.StmtExprMd) :
  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.

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).