Iter 13d: rustdoc polish for ailang-core + new docwriter agent

Adds ailang-docwriter to /agents/ — a recurring role for keeping
crate-, module-, and pub-item-level rustdoc accurate. First mission:
ailang-core. Crate root, every module root, every pub item documented;
intra-doc links throughout; Iter-13a additions (TypeDef.vars, Type::Con.args)
get an explicit backwards-compat note. Two stale broken-link warnings in
ailang-check fixed in passing. cargo doc --no-deps now warning-free across
the workspace; promoted to verification invariant 6 in DESIGN.md.

crates/ailang-core/src/pretty.rs

@@ -1,12 +1,29 @@
 //! Pretty-printer: AST → human-readable text form.
 //!
-//! The text form is intended as a diff and review tool. The
-//! canonical source remains the JSON form. Every pretty output is
-//! deterministic.
+//! The text form is intended for diff and review (LLM and human eyes).
+//! The canonical source remains the JSON form, and the pretty output
+//! is deliberately one-way: there is no parser back from text into AST
+//! in this crate. Every pretty output is deterministic.
+//!
+//! Two top-level renderers are provided:
+//! - [`module`] — full S-expression dump of every definition.
+//! - [`manifest`] — one-line summary per def with its type and
+//!   [`crate::def_hash`].
+//!
+//! Helpers [`pattern_to_string`] and [`type_to_string`] are exposed
+//! because diagnostics in `ailang-check` reuse them in error messages.
+//!
+//! This module deliberately does **not** roundtrip text back to AST
+//! and does not attempt to mirror canonical JSON byte-for-byte.
 
 use crate::ast::*;
 use std::fmt::Write;
 
+/// Render a complete [`Module`] as an S-expression-style text block.
+///
+/// Output format is stable but not part of the on-disk schema —
+/// consumers should treat it as documentation, not a serialization
+/// format. Used by `ail print` and by the pretty-print review flow.
 pub fn module(m: &Module) -> String {
     let mut s = String::new();
     writeln!(s, "(module {}", m.name).unwrap();
@@ -31,6 +48,12 @@ pub fn module(m: &Module) -> String {
     s
 }
 
+/// Render a one-line-per-def manifest of a [`Module`].
+///
+/// Each line carries the def kind keyword (`fn` / `const` / `type`),
+/// the name padded to a fixed width, the rendered type, and the
+/// 16-hex-char [`crate::def_hash`] in brackets. Used by `ail manifest`
+/// and as the canonical "what's in this module" summary.
 pub fn manifest(m: &Module) -> String {
     let mut s = String::new();
     writeln!(s, "module {}", m.name).unwrap();
@@ -246,6 +269,10 @@ fn term_block(t: &Term, indent: usize) -> String {
     }
 }
 
+/// Render a [`Pattern`] as a single-line string.
+///
+/// Used both internally by [`module`] for match arms and externally by
+/// `ailang-check` when constructing diagnostic messages.
 pub fn pattern_to_string(p: &Pattern) -> String {
     match p {
         Pattern::Wild => "_".into(),
@@ -340,6 +367,13 @@ fn lit_to_string(l: &Literal) -> String {
     }
 }
 
+/// Render a [`Type`] as a single-line string.
+///
+/// The format mirrors typical ML-family notation: type-constructor
+/// applications use angle brackets (`List<Int>`), function types use
+/// arrow syntax (`(Int, Int) -> Int`) with optional `!eff1,eff2`
+/// effect suffixes, and `Forall` becomes `forall a b. ...`. Used by
+/// [`manifest`] and by `ailang-check` diagnostics.
 pub fn type_to_string(t: &Type) -> String {
     match t {
         Type::Con { name, args } => {