# Kernel Architecture


This chapter describes the type-checking kernel: its pipeline, its
primitives, and how to write verified implementations that the kernel
checks and extracts back to usable Nix functions.

## Two kernels

nix-effects combines an effects kernel with a type-checking kernel:

- The **effects kernel** (`src/kernel.nix`, `src/comp.nix`,
  `src/queue.nix`) implements the freer monad with FTCQueue. It
  defines the `Computation` ADT (`Pure a | Impure (Effect x)
  (FTCQueue x a)`) and the monadic operations `pure`, `impure`,
  `send`, `bind`, `map`, `seq`, `pipe`, `kleisli`.
- The **type-checking kernel** (`src/tc/`) implements Martin-Löf
  type theory with normalization by evaluation and bidirectional
  checking. Core modules define terms, values, evaluation, quotation,
  conversion, and checking; adjacent HOAS, elaboration, generic, and
  ornament modules provide the user-facing structure.

The type-checking kernel's higher layers use the effects kernel for
error reporting. When `check` or `infer` rejects a term, it does not
throw — it calls `send "typeError" { msg; expected; got; term; }`,
producing an `Impure` computation. Handlers in
`src/effects/typecheck.nix` (`strict`, `collecting`, and others)
interpret that request with different strategies: `strict` throws on
the first error, `collecting` accumulates errors into handler state.
The TCB (`eval`, `quote`, `conv`) never sends effects — it only
throws on kernel-invariant violations.

```
Type system API (src/types/)
  Record, ListOf, DepRecord, refined, Pi, Sigma, ...
       |
       | elaboration (src/tc/elaborate/, src/tc/hoas/)
       v
Type-checking kernel (MLTT, src/tc/)
       |
       | typeError sent as effect request
       v
Effects kernel (freer monad + FTCQueue, src/kernel.nix)
       |
       | handler (strict / collecting / ...) interprets effects
       v
Pure Nix
```

Every `fx.types` type carries a `_kernel` field — a HOAS tree that
elaborates to a kernel type. `.check` is derived from
`decide(_kernel, v)`; `.validate` wraps `decide` in a `typeCheck`
effect so handlers can do blame-annotated reporting; `.prove`
type-checks HOAS proof terms; `verifyAndExtract` runs the full
pipeline (check → eval → extract) to produce a Nix value from a HOAS
implementation. Refinement types add a `guard` predicate that runs
alongside the kernel check (`check = kernelDecide(v) ∧ guard(v)`),
handling constraints the kernel cannot express.

## The kernel pipeline

The kernel implements normalization by evaluation (NbE) with
bidirectional type checking. The core pipeline has one responsibility
per module family:

```
term.nix --> eval/ --> value.nix
                              |
                          quote.nix --> term.nix
                              |
                          conv.nix
                              |
                          check/
```

| Module | Function | Signature |
|--------|----------|-----------|
| `term.nix` | Term constructors | `mkVar`, `mkPi`, `mkLam`, `mkApp`, ... |
| `eval/` | Evaluation | `Env × Tm -> Val` |
| `value.nix` | Value constructors | `VLam`, `VPi`, `VPair`, `VMu`, ... |
| `quote.nix` | Quotation | `ℕ × Val -> Tm` |
| `conv.nix` | Conversion checking | `ℕ × Val × Val -> Bool` |
| `check/` | Type checking | `Ctx × Tm × Val -> Tm` / `Ctx × Tm -> Tm × Val` |

**Terms** (`Tm`) are the syntax — de Bruijn indexed expressions with
explicit binding structure. **Values** (`Val`) are the semantics —
fully normalized forms where lambdas carry defunctionalized closures.
The TCB does not use Nix lambdas as semantic closures. **Evaluation**
converts terms to values. **Quotation** reads values back to terms.
**Conversion** checks whether two values are definitionally equal by
comparing their semantic structure.

The type checker is bidirectional:

- `check(Γ, t, T)` — check that term `t` has type `T` (type-directed)
- `infer(Γ, t)` — infer the type of term `t` (term-directed)
- `checkTypeLevel(Γ, T)` — compute the universe level of a type

### Trust model

The kernel has three layers with decreasing trust requirements:

**Layer 0 — Trusted Computing Base.** `eval`, `quote`, `conv`. Pure
functions. No side effects. No imports from the effect system. Bugs
here compromise soundness.

