Files
AILang/crates/ailang-check/src/diagnostic.rs
T
Brummel 832375f2ac convention: counter-prefix file naming across docs/specs/, docs/plans/, design/contracts/, design/models/
All 176 files in the four accumulating directories now use a
zero-padded 4-digit counter prefix that reflects creation order
(`NNNN-slug.md`). The counter is assigned per directory in strict
git-log creation order; ties broken alphabetically by original name.
The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is
dropped — the date is recoverable from git log and the counter
carries the ordering.

A file's counter is stable for the life of the file: never reassigned,
never reused, never compacted. Deleted files retire their counter;
subsequent files do not fill the gap. This is the property that lets
cross-references stay literal — refs use the full filename including
the counter (`design/contracts/0007-honesty-rule.md`) so they grep
cleanly and resolve directly without a glob step.

313 cross-references updated across .md/.rs/.toml/.c/.json files
(test pins, include_str! paths, design-INDEX entries, baseline notes,
runtime C comments, inter-contract markdown links incl. bare basename
and `../models/foo.md` forms).

CLAUDE.md gets a new "File-naming convention" section spelling out
the rule and rationale. skills/brainstorm/SKILL.md and
skills/planner/SKILL.md updated so new spec/plan creation produces
counter-prefixed names from the start.

The full test suite (cargo test --workspace) passes.
2026-05-28 13:31:31 +02:00

280 lines
13 KiB
Rust

