AILang/docs/plans/0058-24.tidy.md

iter 24.tidy — close 5 actionable drift items from audit-24 — Implementation Plan

Parent spec: docs/journals/2026-05-13-audit-24.md (the audit-24 drift report functions as the spec for this tidy iter — mirror of the mq.tidy pattern).

For agentic workers: REQUIRED SUB-SKILL: use skills/implement to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Close the 5 actionable drift items audit-24 surfaced — documenting the three iter-24.3 strengthenings as load-bearing invariants in DESIGN.md, pinning the codegen import_map-fallback path with an integration test, asserting the dot-qualified-branch invariant for bare-name poly free fns, tightening the unwrap_or_default() method-name fallback to surface class-index drift, and extracting the duplicated normalize_type_for_lookup body into a single helper enforced by construction.

Architecture: This tidy iter is heterogeneous: one DESIGN.md doc-anchor (T1), two new integration test files (T2 + T3), one minimal-edit error-handling tightening (T4), one helper extraction across two mono.rs sites (T5), and one integration verification (T6). All five touch non-overlapping surfaces — the iter can be sequenced in any order, but the recommended order below ships the doc anchor first (lowest risk), refactors second (mechanical, T5), pins third (T2 + T3), tightens fourth (T4), verifies last (T6). No production semantic changes; the iter is documentation + test + refactor only.

