Elaborate

Bridges the fx.types layer to the kernel's term representation via the HOAS combinator layer. Provides the Nix ↔ kernel boundary.

Type Elaboration

elaborateType : FxType → Hoas — convert an fx.types type descriptor to an HOAS tree. Dispatches on: (1) _kernel annotation, (2) structural fields (Pi: domain/codomain, Sigma: fstType/sndFamily), (3) name convention (Bool, Nat, String, Int, Float, ...). Dependent Pi/Sigma require explicit _kernel annotation.

Value Elaboration

elaborateValue : Hoas → NixVal → Hoas — convert a Nix value to an HOAS term tree given its HOAS type. Bool→true/false, Int→natLit, List→cons chain, Sum→inl/inr, Sigma→pair. Trampolined for large lists.

Structural Validation

validateValue : Path → Hoas → NixVal → [{ type; context; value; path; reason; }] — collecting-handler bridge over fx.tc.generic.check.deriveCheck. Accumulates every typeCheck effect emission from the canonical structural validator into a list of typed error records carrying structured Path (Position-list) descents to each failure site. Empty list ↔ elaborateValue would succeed (soundness invariant).

Value Extraction

extract : Hoas → Val → NixValue — reverse of elaborateValue. Converts kernel values back to Nix values. Generated Nat/List VDescCon chains become Nix ints/lists; generated sums become tagged unions. Pi extraction wraps the VLam as a Nix function with boundary conversion. Opaque types (Attrs, Path, Function, Any) throw — kernel discards payloads.
extractInner : Hoas → Val → Val → NixValue — three-argument extraction with kernel type value threading. Supports dependent Pi/Sigma via closure instantiation instead of sentinel tests.
reifyType : Val → Hoas — converts a kernel type value back to HOAS. Fallback for when HOAS body application fails (dependent types). Loses sugar (VSigma→sigma, not record).

Decision Procedure

decide : Hoas → NixVal → Bool — returns true iff elaboration and kernel type-checking both succeed. Uses tryEval for safety.
decideType : FxType → NixVal → Bool — elaborate type then decide.

Full Pipeline

verifyAndExtract : Hoas → Hoas → NixValue — type-check an HOAS implementation against an HOAS type, evaluate, extract to Nix value. Throws on type error.

Value Embedding

