Error

Diagnostic Error ADT.

An Error has a Layer (Kernel | Generic | Contract), a layer-discriminated Detail record, a short msg, an optional hint, and a list of children. A leaf has children = []; a branch has a non-empty children list whose entries are { position, error } pairs. Sibling failures produce many children; a chained descent produces one child; a leaf has none.

Constructors: mkKernelError { position?, rule, msg, expected?, got?, ctx_depth?, hint? } mkGenericError { type?, context?, value, desc?, index?, guard?, msg, hint? } mkContractError { type?, context?, value, guard, msg, hint? }

Per-layer Detail builders: mkKernelDetail / mkGenericDetail / mkContractDetail

Combinators: nestUnder : Position -> Error -> Error addChild : Position -> Error -> Error -> Error setLeafHint : Hint -> Error -> Error

Layer constants: Kernel, Generic, Contract. Predicates: isError, isLayer, isDetail, isKernel, isGeneric, isContract. Equality: eq (structural).

Pure data. No dependencies on kernel, trampoline, effects, tc, or types modules.

Contract

Contract: Layer constant tagging a value with the correct shape that violates a refinement predicate (guard).

Paired with a ContractDetail carrying value, the mandatory guard = { predicate = "…"; }, and optionally the surface type and outer context. Renderer formats Contract failures as predicate violations distinct from shape mismatches. Pre-allocated; never construct via { _tag = ...; }.

Generic

Generic: Layer constant tagging a value whose shape fails to inhabit a description.

Emitted by sugar validators (fx.types.*) and the generic descElim-driven shape checker. Paired with a GenericDetail carrying value (the failing input) and usually type / desc identifying the violated contract. Pure shape failures (record-field type mismatch, wrong variant tag) live here; refinement-predicate failures belong in Contract.

Kernel

Kernel: Layer constant tagging a kernel-layer diagnostic error; Error.layer is set to this for typechecker/elaborator failures.

Emitted by checkHoas / infer / elaborator passes. Paired with a KernelDetail carrying rule (the failing kernel rule name) and typically expected / got carrying normalised value-domain types. Pre-allocated; never construct via { _tag = ...; }.

addChild

addChild: append a keyed child Error to a branching parent; used by collecting handlers that gather many sibling failures under one root without flattening the blame paths.

addChild : Position -> Error -> Error -> Error  -- position, parent, child

Use for sibling collection (record fields, variant cases, list elements all rejected against the same root contract). Order of insertion is preserved in the resulting children list, so callers control reporting order. The parent's layer / detail / msg are not overwritten — they describe the outer-shape failure, while each child describes one element's failure. For descent (one-deep hop), use nestUnder instead; addChild is the multi-sibling counterpart.

appendTrace

appendTrace: append a { rule, position } entry to a Kernel-layer error's detail.trace; non-Kernel errors pass through unchanged. Used by bindP/bindPR to auto-capture the descent chain as the error unwinds.

appendTrace : (String | null) -> Position -> Error -> Error

captureFrame

captureFrame: project a typing context into a { depth, env, types, names } Frame suitable for KernelDetail.frame; reads ctx.names defensively so contexts without name tracking still produce a well-formed frame.

captureFrame : Ctx -> Frame

eq

eq: structural equality on Error values — relies on Nix's attrset-by-content comparison so equal trees compare equal regardless of construction path.

eq : Error -> Error -> Bool

Equality is content-based, so two distinct constructions of the same shape (mkKernelError { rule = "r"; msg = "m"; } twice) compare equal — useful for test assertions and for deduplicating siblings in a collecting handler. Position ADT values inside children participate in the comparison, so chains with reordered hops are not equal.

isContract

isContract: Layer variant predicate — true iff the value is the Contract constant.

isContract : Any -> Bool

isDetail

isDetail: predicate recognising the Detail ADT — checks _tag == "Detail" plus the presence of a layer self-discriminator.

isDetail : Any -> Bool

isError

isError: predicate recognising the Error ADT — checks _tag == "Error" plus the required fields layer, detail, msg, children.

isError : Any -> Bool

Use at module boundaries where input could be anything; internal code that constructs Errors via the per-layer constructors doesn't need to check. The predicate rejects bare attrsets that happen to have _tag = "Error" but are missing required fields — guards against accidental partial construction more than against type confusion.

isGeneric

isGeneric: Layer variant predicate — true iff the value is the Generic constant.

isGeneric : Any -> Bool

isKernel

isKernel: Layer variant predicate — true iff the value is the Kernel constant.

