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 recorded alongside holes in CheckLog and returned in Checked. The CLI and LSP decide how to present 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.

Record a warning, once: a term can be elaborated twice (a definition's parameter annotation is checked for the signature and again as the domain of the body's λ), and the second elaboration makes the same finding at the same location.