Diag
The diag namespace provides typed diagnostic Errors and
structured Hints for the type-checker and runtime contracts.
error
Diagnostic Error ADT.
An Error has a Layer (Kernel | Generic), a Detail record whose fields
are all optional, 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? }
Combinators: nestUnder : Position -> Error -> Error addChild : Position -> Error -> Error -> Error
Layer constants: Kernel, Generic. Predicates: isError, isLayer. Equality: eq (structural).
Pure data. No dependencies on kernel, trampoline, effects, tc, or types modules.
positions
Shared diagnostic alphabet. Pure data.
A Position names the blame location in a structural descent through
a Desc or through raw MLTT structure (Π / Σ / Ann / μ / App). The
alphabet is description-centric: names such as DArgSort, DPlusL,
and PiDom identify sub-positions by their meaning in the structure,
not by the code path that happens to visit them.
Two kinds of consumer:
- A kernel enrichment layer that wraps rule delegations, emitting
a child error tagged with the
Positionof the sub-call that failed. - A value-level validator (record / list / variant field walkers)
that emits
Field/Elem/Tagpositions from its per- component blame traversal.
Both consumers produce Error trees whose children are keyed by
Position, allowing errors from either source to compose into one
tree.
pretty
Pretty-printing for diagnostic Errors.
Exports: pathSegments : Error -> [String] pathString : Error -> String oneLine : Error -> String multiLine : Error -> String
Chain walkers recurse directly up to 500
frames, then fall through to a builtins.genericClosure slow
path that WHNF-forces the next node at each step.
Pure data -> string; no effects.
hints
Hint resolver for diagnostic Errors.
Exports:
resolve : Error -> Hint | null
classify : Error -> String
hints : {
A Hint is { _tag = "Hint"; text; category; severity; docLink; }.
The _tag marker keeps it terminal for api.extractValue, and
the remaining fields are plain data consumable by renderers,
LSPs, docs, and linters. Severity is "error" at this layer;
docLink points at the per-key heading anchor on the
auto-generated diag module page (/nix-effects/core-api/diag).
The anchor slug matches the docs-site markdown renderer's
heading-id slugification rule, so each hint's docLink lands
precisely on the rendered section for its key.
Keys encode a leaf-anchored suffix of the blame path plus the
classifier pattern: "<pos1>.<pos2>...<posN>::<pattern>". A key
matches when its positions equal the last N tags of the blame
path; resolve returns the hint under the longest matching
suffix. Single-position keys are the 1-hop special case. Hint
text is position-semantic: no kernel-rule strings, no source-file
references.
Chain walking recurses directly up to 500
frames, then falls through to a builtins.genericClosure slow
path that WHNF-forces the next node.
Hint registry
The Hint table maps each blame-path-suffix · classifier-pattern
key to a structured Hint record. Each subsection below
corresponds to one such key; the heading anchor is the canonical
docLink target referenced from hints.nix.
AnnTerm::type-mismatch
Category: type-mismatch · Severity: error
the annotated term does not match its declared type
AnnType::not-a-type
Category: sort · Severity: error
the annotation position must be a type (live in some U(k)), not a term. Write a type expression such as nat, bool, u 0, or a user-defined datatype.
AppArg::type-mismatch
Category: type-mismatch · Severity: error
the argument does not match the function's domain
AppHead::not-a-function
Category: arity · Severity: error
the head of an application must have a function type (Pi)
Case::type-mismatch
Category: elimination · Severity: error
this case-body's inferred type does not match the type the eliminator's motive requires
DArgBody::not-a-desc
Category: description · Severity: error
the body of arg must produce a description (Desc I), not an ordinary value. Build one with descRet, descArg, descRec, descPi, or descPlus.
DArgSort::universe-mismatch
Category: universe · Severity: error
the sort position of arg must live in U(0); descriptions only carry small types. Pass u 0, or factor the dependency through descRec / descPi if a larger type is genuinely needed.
DPiBody::not-a-desc
Category: description · Severity: error
the body of pi must produce a description for each input, not a plain term. Return a Desc I via descRet, descArg, descRec, descPi, or descPlus.
DPiFn::not-a-function
Category: arity · Severity: error
the index selector f of pi must be a function S -> I
DPiFn::type-mismatch
Category: indexing · Severity: error
the index selector's domain must match the declared sort S
DPiSort::universe-mismatch
Category: universe · Severity: error
the sort position of pi must live in U(0); descPi takes a small domain. Use u 0, or encode the dependency through an index instead of the Pi domain.
DPlusL::not-a-desc
Category: description · Severity: error
the left summand of plus must be a description (Desc I)
DPlusR::not-a-desc
Category: description · Severity: error
the right summand of plus must be a description at the same index type as the left summand
DRecIndex::type-mismatch
Category: indexing · Severity: error
the index position of rec must match the Desc's declared index type. Pass a term of that index type, or adjust the enclosing μ I ... to match.
DRecTail::not-a-desc
Category: description · Severity: error
the tail position of rec must itself be a description, not an ordinary term. Continue the spine with descRet, descArg, descRec, descPi, or descPlus.
DRetIndex::type-mismatch
Category: indexing · Severity: error
the index position of ret must match the Desc's declared index type. Supply a term of that index type, or redefine the enclosing μ I ... over the index you actually have.
Elem::inhabitation-failed
Category: inhabitation · Severity: error
the element does not inhabit the list's element type
Elem::refinement-failed
Category: refinement · Severity: error
the element violates the element type's refinement predicate
Field::inhabitation-failed
Category: inhabitation · Severity: error
the field's value does not inhabit the declared field type
Field::refinement-failed
Category: refinement · Severity: error
the field's value violates the field type's refinement predicate
JType::not-a-type
Category: sort · Severity: error
the type parameter of J must be a type (live in some U(k)), not a term. Pass a type expression like nat, u 0, or the type shared by J's two endpoints.
JType::type-mismatch
Category: type-mismatch · Severity: error
the type parameter of J must match the type of its two endpoints
LevelMaxLhs::type-mismatch
Category: universe · Severity: error
the left operand of max must be a Level
LevelMaxRhs::type-mismatch
Category: universe · Severity: error
the right operand of max must be a Level
LevelSucPred::type-mismatch
Category: universe · Severity: error
the predecessor of suc must be a Level
Motive.PiDom::not-a-type
Category: sort · Severity: error
the motive's domain must be a type (live in some U(k)). The motive receives the scrutinee's type as its domain and returns a type; supply a concrete type such as nat, u 0, or the datatype being eliminated.
Motive::not-a-function
Category: arity · Severity: error
the motive must be a function from the scrutinee's type into a type, not a bare type or value. Supply a one-argument function whose body lives in some U k.
Motive::not-a-type
Category: sort · Severity: error
an eliminator's motive must return a type (live in some U(k))
MuDesc::not-a-desc
Category: description · Severity: error
the description argument of μ must be a Desc I term, not an ordinary value. Construct it with descRet, descArg, descRec, descPi, or descPlus.
MuIndex::type-mismatch
Category: indexing · Severity: error
the index passed to con must have the description's index type
MuPayload::type-mismatch
Category: indexing · Severity: error
the payload of con must inhabit the description's interpretation at the given index
OpaqueType::not-a-function
Category: arity · Severity: error
the annotation on an opaque lambda must be a Pi type
OpaqueType::type-mismatch
Category: type-mismatch · Severity: error
the opaque lambda's declared domain does not match the expected domain
PiCod::not-a-type
Category: sort · Severity: error
the codomain family of Π must return a type for each argument, not an ordinary value. Provide a function whose body inhabits some U k.
PiDom::not-a-type
Category: sort · Severity: error
the domain of Π must be a type (live in some U(k)), not a term or value. Supply a type expression like nat, bool, u 0, or a user-defined datatype.
Scrut::type-mismatch
Category: elimination · Severity: error
the scrutinee's type must match the eliminator's expected shape. Annotate the scrutinee via ann, or switch to the eliminator that matches its inferred type.
SigmaFst::inhabitation-failed
Category: inhabitation · Severity: error
the first component does not inhabit the declared fst type
SigmaFst::refinement-failed
Category: refinement · Severity: error
the first component violates the fst type's refinement predicate
SigmaSnd::inhabitation-failed
Category: inhabitation · Severity: error
the second component does not inhabit the dependent snd type
SigmaSnd::refinement-failed
Category: refinement · Severity: error
the second component violates the snd type's refinement predicate
Tag::inhabitation-failed
Category: inhabitation · Severity: error
the variant's payload does not inhabit the branch type
Tag::refinement-failed
Category: refinement · Severity: error
the variant's payload violates the branch type's refinement predicate
ULevel::type-mismatch
Category: universe · Severity: error
the level argument of U must be a Level