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 the checker’s working context (v0.29.10). Empty (Default) for pure functions / non-context code.

CapabilityInfo

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

CapabilityOpInfo

CheckSinks

#522: the six output sinks a handler-body check writes into. One struct at each call site instead of six positional &mut arguments.

CheckedProgram

T3.7 (R3.10): the gate between analysis and emission, as a type rather than a control-flow decision — constructible only by certify, so no unchecked or error-carrying TypedCommons can reach the emitter by construction (previously enforced only by every caller happening to check a Result first). certify rejects on any error-severity diagnostic; T3.3a’s Ty::Error is what a diagnosed checker failure records into expr_types, so in practice a Ty::Error never reaches a CheckedProgram either — R4.3’s “rejected by certify” already holds today via the same diagnostic-severity gate certify makes structural.

HandlerBodyCheck

#522: everything check_handler_body needs to know about the handler — signature, capability scope, agent state, and held bindings. Replaces what was 17 positional parameters (of a 24-parameter signature); Self::new fills the agent/actor/store extras with empties, so a simple site (provider op, test body) sets only the fields it actually uses.

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.

TestHandler

One service handler, as a test body sees it (v0.178 / v0.182).

TestServiceSig

v0.178 (Slice 0, #662) / v0.182 (Slice A, #664): the shape a test body needs to resolve a service invocation. Built by the project test pass from the target unit’s service declarations, so the checker can resolve the addressed handler (svc.call(...) on an on call service, or — Slice A — svc.GET("/x") / svc.schedule("…") / svc.message(m) on a from http / cron / queue service) and check its arity, argument types, and principal.

TyId

T3.6b (R4.1/R4.2): a Ty’s identity above the intern table — Copy, Hash, Ord, cheap to pass and compare. Resolved back to a Ty only via the Types table it was interned into (see that type’s own doc).

TypedCommons

Output of type checking.

TypedExpr

T3.4: an expr_types entry — the checked type, plus the span of the node it was computed for. Deref-free by design (.ty/.span, not .0/.1) so call sites read the same as they did against a bare Ty before this.

Types

T3.6b (R4.1): the intern table TyId is minted from. Owned per check_record invocation (design settled in the identity-and-totality track doc §9 before this slice started): created fresh at check_record’s entry, threaded through Ctx, carried out on TypedCommons/RecordCheck alongside expr_types, and forwarded across the bynk-check→bynk-emit boundary on CheckedProgram (T3.7a/T3.7b already built that seam). Confirmed safe by checking how cross-unit type references actually flow: compose_unit_symbols merges TypeDecl (immutable AST declarations) across units, never an already-interned Ty/TyId — every unit re-interns its own Ty graph from shared declarations, so TyIds are never compared across two different check_record invocations.

VariantInfo

A flattened view of a type’s variants (name + payload types).

Enums

Callee

P6.0 (design/tracks/the-ir.md §6, #1139): a resolved classification of a call-shaped expression, recorded once by the checker’s own dispatch (checker::calls) rather than re-derived by each later consumer — closing R6.10’s duplicated-classification gap between bynk-check and bynk-emit’s lower_method_call/lower_call.

NamedKind

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

QueryRole

Whether a Callee::Query call returns another Query[T] (chainable) or executes and returns Effect[T] — R6.12: “the builder/terminal split is a field on the callee, not a name list.” Primarily read back from check_query_kernel_method’s own return type at the recording site (query_role, below) — falling back to is_query_builder_name only when the call didn’t type at all (an arity mismatch, or a type error deeper inside the call — map’s own lambda body, say — both return None too, not just an arity failure), so a best-effort reader of an uncertified/erroring unit still gets the right role.

StoreField

One agent store field’s kind and shape (finding #36) — the checker’s dispatch keys off this instead of five separate per-kind maps, so a new storage kind is one new variant rather than a sixth map threaded through every constructor and lookup site.

Ty

A resolved type.

Functions

call_record_type_name

The synthetic record type name for trace(Cap.op)’s call records (v0.117): one record per capability operation, its fields the operation’s parameters.

certify

The single place “may we emit?” is asked (R3.10). Rejects — returning every diagnostic, not just the error-severity ones, matching check_record’s own error-path convention — if diagnostics contains an error-severity entry; otherwise wraps program as certified.

check

check_body

Type-check a bare body against return_ty in scope, with caps available as both in-scope and declared capabilities and (if non-empty) test_services/test_actors in scope for a test-case body’s svc.call/ by <Actor>(...) resolution (§32/#33: the one shape every hand-rolled Ctx outside this crate needed, letting Ctx itself stay pub(crate)). where_pred, if present, is checked first against Bool (a property’s optional for all ... where filter — bynk.property.where_not_bool on mismatch), sharing ctx with the main body so both populate the same expr_types/errors sinks. Unlike check_handler_body, this skips the linearity pass, the return-type-mismatch diagnostic, and the unused-given diagnostic — nothing outside this crate that built its own Ctx ran those either, and adding them here would be a behaviour change, not a refactor.

check_contracts

Check a function’s contract clauses (v0.115 §, testing track slice 3). A contract is the invariant predicate attached to a function (ADR 0144 — one predicate surface): each requires/ensures is a pure Bool-typed expression, requires over the parameters and ensures over the parameters plus result (the return value; the awaited element for an Effect). The pass enforces, mirroring check_invariants:

check_event_field_default

Events slice 3a (#972): type-check an event field’s default expression (field: T = init), reusing check_static_initialiser’s empty-pure-scope discipline. Pushes bynk.event.bad_field_default.

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_record_in

check_record against a caller-supplied intern table (T3.6b, R4.1).

check_state_initialiser

v0.11: type-check an agent state-field initialiser (field: T = init). See check_static_initialiser. Pushes bynk.agents.bad_state_initialiser.

check_transitions

Check an agent’s step invariants (v0.116 §, testing track slice 4). A transition is the invariant predicate widened to the step (ADR 0144 — one predicate surface): a pure Bool predicate over the old/new state pair, each bound to the agent’s synthetic state record (state_ty), so old.status / new.status resolve like any record field. The pass enforces, mirroring check_invariants:

compatible

t is usable where u is expected.

embedding_for

v0.154 (ADR 0178): the declared error embedding that converts source_err into target_err, if one exists. When target_err is a sum declaring embeds E as V with E compatible with source_err, returns (sum_type_name, variant_name) — the variant a value of source_err auto-wraps into. One level only: the source must match a declared embedding directly. Used by ? in the checker (to accept the conversion) and the emitter (to lower the Err-wrap) from the same rule, so the two cannot diverge.

instantiate_field_ty

v0.157 (ADR 0183): the type of a generic record’s field at a concrete instantiation. The field’s declared type is resolved with the declaration’s type parameters in scope as rigid vars, then those vars are replaced by the instantiation’s args. For a non-generic record this is a plain resolve.

locale_tag_accepts

Whether tag satisfies LocaleTag’s refinement — the check behind bynk.messages.invalid_locale_tag. Evaluated with the same regex-engine semantics (regress, anchored, no flags) the emitted new RegExp(...) runs under, so a tag accepted here is one the runtime cast is honest about.

locale_tag_pattern

The pattern LocaleTag’s refinement matches against, for a diagnostic that names it. None if the type carries no Matches predicate.

map_entry_ty

v0.158 (ADR 0184): the compiler-known MapEntry[K, V] record — the element a store Map[K, V]’s .entries query yields. A nominal generic record ({ key: K, value: V }), so it flows through unify/compatible/display and the ADR 0183 non-boundary rule like any generic-record instantiation; its fields are resolved by name in check_field_access (it has no user-visible TypeDecl, like JsonError).

named_ty

Build a Ty::Named for the given declaration (no applied type arguments).

named_ty_with_args

Build a Ty::Named for the given declaration with the given applied type arguments (empty for a non-generic reference).

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_param_subst

v0.157 (ADR 0183): the substitution mapping a generic record’s declared type parameters onto a concrete instantiation’s arguments. Empty when the type is non-generic or args is empty (an under-applied reference — the resolver reports that separately).

variants_of

pub since P6.4 (#1157, Decision A) — see VariantInfo’s own doc comment for why bynk-emit needs this exact function rather than a re-derived copy (R5.11, for the IR side).

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.