Iter 13e: rustdoc polish for ailang-check

Second docwriter mission. Pure rustdoc additions (no API or
behaviour change) across the typechecker crate:

- builtins.rs: module root expanded; EffectOpSig (struct + 3
  fields) and install() got /// strings.
- diagnostic.rs: Severity (+ both variants), Diagnostic (+
  severity/code/message fields) and the error/with_def/with_ctx
  helpers got /// strings; super:: link rewritten to crate::.
- lib.rs: CheckError + every variant, to_diagnostic, CheckedModule
  (+ symbols), check, Env (+ globals/effect_ops/types/
  module_globals/current_module), CtorRef (+ type_name) got ///
  strings; crate-root prose upgraded with intra-doc link to
  check_module.

Verification: cargo doc --no-deps zero warnings; cargo build
--workspace green; cargo test --workspace 64/64 + 3 ignored
doctests green. Diff is 188 LOC, all in /// or //! lines (verified
by filtering).

Findings (not fixed; orchestrator-deferred):
- Env is pub but only privately constructable.
- CheckError::CtorArity and ::ArityMismatch share the public
  diagnostic code "arity-mismatch" by design.
- Diagnostic / Severity reachable via two paths because the
  diagnostic module is pub.

JOURNAL.md updated with the Iter 13e entry. 13f (ailang-codegen
+ ail) and 14a (List a rewrite) remain queued.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

crates/ailang-check/src/builtins.rs

@@ -1,14 +1,52 @@
 //! Built-in operations known to the typechecker (and codegen).
+//!
+//! This module owns the **fixed** symbol set the language ships with — the
+//! arithmetic / comparison / logical operators (`+`, `==`, `not`, ...) and
+//! the IO effect ops (`io/print_int`, ...). User code cannot define
+//! anything in here; conversely the typechecker treats every entry as
+//! always-in-scope without an explicit import.
+//!
+//! Builtins are kept in a **separate table** from user globals (see
+//! [`crate::Env::globals`] vs [`crate::Env::effect_ops`]) only because the
+//! two channels surface differently in the AST: value-level builtins are
+//! reached through `Term::Var { name }` (they live alongside user defs in
+//! `Env.globals`), while effect ops are reached through `Term::Do { op }`
+//! and need to carry an extra effect label, hence the dedicated
+//! [`struct@EffectOpSig`] payload in `Env.effect_ops`.
+//!
+//! The typechecker calls [`install()`] once per module-check, before any
+//! user-supplied globals are added. The CLI's `ail builtins` subcommand
+//! reflects the same data via [`list()`] / [`value_names()`].
 
 use ailang_core::ast::Type;
 
+/// Signature of a builtin effect operation: the effect label it raises,
+/// its parameter types, and its return type.
+///
+/// The typechecker consults this when synthesising the type of a
+/// `Term::Do { op, args }` — it unifies `args` against `params`, returns
+/// `ret`, and inserts `effect` into the body's accumulated effect set so
+/// the surrounding fn's declared effect row is checked against actual
+/// usage.
 #[derive(Debug, Clone)]
 pub struct EffectOpSig {
+    /// Effect label this op raises (e.g. `"IO"`). Compared against the
+    /// declared effect row on the enclosing fn type.
     pub effect: String,
+    /// Positional parameter types. Length and order are the contract for
+    /// `Term::Do { args }`.
     pub params: Vec<Type>,
+    /// Return type of the op. Often [`Type::unit`] for sinks like
+    /// `io/print_int`.
     pub ret: Type,
 }
 
