# 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`

_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:

1. `_kernel` annotation: returned directly. This is the
   authoritative path for types built via `mkType` with an
   explicit `kernelType` (covers refinement, dependent, linear,
   levitated descriptions).
2. 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.
3. 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. Evaluates the term returned by
`checkHoas` — not a fresh elaboration of the impl — so the
extracted value is the one that was verified, with all metas
(e.g. a polymorphic list's element type, solved only by
checking against the expected type) already pinned. The kernel
type value is the direct elaboration of `hoasTy`; `extractInner`
reads descriptions through `descView`, which treats primitive
and encoded shapes uniformly, so the type's representation need
not match the checked term's.

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.

## Sub-namespaces

- [`_internal`](/nix-effects/type-checker/elaborate/_internal)
- [`meta`](/nix-effects/type-checker/elaborate/meta)

## Source

- [`src/tc/elaborate/check.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/check.nix)
- [`src/tc/elaborate/conv.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/conv.nix)
- [`src/tc/elaborate/core.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/core.nix)
- [`src/tc/elaborate/effects.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/effects.nix)
- [`src/tc/elaborate/eval-overlay.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/eval-overlay.nix)
- [`src/tc/elaborate/extract.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/extract.nix)
- [`src/tc/elaborate/infer.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/infer.nix)
- [`src/tc/elaborate/insertion.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/insertion.nix)
- [`src/tc/elaborate/meta-core.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta-core.nix)
- [`src/tc/elaborate/quote.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/quote.nix)
- [`src/tc/elaborate/runElab.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/runElab.nix)
- [`src/tc/elaborate/value.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/value.nix)