iter 24.tidy: close 5 actionable drift items from audit-24

Documents the three iter-24.3 strengthenings as load-bearing
invariants and tightens two error-handling sites:

T1: DESIGN.md gains new subsection §Cross-module references in
synthesised bodies (between Resolution-and-monomorphisation and
Defaults-and-superclasses) documenting three invariants installed
in iter 24.3 — (1) MonoTarget::FreeFn::type_args carries canonical
types post-collection via normalize_type_for_lookup; (2) post-mono
synthesised body cross-module refs may bypass the source template's
import_map (codegen falls back to module_user_fns / module_def_ail_types);
(3) FreeFnCall synth pushes one ResidualConstraint per declared
forall-constraint with rigid vars substituted by fresh metavars.

T2: codegen_import_map_fallback_pin.rs (integration test) asserts
the synthesised prelude.print__<IntBox> body references
show_user_adt.show__<IntBox> AND prelude module's imports do not
contain show_user_adt — proving the cross-module ref bypasses
import_map at codegen.

T3: polyfn_dot_qualified_branch_pin.rs (integration test) asserts
bare-name print f (f : Int -> Int) fires exactly one no-instance
diagnostic at typecheck with zero unknown-variable diagnostics —
proving the bare-name resolution reaches the dot-qualified synth
branch where the constraint-residual push fires.

T4: check/lib.rs:2858 unwrap_or_default() replaced with .expect()
carrying the registry-coherence message — class_methods index
drift now surfaces explicitly rather than rendering NoInstance
with an empty method name.

T5: mono.rs gains apply_subst_and_normalize helper (Option<Type>
return) extracted from two byte-identical call sites at
collect_mono_targets and collect_residuals_ordered. Each call site
retains its own rigid-var / unit-default policy in the None arm
(site 1: rigid → has_rigid+break, unbound → Type::unit; site 2:
non-concrete → Type::unit). Byte-identity invariant on mono-symbol
hashes enforced by construction.

Tests: 558 passed (was 556 + 2 new pins). No production semantic
change — pure documentation + test pin + error-handling tightening
+ helper refactor. bench/cross_lang exit 0; bench/compile_check +
bench/check exit 0 this run (latency.implicit_at_rc / latency.explicit_at_rc /
bench_list_sum.bump_s noise envelope unobserved, lineage continues
at 10th consecutive observation without firing this run).

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -0,0 +1,124 @@
+//! Pin for the iter-24.3 codegen `import_map`-fallback path
+//! (DESIGN.md §"Cross-module references in synthesised bodies"
+//! invariant 2).
+//!
+//! Property protected: post-mono synthesised body cross-module
+//! references resolve at codegen via the fallback to
+//! `module_user_fns` / `module_def_ail_types` when the prefix is
+//! NOT in the current module's `import_map`. Specifically, the
+//! synthesised `prelude.print__<UserType>` body references
+//! `<user_module>.show__<UserType>` even though `prelude` does not
+//! import user modules.
+//!
+//! Failure mode this pin catches: a future codegen refactor
+//! tightens `resolve_top_level_fn` or `lower_app`'s cross-module
+//! arm or `synth_with_extras`'s Var arm back to `import_map`-only.
+//! Without this pin, the regression surfaces only at the
+//! `show_user_adt` E2E (which builds + runs a binary, slow to
+//! bisect).
+
+use ailang_check::{check_workspace, monomorphise_workspace};
+use ailang_core::ast::{Def, Term};
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture_path() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join("show_user_adt.ail.json")
+}
+
+#[test]
+fn synthesised_print_uses_user_module_show_via_fallback() {
+    // Step 1: workspace loads + typechecks clean.
+    let ws = load_workspace(&fixture_path()).expect("workspace loads");
+    let diags = check_workspace(&ws);
+    assert!(
+        diags.is_empty(),
+        "typecheck diagnostics in show_user_adt fixture: {diags:?}"
+    );
+
+    // Step 2: mono synthesis produces `prelude.print__<IntBox>` whose
+    // body references `show_user_adt.show__<IntBox>` (cross-module).
+    let post_mono = monomorphise_workspace(&ws).expect("mono green");
+    let prelude_mod = post_mono
+        .modules
+        .get("prelude")
+        .expect("prelude post-mono module present");
+
+    let print_def = prelude_mod
+        .defs
+        .iter()
+        .find_map(|d| match d {
+            Def::Fn(f) if f.name.starts_with("print__") => Some(f),
+            _ => None,
+        })
+        .expect("synthesised print__<UserType> not found in prelude post-mono module");
+
+    // Step 3: recursively walk `print_def.body` looking for a Var
+    // whose name carries the `show_user_adt.` prefix (the cross-
+    // module reference invariant 2 protects).
+    fn contains_xmod_show_var(t: &Term) -> bool {
+        match t {
+            Term::Var { name } => {
+                name.starts_with("show_user_adt.") && name.contains("show__")
+            }
+            Term::Let { value, body, .. } => {
+                contains_xmod_show_var(value) || contains_xmod_show_var(body)
+            }
+            Term::LetRec { body, in_term, .. } => {
+                contains_xmod_show_var(body) || contains_xmod_show_var(in_term)
+            }
+            Term::App { callee, args, .. } => {
+                contains_xmod_show_var(callee) || args.iter().any(contains_xmod_show_var)
+            }
+            Term::Do { args, .. } => args.iter().any(contains_xmod_show_var),
+            Term::Lam { body, .. } => contains_xmod_show_var(body),
+            Term::If { cond, then, else_ } => {
+                contains_xmod_show_var(cond)
+                    || contains_xmod_show_var(then)
+                    || contains_xmod_show_var(else_)
+            }
+            Term::Match { scrutinee, arms } => {
+                contains_xmod_show_var(scrutinee)
+                    || arms.iter().any(|a| contains_xmod_show_var(&a.body))
+            }
+            Term::Ctor { args, .. } => args.iter().any(contains_xmod_show_var),
+            Term::Seq { lhs, rhs } => {
+                contains_xmod_show_var(lhs) || contains_xmod_show_var(rhs)
+            }
+            Term::Clone { value } => contains_xmod_show_var(value),
+            Term::ReuseAs { source, body } => {
+                contains_xmod_show_var(source) || contains_xmod_show_var(body)
+            }
+            Term::Lit { .. } => false,
+        }
+    }
+
+    assert!(
+        contains_xmod_show_var(&print_def.body),
+        "synthesised print body should contain a `show_user_adt.<suffix>` Var \
+         referencing the user-module's show__<IntBox> mono symbol — \
+         this is the cross-module reference codegen resolves via the \
+         import_map-fallback path. Body: {:?}",
+        print_def.body
+    );
+
+    // Step 4: confirm prelude module's `imports` does NOT contain
+    // `show_user_adt` — the resolution at codegen time genuinely
+    // bypasses the source template's import_map.
+    let prelude_src = ws
+        .modules
+        .get("prelude")
+        .expect("prelude source module present");
+    assert!(
+        prelude_src
+            .imports
+            .iter()
+            .all(|imp| imp.module != "show_user_adt"),
+        "prelude must not import show_user_adt (the invariant is that \
+         codegen resolves the cross-module ref WITHOUT going through \
+         import_map). Got imports: {:?}",
+        prelude_src.imports
+    );
+}