+/// Populates `env` with every built-in operator and effect op.
+///
+/// Called once at the start of `check_in_workspace`, before user
+/// type defs and globals are folded in. After this returns, every name in
+/// [`list()`] is resolvable in `env`. Idempotent for a fresh `Env`; calling
+/// it twice would shadow the same entries with identical types.
 pub fn install(env: &mut crate::Env) {
     let int_int_int = Type::Fn {
         params: vec![Type::int(), Type::int()],

crates/ailang-check/src/diagnostic.rs

@@ -6,7 +6,7 @@
 //! (`"error"` / `"warning"`); the `code` field is a stable kebab-case identifier
 //! that tooling can consume without parsing the `message` text.
 //!
-//! Convention: each call to [`super::check_module`] reports at most one
+//! 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.
 //!
@@ -42,17 +42,38 @@
 
 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.
+/// The MVP only emits [`Severity::Error`]; [`Severity::Warning`] is
+/// reserved for future lints.
 #[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. Reserved; the typechecker does not emit
+    /// warnings yet.
     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
@@ -63,6 +84,10 @@ pub struct Diagnostic {
 }
 
 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,
@@ -73,11 +98,18 @@ impl Diagnostic {
         }
     }
 
+    /// 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

crates/ailang-check/src/lib.rs

@@ -1,5 +1,11 @@
 //! Typechecker for AILang (MVP).
 //!
+//! Sits between `ailang-core` (AST + canonical JSON + content hash) and
+//! `ailang-codegen` (LLVM IR emit) in the pipeline `core → check →
+//! codegen → ail`. Top-level entry points: [`check_module`] (one module,
+//! returns [`Diagnostic`]s), [`check_workspace`] (multi-module), and
+//! [`check`] (single-error legacy form returning a [`CheckedModule`]).
+//!
 //! HM with explicit top-level polymorphism. All top-level defs must carry
 //! their full type annotation; lambda bodies inside defs are checked
 //! monomorphically against their declared types. Polymorphism is opt-in
@@ -9,7 +15,8 @@
 //! Effects are propagated as a set and reconciled against the annotation
 //! on the function type.
 //!
-//! Built-in operations are resolved via the internal `Builtins` table.
+//! Built-in operations are resolved via the [`builtins`] table installed
+//! into every fresh [`Env`].
 //!
 //! ## Internals
 //!
@@ -235,23 +242,46 @@ pub mod diagnostic;
 
 pub use diagnostic::{Diagnostic, Severity};
 
+/// Internal error type produced by the typechecker.
+///
+/// One variant per stable diagnostic code (see [`CheckError::code`]). The
+/// [`CheckError::Def`] wrapper attaches the name of the def in which the
+/// inner error was raised — recursive accessors ([`CheckError::code`],
+/// [`CheckError::ctx`], [`CheckError::message`]) transparently see
+/// through the wrapping.
+///
+/// Typically this enum is converted to [`Diagnostic`] via
+/// [`CheckError::to_diagnostic`] before crossing the crate boundary;
+/// public API functions [`check_module`] and [`check_workspace`] already
+/// return `Vec<Diagnostic>`.
 #[derive(Debug, thiserror::Error)]
 pub enum CheckError {
+    /// Wraps an inner error with the name of the def it occurred in. The
+    /// inner error carries the actual code and ctx; the wrapper only the
+    /// def context that is later projected onto [`Diagnostic::def`].
     #[error("def `{0}`: {1}")]
     Def(String, Box<CheckError>),
 
+    /// Two types failed to unify. Code: `type-mismatch`.
     #[error("type mismatch: expected {expected}, got {got}")]
     TypeMismatch { expected: String, got: String },
 
+    /// A `Term::Var { name }` could not be resolved against locals,
+    /// globals, or the qualified-import path. Code: `unbound-var`.
     #[error("unknown identifier: `{0}`")]
     UnknownIdent(String),
 
+    /// `Term::Do { op }` referenced an op not in
+    /// [`Env::effect_ops`]. Code: `unknown-effect-op`.
     #[error("unknown effect operation: `{0}`")]
     UnknownEffectOp(String),
 
+    /// A non-function value was applied with `Term::App`. Code:
+    /// `not-a-function`.
     #[error("`{0}` is not a function (got {1})")]
     NotAFunction(String, String),
 
+    /// Wrong number of args at a call site. Code: `arity-mismatch`.
     #[error("arity mismatch for `{name}`: expected {expected} args, got {got}")]
     ArityMismatch {
         name: String,
@@ -259,12 +289,18 @@ pub enum CheckError {
         got: usize,
     },
 
+    /// An effect was raised in a body but not listed on the enclosing
+    /// fn's effect row. Code: `undeclared-effect`.
     #[error("undeclared effect `{0}` used in body")]
     UndeclaredEffect(String),
 
+    /// A `Def::Fn` was declared with a non-`Type::Fn` (and non-`Forall<Fn>`)
+    /// type. Code: `fn-type-required`.
     #[error("function type required for fn `{0}`, got {1}")]
     FnTypeRequired(String, String),
 
+    /// `FnDef.params.len()` does not match the parameter list of
+    /// `FnDef.ty`. Code: `param-count-mismatch`.
     #[error("param count mismatch in `{name}`: type has {ty_count}, params has {param_count}")]
     ParamCountMismatch {
         name: String,
@@ -272,21 +308,34 @@ pub enum CheckError {
         param_count: usize,
     },
 
+    /// A `Type::Forall` showed up where the MVP doesn't support
+    /// generalisation (e.g. inside `Def::Const`). Code:
+    /// `polymorphic-not-supported`.
     #[error("polymorphic types not supported in MVP body of `{0}`")]
     PolymorphicNotSupported(String),
 
+    /// A `Def::Const` body raised an effect — illegal because consts are
+    /// pure by construction. Code: `const-has-effects`.
     #[error("const `{0}` may not have effects (got !{1:?})")]
     ConstHasEffects(String, Vec<String>),
 
+    /// A `Type::Con` named a type not in [`Env::types`] or with a wrong
+    /// arity for a parameterised ADT. Code: `unknown-type`.
     #[error("unknown type: `{0}`")]
     UnknownType(String),
 
+    /// A `Term::Ctor` referenced a ctor that doesn't belong to the
+    /// declared ADT. Code: `unknown-ctor`.
     #[error("type `{ty}` has no constructor `{ctor}`")]
     UnknownCtor { ty: String, ctor: String },
 
+    /// A pattern referenced a ctor not in [`Env::ctor_index`]. Code:
+    /// `unknown-ctor-in-pattern`.
     #[error("unknown constructor `{0}` in pattern")]
     UnknownCtorInPattern(String),
 
+    /// Wrong number of fields in a ctor application or pattern. Code:
+    /// `arity-mismatch` (shared with `ArityMismatch`).
     #[error("constructor `{ty}/{ctor}` arity: expected {expected} fields, got {got}")]
     CtorArity {
         ty: String,
@@ -295,33 +344,55 @@ pub enum CheckError {
         got: usize,
     },
 
+    /// A `Term::Match` does not cover every ctor of an ADT (and has no
+    /// open arm). Code: `non-exhaustive-match`. `ctx` carries the
+    /// `missing` ctor names.
     #[error("non-exhaustive match on `{ty}`: missing cases {missing:?}")]
     NonExhaustive { ty: String, missing: Vec<String> },
 
+    /// A `Term::Match` on a primitive type lacks a wildcard or var arm.
+    /// Code: `primitive-needs-wildcard`.
     #[error("primitive type `{0}` requires a wildcard or variable arm in match")]
     PrimitiveNeedsWildcard(String),
 
+    /// A `Pattern::Ctor` was matched against a value of a different ADT.
+    /// Code: `pattern-type-mismatch`.
     #[error("cannot match constructor pattern `{ctor}` against type `{ty}`")]
     PatternTypeMismatch { ctor: String, ty: String },
 
+    /// Two `Def::Type` defs share a name. Code: `duplicate-type`.
     #[error("duplicate type definition: `{0}`")]
     DuplicateType(String),
 
+    /// Same ctor name registered in two different ADTs. Code:
+    /// `duplicate-ctor`.
     #[error("duplicate constructor: `{ctor}` (in types `{a}` and `{b}`)")]
     DuplicateCtor { ctor: String, a: String, b: String },
 
+    /// Two top-level defs in the same module share a name. Code:
+    /// `duplicate-def`.
     #[error("duplicate definition: `{0}`")]
     DuplicateDef(String),
 
+    /// A `Pattern::Ctor` has a non-`Var`/non-`Wild` sub-pattern. The
+    /// MVP forbids decision-tree lowering of nested patterns. Code:
+    /// `nested-ctor-pattern-not-allowed`.
     #[error("nested constructor pattern not allowed in MVP: `{0}`")]
     NestedCtorPatternNotAllowed(String),
 
+    /// A qualified `Term::Var { name: "<m>.<n>" }` references a module
+    /// alias not declared in the current module's imports. Code:
+    /// `unknown-module`.
     #[error("unknown module prefix `{module}` in qualified reference")]
     UnknownModule { module: String },
 
+    /// The aliased module exists but does not export the named def.
+    /// Code: `unknown-import`.
     #[error("module `{module}` has no top-level def `{name}`")]
     UnknownImport { module: String, name: String },
 
+    /// A def was declared with a name containing `.`, which is reserved
+    /// for qualified cross-module references. Code: `invalid-def-name`.
     #[error("invalid def name `{name}`: contains `.` (reserved for qualified refs)")]
     InvalidDefName { name: String },
 }
@@ -419,6 +490,10 @@ impl CheckError {
         format!("{}", self.inner())
     }
 
+    /// Lowers this error into the public [`Diagnostic`] shape consumed
+    /// by `ail check --json`. Pulls `code`, `message`, and `ctx` through
+    /// the recursive accessors and attaches the optional def name from
+    /// any wrapping [`CheckError::Def`].
     pub fn to_diagnostic(&self) -> Diagnostic {
         let mut d = Diagnostic::error(self.code(), self.message()).with_ctx(self.ctx());
         if let Some(name) = self.def() {
@@ -468,7 +543,7 @@ pub fn check_module(m: &Module) -> Vec<Diagnostic> {
 /// if imported without an alias).
 ///
 /// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
-/// Pass-1 (symbol table) stays fail-fast — see `check_module`.
+/// Pass-1 (symbol table) stays fail-fast — see [`check_module`].
 /// Module iteration order is deterministic: entry first, then the rest in
 /// BTreeMap order, so output ordering is stable.
 pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
@@ -508,9 +583,21 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
 /// (type, hash) — ready for `manifest` output.
 #[derive(Debug, Clone)]
 pub struct CheckedModule {
+    /// Top-level symbols of the module in declaration order. The value
+    /// is `(declared_type, content_hash)` — the hash is the BLAKE3 def
+    /// hash from `ailang_core::hash::def_hash`, used by `ail diff` and
+    /// the cross-module manifest.
     pub symbols: IndexMap<String, (Type, String)>,
 }
 
+/// Single-error entry point. Typechecks `m` standalone (trivial
+/// workspace), returning a [`CheckedModule`] with the symbol-to-hash
+/// table on success or the **first** [`CheckError`] on failure.
+///
+/// Prefer [`check_module`] for new callers — it returns
+/// `Vec<Diagnostic>` (multi-diagnose, JSON-ready). This function is
+/// kept for legacy callers (snapshot tests, the `manifest` codepath
+/// that needs the hash-to-type mapping).
 pub fn check(m: &Module) -> Result<CheckedModule> {
     // Trivial workspace: the module alone, without cross-module resolution.
     let mut modules = BTreeMap::new();
@@ -1247,10 +1334,33 @@ fn expect_eq(expected: &Type, got: &Type) -> Result<()> {
     }
 }
 
+/// Typechecker environment for a single module-check pass.
+///
+/// Cloned cheaply when we need a scoped extension (e.g. installing
+/// rigid vars while checking a polymorphic def's body) so that the
+/// parent scope stays immutable. Construction goes through
+/// [`Env::default`] / the internal `new`; population is the
+/// responsibility of [`builtins::install`] and the per-module setup in
+/// `check_in_workspace`.
+///
+/// Several of the fields are conceptually disjoint name-spaces (term
+/// vars vs effect ops vs ADT names vs ctor names), kept as separate
+/// maps because the AST already commits to which channel a reference
+/// goes through (`Term::Var` vs `Term::Do` vs `Term::Ctor` vs
+/// `Pattern::Ctor`).
 #[derive(Debug, Default, Clone)]
 pub struct Env {
+    /// Term-level names in scope — built-in operators, user fn/const
+    /// defs of the current module, and (after pass-1) an entry per
+    /// local def. Looked up by `Term::Var { name }` lookup.
     pub globals: IndexMap<String, Type>,
+    /// Effect-op table. Looked up by `Term::Do { op }`. See
+    /// [`builtins::EffectOpSig`] for the payload shape.
     pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
+    /// User-declared ADTs of the current module, by name. Populated
+    /// from `Def::Type` entries; consulted by `Term::Ctor`,
+    /// `Pattern::Ctor`, and the well-formedness check on declared
+    /// types.
     pub types: IndexMap<String, TypeDef>,
     /// Inverse index: ctor name -> reference to the owning ADT.
     pub ctor_index: IndexMap<String, CtorRef>,
@@ -1272,8 +1382,13 @@ pub struct Env {
     pub rigid_vars: BTreeSet<String>,
 }
 
+/// Back-pointer from a ctor name to the ADT that declared it. Stored
+/// in [`Env::ctor_index`] so a `Pattern::Ctor` or `Term::Ctor` can
+/// resolve the owning ADT in O(1).
 #[derive(Debug, Clone)]
 pub struct CtorRef {
+    /// Name of the ADT (i.e. the `Def::Type` name) that declared the
+    /// ctor.
     pub type_name: String,
 }
 

docs/JOURNAL.md

@@ -1242,3 +1242,73 @@ After 13d there's no urgency on 13e/f — `cargo doc` is already
 warning-free. They're "polish iterations to be slotted in
 between feature iters when context budget is short". 14a
 (`List a` rewrite) remains the next-feature default.
+
+## Iter 13e — rustdoc polish for `ailang-check`
+
+Second docwriter mission. Same mandate as 13d, applied to the
+typechecker crate. `lib.rs` (1922 LOC) had a strong crate root
+already — covers HM-with-effects, top-level forall, the
+rigid-vs-metavar split, the `$m<id>` encoding — but its `pub`
+surface (the `Env` struct, `CheckError` + 24 variants,
+`CheckedModule`, `CtorRef`, the `check_module` entry point) was
+mostly undocumented. `builtins.rs` had a one-line module
+header and zero `///` strings on `EffectOpSig` or `install`.
+`diagnostic.rs` had a strong module header (lists every stable
+diagnostic code) but `Diagnostic`, `Severity`, and the
+construction helpers were undocumented.
+
+Agent added 188 LOC of pure rustdoc across the three files; no
+non-doc lines changed (verified by filtering the diff). Each
+`CheckError` variant now carries the AST term/type that
+triggers it and the stable kebab-case `code` it maps to. `Env`
+fields (`globals`, `effect_ops`, `types`, `module_globals`,
+`current_module`) got individual `///` strings that name the
+invariants — most importantly that `module_globals` includes
+the current module, which the agent flagged as undocumented at
+field level (now fixed). Crate-root prose got an upgraded
+intra-doc link to `[`check_module`]`; `super::` reference in
+`diagnostic.rs` rewritten to `crate::` (cosmetic, but the
+canonical form).
+
+**Findings reported** (judgement deferred to me):
+
+- `Env` is `pub` with all-`pub` fields but `Env::new` is
+  private and there's no public builder — external callers can
+  only construct via field-by-field literal, which is fragile
+  if a field is added later. **Not fixing**: changing this is
+  an API decision, not a doc one. Worth raising next time we
+  touch the crate's public surface deliberately.
+- `CheckError::CtorArity` and `CheckError::ArityMismatch` both
+  serialize to the public diagnostic code `arity-mismatch`. The
+  `///` strings now flag the collision per-variant; tooling
+  that consumes the diagnostic JSON sees only the merged code
+  and that's intentional from the iter-5b vintage. **Not
+  fixing.**
+- `Diagnostic` and `Severity` are reachable both via the crate
+  re-export and via `crate::diagnostic::*` because the
+  `diagnostic` module is itself `pub`. Rustdoc renders both
+  pages; harmless but slightly noisy. **Not fixing**: the
+  re-export is the documented entry point and we don't want to
+  hide the module.
+
+**Process note.** Same shape as 13d: I wrote a brief naming
+the deficiencies (numbers of pub items, which files had thin
+roots), the agent did the doc additions inside its mandate,
+the orchestrator-side work was authoring DESIGN/JOURNAL and
+verifying the diff. Cost ≈ 32 tool uses for 188 LOC of doc
+across 3 files — denser than 13d (more sentences per pub item
+because the typechecker invariants need explicit
+articulation), but the per-LOC payoff for a future reader is
+also higher.
+
+**Tests:** 64/64 unit + e2e (unchanged), 3 ignored doctests
+(unchanged). `cargo doc --no-deps`: 0 warnings (was 0; the
+agent introduced 4 transient broken-link warnings during the
+work and resolved all of them before reporting done). `cargo
+build --workspace` green. `cargo test --workspace` green.
+
+**Plan 13f / 14a unchanged.** 13f (`ailang-codegen` + `ail`
+CLI) is the natural next polish iter; 14a (`List a` rewrite of
+`list_map`) remains the next-feature default. Auto-mode is on,
+so I'll continue into 13f directly unless context budget
+pressures a switch.