**Layer 1 — Semi-trusted.** `check`, `infer`, `checkTypeLevel`. Uses
the TCB and sends effects for error reporting. Bugs may produce wrong
error messages or reject valid terms, but cannot cause unsoundness.

**Layer 2 — Untrusted.** The elaborator (`hoas/`, `elaborate/`).
Translates surface syntax to core terms. Can have arbitrary bugs
without compromising safety — the kernel verifies the output.

## Axiomatized primitives

The kernel understands eight Nix primitive types as axioms. Each has a
type former, a literal constructor, and a typing rule. None have
eliminators — the kernel says "String is a type at level 0" and "a
string literal inhabits String" but cannot structurally decompose
these values.

| Nix type | Kernel type | Literal | Level |
|----------|-------------|---------|-------|
| `string` | `String` | `StringLit(s)` | 0 |
| `int` | `Int` | `IntLit(n)` | 0 |
| `float` | `Float` | `FloatLit(f)` | 0 |
| `set` | `Attrs` | `AttrsLit` | 0 |
| `path` | `Path` | `PathLit` | 0 |
| `derivation` | `Derivation` | `DerivationLit` | 0 |
| `lambda` | `Function` | `FnLit` | 0 |
| (any) | `Any` | `AnyLit` | 0 |

`Path` is decided by `builtins.isPath`; `Derivation` is decided by
`(v: builtins.isAttrs v && (v.type or null) == "derivation")`. The two
share no values: `Path` rejects attrsets, `Derivation` rejects strings
and non-derivation attrsets.

The structural type formers with kernel introduction and elimination
rules are `Unit`, `Sigma`, `Pi`, bootstrap identity/coproduct
infrastructure, propositional truncation (`Squash`), universe lifting,
function extensionality as an axiom, and the indexed-description family
(`Desc I`, `μ`, `interpD`, `allD`, `everywhereD`, `desc-ind`). Public
`Nat`, `List`, `Sum`, `Bool`, `Eq`, `Fin`, `Vec`, and `W` are generated
through descriptions and the datatype macro. Their eliminators are
generated adapters over `desc-ind`.

This gives the kernel enough structure to compute with generated
inductive families, pairs, and functions, while treating strings,
integers, and other Nix-native types as opaque tokens.

Axiomatized primitives are critical for real-world use. Without them,
verified modules can only work over `Nat`/`Bool`/`List`/`Sigma`/`Sum`.
With them, modules can handle target classes (`String`), dependency
counts (`Int`), declaration records (nested `Sigma`/`Attrs`), and so on.

## HOAS: the surface API

Writing de Bruijn indexed terms by hand is error-prone. The HOAS
(Higher-Order Abstract Syntax) layer lets you use Nix lambdas for
variable binding. The public API is `fx.types.hoas`.

### Type combinators

```nix
H = fx.types.hoas;

H.nat                         # Nat
H.bool                        # Bool
H.string                      # String
H.int_                        # Int
H.float_                      # Float
H.unit                        # Unit (nullary product)
H.void                        # Void (empty type)
H.listOf H.nat                # List Nat
H.sum H.nat H.bool            # Nat + Bool
H.forall "x" H.nat (_: H.bool)  # Π(x : Nat). Bool
H.sigma "x" H.nat (_: H.bool)   # Σ(x : Nat). Bool
H.u 0                         # U₀ (universe of small types)
```

### Term combinators

```nix
# Lambda: λ(x : Nat). x
H.lam "x" H.nat (x: x)

# Application
H.app f arg

# Natural number literals
H.zero                        # 0
H.succ H.zero                 # 1
H.natLit 42                   # 42 (sugar for 42 succs)

# Boolean literals
H.true_
H.false_

# Pairs
H.pair fst snd

# Projections
H.fst_ p
H.snd_ p

# Sum injections
H.inl leftTy rightTy term
H.inr leftTy rightTy term

# String / Int / Float literals
H.stringLit "hello"
H.intLit 42
H.floatLit 3.14

# Type annotation
H.ann term type
```

### Eliminators

```nix
# Natural number induction
H.ind motive base step scrut

# Boolean elimination (k : Level is the motive's universe level)
H.boolElim k motive onTrue onFalse scrut

# List elimination
H.listElim elemType motive onNil onCons scrut

# Sum elimination
H.sumElim leftTy rightTy motive onLeft onRight scrut

# Equality elimination (J)
H.j type lhs motive base rhs eq
```

### How HOAS compiles

