Documentation

Diagnostic severity, mirroring the usual LSP levels.

A structured diagnostic. Independent of any editor protocol: the LSP maps it to its own Diagnostic, and the CLI serialises it as JSON.

JSON wire format (rzk typecheck --json)

This is a stable format that downstream tools (e.g. richer LSP hovers) pin to. Each diagnostic is an object:

{ "severity": "error" | "warning" | "information" | "hint"
, "code":     <string>           -- "hole", or a TypeError tag (e.g. "TypeErrorUnify")
, "location": { "file": <string|null>, "line": <int|null> } | null
, "message":  <string>           -- human-facing prose (the CLI/LSP display text)
, "hole":     <HoleData> | null  -- present only for hole diagnostics (see 'HoleData')
}

The message field is kept for back-compat (the LSP and the CLI human mode use it). Structured consumers should read the hole object instead of parsing message. For non-hole diagnostics hole is null.

The structured payload of a hole diagnostic: the goal and local context as already-rendered display strings (the same strings the LSP/CLI show, i.e. show = printTree on the underlying terms). Consumers render hole panels from these fields directly, without parsing the human-facing message.

JSON wire format

{ "name":     <string|null>                 -- the ?name, if the hole was named
, "goal":     <string>                       -- the expected type (the goal)
, "shape":    { "binder": <string>, "tope": <string> } | null
, "termVars": [ { "name": <string>, "type": <string> }, ... ]
, "cubeVars": [ { "name": <string>, "type": <string> }, ... ]
, "topes":    [ <string>, ... ]              -- local tope assumptions (excludes ⊤)
}

Notes for consumers:

• shape is non-null only for a shape-restricted argument goal, where the goal reads (binder : goal | tope). For an extension type the boundary is already part of goal (a restricted type A [ … ↦ … ]), and shape is null — read the boundary out of goal.
• cubeVars names can be patterns like "(t, s)" (pair-pattern binders); they are display strings, not single identifiers.

Encode a location as JSON. A plain helper rather than a ToJSON instance, to avoid an orphan instance (LocationInfo is defined in Rzk.TypeCheck).

A stable tag for a type error, used as its diagnostic code. Independent of the variable type, so it survives the scoped-error unfolding.

The tag of a scoped type error (peels the binder layers; the tag does not depend on the variable type).

The source location of a scoped type error (the enclosing command's line).

A structured diagnostic for a type error. The message is the usual formatted error text; severity is always SeverityError.

A structured diagnostic for a hole, carrying the hole's goal and local context. A hole is an unfilled obligation, so it is a SeverityWarning — mirroring Agda's yellow "unsolved" highlight, and visible in the editor's problems panel (unlike SeverityHint, which editors render almost invisibly). Finished work still rejects holes outright: the strict default of rzk typecheck reports them as errors (cf. Agda's --safe).

The structured payload of a hole: its goal and local context rendered to display strings (the same rendering ppHoleInfo uses, but kept as separate fields rather than concatenated into prose). See HoleData.

Render a hole's goal and local context (the structured query) for display, separating term variables, cube variables, and tope assumptions.