//! Structured diagnostics for `ail check --json`.
//!
//! A [`Diagnostic`] is the machine-readable representation of a problem
//! reported by the typechecker (or an upstream load step).
//! [`Severity`] serializes as a lowercase string
//! (`"error"` / `"warning"`); the `code` field is a stable kebab-case identifier
//! that tooling can consume without parsing the `message` text.
//!
//! Convention: each call to [`crate::check_module`] reports at most one
//! diagnostic (single-shot). Multiple diagnostics per run are a future
//! feature; the current format already allows them.
//!
//! Stable codes (as of iteration 5b):
//! - `schema-mismatch`
//! - `unknown-type`
//! - `unbound-var`
//! - `type-mismatch` — `ctx`: `{"expected": "...", "actual": "..."}`
//! - `arity-mismatch` — `ctx`: `{"expected": N, "actual": M}`
//! - `unknown-ctor`
//! - `unknown-effect-op`
//! - `non-exhaustive-match` — `ctx`: `{"missing": ["..."]}`
//! - `unknown-ctor-in-pattern`
//! - `nested-ctor-pattern-not-allowed`
//! - `duplicate-def`
//! - `not-a-function`
//! - `undeclared-effect`
//! - `fn-type-required`
//! - `param-count-mismatch`
//! - `polymorphic-not-supported`
//! - `const-has-effects`
//! - `pattern-type-mismatch`
//! - `primitive-needs-wildcard`
//! - `duplicate-type`
//! - `duplicate-ctor`
//! - `unknown-module` — `ctx`: `{"module": "<prefix>"}` (Iter 5b)
//! - `unknown-import` — `ctx`: `{"module": "<m>", "name": "<def>"}` (Iter 5b)
//! - `invalid-def-name` — `ctx`: `{"name": "<n>", "reason": "contains-dot"}` (Iter 5b)
//! - `module-not-found` — workspace loader (Iter 5b, in the CLI path)
//! - `module-cycle` — workspace loader (Iter 5b, in the CLI path)
//! - `module-name-mismatch` — workspace loader (Iter 5b, in the CLI path)
//! - `module-hash-mismatch` — workspace loader (Iter 5b, in the CLI path)
//! - `tail-call-not-in-tail-position` (see `design/contracts/0012-tail-calls.md`)
//! - `use-after-consume` — `ctx`: `{"binder": "<n>"}` (Iter 18c.2);
//! carries non-empty [`Diagnostic::suggested_rewrites`] showing how to
//! spell the fix in form-A AILang.
//! - `consume-while-borrowed` — `ctx`: `{"binder": "<n>"}` (Iter 18c.2);
//! ditto on `suggested_rewrites`.
//! - `over-strict-mode` (Iter 19a) — `severity: warning`. Emitted by
//! the linearity pass when a fn parameter is annotated `(own T)` but
//! the body never consumes it (and never destructures it via
//! `match`). `ctx`: `{"binder": "<n>", "current_mode": "own",
//! "suggested_mode": "borrow"}`. Carries one
//! [`SuggestedRewrite`] whose `replacement` is the relaxed
//! `(fn-type ...)` in form-A. Pure advisory; the typechecker still
//! accepts the original signature.
//! - `empty-suppress-reason` (Iter 19b) — `severity: error`. Emitted
//! by the per-module suppress filter when a `(suppress (code ...)
//! (because ""))` entry on an `FnDef` has an empty or
//! whitespace-only `because`. `ctx`: `{"code": "<suppressed-code>"}`.
//! Hard-Error: a suppression without a reason is unreviewable, so
//! the build refuses it. Note that an invalid suppression does NOT
//! suppress its target diagnostic — the original still fires
//! alongside this error.
//! - `missing-constraint` — `severity: error`. Emitted
//! by the per-fn typecheck arm when a polymorphic `FnDef` calls a
//! class method (e.g. `show x` where `x: a`) but its declared
//! `Forall.constraints` (after one-step superclass expansion) does
//! not include the residual class constraint. `ctx`:
//! `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`. Concrete-
//! type residuals are deferred to the `no-instance` diagnostic.
//! - `no-instance` — `severity: error`. Emitted by the
//! per-fn typecheck arm when a class-method call resolves the class
//! param to a fully-concrete type that has no matching entry in the
//! workspace instance registry (`(class, canonical-type-hash)`).
//! Dual of `missing-constraint`: when the residual is concrete, the
//! fn cannot push the obligation to a caller, so an existing
//! instance is the only way to discharge it. `ctx`:
//! `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`. An
//! optional `candidate_classes` field is added when the residual
//! originated from the multi-candidate dispatch path; absent on
//! single-class residuals (back-compat).
//! - `ambiguous-method-resolution` — `severity: error`. Emitted
//! by the type-driven dispatch resolver (or the discharge-time
//! multi-candidate refinement) when a bare-method call site survives
//! both type-driven and constraint-driven filtering with more than
//! one candidate class. `ctx`: `{"method": "<m>", "at_type": "<T>",
//! "candidate_classes": ["<C1>", ...]}`. The author disambiguates
//! by writing `<ClassQualifier>.<method> x`.
//! - `unknown-class` — `severity: error`. Emitted by the
//! type-driven dispatch resolver when an explicit class qualifier
//! in a `Term::Var.name` (e.g. `"prelude.Show.show"`) names a
//! qualified class that is not in the workspace registry of
//! candidate classes for the method. `ctx`:
//! `{"name": "<qualified-class>"}`.
//! - `class-method-shadowed-by-fn` — `severity: warning`.
//! Emitted by `synth`'s `Term::Var` arm when a name resolves to a
//! free fn (locals / caller-module-fn / imported-fn) AND a class
//! method of the same name also exists in the workspace. Fn
//! resolution proceeds per lookup precedence; the warning surfaces
//! the shadow so the LLM-author can disambiguate via explicit
//! class-qualified call (`<ClassQualifier>.<method> ...`) if the
//! shadow was unintentional. `ctx`: `{"name": "<resolved-name>",
//! "method": "<bare-method>", "fn_owner_module": "<m>",
//! "candidate_classes": ["<C1>", ...]}`.
use serde::Serialize;
/// Severity of a [`Diagnostic`].
///
/// Serializes as a lowercase string (`"error"` / `"warning"`) so that
/// `ail check --json` consumers can branch on it without parsing prose.
/// Currently the only emitter of [`Severity::Warning`] is the
/// linearity-pass `over-strict-mode` lint.
#[derive(Serialize, Debug, Clone, Copy, PartialEq, Eq)]
#[serde(rename_all = "lowercase")]
pub enum Severity {
/// Hard failure. The module did not typecheck.
Error,
/// Non-fatal observation. Module typechecked; the lint is
/// advisory.
Warning,
}
/// Machine-readable problem report from the typechecker.
///
/// Stable JSON shape: every field is always emitted (no `skip_serializing_if`),
/// so a tool can decode into a fixed schema without conditional handling.
/// See the module-level doc for the list of `code` values.
#[derive(Serialize, Debug, Clone)]
pub struct Diagnostic {
/// Severity of the diagnostic; see [`Severity`].
pub severity: Severity,
/// Stable kebab-case identifier (e.g. `"unbound-var"`,
/// `"type-mismatch"`). Tool consumers should branch on this rather
/// than on `message`. The full enumeration is listed in the module
/// doc.
pub code: String,
/// Human-readable description. Free-form; do not parse. The
/// `code` + `ctx` pair carries the structured equivalent.
pub message: String,
/// Which top-level definition is affected (if known). Always emitted in
/// the JSON — `null` when unknown — so consumers don't have to handle
/// the field conditionally.
pub def: Option<String>,
/// Free structured context. Empty = `{}`.
pub ctx: serde_json::Value,
/// machine-applicable fix suggestions, each a snippet of
/// form-A AILang the author can paste back at the offending site.
/// Empty = no rewrite suggested. The list is always emitted (so JSON
/// consumers see a stable shape; they can branch on `.is_empty()`).
/// Currently populated by the linearity check (`use-after-consume` /
/// `consume-while-borrowed` codes); other diagnostics emit `[]`.
pub suggested_rewrites: Vec<SuggestedRewrite>,
}
/// One machine-applicable rewrite suggestion attached to a [`Diagnostic`].
///
/// emitted by the linearity check to point the author (or an
/// LLM consumer of `ail check --json`) at the spelled fix. `replacement`
/// is form-A AILang text — parseable by `ailang_surface::parse_term`.
#[derive(Serialize, Debug, Clone)]
pub struct SuggestedRewrite {
/// One-line free-form description of what the rewrite does (e.g.
/// `"wrap the offending use in (clone X)"`). Not parsed by tooling.
pub description: String,
/// Form-A AILang snippet to substitute at the offending site. For
/// the linearity-check diagnostics this is typically `(clone <n>)`
/// or a small enclosing rewrite. The string MUST parse via the
/// surface `parse_term` entrypoint; `crate::linearity` tests
/// guard the round-trip.
pub replacement: String,
}
impl Diagnostic {
/// Builds an [`Severity::Error`] diagnostic with the given `code` and
/// `message`. `def` is left unset and `ctx` defaults to `{}` — chain
/// [`Diagnostic::with_def`] / [`Diagnostic::with_ctx`] to fill them
/// in.
pub fn error(code: impl Into<String>, message: impl Into<String>) -> Self {
Self {
severity: Severity::Error,
code: code.into(),
message: message.into(),
def: None,
ctx: serde_json::Value::Object(serde_json::Map::new()),
suggested_rewrites: Vec::new(),
}
}
/// builds a [`Severity::Warning`] diagnostic. Same shape
/// as [`Diagnostic::error`] otherwise. Used by lint-style passes
/// that report observations rather than hard typecheck failures
/// (currently the only emitter is the linearity pass's
/// `over-strict-mode` lint).
pub fn warning(code: impl Into<String>, message: impl Into<String>) -> Self {
Self {
severity: Severity::Warning,
code: code.into(),
message: message.into(),
def: None,
ctx: serde_json::Value::Object(serde_json::Map::new()),
suggested_rewrites: Vec::new(),
}
}
/// append a [`SuggestedRewrite`]. Builder-style. Used by
/// the linearity check to attach the form-A fix it computed. Other
/// diagnostics leave the field empty.
pub fn with_suggested_rewrite(
mut self,
description: impl Into<String>,
replacement: impl Into<String>,
) -> Self {
self.suggested_rewrites.push(SuggestedRewrite {
description: description.into(),
replacement: replacement.into(),
});
self
}
/// Sets the affected top-level def name. Builder-style: returns
/// `self`. Used by [`crate::CheckError::to_diagnostic`] when the
/// error was wrapped in [`crate::CheckError::Def`].
pub fn with_def(mut self, def: impl Into<String>) -> Self {
self.def = Some(def.into());
self
}
/// Replaces the `ctx` payload. Builder-style: returns `self`. Pass a
/// `serde_json::Value` whose shape matches the `code`-specific
/// schema documented at the module level (e.g.
/// `{"expected": "...", "actual": "..."}` for `type-mismatch`).
pub fn with_ctx(mut self, ctx: serde_json::Value) -> Self {
self.ctx = ctx;
self
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn serializes_with_stable_shape() {
let d = Diagnostic::error("unbound-var", "unknown identifier: `x`")
.with_def("main");
let s = serde_json::to_string(&d).unwrap();
// All fields must be present, severity lowercase, ctx is an
// empty object (not null, not omitted), suggested_rewrites is
// always-emitted as `[]` for non-linearity diagnostics.
assert!(s.contains("\"severity\":\"error\""), "{s}");
assert!(s.contains("\"code\":\"unbound-var\""), "{s}");
assert!(s.contains("\"def\":\"main\""), "{s}");
assert!(s.contains("\"ctx\":{}"), "{s}");
assert!(s.contains("\"suggested_rewrites\":[]"), "{s}");
}
#[test]
fn ctx_can_carry_structured_data() {
let d = Diagnostic::error("type-mismatch", "type mismatch")
.with_ctx(serde_json::json!({"expected": "Int", "actual": "Bool"}));
let s = serde_json::to_string(&d).unwrap();
assert!(s.contains("\"expected\":\"Int\""), "{s}");
assert!(s.contains("\"actual\":\"Bool\""), "{s}");
}
/// a diagnostic carrying a `SuggestedRewrite` serialises
/// the rewrite under `suggested_rewrites` with the description and
/// the form-A replacement.
#[test]
fn suggested_rewrite_serializes() {
let d = Diagnostic::error("use-after-consume", "use of `xs` after consume")
.with_suggested_rewrite("wrap earlier use in (clone)", "(clone xs)");
let s = serde_json::to_string(&d).unwrap();
assert!(s.contains("\"suggested_rewrites\":["), "{s}");
assert!(s.contains("\"description\":\"wrap earlier use in (clone)\""), "{s}");
assert!(s.contains("\"replacement\":\"(clone xs)\""), "{s}");
}
}