Module checker 

Type checker and refinement validator (spec §§5–6, v0.1 §4.2, v0.2 §4.2).

Operates on a ResolvedCommons. Walks declarations, validates each refinement against the spec’s predicate-base compatibility and combination rules, then type-checks every function and method body.

v0.2 extensions:

• Record types (compatibility, field access, construction).
• Sum types and variant construction (qualified and unqualified).
• Methods (instance and static) with UFCS-style call resolution.
• Pattern matching with exhaustiveness checking.
• The is operator with binding flow into truthy contexts.
• The built-in generic Option[T].

Structs

CapabilityCtx

Mutable per-function context. Capability bookkeeping for the checker — the given-clause lifecycle and capability dispatch, grouped out of Ctx (v0.29.10). Empty (Default) for pure functions / non-context code.

CapabilityInfo

Per-capability info for checker dispatch within a handler body.

CapabilityOpInfo

Ctx

RecordCheck

The outcome of check_record: the typed model (Err if the file had any error) and, on the error path, the best-effort partial expr_types the checker computed before bailing. Analyse mode surfaces that partial map for .-member completion and signature help even on a broken buffer (ADR 0094); on the Ok path the types live in the TypedCommons, so this is empty.

TypedCommons

Output of type checking.

Enums

NamedKind

The shape of a named type — what its declaration looks like.

Ty

A resolved type.

Functions

check

check_handler_body

Check a single handler body (used for service and agent handlers).

check_invariants

Check an agent’s invariant declarations (v0.80 §14). Each predicate is a pure Bool-typed expression over the agent’s state fields (referenced by bare name), plus implies/is. The pass enforces:

check_record

check, recording binding edges into refs at the checker’s resolution sites (v0.25). A fresh sink records nothing.

check_state_initialiser

v0.11: type-check an agent state-field initialiser (field: T = init). The initialiser must be a static value of the field type — it is checked in an empty, pure scope (so self, parameters, capabilities, and effects are all out of reach) with the field type as the expected type, so refined literals admit (v0.9.4) and sum variants resolve. The init’s expression types are recorded into expr_types for emission; a single bynk.agents.bad_state_initialiser is pushed on any failure.

compatible

t is usable where u is expected.

named_ty

Build a Ty::Named for the given declaration.

record_type_refs

v0.25 (ADR 0053): record a binding edge for every Named reference inside a type-ref that resolved. Called alongside the resolve_type_ref* annotation sites; skip holds the enclosing fn’s type parameters (rigid vars are not type symbols). Handler signatures and body annotations never pass through the resolver’s reference walk, so these sites are their only recording point; where both passes run, assembly dedupes.

resolve_type_ref

resolve_type_ref_in

v0.20a: like resolve_type_ref, with a set of in-scope type parameters: a Named reference matching one resolves to Ty::Var (checked before the type-table lookup — a type parameter shadows a same-named declaration; the collision is diagnosed at the declaration).

type_from_decl

Build a Ty from a TypeDecl name reference.

type_of

type_of_block

zero_value_ts

The TypeScript zero-value expression for type_ref (with an optional inline field refinement), or None if the type is not zeroable.