# Check


The single polymorphic fold over the full HOAS type algebra,
parameterised by an `Algebra A`. Two canonical algebras live
alongside it: `unitAlg` returns `null` at every node and is
used for validation (the walker emits `typeCheck` effects on
failure); `hoasAlg` constructs the corresponding HOAS term at
every node and is used for elaboration. Validation and
elaboration are not two functors — they are one fold
instantiated at two carriers.

`deriveCheck` and `deriveElaborate` thread `unitAlg` /
`hoasAlg` respectively. Both accept `(ty, path, value)` and
return a `Computation A`; the walker owns shape inspection,
`_htag` dispatch, `fx.kernel` effect emissions, path
threading, and the dependent-Σ snd-type derivation via an
internal strict-handler trampoline on fst. Algebras own
per-shape success-case construction and the field-walker (so
`unitAlg` matches the legacy `f.type`-only traversal while
`hoasAlg` threads `prev` through `fieldType` for
dependent-field resolution).

`checkWithGuard` composes `deriveCheck` with a refinement
predicate: shape-check via the unit walker first, predicate
second (the two cannot run in parallel — the predicate's
domain is exactly the values that pass shape). When the
eventual Σ-with-Decide-snd encoding lands, this special case
collapses into `deriveCheck` over Σ-types and the helper
deletes.

Failure reasons carry one of `shape-mismatch`, `missing-field`,
`extra-field`, `predicate-failed`, or `deferred-pi`, routed by
handlers under `fx.effects.typecheck.*`.

## `checkWithGuard`

_checkWithGuard: refinement-predicate-aware variant of `deriveCheck` — runs shape check first via `unitAlg`, then composes the type's refinement predicate when present; required while refined types are encoded outside the canonical Σ-with-Decide-snd form._

```
checkWithGuard : Type -> Path -> Value -> Computation Null
```

## `deriveCheck`

_deriveCheck: canonical typed walker over the HOAS algebra threading `unitAlg` — emits `fx.effects.typecheck` failures with structured `reason` (shape-mismatch, missing-field, extra-field, predicate-failed, deferred-pi) and `path` (a `fx.diag.positions` chain)._

```
deriveCheck : Type -> Path -> Value -> Computation Null
```

## `deriveElaborate`

_deriveElaborate: canonical typed walker over the HOAS algebra threading `hoasAlg` — reconstructs the corresponding HOAS term at every successfully-checked node; shares path threading and dispatch with `deriveCheck`._

```
deriveElaborate : Type -> Path -> Value -> Computation Hoas
```