Type Checker

fx.tc.term: kernel term constructors (Pi, Sigma, U, Id, J, datatype/desc nodes) de-Bruijn indexed; each carries `tag` distinct from value-domain `_tag`.

fx.tc.value: semantic domain produced by evaluation; values use de Bruijn LEVELS (counting outward) so substitution under binders stays unproblematic.

fx.tc.quote: TCB read-back from values to terms, translating de Bruijn levels back to indices; pure, no type information, no effects.

fx.tc.conv: structural conversion check on de Bruijn level values; pure TCB component asking whether two values are definitionally equal at a given depth.

fx.tc.eval: pure kernel evaluator for `eval`/`evalF`/`instantiate` plus elimination helpers; zero effect-system imports, part of the TCB.

fx.tc.eval._internal: cross-part evaluator helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.

fx.tc.eval.dispatch: full kernel evaluator self-fixpoint. Consumed by overlay constructions (notably `tc/elaborate/eval-overlay.nix`) that need to build a me...

fx.tc.check: bidirectional type checker with check/infer/checkType/checkTypeLevel, cumulativity, and trampolined succ/cons chains.

fx.tc.check.diag: outside-the-trust-boundary diagnostic shell that routes kernel `check`/`infer` results, attaches hints, and formats failures for editors.

fx.tc.check._internal: cross-part checker helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.

fx.tc.elaborate: bridge between `fx.types` and the kernel — `elaborateType`/`elaborateValue`/`extract`/`decide` translate values to kernel terms and back.

fx.tc.elaborate.meta: meta-aware overlay — `VMeta`, overlay check/infer, overlay eliminators, quote, `elabConv`, five scoped meta-effects (force/getMetas/a...

fx.tc.elaborate._internal: cross-part elaboration helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.

fx.tc.hoas: HOAS surface combinators for kernel terms — types, binders, descriptions, datatypes, ornaments, and the elaborator that compiles to de Bruijn `...

Unstable internal surface — boot-sum/boot-eq helpers, kernel-Tm encoders, and indexed-variant scaffolding; prefer SumDT/EqDT-generated forms in user code.

Kernel-Tm and Val-level encoders for surface description combinators; consumed by `tc/eval` (descDescVal) and `tc/generic` (encodeDescXTm pre-evaluations).

Forced-argument analysis helpers for datatype constructors; consumed by datatype elaboration and tests that inspect recoverable constructor fields.

Indexed/equality-aligned combinators (`muI`, `piI`, `recI`, `plusI`, `inrAt`, `fieldAt`) consumed by ornament construction and indexed-datatype test fixtures.

fx.tc.surface: additive surface-language elaboration framework over HOAS.

Surface elaborator registry operations. empty Empty surface elaboration registry. Registry emptyRegistry Alias for the...

fx.tc.generic: datatype-generic reflection over levitated descriptions — desc/datatype/value/derive helpers plus the algebraic/functional ornaments surface.

desc: views and folds over levitated descriptions — `descView` peels one layer, `foldDesc` recurses, `mapDesc` rewrites, predicates split by constructor.

datatype: normalise + lookup over `_dtypeMeta` — extract canonical constructor / field lists, resolve dependent field types, instantiate polymorphic parame...

value: bidirectional views over generated datatypes — `view`/`review` swap HOAS and Nix constructor records; `fold` and `mapChildren` operate generically.

derive: structured artifacts from datatype metadata — type descriptors, JSON-Schema, docs scaffolds, fold scaffolds, and node-and-edge dependency graphs.

check: canonical typed walker over the HOAS algebra — one fold at two carriers (unit for validation, HOAS for elaboration), plus refinement-guard composition.

checkD: generic bidirectional checker for Desc payloads — validates terms against `interpD level I D X i` by walking the description.

ornaments: algebraic + functional ornament constructions over generated datatypes — spec validation, fold/producer/transform lifting, and forgetful maps.

fx.tc.verified: high-level combinators for writing kernel-checked implementations; build a program, call `.verify` to type-check it against the kernel.