# 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).

## Source

- [`src/tc/check/diag/shell.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/diag/shell.nix)
- [`src/tc/check/diag/source_map.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/check/diag/source_map.nix)