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 resolves to a dedicated per-key page on
docs.kleisli.io of the form
/nix-effects/diag-hints/<slug>, where <slug> matches the
docs-site heading-id slugification rule applied to the key.
Each per-key page is also exposed as an MCP resource at
docs://kleisli/nix-effects/diag-hints/<slug>, so a compiler
Hint dereferences to focused agent-readable content in one
fetch.
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.
classify
classify: derive the classifier pattern string from an Error's detail and leaf position — yields the right-hand side of suffix-keys consumed by resolve (e.g. "universe-mismatch").
classify : Error -> Stringhints
hints: the closed { key = Hint } registry indexed by <pos1>.<pos2>...<posN>::<pattern> keys; each value carries text, category, severity, docLink to the per-key /nix-effects/diag-hints/<slug> page.
mkHint
mkHint: structured Hint constructor from a category and text — sets _tag = "Hint" (terminal for extractValue), severity = "error", and the default docLink pointing at the diag-hints section root.
mkHint : Category -> String -> Hintresolve
resolve: walk a blame path inward from leaf to root, returning the Hint under the longest matching suffix-key — the canonical lookup for surfacing position-semantic guidance on a kernel Error.
resolve : Error -> Hint | nulltaxonomy
taxonomy: closed list of allowed Hint.category values ("universe", "sort", "description", "arity", "indexing", "inhabitation", …); enforced by the hints-categories-in-taxonomy test.
Hint registry
Diagnostic hints give stable names to recurring checker and validation
failures. Use the per-hint pages when an error includes a Hint::<key>
token, or scan the registry below to see the available hint keys.
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.
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.
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
ULevel::type-mismatch
Category: universe · Severity: error
the level argument of U must be a Level
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.
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.
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-type
Category: sort · Severity: error
an eliminator's motive must return a type (live in some U(k))
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.
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.
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.
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
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.
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.
AppHead::not-a-function
Category: arity · Severity: error
the head of an application must have a function type (Pi)
DPiFn::not-a-function
Category: arity · Severity: error
the index selector f of pi must be a function S -> I
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.
OpaqueType::not-a-function
Category: arity · Severity: error
the annotation on an opaque lambda must be a Pi type
DPiFn::type-mismatch
Category: indexing · Severity: error
the index selector's domain must match the declared sort S
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.
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.
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
Elem::inhabitation-failed
Category: inhabitation · Severity: error
the element does not inhabit the list's element type
Field::inhabitation-failed
Category: inhabitation · Severity: error
the field's value does not inhabit the declared field type
SigmaFst::inhabitation-failed
Category: inhabitation · Severity: error
the first component does not inhabit the declared fst type
SigmaSnd::inhabitation-failed
Category: inhabitation · Severity: error
the second component does not inhabit the dependent snd type
Tag::inhabitation-failed
Category: inhabitation · Severity: error
the variant's payload does not inhabit the branch type
Elem::refinement-failed
Category: refinement · Severity: error
the element violates the element type's refinement predicate
Field::refinement-failed
Category: refinement · Severity: error
the field's value violates the field type's refinement predicate
SigmaFst::refinement-failed
Category: refinement · Severity: error
the first component violates the fst type's refinement predicate
SigmaSnd::refinement-failed
Category: refinement · Severity: error
the second component violates the snd type's refinement predicate
Tag::refinement-failed
Category: refinement · Severity: error
the variant's payload violates the branch type's refinement predicate
Case::type-mismatch
Category: elimination · Severity: error
this case-body's inferred type does not match the type the eliminator's motive requires
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.
AnnTerm::type-mismatch
Category: type-mismatch · Severity: error
the annotated term does not match its declared type
AppArg::type-mismatch
Category: type-mismatch · Severity: error
the argument does not match the function's domain
JType::type-mismatch
Category: type-mismatch · Severity: error
the type parameter of J must match the type of its two endpoints
OpaqueType::type-mismatch
Category: type-mismatch · Severity: error
the opaque lambda's declared domain does not match the expected domain
::unhandled-boot-inl
Category: shape · Severity: error
the left injection inl x has no inference rule — the sum type's right summand is not determined by the syntax of x alone. Annotate with ann (inl x) (sum A B) to fix the expected sum, or place it where checking already provides one.
::unhandled-boot-inr
Category: shape · Severity: error
the right injection inr y has no inference rule — the sum type's left summand is not determined by the syntax of y alone. Annotate with ann (inr y) (sum A B) to fix the expected sum, or place it where checking already provides one.
::unhandled-boot-refl
Category: shape · Severity: error
refl has no inference rule — the type of the equated endpoint is not determined by its syntax. Annotate with ann refl (eq A x x), or use refl where the surrounding rule already supplies an expected equality type.
::unhandled-lam
Category: shape · Severity: error
this lambda has no inference rule — its domain and codomain types are not determined by its syntax. Annotate with ann (lam …) (pi A B) to drive checking, or place it where the surrounding rule already supplies an expected Pi type.
::unhandled-other
Category: shape · Severity: error
this intro form has no inference rule — its type is not determined by its syntax alone. Either annotate the term with ann <term> <type> to switch the kernel into checking mode, or move it inside a context where an expected type is already known.
::unhandled-pair
Category: shape · Severity: error
this pair has no inference rule — its component types are not determined by its syntax. Annotate with ann (pair …) (sigma A B) to drive checking, or place it where the surrounding rule already supplies an expected Sigma type.
::unhandled-tt
Category: shape · Severity: error
the unit value tt has no inference rule — there is exactly one type it can inhabit. The kernel still asks for an annotation to keep inference syntax-directed. Use ann tt unit at the use site, or check tt against an expected unit type.