Binding combinators produce HOAS markers — lightweight attrsets that
stand for bound variables at a specific depth. The `elaborate`
function (in `hoas.nix`) converts these to de Bruijn indexed `Tm`
terms:

```
H.lam "x" H.nat (x: H.succ x)
  │
  │ HOAS: x is a marker { _hoas = true; level = 0; }
  │
  ▼ elaborate (depth=0)
  │
  │ marker at level 0 -> T.mkVar(0 - 0 - 1) = T.mkVar(0)
  │
  ▼
Lam("x", Nat, Succ(Var(0)))   ← de Bruijn term
```

The elaboration of nested binding forms is trampolined via
`builtins.genericClosure` for stack safety on deeply nested terms.

## The elaboration bridge

The elaboration bridge (`elaborate.nix`) connects the user-facing type
system to the kernel. It has six operations:

| Operation | Signature | Direction |
|-----------|-----------|-----------|
| `elaborateType` | `FxType -> HoasTree` | type system -> kernel |
| `elaborateValue` | `HoasTree × NixVal -> HoasTree` | Nix value -> kernel term |
| `extract` | `HoasTree × Val -> NixValue` | kernel value -> Nix value |
| `decide` | `HoasTree × NixVal -> Bool` | decision procedure |
| `decideType` | `FxType × NixVal -> Bool` | elaborate type, then decide |
| `verifyAndExtract` | `HoasTree × HoasTree -> NixValue` | full pipeline |

### elaborateType

Converts an `fx.types` type into a HOAS tree. Dispatches on three
things, in order:

1. The `_kernel` field (types built via `mkType` with `kernelType`)
2. Structural fields (Pi: `domain`/`codomain`, Sigma: `fstType`/`sndFamily`)
3. Name convention (`"Bool"` -> `H.bool`, `"String"` -> `H.string`, etc.)

### elaborateValue

Converts a Nix value into a HOAS term, guided by a HOAS type. For
example, given `H.nat` and the Nix integer `3`, produces
`H.succ (H.succ (H.succ H.zero))`. Given `H.string` and `"hello"`,
produces `H.stringLit "hello"`.

### extract — the reverse direction

`extract` converts kernel values back to Nix values. It is the reverse
of `elaborateValue`. This is where the verification story becomes
interesting: you write an implementation as a HOAS term, the kernel
verifies it, `eval` produces a kernel value, and `extract` converts
the result to a usable Nix value.

```nix
# extract : HoasTree -> Val -> NixValue
extract H.nat (VDescCon ... <succ payload>)        # -> 2
extract H.bool (VDescCon ... <true payload>)       # -> true
                                                     # H.bool is derived
extract H.string (VStringLit "hi")                 # -> "hi"
extract (H.listOf H.nat) (VDescCon ... <cons ...>) # -> [1 2 3]
extract (H.forall "x" ...) (VLam ...)              # -> Nix function (!)
```

The Pi case is the most important. Extracting a verified function
produces a Nix function that:

1. Elaborates its argument into a kernel value (Nix -> kernel)
2. Applies the kernel-verified closure
3. Extracts the result back (kernel -> Nix)

Correct by construction — the kernel verified the term, `eval`
produced the closure, `extract` wraps with value conversion at the
boundaries.

### decide

The decision procedure. Returns `true` iff both elaboration and
kernel type-checking succeed:

```nix
decide = hoasTy: value:
  let
    result = builtins.tryEval (
      let
        hoasVal = elaborateValue hoasTy value;
        checked = H.checkHoas hoasTy hoasVal;
      in !(checked ? error)
    );
  in result.success && result.value;
```

This is the function that `mkType` uses to derive `.check`. Every
type's `.check` is `v: decide(kernelType, v)` — no hand-written
predicates.

### verifyAndExtract — the full pipeline

Type-check a HOAS term against a HOAS type, then extract the result:

```nix
verifyAndExtract = hoasTy: hoasImpl:
  let
    checked = H.checkHoas hoasTy hoasImpl;
  in if checked ? error
    then throw "verifyAndExtract: type check failed"
    else
      let
        tm = H.elab hoasImpl;         # HOAS -> de Bruijn
        val = E.eval [] tm;           # evaluate to Val
      in extract hoasTy val;          # Val -> Nix value
```

## Convenience combinators

Raw HOAS is verbose. The convenience combinator layer (`fx.types.verified`,
accessed as `v`) provides sugar that produces valid HOAS term trees:

```nix
v = fx.types.verified;
H = fx.types.hoas;
```

### Literals

