Check

Semi-trusted (Layer 1): uses the TCB (eval/quote/conv) and reports type errors via send "typeError". Bugs here may produce wrong error messages but cannot cause unsoundness.

Core Functions

check : Ctx → Tm → Val → Computation Tm — checking mode. Verifies that tm has type ty and returns an elaborated term.
infer : Ctx → Tm → Computation { term; type; } — synthesis mode. Infers the type of tm and returns the elaborated term with its type.
checkType : Ctx → Tm → Computation Tm — verify a term is a type.
checkTypeLevel : Ctx → Tm → Computation { term; level; } — like checkType but also returns the universe level.

Context Operations

emptyCtx — empty typing context { env = []; types = []; depth = 0; }
extend : Ctx → String → Val → Ctx — add a binding (index 0 = most recent)
lookupType : Ctx → Int → Val — look up a variable's type by index

Test Helpers

runCheck : Computation → Value — run a computation through the trampoline handler, aborting on typeError effects.
checkTm : Ctx → Tm → Val → Tm|Error — check and unwrap.
inferTm : Ctx → Tm → { term; type; }|Error — infer and unwrap.

Key Behaviors

Sub rule: when checking mode doesn't match (e.g., checking a variable), falls through to infer and uses conv to compare.
Cumulativity: U(i) ≤ U(j) when i ≤ j.
Large elimination: motives may return any universe, enabling type-computing eliminators (checkMotive).
Trampolining: Succ and Cons chains checked iteratively.

`bindP`

bindP: position-tagged bind for kernel rule bodies — sequences two computations and wraps any typeError raised by the inner one under the given Position before re-raising.

bindP : Position -> Computation a -> (a -> Computation b) -> Computation b

Installs a local typeError handler around the inner computation m that calls D.nestUnder position on every emitted diag.Error before re-raising. The wrapping records the descent coordinate at the caller site — precision that downstream generic paths (the check → infer catch-all, deep conv failures) cannot supply.

The continuation k runs unwrapped on success; errors raised by k itself are not intercepted. Pure fast-path: when m is K.pure v, no handler is installed and the combinator reduces to k v.

Use over K.bind whenever the failing site has a definite positional identity in the surface syntax. Pair with bindPChain to thread N positions through a single shared handler.

`bindPChain`

bindPChain: fused sequential variant of bindP — threads a list of positions through a single shared typeError handler so the emitted blame chain has positions[0] as the outermost edge.

bindPChain : [Position] -> Computation a -> (a -> Computation b) -> Computation b

Equivalent to nested bindP p_1 (bindP p_2 (... (bindP p_n m) k_pure) k_pure) k when intermediate continuations are pure passthroughs, but installs only one handler with a pre-composed wrap function. Empty positions falls back to K.bind; pure m short-circuits to k m.value as in bindP.

`bindPR`

bindPR: rule-annotated variant of bindP — wraps the inner computation under withRule rule position so the blame edge records both the structural coordinate and the kernel-rule identity that emitted the descent.

bindPR : Position -> String -> Computation a -> (a -> Computation b) -> Computation b

Equivalent to bindP (fx.diag.positions.withRule rule position) m k. The hint resolver consults only position.tag, so the rule annotation never changes hint lookup — it surfaces in pretty-printed output and is available to any consumer reading Position.rule directly. Pure fast-path matches bindP: when m is K.pure v, the combinator reduces to k v with no handler install.

`check`

check: bidirectional checking-mode entry — verify tm : ty and return the elaborated kernel term; dispatches intro-form rules against their type-formers and falls through to synthesis plus structural conversion.

check : Ctx -> Tm -> Val -> Comp Tm

Dispatches intro forms against their corresponding type formers: lam vs VPi, pair vs VSigma, tt vs VUnit, boot-inl/boot-inr vs VBootSum, boot-refl vs VBootEq, squash-intro vs VSquash, string-lit/int-lit/... vs their primitive value types, and the trampolined desc-con vs VMu. Anything not matched falls through to infer plus a structural C.conv round-trip — the sole CHECK-to-INFER bridge in the bidirectional rules.

The kernel is Tarski-style and non-cumulative: a term checked against U(k) must have inferred type exactly U(k) modulo convLevel. No universe-cumulativity coercion fires here. Per-summand level mixing in desc-arg / desc-pi is handled through the bound-witness slot at synthesis time.

The desc-con branch is trampolined for deep recursive data (5000+ layers): it peels homogeneous linear-recursive chains along a single recursive position when the description is a plus-coproduct A + B with exactly one linear-recursive summand. Non-linear shapes (tree, mutual recursion, multiple recursive constructors, non-plus D) fall through to per-layer checking via the degenerate n = 0 branch. Constructor certificates (_descConCert) accelerate the non-recursive case by skipping the chain walk entirely.