Tech Stack: docs/DESIGN.md (one new subsection), ailang-check (one error-handling line + one helper extraction across two sites), two new crates/ail/tests/*.rs integration test files.

---

Pre-flight notes (Boss-ratified post-recon)

Recon-corrected line ranges. Audit-24 named line ranges that recon verified post-iter-24.3:

• mono.rs:687-696 → actual span is :685-714 (full for m in &fc.metas loop).
• mono.rs:1287-1294 → actual span is :1284-1303 (full .map(|m| ...) collector).
• check/lib.rs:2820-2865 → confirmed.
• check/lib.rs:2852-2858 → confirmed, sits inside a for c in constraints loop emitting residuals (not nested in type-inference logic; structurally simple swap).
• codegen/lib.rs:1980-2000, :2200-2244, :2776-2816 → confirmed; all three carry matching // Iter 24.3: comments naming each other (the iter-24.3 implementer already cross-referenced them).

Boss decisions on recon-surfaced open questions:

1. T1 placement: DESIGN.md has no top-level §"Monomorphisation" — it's a subsection of ## Decision 11: typeclasses at line 1478 (### Resolution and monomorphisation at 1620). Insert a new subsection ### Cross-module references in synthesised bodies between line 1693 (end of existing Monomorphisation paragraph) and line 1695 (### Defaults and superclasses). The new subsection groups the three iter-24.3 strengthenings as anchorable / citable invariants.

2. T2 + T3 test placement: Use integration-style tests in crates/ail/tests/ (canonical pattern per mono_xmod_qualified_ref.rs, mono_xmod_ctor_pattern.rs). The codegen crate has rare in-crate tests (crates/ailang-codegen/src/lib.rs:2990, escape.rs:477); adding new #[cfg(test)] modules there would be inconsistent.

3. T5 helper signature: apply_subst_and_normalize(env, module_name, m, subst) -> Option<Type> — extracts only the common concrete-resolved arm. Each call site retains its own divergent rigid-var / unit-default policy: site 1 (collect_mono_targets) sets has_rigid = true + break when the helper returns None from a rigid path; site 2 (collect_residuals_ordered) returns Type::unit() when the helper returns None. The helper signature returning Option<Type> makes the divergence at the call sites explicit by construction.

Registry::normalize_type_for_lookup signature (from crates/ailang-core/src/workspace.rs:127):

pub fn normalize_type_for_lookup(&self, caller_module: &str, t: &Type) -> Type

---

Files this plan creates or modifies

Create:

• crates/ail/tests/codegen_import_map_fallback_pin.rs — T2 pin: post-mono synthesised cross-module reference resolves via the import_map-fallback path.
• crates/ail/tests/polyfn_dot_qualified_branch_pin.rs — T3 pin: bare-name poly-fn refs route through the dot-qualified branch (constraint-residual push fires).

Modify:

• docs/DESIGN.md:1693-1695 — insert new subsection ### Cross-module references in synthesised bodies documenting three iter-24.3 strengthenings.
• crates/ailang-check/src/lib.rs:2852-2858 — replace unwrap_or_default() with explicit .expect(...).
• crates/ailang-check/src/mono.rs:685-714 + :1284-1303 — replace duplicated normalization bodies with single helper call.
• crates/ailang-check/src/mono.rs (or a near anchor) — add the new apply_subst_and_normalize helper.

---

Task 1: DESIGN.md — new subsection documenting iter-24.3 strengthenings

Files:

• Modify: docs/DESIGN.md:1693-1695 — insert new subsection.

• Step 1: Confirm DESIGN.md current state at the insertion point.

Run: sed -n '1690,1700p' docs/DESIGN.md

Expected output: the end of the ### Resolution and monomorphisation paragraph at line 1693, followed by line 1694 (likely blank), then ### Defaults and superclasses at line 1695. If the structure differs (e.g. another subsection has been added since recon), adjust the insertion line.

• Step 2: Insert the new subsection.

Insert after line 1693 (after the closing paragraph of ### Resolution and monomorphisation), before line 1695 (### Defaults and superclasses):

### Cross-module references in synthesised bodies

The unified mono pass (per Decision 11's milestone-23.4 reorganisation)
synthesises mono symbols for polymorphic free fns and class-method
instances in the symbol's owner module — e.g. `print__Int` lives in
`prelude` (because `print` is defined in the prelude), but a
user-ADT call site `print (MkIntBox 7)` causes synthesis of
`prelude.print__IntBox` whose body references
`show_user_adt.show__IntBox` (the user instance lives in the
user-defining module per Decision 11 coherence). The synthesised body
crosses a module boundary the source template did not.

Three invariants make this work, all installed in milestone 24's iter
24.3 and worth keeping load-bearing:

1. **`MonoTarget::FreeFn::type_args` carries canonical types
   post-collection.** At every site where `subst.apply(m)` produces a
   concrete substitution that enters `MonoTarget::FreeFn::type_args`
   (`crates/ailang-check/src/mono.rs::collect_mono_targets` and
   `::collect_residuals_ordered`), the resolved `Type` must be passed
   through `Registry::normalize_type_for_lookup(caller_module, &t)`
   before being pushed. The downstream synthesised body's Phase 3
   rewrite cursor (which runs in the OWNER module's context, not the
   caller's) keys lookups in `Registry::entries` by the canonical
   qualified form; a bare type-con reference at the type_args layer
   silently drops the cross-module mono-symbol synthesis and leaves a
   bare `Var "show"` post-mono that codegen later rejects with
   `unknown variable`.

2. **Post-mono synthesised body cross-module references may bypass
   the source template's `import_map`.** `prelude` does not import
   user modules (the auto-injection runs one-way: user workspaces
   import prelude, never the inverse). But a synthesised body for
   `prelude.print__<UserType>` references `<user_module>.show__<UserType>`,
   created by mono — not by the prelude source. Codegen's
   cross-module name-resolution must accept this: at
   `crates/ailang-codegen/src/lib.rs::resolve_top_level_fn` (Var-
   resolution), `::lower_app`'s cross-module call arm, and
   `::synth_with_extras`'s Var arm, the resolution first tries the
   current module's `import_map`, then falls back to a direct
   `module_user_fns` / `module_def_ail_types` lookup against the
   prefix. Both ends were independently typechecked under their own
   module contexts before mono ran; the cross-module reference is a
   post-mono construct, not a source-language one.

3. **FreeFnCall synth pushes one residual per declared forall-
   constraint.** At `crates/ailang-check/src/lib.rs`'s synth Var arm
   for the `prefix.suffix` free-fn path, when the type is a
   `Type::Forall { vars, constraints, body }`, instantiation produces
   fresh metavars for the `vars` AND pushes one `ResidualConstraint`
   per entry in `constraints` (with rigid vars substituted by the
   freshly-generated metavars). The downstream discharge loop at
   `check_fn`'s post-synth phase resolves each residual against the
   workspace registry; if no instance satisfies the residual at the
   unified concrete type, the `NoInstance` diagnostic fires at
   typecheck (correctly), not at codegen (confusingly). Without the
   residual push, milestone-23-shape negative cases (e.g. `print f`
   where `f : Int -> Int`) silently typecheck and surface as
   `unknown variable: show` from codegen instead of the right
   typecheck-phase NoInstance Show.

The three invariants are lockstep partners: invariant (1) creates the
cross-module reference, invariant (2) makes codegen able to resolve
it, invariant (3) makes the typecheck-time discharge fire correctly
when no instance exists. A future refactor that loosens any one of
the three breaks the user-ADT trajectory; the test pins at
`crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
`crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
+ lockstep), and the existing `crates/ail/tests/show_user_adt`
fixture (full trajectory) collectively protect the contract.

• Step 3: Verify DESIGN.md still parses.

Run: wc -l docs/DESIGN.md

Expected: line count grew by ~50-55 lines compared to post-iter-24.3 baseline (was at ~2707-2710 lines).

Run: sed -n '1693,1755p' docs/DESIGN.md

Expected: new ### Cross-module references in synthesised bodies subsection visible, terminated by the existing ### Defaults and superclasses header.

---

Task 2: Codegen import_map-fallback path pin

Files:

• Create: crates/ail/tests/codegen_import_map_fallback_pin.rs — integration-style test.

• Step 1: Read the canonical xmod-integration-test pattern.

Run: head -60 crates/ail/tests/mono_xmod_qualified_ref.rs

Confirm: the file loads a workspace via load_workspace, runs check_workspace + monomorphise_workspace, then either inspects post-mono state OR runs ail build for full E2E. The pattern's signature features are: workspace from examples/, post-mono inspection assertions, doc-comment header naming the regression.

• Step 2: Write the test file.

Note: the existing examples/show_user_adt.ail.json fixture already exercises the import_map-fallback path end-to-end. The pin's job is to make the failure mode visible at unit-test granularity: when codegen tightens resolve_top_level_fn back to import_map-only, the pin fires with a localised assertion BEFORE the E2E reports a cryptic build failure.

//! 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).
    // The exact type-suffix is content-addressed; we look for a
    // `Def::Fn` whose name starts with `print__` AND whose body
    // contains a `Term::Var { name: "show_user_adt.<suffix>" }` (or
    // analogous post-mono shape with the fully-qualified suffix).
    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::App { fn: f, args } => {
                contains_xmod_show_var(f) || 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),
            _ => 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 != "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
    );
}

If the AST Term variants are named differently (e.g. Term::Application vs Term::App), adjust the pattern match. The load-bearing assertions are (a) the synthesised body contains a cross-module Var reference whose prefix is the user module, and (b) the prelude source-level module does not import the user module.

If the WorkspaceModule struct does not expose an imports field directly (recon did not verify this), the implementer adapts to the actual field name (could be module_imports, deps, or accessed via a method).

• Step 3: Run the test.

Run: cargo test --workspace --no-fail-fast -p ail --test codegen_import_map_fallback_pin 2>&1 | tail -10

Expected: test result: ok. 1 passed.

If the test fails with "synthesised print__ not found": the iter-24.3 mono synthesis path was inadvertently broken; the implementer should NOT just adjust the test — surface to Boss because invariant 1 from Task 1 is at risk.

If the test fails with "synthesised print body should contain a show_user_adt.<suffix> Var": the mono synthesis is producing the symbol but the body does not reference the user module — likely the iter-24.3 strengthening at mono.rs::collect_mono_targets was reverted or the test's recursive walker is missing a Term variant. Read the actual print_def.body shape from the failure message and adapt the walker.

---

Task 3: Bare-name poly-fn dot-qualified-branch invariant pin

Files:

• Create: crates/ail/tests/polyfn_dot_qualified_branch_pin.rs — integration-style test.

• Step 1: Write the test file.

The invariant per audit-24 [high-3]: "poly free fns always reach synth via the dot-qualified branch". For prelude poly fns (ne/lt/le/gt/ge/print), the auto-injected prelude path makes bare-name references resolve via the prefix.suffix synth arm internally. The pin asserts the observable consequence: calling a prelude poly fn by bare name AT A CONCRETE TYPE (where the constraint is satisfied) succeeds, AND calling it at a TYPE WITH NO INSTANCE fails with the NoInstance diagnostic (proving the constraint-residual push fired even via bare-name path).

This pin overlaps slightly with the existing show_print_e2e (positive) and show_no_instance_e2e (negative) tests — but those run via ail build / check_workspace on the show fixtures. The new pin uses a synthetic minimal fixture that exercises the bare-name path explicitly and asserts on the synth-level outcome (residual count or diagnostic presence) rather than full E2E.

//! 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()
    );
}

The pin's load-bearing assertions are: (a) exactly one no-instance diagnostic fires (proving the residual push reached the discharge); (b) zero unknown-variable / internal diagnostics (proving the bare-name print resolved at typecheck rather than silently slipping through to codegen).

If the diagnostic .code field names differ (e.g. no_instance rather than no-instance, or unknown_var rather than unknown-variable), adjust to match what crates/ail/tests/show_no_instance_e2e.rs already uses (the iter-24.3 implementer verified that code).

• Step 2: Run the test.

Run: cargo test --workspace --no-fail-fast -p ail --test polyfn_dot_qualified_branch_pin 2>&1 | tail -10

Expected: test result: ok. 1 passed.

If expected exactly one 'no-instance' diagnostic — got 0: the FreeFnCall constraint-residual push at check/lib.rs:2820-2865 was reverted or the bare-name resolution bypassed it. Surface to Boss because invariant 3 from Task 1 is at risk.

If expected zero 'unknown variable' diagnostics: the typecheck-time NoInstance is firing but ALSO an unknown-var is firing — the synthesised body's mono-symbol rewrite did not happen, suggesting invariant 1 (canonical-form type_args) is at risk.

---

Task 4: Replace unwrap_or_default() with explicit .expect(...)

Files:

• Modify: crates/ailang-check/src/lib.rs:2852-2858.

• Step 1: Read the current shape.

Run: sed -n '2846,2865p' crates/ailang-check/src/lib.rs

Confirm: the for c in constraints loop contains a .find_map block producing Option<String> for the method name, with .unwrap_or_default() extracting it. The surrounding code constructs a ResidualConstraint { class, type_, method, candidates: None }.

• Step 2: Swap the fallback.

Use Edit tool to replace the unwrap_or_default() call with an explicit .expect(...) carrying the registry-coherence message:

Concretely (adapting to the actual let method_name = ... line shape at :2852):

let method_name = env
    .class_methods
    .iter()
    .find_map(|((cls, m), _)| {
        if *cls == c_class { Some(m.clone()) } else { None }
    })
    .expect(
        "class_methods registry coherence — a declared constraint's \
         class is missing from env.class_methods. The pre-pass \
         `MissingClass` diagnostic should have rejected this earlier; \
         reaching here means workspace-registry / class-index drift. \
         Surface to debug skill rather than silently render NoInstance \
         with an empty method name.",
    );

The exact pattern of the find_map arm depends on the actual class_methods key type — the recon confirmed it's (class_name: String, method_name: String) -> ClassMethodInfo. If the iteration shape uses a different destructuring, adapt to match.

• Step 3: Run the full workspace test to confirm no regression.

Run: cargo test --workspace --no-fail-fast 2>&1 | tail -5

Expected: test result: ok. 556 passed; 0 failed.

If any test fails with the new .expect(...) panic message: the registry-coherence invariant was already being violated somewhere — the unwrap_or_default() was masking a real bug. Read the panic trace from the failure and decide:

• (a) the violation is in test fixture setup → fix the fixture
• (b) the violation is in production code → surface to Boss, this is a real registry/index drift bug

If 556 tests pass: the .expect(...) is a strict tightening; no regression.

---

Task 5: Extract apply_subst_and_normalize helper

Files:

• Modify: crates/ailang-check/src/mono.rs:685-714 + :1284-1303 — replace duplicated bodies with helper calls.

• Modify: crates/ailang-check/src/mono.rs — add new helper definition near the existing normalize_type_for_lookup callers (or at the top of the file alongside other private helpers).

• Step 1: Read both call sites.

Run: sed -n '685,716p' crates/ailang-check/src/mono.rs

Confirm: this is site 1, the for m in &fc.metas loop in collect_mono_targets. The block has three branches: concrete → normalise + push; rigid → break + set has_rigid; otherwise → (default behaviour, possibly continue).

Run: sed -n '1284,1305p' crates/ailang-check/src/mono.rs

Confirm: this is site 2, the .map(|m| ...) collector. The block has two branches: concrete → normalise; otherwise → Type::unit().

• Step 2: Write the helper.

Add the helper near the top of mono.rs (after the imports / type defs but before collect_mono_targets):

/// Apply the current substitution to a meta and, if the result is
/// fully concrete, normalise it to canonical-form for registry lookup.
///
/// Returns `Some(normalised)` if the meta resolves to a concrete type;
/// `None` if it does not (rigid var or unbound meta — the caller
/// decides the policy: break with `has_rigid = true` at the FreeFn
/// target-collection site, or `Type::unit()`-default at the residual-
/// ordering site).
///
/// Iter 24.tidy: extracted from two byte-identical call sites at
/// `collect_mono_targets` and `collect_residuals_ordered` per
/// audit-24's [medium-2] drift item. The byte-identity invariant
/// (Phase 2 synthesis name must match Phase 3 rewrite cursor's
/// lookup name) is now enforced by construction.
fn apply_subst_and_normalize(
    env: &Env,
    module_name: &str,
    m: &MetaVar,
    subst: &Subst,
) -> Option<Type> {
    let resolved = subst.apply(m);
    if crate::is_fully_concrete(&resolved) {
        Some(env.workspace_registry.normalize_type_for_lookup(module_name, &resolved))
    } else {
        None
    }
}

Adapt the parameter types to the actual signatures (&Env, &MetaVar, &Subst) — recon confirmed the funnel is env.workspace_registry.normalize_type_for_lookup(module_name, &resolved). If Env is a different type name in this scope (e.g. CheckEnv, WorkspaceState), the implementer adapts.

If Subst is not in scope at the helper insertion point, the helper may need to live inside an impl block on the type that owns the substitution context, OR take it as &Subst<...>-generic if it's parametric.

• Step 3: Replace site 1 (collect_mono_targets).

Replace the existing for m in &fc.metas { let resolved = subst.apply(m); ... } block with:

for m in &fc.metas {
    match apply_subst_and_normalize(env, module_name, m, subst) {
        Some(normalised) => type_args.push(normalised),
        None => {
            if contains_rigid_var(&subst.apply(m)) {
                has_rigid = true;
                break;
            }
            // Unbound meta (neither concrete nor rigid): default policy
            // is fall through to existing behaviour at this site.
            // (The original code had no explicit `else` arm after the
            // rigid check — the for loop simply continues to the next
            // meta without pushing. The new shape preserves this.)
        }
    }
}

The exact policy after "neither concrete nor rigid" depends on the original code's pre-extraction behaviour — recon noted "site 1 sets has_rigid = true and breaks" for the rigid path but did not enumerate the unbound-meta path. The implementer reads the pre-extraction block and preserves whatever the original did (likely a continue without push).

• Step 4: Replace site 2 (collect_residuals_ordered).

Replace the existing .map(|m| { let resolved = subst.apply(m); ... }) block with:

.map(|m| {
    apply_subst_and_normalize(env, module_name, m, subst)
        .unwrap_or_else(Type::unit)
})

The unwrap_or_else(Type::unit) preserves the existing fallback semantics for the non-concrete path.

• Step 5: Run the full workspace test to confirm byte-identity preserved.

Run: cargo test --workspace --no-fail-fast 2>&1 | tail -5

Expected: test result: ok. 556 passed; 0 failed.

The byte-identity invariant means the mono-symbol names produced post-extraction MUST match the names produced pre-extraction. If mono_hash_stability::primitive_eq_ord_mono_symbol_hashes_stay_bit_identical or primitive_show_mono_symbol_hashes_stay_bit_identical fail, the extraction inadvertently changed the normalisation form. Diagnose by running:

cargo test --workspace --no-fail-fast -p ail --test mono_hash_stability 2>&1 | tail -15

If hashes drifted: revert and re-do the extraction more carefully — the helper must produce byte-identical output to the inlined code it replaces.

---

Task 6: Integration verification + bench

Files: none modified; verification-only.

• Step 1: Full workspace test.

Run: cargo test --workspace --no-fail-fast 2>&1 | grep -E '^test result' | awk '{s+=$4; f+=$6} END {print "passed:", s, "failed:", f}'

Expected: passed: 558 failed: 0 — 556 from iter 24.3 + 2 new (codegen_import_map_fallback_pin + polyfn_dot_qualified_branch_pin).

If failed is non-zero, diagnose via cargo test --workspace --no-fail-fast 2>&1 | grep -B2 FAILED | head -30.

• Step 2: Confirm milestone-24 specific tests stay green.

Run: cargo test --workspace --no-fail-fast 2>&1 | grep -E '(show_|print_).*FAILED|prelude_free_fns.*FAILED|mono_hash_stability.*FAILED|typeclass_22b.*FAILED|mq3.*FAILED' | head -10

Expected: empty (no FAILED entries for these test groups).

• Step 3: Bench scripts.

Run: bench/compile_check.py 2>&1 | tail -10

Expected: exit 0 OR exit 1 with documented noise-class metrics per audit-24's 9th-consecutive-observation lineage.

Run: bench/cross_lang.py 2>&1 | tail -10

Expected: exit 0; 25/25 stable.

Run: bench/check.py 2>&1 | tail -15

Expected: exit 0 OR exit 1 with latency.implicit_at_rc.* / latency.explicit_at_rc.* / bench_list_sum.bump_s noise per the documented lineage. Conservative call: baseline pristine — extends the lineage to 10th consecutive observation if exit 1.

If any bench script exits non-zero on a metric NOT in the documented noise envelope, surface to Boss for audit-ratification or rebaseline.

• Step 4: Write the per-iter journal.

Path: docs/journals/2026-05-13-iter-24.tidy.md

Structure (matching mq.tidy journal pattern):

• # iter 24.tidy — close 5 actionable drift items from audit-24
• **Date:** 2026-05-13
• **Started from:** 71dec14
• **Status:** DONE
• **Tasks completed:** 6 of 6
• Summary paragraph
• Per-task notes (T1 placement + content; T2 pin observables; T3 pin observables; T4 expect message + any incidental fixture repairs; T5 helper signature + lockstep argument; T6 bench-lineage continuation)
• Concerns section (the recon-Boss reconciliation if any; the helper-extraction policy decision; any test-pin assertion approximations)
• Known debt (audit's [medium-3] negative-test coverage → P3; [low-1] bench sweep noise → carry-on)
• Files touched (list)
• Stats: bench/orchestrator-stats/2026-05-13-iter-24.tidy.json

Append the index line to docs/journals/INDEX.md: - 2026-05-13 — iter 24.tidy: close 5 actionable drift items from audit-24 (DESIGN.md doc-anchor + 2 codegen/synth pins + expect-tightening + helper extraction) → 2026-05-13-iter-24.tidy.md

---

Self-review checklist (planner Step 5)

Spec coverage:

• audit-24 [high-1] → Task 1 ✓
• audit-24 [high-2] → Task 2 ✓
• audit-24 [high-3] → Task 3 (documented-invariant path per Boss decision) ✓
• audit-24 [medium-1] → Task 4 ✓
• audit-24 [medium-2] → Task 5 ✓
• audit-24 [medium-3] → not in scope (defers to P3) — confirmed in carrier ✓
• audit-24 [low-1] → not in scope (carry-on) — confirmed in carrier ✓
• Integration verification → Task 6 ✓

Placeholder scan: the "If Env is a different type name in this scope" / "If Subst is not in scope" notes in Task 5 Step 2 are explicit adaptation instructions, not TBDs — the implementer reads the actual types and adapts. The "default policy is fall through to existing behaviour at this site" note in Task 5 Step 3 instructs the implementer to read the original code and preserve its semantics — also adaptation, not TBD. No genuine TBDs.

Type consistency: apply_subst_and_normalize, normalize_type_for_lookup, class_methods, ResidualConstraint, MonoTarget::FreeFn::type_args, import_map, module_user_fns, module_def_ail_types, show__T, print__T, show_user_adt, prelude.Show, Type::Forall, Type::unit, Term::Var/Let/App/Do/Lam — all consistent across tasks.

Step granularity: every step is a single discrete action (file read, single Edit, single test run, single command). The longest is Task 5 Step 3 (replace site 1 block) at ~5 minutes if the original code has subtle branching the helper must preserve.

No commit steps: none of the 6 tasks include git commit. The Boss commits at iter close per CLAUDE.md.