docs: correct stale mono.rs module header — pass is implemented, not a skeleton

The module-level doc still described the iter-22b.3 Task-1 state
("no-op skeleton", "Planned (later tasks)", "eventual-state"
invariant) though later 22b.3 + 23.4 tasks filled in the full
synthesis fixpoint and call-site rewrite. Rewrite the header in
present tense to describe the implemented pass (early-out,
ClassMethod/FreeFn fixpoint, call-site rewrite, symbol-hashing
invariant as a current fact). No code change; same doc-honesty
class as a29700c (effect-doc-honesty).

crates/ailang-check/src/mono.rs

@@ -1,55 +1,59 @@
-//! Iter 22b.3: workspace monomorphisation pass.
+//! Workspace monomorphisation pass (introduced iter 22b.3; the
+//! free-fn entry was added in iter 23.4).
 //!
 //! Slots into the build pipeline after [`crate::lift_letrecs`] and
-//! before `ailang_codegen::lower_workspace_with_alloc`.
+//! before `ailang_codegen::lower_workspace_with_alloc`. It is only
+//! on the `build` / `run` paths — `ail check` stops at typecheck and
+//! never runs this pass.
 //!
-//! ## What Task 1 delivers
+//! ## What the pass does
 //!
-//! Skeleton only. [`monomorphise_workspace`] is a no-op pass with
-//! two branches:
+//! [`monomorphise_workspace`] turns a polymorphic, typechecked
+//! workspace into a fully monomorphic one that codegen can lower
+//! without any instance dispatch or `Type::Forall` instantiation:
 //!
-//! - Class-free workspaces (no [`Def::Class`] / [`Def::Instance`]
-//!   anywhere) take the early-out and the input workspace is
-//!   cloned unchanged.
-//! - Class-present workspaces fall through to a second
-//!   `Ok(ws.clone())`, dead-equivalent today but the placeholder
-//!   for the real fixpoint body that later tasks will fill in.
-//!
-//! Both branches return a byte-identical workspace clone, so
-//! `module_hash` is preserved end-to-end through the pass at this
-//! stage of the iteration.
-//!
-//! ## Planned (later tasks in iter 22b.3)
-//!
-//! See `docs/plans/2026-05-09-22b3-monomorphisation.md` for the
-//! full task list. The eventual contract is for the pass to
-//! consume the workspace's typeclass [`ailang_core::workspace::Registry`] and the per-
-//! module class-method tables (already populated by
-//! `crate::check_in_workspace`) and produce a workspace with:
-//!
-//! 1. Synthesised [`Def::Fn`] entries — one per unique
-//!    `(class, method, type-hash)` triple observed at any
-//!    class-method call site — appended to the registry's
-//!    `defining_module` for that instance.
-//! 2. Rewritten call sites — every `Term::Var { name }` whose
-//!    `name` resolves through `crate::Env::class_methods` is replaced
-//!    by the corresponding mono-symbol name (qualified with the
-//!    instance's `defining_module` iff that module differs from
-//!    the calling module).
+//! - **Early-out.** Workspaces with no specialisable targets
+//!   (`workspace_has_specialisable_targets` — no resolvable
+//!   class-method call sites and no concretely-instantiated
+//!   polymorphic free fns) are returned cloned unchanged, so their
+//!   `module_hash` is preserved bit-for-bit.
+//! - **Synthesis fixpoint.** Otherwise the pass repeatedly walks
+//!   every fn / const body in every module, collecting
+//!   [`MonoTarget`]s, and synthesises one top-level [`Def::Fn`] per
+//!   unique target, appended to that target's `defining_module`.
+//!   Two target kinds share one fixpoint:
+//!     1. `MonoTarget::ClassMethod` — the resolved instance body is
+//!        looked up via [`ailang_core::workspace::Registry`], the
+//!        class parameter substituted to the concrete type, and a
+//!        `<method>__<type>` fn synthesised.
+//!     2. `MonoTarget::FreeFn` — a `Type::Forall` free fn called at
+//!        a fully-concrete substitution; the source body is taken
+//!        directly and rigid-var-substituted into a
+//!        `<name>__<type>…` fn.
+//!   The loop re-walks bodies added by the previous round, which is
+//!   what closes it over chained class-method calls (e.g.
+//!   `Eq.ne x y = not (eq x y)`). Targets are deduplicated within a
+//!   round and across rounds via [`mono_target_key`].
+//! - **Call-site rewrite.** A final pass rewrites every
+//!   class-method / poly-free-fn `Term::Var` to its synthesised
+//!   mono-symbol name (qualified with the instance's
+//!   `defining_module` when it differs from the calling module),
+//!   using a cursor aligned position-by-position with
+//!   `collect_residuals_ordered`.
 //!
 //! Pre-existing `Def::Class` and `Def::Instance` entries are
 //! preserved verbatim — codegen ignores them, but downstream
 //! tooling (e.g. `ail describe`) may still consult them.
 //!
-//! ## Symbol-hashing invariant (eventual-state)
+//! ## Symbol-hashing invariant
 //!
-//! Once the synthesis body lands, synthesised FnDefs will be
-//! post-typecheck artefacts. They will NOT enter
-//! `CheckedModule.symbols` (built from the original module at
-//! typecheck time and used by `ail diff` / `ail manifest`). Same
-//! convention as [`crate::lift_letrecs`]. Documented here ahead of
-//! the implementation so the constraint is visible to anyone
-//! extending the skeleton.
+//! Synthesised FnDefs are post-typecheck artefacts. They do NOT
+//! enter `CheckedModule.symbols` (built from the original on-disk
+//! module at typecheck time and used by `ail diff` / `ail manifest`),
+//! same convention as [`crate::lift_letrecs`]. The early-out path
+//! additionally guarantees byte-identical workspace output —
+//! `module_hash` is unchanged end-to-end for any workspace with no
+//! monomorphisation targets.
 
 use ailang_core::ast::{Arm, ClassDef, ConstDef, Def, FnDef as AstFnDef, InstanceDef, Pattern, Term, Type};
 use ailang_core::workspace::Workspace;