Kernel — nix-effects

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