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.
Non-cumulative universes: Tarski-style, exact-level — U(i) does not subsume into U(j) for i < j; conv compares levels by convLevel with no cumulativity coercion.
Large elimination: motives may return any universe, enabling type-computing eliminators (checkMotive).
Trampolining: Succ and Cons chains checked iteratively.

_blame: shared blame-frame discipline for bindP — { handlers, fold, empty } installed by every trampoline that runs a kernel check Computation so position wrapping is reconstructed at the single top-level typeError handler. blame is an opaque cons list (deepSeq-opaque ⇒ O(1)/step, structurally shared); empty is its nil for state init.

_blame : { handlers : Handlers, fold : Blame -> Error -> Error, empty : Blame }

`_yield`

__yield: tcYield defer discipline — { handlers, wrap } installed alongside blame by every trampoline running a kernel check Computation. A head wrap makes a recursive checker entry effect-first (O(1) WHNF), so the bindP isPure fast path stays flat on recursive arms while leaving syntactic leaves Pure. tcYield carries no state and no blame frame — observationally invisible.

_yield : { handlers : Handlers, wrap : Computation a -> Computation a }

`bindP`

bindP: position-tagged bind for kernel rule bodies — brackets the inner computation with a push/pop blame frame so any typeError it raises is wrapped under the given Position before reaching the top-level handler.

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

Brackets an impure inner computation m with a tcBlamePush/tcBlamePop frame whose wrap calls D.nestUnder position on every diag.Error m raises. A pure m skips the frame and threads its value to k (it raises nothing, so push-then-pop is a no-op). The push is emitted before an impure m, so the combinator is Impure in O(1) and forces m only to WHNF — recursion in m defers into the trampoline. 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 after the pop, so errors it raises are not wrapped by this frame. Frames are reconstructed onto the leaf error by the single top-level handler (see _blame). 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 one bracket.

`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 pushes a single composite frame nesting the positions outermost-first. positions is forced only on the error path; empty positions push an identity frame.

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

`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 = envNil; types = envNil; names = envNil; depth = 0; } — the zero of extend; starting point for top-level check/infer invocations. env/types/names are de Bruijn cons-list spines (index 0 = most recent binding) walked iteratively by envNth, so deep contexts stay host-stack- and call-depth-flat.

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. depth/eb are forced at each extend so the scalar counters stay plain ints, never deferred +1/or-thunk chains that recurse N-deep on the C-stack when finally forced (cf. value.nix env-spine memo). The entry-yield budget eb carries through unchanged (consumed only at check/infer heads).

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. Indexes the types cons-list spine via the iterative envNth (host-stack- and call-depth-flat); the bound check uses the O(1) depth counter (= spine length) instead of re-walking the spine.

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.