```nix
v.nat 5          # H.natLit 5
v.str "hello"    # H.stringLit "hello"
v.int_ 42        # H.intLit 42
v.float_ 3.14    # H.floatLit 3.14
v.true_          # H.true_
v.false_         # H.false_
v.null_          # H.tt (unit)
```

### Binding forms

```nix
# Lambda: λ(x : Nat). body
v.fn "x" H.nat (x: body)

# Let: let x : Nat = 5 in body
v.let_ "x" H.nat (v.nat 5) (x: body)
```

### Eliminators with inferred motives

The convenience combinators construct the required motive automatically
from the result type. The motive is always constant (non-dependent):
`λ_. resultTy`.

```nix
# Boolean: if b then 1 else 0
v.if_ H.nat v.true_ { then_ = v.nat 1; else_ = v.nat 0; }

# Natural number: pattern match on n
v.match H.nat n {
  zero = v.nat 42;
  succ = k: ih: H.succ ih;
}

# List: fold over elements
v.matchList H.nat H.nat list {
  nil = v.nat 0;
  cons = h: t: ih: H.succ ih;   # count elements
}

# Sum: case split
v.matchSum H.nat H.bool H.nat scrut {
  left = x: H.succ x;
  right = _: v.nat 0;
}
```

### Derived combinators

```nix
# Map: apply f to each element
v.map H.nat H.nat succFn myList

# Fold: combine elements with accumulator
v.fold H.nat H.nat (v.nat 0) addFn myList

# Filter: keep elements matching predicate
v.filter H.nat isZeroFn myList
```

### Pairs and sums

```nix
v.pair fstTerm sndTerm sigmaType
v.fst p
v.snd p
v.inl leftTy rightTy term
v.inr leftTy rightTy term
v.app f arg
```

### The verify pipeline

`v.verify` wraps `verifyAndExtract` — type-check and extract in one
call:

```nix
v.verify type implementation
# = verifyAndExtract type implementation
```

## Writing verified implementations

The key insight: instead of writing Nix functions and trying to
elaborate them into kernel terms (which fails for closures), write
implementations as HOAS terms and **extract** Nix functions out. This
is the approach taken by Coq (extraction), Idris (compilation), and
F\*.

### Example: verified addition

```nix
let
  H = fx.types.hoas;
  v = fx.types.verified;

  addTy = H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat));
  addImpl = v.fn "m" H.nat (m: v.fn "n" H.nat (n:
    v.match H.nat m {
      zero = n;
      succ = _k: ih: H.succ ih;
    }));

  # Kernel verifies: addImpl : Π(m:Nat). Π(n:Nat). Nat
  # Then extracts a 2-argument Nix function
  add = v.verify addTy addImpl;
in
  add 2 3    # -> 5
```

What happens step by step:

1. `v.verify` calls `H.checkHoas addTy addImpl` — the kernel
   type-checks the HOAS term against the HOAS type
2. `H.elab addImpl` converts HOAS to de Bruijn indexed `Tm`
3. `E.eval [] tm` evaluates to a `VLam` value (a Nix closure via NbE)
4. `extract addTy val` wraps the `VLam` as a Nix function that
   elaborates arguments at call boundaries

The resulting `add` is an ordinary Nix function. Call it with Nix
integers. At each call, the argument is elaborated into a kernel
value, the verified closure runs, and the result is extracted back.

### Example: verified list operations

```nix
let
  H = fx.types.hoas;
  v = fx.types.verified;

  # Successor function: Nat -> Nat
  succFn = v.fn "x" H.nat (x: H.succ x);

  # Map successor over a list
  input = H.cons H.nat (v.nat 0)
    (H.cons H.nat (v.nat 1)
      (H.cons H.nat (v.nat 2) (H.nil H.nat)));

  result = v.verify (H.listOf H.nat) (v.map H.nat H.nat succFn input);
in
  result    # -> [1 2 3]
```

### Example: verified filter

```nix
let
  H = fx.types.hoas;
  v = fx.types.verified;

  # isZero : Nat -> Bool
  isZero = v.fn "n" H.nat (n:
    v.match H.bool n {
      zero = v.true_;
      succ = _k: _ih: v.false_;
    });

  input = H.cons H.nat (v.nat 0)
    (H.cons H.nat (v.nat 1)
      (H.cons H.nat (v.nat 0)
        (H.cons H.nat (v.nat 2) (H.nil H.nat))));

  result = v.verify (H.listOf H.nat) (v.filter H.nat isZero input);
in
  result    # -> [0 0]
```

