A binding shown in a hole's local context: the display name and its type, already rendered.

The structured goal and context at a hole, recorded in lenient mode (see allowHoles). Everything is rendered to user-facing names at record time, so HoleInfo is independent of the scope it came from. Local hypotheses are split into ordinary term variables and cube variables (the cube/tope layer is specific to Rzk); the global environment is deliberately excluded — it belongs in a searchable inventory, not the goal panel.

A non-fatal finding of the checker, recorded on the writer channel beside the holes and carried out of a run in Checked. Structured, so the CLI, the LSP, and (later) safe mode each decide how to present or escalate it.

Where a warning points, for per-file attribution.

Which candidate rule of the meta-parameter layer check flags a MetaPrefixWarning (see Rzk.TypeCheck.MetaPrefix): the structural rule, or only its stricter variant. Both are emitted so the two candidate defaults can be measured on a corpus side by side.

What a run records besides its result: the holes it found and the non-fatal findings it made. Both accumulate in reverse and are turned around by checkLog when the run ends.

What a run recorded, in the order it was recorded.

The record of a run is kept in the state, beneath the error channel, rather than on a writer channel above it.

The two differ exactly where a caught error is concerned: a writer discards what the failing action wrote, and the state keeps it. That is what the checker wants. A command that fails still reports the holes the user wrote in it, and checking goes on to the next command with those holes in hand (see withCommand in Rzk.TypeCheck.Decl). A probe that wants the older behaviour asks for it, with suppressing.

Run a judgement in a given context, keeping what it recorded.

Run a judgement in the empty context, discarding the holes it records.

Run a judgement in a given context, discarding the holes it records.

Run a judgement in another scope's context.

The error channel and the hole channel are shared and carry no scope index, so there is nothing to translate: this is runReaderT with the inner scope's context, lifted back. Holes recorded inside land in the same state, and an error thrown inside already carries its own context.

Raise a type error, capturing the context it happened in.

Render the enclosed action with the proof term hidden.

The depth of nested judgements at which type checking gives up. Well-typed input stays far below it; the cap catches a non-terminating search. FIXME: expose as a parameter (--max-depth and rzk.yaml).

Point the location at the sub-term an action is about.

The checker descends through performing, so the location narrows as it goes and an error is reported where the sub-term that caused it was written, rather than at the declaration it is in (issue #81). A judgement about a term the checker built itself carries no position, and leaves the location as it found it: that is the innermost enclosing term the user did write.

Run a probe for its answer alone, discarding whatever it records.

A hole's inventory is built by trying candidate moves and seeing which fit, and each trial checks terms of its own; their holes and warnings are not the user's and must not reach the report. This is what the writer channel's censor did before the record moved into the state: the state survives an error, so it is put back on that path too.