Diag — nix-effects

Diag

Outside the trust boundary. Routes kernel check/infer results through the trusted core and decorates failures with a resolved hint + a SourceMap-sourced surface origin. No new effects.

API

sourceMap — SourceMap data type and combinators. See the module's own doc for the full surface.
checkD : Ctx -> Tm -> Val -> SourceMap -> Any
inferD : Ctx -> Tm -> SourceMap -> Any
runCheckD : SourceMap -> Computation -> Any
runCheckDLazy : (Unit -> SourceMap) -> Computation -> Any

On success, these return what the trusted core returned (the elaborated Tm for checkD, {term; type;} for inferD). On failure, they return { error; msg; expected; got; hint; surface; }.

runCheckDLazy defers mkSm null into the failure branch, so the success path pays one closure allocation instead of the full SM walker. Kernel HOAS entry points (checkHoas/inferHoas) use this variant.

hint is a Hint record ({ _tag="Hint"; text; category; severity; docLink; }) from fx.diag.hints.resolve, or null. surface is the SourceMap's hoas payload at the blame chain's leaf, or null when the chain exits the mapped region.

Soundness audit: this module contains no kernel rule logic. A bug here can produce wrong hint text or an incorrect surface back-map; it cannot cause an ill-typed term to be accepted.

`checkD`

checkD: check with diagnostic decoration — shorthand for runCheckD sm (C.check ctx tm ty); returns the elaborated term on success, decorated error record on failure.

checkD : Ctx -> Tm -> Val -> SourceMap -> Tm | { error; msg; expected; got; hint; surface }

`inferD`

inferD: infer with diagnostic decoration — shorthand for runCheckD sm (C.infer ctx tm); returns { term; type } on success, decorated error record on failure.

inferD : Ctx -> Tm -> SourceMap -> { term; type } | { error; msg; expected; got; hint; surface }

`runCheckD`

runCheckD: kernel-result decorator — runs C.runCheck then, on failure, attaches a resolved hint (via fx.diag.hints.resolve) and a SourceMap-sourced surface back-mapping; success path untouched.

runCheckD : SourceMap -> Computation -> Tm | { error; msg; expected; got; hint; surface }

Lives outside the trust boundary: no new effect handlers, no rule logic. The trusted typeError handler from ctx.nix runs first; this combinator is a value-level transform on the failure attrset.

On success, returns whatever the trusted core returned (elaborated Tm). On failure, augments the flat record with hint (a Hint record or null) and surface (the SourceMap's hoas payload at the blame chain's leaf, or null when the chain exits the mapped sub-tree).

`runCheckDLazy`

runCheckDLazy: deferred-SourceMap variant of runCheckD — takes a thunk that's forced only on failure, sparing the success path the full SourceMap walker allocation.

runCheckDLazy : (Unit -> SourceMap) -> Computation -> Tm | { error; msg; expected; got; hint; surface }

Used by kernel HOAS entry points (checkHoas / inferHoas) where the SourceMap is a pure byproduct of elaboration and is consulted only when resolving surface positions on error. The success path pays one closure allocation instead of the full SourceMap construction.

`sourceMap`

sourceMap: parallel structure threaded alongside elaborated Tm — back-maps a kernel Error's Position-chain blame to the HOAS surface node that produced the offending sub-term.

A SourceMap mirrors the shape of an elaborated Tm, carrying at each node an opaque HOAS-origin reference plus a map from Position keys to child SourceMaps. Its sole purpose is back-mapping: given an error raised by the kernel during check/infer — whose blame is expressed as a Position chain threaded through Error.children by bindP — resolve that chain to the HOAS surface node that produced the offending sub-Tm.

Structure:

SourceMap = {
  _tag = "SourceMap";
  hoas : Any | null;          # HOAS-origin reference (opaque)
  subs : AttrSet SourceMap;   # keyed by positionKey(Position)
}

Surface: constructors (leaf, node, opaque), descent (descend, descendChain, hoasAt, hoasAtError), chain extraction (chainPositions), key derivation (positionKey), and the type predicate (isSourceMap). The key alphabet is whatever src/diag/positions.nix emits via positionKey; chain walking uses the same fast/slow split as src/diag/pretty.nix (builtins.genericClosure beyond 500 steps).