From 0e27533e73979b7a1da700d07623c7059e1e34f2 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 04:17:59 +0200 Subject: [PATCH] =?UTF-8?q?plan:=2024.tidy=20=E2=80=94=20close=205=20actio?= =?UTF-8?q?nable=20drift=20items=20from=20audit-24,=206=20tasks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tasks: T1 DESIGN.md new subsection §Cross-module references in synthesised bodies documenting three iter-24.3 strengthenings (canonical-form type_args, post-mono cross-module-ref import_map- bypass, FreeFnCall constraint-residual push). T2 codegen import_map- fallback pin (integration-style in crates/ail/tests/). T3 bare-name poly-fn dot-qualified-branch invariant pin (asserts NoInstance fires at typecheck not codegen). T4 replace unwrap_or_default() at check/lib.rs:2852-2858 with expect(class_methods registry coherence). T5 extract apply_subst_and_normalize helper from duplicated mono.rs sites at :685-714 + :1284-1303. T6 integration + bench verification. Boss decisions in Pre-flight section: T1 placement = new subsection between DESIGN.md:1693 and :1695 (anchorable block beats append-in- place); T2+T3 = integration-style tests (canonical xmod-test pattern, not in-crate codegen); T5 helper extracts common concrete-resolved arm only, returns Option so each call site keeps its rigid- var / unit-default policy explicit. --- docs/plans/24.tidy.md | 627 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 627 insertions(+) create mode 100644 docs/plans/24.tidy.md diff --git a/docs/plans/24.tidy.md b/docs/plans/24.tidy.md new file mode 100644 index 0000000..549b57f --- /dev/null +++ b/docs/plans/24.tidy.md @@ -0,0 +1,627 @@ +# 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` — 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` 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__` references `.show__`, + 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__` body references +//! `.show__` 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__` whose + // body references `show_user_adt.show__` (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." }` (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__ 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.` Var \ + referencing the user-module's show__ 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.` 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` 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 { + 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.