crates/ail/tests/polyfn_dot_qualified_branch_pin.rs

@@ -0,0 +1,71 @@
+//! Pin for the iter-24.3 FreeFnCall constraint-residual-push
+//! invariant (DESIGN.md §"Cross-module references in synthesised
+//! bodies" invariant 3).
+//!
+//! Property protected: bare-name references to polymorphic free fns
+//! that resolve through the auto-injected-prelude path AT THE
+//! DOT-QUALIFIED SYNTH BRANCH push residuals for the fn's declared
+//! constraints. The discharge loop then fires `NoInstance` at
+//! typecheck if no instance ships for the unified concrete type.
+//!
+//! Failure mode this pin catches: a future refactor changes the
+//! prelude auto-injection resolution path so that bare-name `print`
+//! reaches synth via a different branch (e.g. locals, env.module_globals
+//! direct hit) that does NOT push residuals. Without this pin, the
+//! regression surfaces as `unknown variable: show` from codegen for
+//! the negative case — confusing diagnostic, hard to bisect.
+
+use ailang_check::check_workspace;
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture_path() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join("show_no_instance.ail.json")
+}
+
+#[test]
+fn bare_name_polyfn_fires_typecheck_no_instance_not_codegen_unknown_var() {
+    // The fixture calls `print f` bare-name (no `prelude.` qualifier)
+    // where `f : Int -> Int`. The auto-injected-prelude resolution
+    // must route this through the dot-qualified synth branch so that
+    // the `Show a` declared constraint of `print` produces a residual,
+    // and the discharge loop fires `no-instance`.
+    let ws = load_workspace(&fixture_path()).expect("workspace loads");
+    let diags = check_workspace(&ws);
+
+    // Exactly one `no-instance` diagnostic — proves:
+    //   (a) the bare-name `print` resolved (was not "unknown variable")
+    //   (b) the resolution reached the dot-qualified synth branch
+    //       which pushes the declared-constraint residual
+    //   (c) the discharge loop ran with the residual and fired the
+    //       NoInstance because no `Show (Int -> Int)` instance exists.
+    let no_inst: Vec<_> = diags.iter().filter(|d| d.code == "no-instance").collect();
+    assert_eq!(
+        no_inst.len(),
+        1,
+        "expected exactly one 'no-instance' diagnostic — got {} (all diags: {diags:?})",
+        no_inst.len()
+    );
+
+    // No "unknown variable" or other codegen-grade errors at typecheck:
+    // if the residual push did NOT fire, the typecheck would pass
+    // silently and the error would only surface at codegen.
+    let unknown_vars: Vec<_> = diags
+        .iter()
+        .filter(|d| {
+            d.code == "unknown-variable"
+                || d.message.contains("unknown variable")
+                || d.code == "internal"
+        })
+        .collect();
+    assert!(
+        unknown_vars.is_empty(),
+        "expected zero 'unknown variable' or 'internal' diagnostics at typecheck — \
+         got {} (all diags: {diags:?}). If this fires, the bare-name `print` \
+         resolution bypassed the dot-qualified synth branch and the constraint \
+         residual was never pushed.",
+        unknown_vars.len()
+    );
+}