# 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` __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. ## Sub-namespaces - [`_internal`](/nix-effects/type-checker/check/_internal) - [`diag`](/nix-effects/type-checker/check/diag) ## Source - [`src/tc/check/bindP.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/bindP.nix) - [`src/tc/check/check.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/check.nix) - [`src/tc/check/ctx.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/ctx.nix) - [`src/tc/check/infer.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/infer.nix) - [`src/tc/check/type.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/type.nix)