Failure modes emit D.mkKernelError via the typeError effect; positions and rule keys identify the failure site for the diagnostic renderer. Cross-ref: infer for the synthesis side, checkMotive for eliminator motive validation.

`checkTm`

checkTm: unwrapped variant of check — runs runCheck (self.check ctx tm ty) so callers get the elaborated term or a flat error record without manual trampoline handling.

checkTm : Ctx -> Tm -> Val -> Tm | { error; msg; expected; got }

`checkType`

checkType: thin wrapper around checkTypeLevel that discards the level — verifies tm is a type and returns the elaborated term only.

checkType : Ctx -> Tm -> Computation Tm

`checkTypeLevel`

checkTypeLevel: type-formation judgement — verifies that tm is a type and returns both the elaborated term and the universe Level value it inhabits.

checkTypeLevel : Ctx -> Tm -> Computation { term; level }

level is a kernel Level value (V.vLevelZero, V.vLevelSuc, V.vLevelMax) — not a Nix integer — so level-polymorphic types (U(k) for a variable k : Level) flow through without ad-hoc integer machinery. Levels come from the typing derivation, not post-hoc value inspection (e.g., Π(x:A). B computes its level as the vLevelMax of domain/codomain levels). The fallback path delegates to infer and succeeds iff the inferred type is a universe; in that case .type.level is already a Level value and is forwarded verbatim.

`emptyCtx`

emptyCtx: empty typing context { env = []; types = []; names = []; depth = 0; } — the zero of extend; starting point for top-level check/infer invocations.

emptyCtx : Ctx

`extend`

extend: append a binding to a typing context — pushes a fresh de Bruijn variable at depth ctx.depth, the new type at index 0, and the name at index 0 of names; depth increments by one.

extend : Ctx -> String -> Val -> Ctx

`infer`

infer: bidirectional synthesis-mode entry — given a term, return both the elaborated kernel term and a Val representing its inferred type; covers variables, annotations, application, projections, eliminators, the universe hierarchy, primitive type formers, and Desc/Mu operations.

infer : Ctx -> Tm -> Comp { term : Tm; type : Val; }

Dispatches on tm.tag to one rule per term shape. Type formers (pi, sigma, list, boot-sum, boot-eq, mu, squash) delegate to checkTypeLevel and lift the returned level into a VU type. Eliminators (bool-elim, list-elim, sum-elim, desc-ind, j, squash-elim, ...) are the most intricate dispatches: each builds expected motive/step types by quoting the motive at the appropriate de Bruijn depth, accounting for the fresh binders introduced by each step lambda.

Variables look up their type in ctx.types by index. ann elaborates the type annotation first, then checks the body against the resulting Val — with one optimisation: when _descRef is present and the body is trusted (emitted only by T.mkAnnTrusted inside the kernel itself), the body is accepted without re-checking. This avoids quadratic blowup on deep recursive-data CHECK where every layer carries the same encoded element description. app infers the function side, validates the argument against the domain, and instantiates the codomain closure with the argument's value.

Failure to find an applicable rule emits a typeError with rule "infer" and message "cannot infer type". Per-rule positions and rules identify the specific failure for the diagnostic renderer. Cross-ref: check for the checking-mode side, checkTypeLevel for type-former level extraction, checkMotive for motive validation in eliminator rules.

`inferTm`

inferTm: unwrapped variant of infer — runs runCheck (self.infer ctx tm) so callers get { term; type } or a flat error record without manual trampoline handling.

inferTm : Ctx -> Tm -> { term; type } | { error; msg; expected; got }

`lookupType`

lookupType: read a variable's type from a context by de Bruijn index — index 0 is the most recent binding; throws on out-of-range index with a descriptive message.

lookupType : Ctx -> Int -> Val

`runCheck`

runCheck: discharge a checking computation through the trampoline handler — collapses typeError into a flat { error; msg; expected; got } record; returns the success value on the happy path.

runCheck : Computation a -> a | { error; msg; expected; got }

Installs a typeError handler that aborts the computation on the first emission, exposing the structured diag.Error as error plus convenience projections msg, expected, and got (the leaf detail fields). The success branch returns whatever the computation yielded; only the post-handle result.value is exposed (state is discarded).

Pair with checkTm / inferTm for the unwrapped form, or with fx.tc.check.diag.runCheckD / runCheckDLazy for hint-decorated failures.