# Generic


Reflection over levitated descriptions and datatype macro outputs.
Datatype consumers should use this layer instead of raw `_dtypeMeta`.
Generic algebraic ornament helpers check algebra descriptors against
`generic.desc.shape`; the supported fragment is ret/arg/rec/plus.
Ornament validation exposes total structured diagnostics for expected
surface errors; semantic ornament maps remain pure over validated inputs.
Functional ornaments expose manual sections for canonical
base-to-ornamented construction; synthesis is layered on later.
The first synthesis layer accepts `{ base; spec; synth; }`, reuses the
ordinary ornament spec, and requires explicit builders for inserted fields.
Proof-marked inserted fields use `prove` or `synth.constructors.<name>.proofs`
and report unresolved proof obligations as structured diagnostics.
Declared measures feed algebraic/measure-derived inserted fields through
the synthesis builder context and produce missing-measure obligations.
Function transport lifts base producers and transforms through canonical
functional output sections while existing pullback remains forget-then-run.

## `path`

_path: list-level operations on a `[Position]` descent chain — `empty`, `extend`, `render`, `renderAll`. Position segments themselves are constructed via `fx.diag.positions` (`P.Field name`, `P.Elem i`, etc.); this module only handles the list assembly and pretty-rendering._

```
path : { empty, extend, render, renderAll }
```

Operations on a path (a list of `Position` segments naming a
structural descent from a validation root to a failure site):

- `empty = []` is the root path.
- `extend : Path -> Position -> Path` appends a segment.
- `render : Position -> String` pretty-renders one segment.
- `renderAll : Path -> String` concatenates rendered segments.

Position segments are produced by `fx.diag.positions` (the
canonical curried constructors `Field`, `Elem`, `Tag`, `Tuple`,
plus the ~30 nullary description/MLTT positions). Handlers
consume the same `Position` records regardless of whether they
come from kernel descent or value-side `verify=` walks.

## Sub-namespaces

- [`check`](/nix-effects/type-checker/generic/check)
- [`checkD`](/nix-effects/type-checker/generic/checkD)
- [`datatype`](/nix-effects/type-checker/generic/datatype)
- [`derive`](/nix-effects/type-checker/generic/derive)
- [`desc`](/nix-effects/type-checker/generic/desc)
- [`ornaments`](/nix-effects/type-checker/generic/ornaments)
- [`value`](/nix-effects/type-checker/generic/value)

## Source

- [`src/tc/generic/check.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/check.nix)
- [`src/tc/generic/checkD.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/checkD.nix)
- [`src/tc/generic/datatype.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/datatype.nix)
- [`src/tc/generic/derive.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/derive.nix)
- [`src/tc/generic/desc.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/desc.nix)
- [`src/tc/generic/ornaments.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/ornaments.nix)
- [`src/tc/generic/path.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/path.nix)
- [`src/tc/generic/value.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/generic/value.nix)