## The verification spectrum

The architecture supports a spectrum of assurance levels. Each level
offers a different trade-off between verification strength and
implementation cost.

### Level 1: Contract

The baseline. Types check values at introduction via `.check` (which
calls `decide` under the hood). No HOAS, no proof terms — just write
normal Nix code and let the type system validate data at boundaries.

```nix
let
  inherit (fx.types) String refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  # Refinement with string guard — kernel checks String, guard checks membership
  LogLevel = refined "LogLevel" String
    (x: builtins.elem x [ "debug" "info" "warn" "error" ]);
in {
  module = TargetClass.check "module"; # true
  fleet = TargetClass.check "fleet"; # false

  info  = LogLevel.check "info";    # true
  trace = LogLevel.check "trace";   # false — not in the allowed set

  # Effectful validation with blame context
  result = fx.run (TargetClass.validate "fleet")
    fx.effects.typecheck.collecting [];
  # result.state = [ { context = "TargetClass"; ... } ]
}
```

**Cost:** Zero — write normal Nix. The kernel runs behind the scenes.
Refinement types compose: `ListOf TargetClass` checks that every element
is a known renderer class. The kernel elaborates the list, the guard
runs per element.

### Level 2: Boundary

Data values are checked by the kernel at module interfaces. Types
carry `kernelType` and `.check` is derived from the kernel's `decide`
procedure. This is what every type does by default.

```nix
let
  inherit (fx.types) Bool String ListOf DepRecord refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  # Dependent record: generated aspects must target a known renderer class.
  # The kernel elaborates the record to a Sigma chain, checks each field's type
  # against its kernelType, and the guard on TargetClass validates membership.
  AspectDecl = DepRecord [
    { name = "generated"; type = Bool; }
    { name = "target"; type = self:
        if self.generated then TargetClass else String; }
    { name = "requires"; type = _: ListOf String; }
  ];
in {
  ok = AspectDecl.checkFlat {
    generated = true;
    target = "module";
    requires = [ "toolchain" ];
  };   # true

  bad = AspectDecl.checkFlat {
    generated = true;
    target = "fleet";
    requires = [ ];
  };   # false

  external = AspectDecl.checkFlat {
    generated = false;
    target = "external-renderer";
    requires = [ ];
  };   # true
}
```

**Cost:** Low — add `kernelType` to custom types (built-in types
already have it). The dependent record pattern shows how boundary
checking scales: the kernel handles structural verification, guards
handle domain predicates, and the dependency between fields is
resolved at check time.

### Level 3: Property

Universal properties verified via proof terms. Write proofs in HOAS
that the kernel checks. The proof term is separate from the
implementation — you write separate Nix code alongside, and the
kernel verifies that the stated property holds.

```nix
let
  H = fx.types.hoas;
  inherit (H) nat bool eq forall refl checkHoas;

  # Define addition by structural recursion on the first argument
  add = m: n:
    H.ind (H.lam "_" nat (_: nat)) n
      (H.lam "k" nat (_: H.lam "ih" nat (ih: H.succ ih))) m;

  not_ = b:
    H.boolElim 0 (H.lam "_" bool (_: bool)) H.false_ H.true_ b;
in {
  # Prove: 3 + 5 = 8
  # The kernel normalizes add(3,5) via generated natural induction,
  # then confirms Refl witnesses Eq(Nat, 8, 8).
  arithmetic = (checkHoas
    (eq nat (add (H.natLit 3) (H.natLit 5)) (H.natLit 8))
    refl).tag == "refl";

  # Prove: not(not(true)) = true
  # The kernel evaluates two BoolElim steps and confirms the result.
  doubleNeg = (checkHoas
    (eq bool (not_ (not_ H.true_)) H.true_)
    refl).tag == "refl";

  # Prove: append([1,2], [3]) = [1,2,3]
  # Generated list induction unfolds the first list onto [3].
  listAppend = let
    list12  = H.cons nat (H.natLit 1) (H.cons nat (H.natLit 2) (H.nil nat));
    list3   = H.cons nat (H.natLit 3) (H.nil nat);
    list123 = H.cons nat (H.natLit 1) (H.cons nat (H.natLit 2)
                (H.cons nat (H.natLit 3) (H.nil nat)));
    append = xs: ys:
      H.listElim nat (H.lam "_" (H.listOf nat) (_: H.listOf nat)) ys
        (H.lam "h" nat (h: H.lam "t" (H.listOf nat) (_:
          H.lam "ih" (H.listOf nat) (ih: H.cons nat h ih)))) xs;
  in (checkHoas (eq (H.listOf nat) (append list12 list3) list123) refl).tag == "refl";
}
```

