# Hints Hint resolver for diagnostic Errors. Exports: resolve : Error -> Hint | null classify : Error -> String hints : { = Hint; } 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/`, where `` 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/`, 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: `"....::"`. 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 -> String ``` ## `hints` _hints: the closed `{ key = Hint }` registry indexed by `....::` keys; each value carries `text`, `category`, `severity`, `docLink` to the per-key `/nix-effects/diag-hints/` 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 -> Hint ``` ## `resolve` _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 | null ``` ## `taxonomy` _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::` 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 ` 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.