# Kernel


Kernel-internal `validate` for the internalizable fragment of
`mkType`-buildable types. A code is a base carrier type (any `U_0`
type — a mu-encoded inductive or a primitive) paired with a finite
stack of predicates over that carrier; the decider is the conjunction
of the stack.

## Surface (`ktype`)

- `KType : U_1` — a base carrier type paired with a predicate stack
- `beta t : U_0` — the base carrier of a code (constant along refinement)
- `psi t : beta t -> Bool` — the accumulated membership predicate
- `El t` — the derived refinement subtype `Sigma x:beta t. P (psi t x)`
- `P` — the `Bool -> U_0` membership decoder (`P true ~> Unit`, `P false ~> Void`)
- `betaFn`/`decideFn`/`ElFn` — the same functions as closed kernel terms
- `andB`, `iota`/`refine` constructor helpers

## Decision (`decide`)

- `decide t : beta t -> Bool` — membership in `El t`; `decide = psi`

## `decide`

_fx.tc.kernel.decide: the membership decision procedure decide = psi : (t:KType) -> beta t -> Bool._

## `failure`

_fx.tc.kernel.failure: the kernel transcription of the diagnostic Error ADT (DiagError — a mono-constructor record over Layer/Detail/msg/hint and an opaque Unit children slot) and the Failure of a rejected check as a dependent Sigma-chain (FailureTy = Sigma ktp:KType. Sigma x:(beta ktp). Sigma ctx. Sigma rsn. Sigma pth. DiagError; FailureTheory the base-only Sigma). Layer/Detail sub-shapes, the layerOf/detailOf/mkDiag/mkFailure constructors, the fst_/snd_-spine Failure projections, and the named DiagError field projections._

## `handlers`

_fx.tc.kernel.handlers: the six typecheck-policy handlers (strict/collecting/logging/firstN/summarize/pretty) as closed kernel step terms folding a stream of membership decisions into accumulated state. A decision is a host-known boolean `passed` plus an opaque host-rendered residue Rec; each step is `... -> Σ State payload` whose reduction is the state transition. firstN carries an O(1) down-counter; summarize renders the reason enum to its production key token via `reasonName` and groups failures into a `List (Σ String Nat)` assoc list via `insertOrIncrement` (a `listElim`+`strEq` fold). Exports the step terms, their result shapes, and the Reason/assoc grouping vocabulary._

## `ktype`

_fx.tc.kernel.ktype: flat predicate-stack datum — KType : U_1 (a base carrier type paired with a predicate stack over it), beta (the carrier), the accumulator-fold decider psi/decide, derived El, the membership decoder P, andB, and the iota/refine constructors._

## `reflect`

_fx.tc.kernel.reflect: reflect a Nix-side carrier type into its KType code (reflect/reflectRefine), the checkable Boolean predicate vocabulary for refinement arms — Int over the primitive carrier via the host-backed intLe/intEq (positiveInt, nonNegativeInt, inRangeInt, eqInt) and String literal-set membership (oneOfStrTerm, via strEq) plus non-emptiness (strNonEmptyTerm, via strLen) — and the KernelPred witness layer (mkKernelPred, andKP, isKernelPred, sealed, kernelExpressible, ktypeOf, deriveGuard) with ready-made witnesses: Int (intPositive, intNonNegative, intInRange, intEq) and String (strOneOf, strNonEmpty), O(1)-bridged and guard-derived from their kernel terms._

## `validate`

_fx.tc.kernel.validate: the membership-decision arm of typechecking. validateClosed t v context reason path diagError decides membership with the kernel oracle (elaborate.decide) and either returns `pure v` or raises the host `typeCheck` effect with the caller-supplied diagnostics — the closed-input generalization of the auto-derived validateAt. validateK R t reason path carrier x is the kernel-internal report producer: it emits one kernel `report` op whose decision is the KType decider applied to the carrier (`decide t x`), returning `freeFx (EffTypeCheck R) Resp Unit` for the kernel handlers to fold. validateEl R t payload x is the kernel-internal certifier — the membership-witness dual of validateK: it produces the dependent witness `El t` when `decide t x` accepts, and otherwise aborts on EffError's strict (Void-response) raise carrying the opaque payload, so no witness is ever forged; returns `freeFx (EffError R) Resp_strict (El t)`._

## Source

- [`src/tc/kernel/decide.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/decide.nix)
- [`src/tc/kernel/failure.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/failure.nix)
- [`src/tc/kernel/flat-faithfulness.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/flat-faithfulness.nix)
- [`src/tc/kernel/handlers.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/handlers.nix)
- [`src/tc/kernel/ktype.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/ktype.nix)
- [`src/tc/kernel/level-soundness.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/level-soundness.nix)
- [`src/tc/kernel/reflect.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/reflect.nix)
- [`src/tc/kernel/soundness.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/soundness.nix)
- [`src/tc/kernel/validate.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/kernel/validate.nix)