embedVal : Val → Hoas — lift a kernel value back into HOAS. quote 0 reads the value to a closed Tm; H.embedTm wraps it via the pre-elab rule. Use when a Val produced by kernel evaluation (e.g. an effect handler's response) needs to flow into a surrounding HOAS expression that is itself about to be elaborated and re-evaluated.

`decide`

decide: boolean decision procedure — returns true iff elaborateValue succeeds and the kernel type-checker accepts the resulting HOAS value; tryEval catches all elaboration throws.

decide : Hoas -> NixVal -> Bool

`decideType`

decideType: decide lifted to fx.types descriptors — runs elaborateType then decide. Convenience for users working with fx.types rather than raw HOAS types.

decideType : FxType -> NixVal -> Bool

elaborateType: convert an fx.types type descriptor to an HOAS type tree — dispatches on _kernel annotation, structural fields (Pi: domain/codomain, Sigma: fstType/sndFamily), then name convention (Bool, Nat, Unit, ...). Dependent Pi/Sigma require explicit _kernel.

elaborateType : FxType -> Hoas

Three dispatch tiers, tried in order:

_kernel annotation: returned directly. This is the authoritative path for types built via mkType with an explicit kernelType (covers refinement, dependent, linear, levitated descriptions).
Structural fields: Pi { domain, codomain, checkAt } → H.forall; Sigma { fstType, sndFamily, proj1 } → H.sigma. Only non-dependent families (constant-codomain / constant-sndFamily) are accepted at this tier — dependent families throw and demand the _kernel path.
Name convention: primitives (Bool, Nat, Unit, Null, String, Int, Float, Attrs, Path, Function, Any) map to their HOAS prelude entries.

Unknown types throw with a message directing the author to add _kernel. Cross-ref: elaborateValue for the dual on values, decideType for the boolean pipeline.

`elaborateValue`

elaborateValue: strict-handler bridge over fx.tc.generic.check.deriveElaborate — produces the HOAS term that witnesses the value's typing, throwing on the first shape mismatch (catchable by tryEval).

elaborateValue : Hoas -> NixVal -> Hoas

Composes the canonical structural walker fx.tc.generic.check.deriveElaborate with the strict handler from fx.effects.typecheck.strict. The walker is the same fold as validateValue instantiated at carrier Hoas; the strict handler throws on the first emitted typeCheck failure.

Per-tag construction is owned by the hoasAlg algebra inside tc/generic/check.nix: Bool → true_/false_; Nat → natLit; String/Int/Float → primitive literals; List → cons chain via an O(1)-per-step continuation accumulator; Sum → inl/inr; Sigma → pair; constructor records → prev-threaded H.app chain via D.fieldType (typeFn-aware for dependent fields).

Fails fast on the first shape mismatch via builtins.throw. Soundness invariant: validateValue [] hoasTy v is [] iff elaborateValue hoasTy v does not throw on the same input.

`embedVal`

embedVal: Val-to-HOAS lift — embedVal v reflects a closed kernel Val into HOAS via H.litVal; the elaborator emits T.mkLitVal and eval returns the value verbatim. O(1) regardless of value depth.

embedVal : Val -> Hoas

Use when a kernel value needs to flow into a surrounding HOAS expression that will be re-elaborated and re-evaluated. The canonical example is an effect handler's response handed to a user continuation: the continuation receives a Val but wants to build further HOAS like H.app H.succ response for the next program fragment. Without the lift, H.elab recurses into the Val (which lacks _htag) and throws.

Soundness: the splice rule eval ρ (LitVal v) = v discards the environment, so v must be closed (no free de Bruijn levels). The bridge guarantees this — values reaching the embed site are evaluation results of closed handler programs.

Cost: O(1). The prior H.embedTm (quote 0 v) composition walked v structurally each call, producing quadratic blow-up in iterative bridge use (a chain of N bind get (n: …embedVal n…) steps quoted progressively deeper state Vals).

Reference: two-level type theory splice (Kovács, "Staged Compilation with Two-Level Type Theory", POPL 2024; Annenkov–Capriotti–Kraus–Sattler 2019).

`evalOverlay`

evalOverlay: default-fuel wrapper around evalOverlayF.

evalOverlay : Env -> Tm -> ElabVal

`evalOverlayF`

evalOverlayF fuel env tm: meta-aware kernel-term evaluator. Substitute for evalF at sites that may evaluate closure bodies whose environment contains VMeta values.

evalOverlayF : Fuel -> Env -> Tm -> ElabVal

`extract`

extract: kernel-value to Nix-value extraction — reverse of elaborateValue; computes the kernel type from the HOAS type once, then delegates to extractInner for the recursive walk with kernel type-value threading.

extract : Hoas -> Val -> NixValue

`extractInner`

extractInner: three-argument kernel value extraction — takes an HOAS type (for dispatch and sugar), a kernel type value (for dependent codomain/snd computation), and the kernel value to extract.

extractInner : Hoas -> Val -> Val -> NixValue

Inner workhorse for fx.tc.elaborate.extract. Threads the kernel type value alongside the HOAS form so dependent Pi / Sigma codomains can be instantiated through closure application rather than sentinel-test heuristics. The Pi branch wraps Nix arguments via self.elaborateValue before feeding them back into the kernel; the mutual recursion closes through self.

Decoding strategy varies by type tag: Nat / List / Sum generated shapes are walked via VDescCon-chain decomposition (trampolined via genericClosure for stack safety on deep values); Pi extraction wraps a VLam as a Nix function with boundary conversion; opaque types (Attrs, Path, Function, Any) throw because the kernel discards their payloads.

`instantiateOverlay`

instantiateOverlay: default-fuel wrapper around instantiateOverlayF.

instantiateOverlay : Closure -> ElabVal -> ElabVal

`instantiateOverlayF`

instantiateOverlayF fuel cl arg: meta-aware closure instantiation. Where kernel instantiateF crashes when the closure environment contains a VMeta (kernel vAppF reads .tag which VMeta lacks), this overlay routes app/elim dispatch through VMeta-aware variants and threads overlay evaluation transitively through closure bodies.

instantiateOverlayF : Fuel -> Closure -> ElabVal -> ElabVal

`reifyType`

reifyType: kernel-to-HOAS type rebuild — converts a kernel type Val back to an HOAS type for extract dispatch; loses sugar (VSigma → H.sigma rather than H.record).

reifyType : Val -> Hoas

Used as a fallback when the HOAS body cannot be applied (dependent-type instantiation, polymorphic app-spine reduction). The HOAS body is preferred when available since it preserves record/variant/maybe structure.

Generated nat / list / sum shapes reify to raw-tag HOAS attrsets rather than the module-level H.nat / H.listOf / H.sum combinators — the public combinators carry app-spines or _dtypeMeta, while raw tags dispatch directly to extractInner's decoders and avoid re-entering type reify.

`validateValue`

validateValue: collecting-handler bridge over fx.tc.generic.check.deriveCheck — accumulates every typeCheck effect emission produced by the canonical structural validator.

validateValue : Path -> Hoas -> NixVal -> [{ type; context; value; path; reason; }]

Composes the canonical structural validator fx.tc.generic.check.deriveCheck with the collecting handler from fx.effects.typecheck.collecting to accumulate every typed failure across the value tree.

The path argument is a structured Position list from fx.tc.generic.path (alias of fx.diag.positions); each emitted error record carries the descent path to its failure site under reason ∈ { shape-mismatch, missing-field, predicate-failed, deferred-pi }.

Returns [] iff elaborateValue would not throw on the same input. Use for upfront validation in build-time gates and structural diagnostics; use elaborateValue directly when only the elaborated value is needed.

`verifyAndExtract`

verifyAndExtract: full type-check + evaluate + extract pipeline — given an HOAS type and an HOAS implementation, type-check the impl against the type, evaluate to a kernel value, and extract to a Nix value; throws on type error.

verifyAndExtract : Hoas -> Hoas -> NixValue

The canonical entry point for closing a verified-impl pipeline back to ordinary Nix data. The kernel type value is computed once and reused by extractInner so dependent codomain/snd closures evaluate against the same type representation the checker consumed.

On type-check failure throws "verifyAndExtract: type check failed" — callers needing structured diagnostics should split the pipeline: H.checkHoas for the error attrset, then extract/extractInner only on success.