# 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`):
```rust
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`):

```markdown

### 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.

```rust
//! 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__<UserType> 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.

```rust
//! 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):

```rust
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`):

```rust
/// 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:

```rust
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:

```rust
.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.