isKernel : Any -> Bool

isLayer

isLayer: predicate recognising the Layer ADT — checks _tag == "Layer" plus the presence of tag; accepts Kernel, Generic, and Contract.

isLayer : Any -> Bool

Does not distinguish the variants — pair with a check on .tag for layer-specific dispatch, or use isKernel / isGeneric / isContract. Rejects plain attrsets { tag = "Kernel"; } that lack _tag, so renderer branching can trust a positive result to mean a canonical constant.

mkContractDetail

mkContractDetail: build a Contract-layer Detail record from optional field overrides; defaults set every field to null and carry the layer self-discriminator. Callers should always populate guard.

mkContractDetail : { type?, value?, context?, guard? } -> Detail

mkContractError

mkContractError: build a contract-layer leaf Error from { value, guard, msg, type?, context?, hint? }; value has the correct shape but guard rejected it.

mkContractError : { value, guard, msg, type?, context?, hint? } -> Error

guard is mandatory — a { predicate = "…"; } record naming the refinement that rejected value. Without a guard the failure is structural, not contractual, and belongs in mkGenericError. type and context describe the surrounding contract for the renderer.

mkGenericDetail

mkGenericDetail: build a Generic-layer Detail record from optional field overrides; defaults set every field to null and carry the layer self-discriminator.

mkGenericDetail : { type?, desc?, value?, context?, index?, guard? } -> Detail

mkGenericError

mkGenericError: build a generic-layer leaf Error from { value, msg, type?, context?, desc?, index?, guard?, hint? }; value is the thing whose shape failed to inhabit the description.

mkGenericError : { value, msg, type?, context?, desc?, index?, guard?, hint? } -> Error

type is the surface name presented to the user ("PersonT", "NonEmptyList"); desc is the underlying Desc I shape if the producer has it; context is an outer-scope name used in nested record/variant failures. The guard slot is retained for callers that have not yet migrated refinement failures to mkContractError; prefer Contract for new producers.

mkKernelDetail

mkKernelDetail: build a Kernel-layer Detail record from optional field overrides; defaults set every field to null (trace to []) and carry the layer self-discriminator.

mkKernelDetail : { rule?, expected?, got?, ctx_depth?, term?, frame?, trace? } -> Detail

mkKernelError

mkKernelError: build a kernel-layer leaf Error from { rule, msg, position?, expected?, got?, ctx_depth?, term?, frame?, trace?, hint? }; when position is supplied, wraps the leaf in nestUnder so the rule emits its own descent coordinate.

mkKernelError : { rule, msg, position?, expected?, got?, ctx_depth?, term?, frame?, trace?, hint? } -> Error

rule is the kernel-rule identifier — hints.nix keys its Hint table off rule plus blame-path-suffix, so use the canonical name ("check", "desc-arg", "univ-poly", …) not an ad-hoc string. expected / got should be value-domain terms (post-eval), not unelaborated HOAS — the diff renderer expects normalised shape. Supplying position is equivalent to nestUnder p (mkKernelError { … }); use it when the rule emits a single descent hop, not when the caller will add hops of its own. term names the failing surface-term shape; frame is a Ctx snapshot via captureFrame; trace is usually left empty at emission and populated by bindP / bindPR as the error unwinds.

nestUnder

nestUnder: add a positional hop above inner, producing a new branch whose single child carries position as its edge label; pass-through of layer/detail/msg/hint preserves leaf rendering at any depth.

nestUnder : Position -> Error -> Error

Pass-through invariant: the wrapper's layer, detail, msg, and hint are copied from inner. This is what lets the renderer pick its branch (Kernel vs Generic) and pick the leaf's payload at any depth without descending the chain — the entire single-child chain reports the same diagnostic, just with a longer blame path. Stacking is by repeated application: nestUnder pOuter (nestUnder pInner leaf) yields a chain whose outer edge is pOuter, inner edge pInner.

setLeafHint

setLeafHint: walk the single-child chain to its leaf and overwrite hint on the endpoint, returning a structurally-equivalent tree; stack-safe via splitChainFast/splitChainSlow to kernel-descent depth.

setLeafHint : Hint -> Error -> Error

Only mutates the chain endpoint. If the endpoint is branching (children count > 1), returns the tree unchanged — sibling- specific hint attachment is the caller's responsibility, the function is intentionally a no-op there to avoid clobbering ambiguity. Stack-safe to arbitrary depth: switches from direct recursion to a genericClosure worklist past fastPathLimit (500) frames. Use after hints.resolve has produced a Hint for the failure, not before.