**Cost:** Medium — write proofs in HOAS. The proofs are separate from
production code, so you can add them incrementally to an existing
codebase without rewriting anything.

### Level 4: Full

The implementation IS the proof term. Write the entire implementation
in HOAS, the kernel verifies it, and `extract` produces a Nix
function that is correct by construction. The extracted function is
plain Nix — no kernel overhead at call time.

```nix
let
  H = fx.types.hoas;
  v = fx.types.verified;

  AspectDecl = H.record [
    { name = "name";     type = H.string; }
    { name = "target";   type = H.string; }
    { name = "requires"; type = H.listOf H.string; }
  ];

  targets =
    H.cons H.string (v.str "module")
      (H.cons H.string (v.str "file")
        (H.cons H.string (v.str "package")
          (H.cons H.string (v.str "check") (H.nil H.string))));

  # Verified aspect validator: checks that the target class is supported.
  # The kernel type-checks the implementation against AspectDecl -> Bool,
  # verifies field projections, and confirms strElem composes correctly.
  validateAspect = v.verify (H.forall "a" AspectDecl (_: H.bool))
    (v.fn "a" AspectDecl (a:
      v.strElem (v.field AspectDecl "target" a) targets));

  # Verified addition: structural recursion extracted as Nix function
  add = v.verify (H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat)))
    (v.fn "m" H.nat (m: v.fn "n" H.nat (n:
      v.match H.nat m {
        zero = n;
        succ = _k: ih: H.succ ih;
      })));
in {
  sum   = add 2 3;    # -> 5, correct by construction
  ok    = validateAspect {
    name = "workspace-shell";
    target = "module";
    requires = [ "toolchain" ];
  };   # -> true
  bad   = validateAspect {
    name = "workspace-aspect";
    target = "fleet";
    requires = [ ];
  };   # -> false
}
```

**Cost:** High — write the implementation in HOAS. Best reserved for
code where the cost is justified by the assurance. See the
[Proof Guide](/nix-effects/guide/proof-guide) for a progressive
tutorial from simple proofs through the J eliminator to verified
extraction of plain Nix functions.

## How mkType derives .check

Every type is built by `mkType` (in `foundation.nix`). The kernel
type IS the type. `.check` is its decision procedure, derived
mechanically:

```
_kernel : HoasType        ← the type IS this
check : Value -> Bool       ← derived from decide(kernelType, value)
kernelCheck : Value -> Bool ← same as check (legacy alias)
prove : HoasTerm -> Bool    ← kernel proof checking
universe : Int             ← computed from checkTypeLevel(kernelType)
```

For refinement types, an optional `guard` adds a runtime predicate
on top of the kernel check: `check = decide(kernelType, v) && guard(v)`.
The guard handles predicates the kernel cannot express — for example,
`x >= 0` for natural numbers, or membership in a finite set for
validated strings.

## Limitations

**Nix closures are opaque.** `decide(H.forall ..., f)` can only
check `builtins.isFunction f`. For full function verification, write
the function in HOAS and use `v.verify` to extract.

**Refinement predicates are opaque.** The kernel cannot represent
`x >= 0` as a type-level assertion. Refinement types always need a
hand-written guard predicate.

**`builtins.tryEval` is limited.** It only catches `throw` and
`assert false`. Cross-type comparison errors, boolean coercion errors,
and missing attribute access crash Nix uncatchably. This affects
`decide` for types whose elaboration might trigger such errors.

**Dependent extraction is limited.** Extracting a dependent Pi or
Sigma requires a sentinel test to detect non-dependence. If the
type family is truly dependent, extraction throws and requires
explicit type annotation.

**Opaque types cannot be extracted.** `Attrs`, `Path`, `Derivation`,
`Function`, and `Any` are axiomatized — the kernel knows they exist
but discards their payloads. Extracting a value of these types throws.
They work for type-checking (deciding membership) but not for the full
verify-and-extract pipeline.

**Extraction has boundary cost.** Extracted functions elaborate their
arguments at every call (Nix -> kernel value -> apply -> extract -> Nix).
For hot paths, the contract layer's `.check` fast path is more
efficient.