AILang/docs/plans/0055-mq.tidy.md

# Iter mq.tidy — Implementation Plan

> **Parent spec:** `docs/specs/0023-module-qualified-class-names.md`
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
> to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** Land the four actionable drift items from `audit-mq`
(commit `f382931`): rigid-var refinement type-unification leg
(high-1); same-module bare-class qualifier shape accepted (high-2);
`class-method-shadowed-by-fn` warning tightened to require an
instance (medium-1); DESIGN.md Data Model schema fragments
cross-reference the canonical-form rule (medium-2).

**Architecture:** Three small surgical edits to
`crates/ailang-check/src/lib.rs` (rigid-var filter at
`lib.rs:2163-2168`, qualifier-shape gate at `lib.rs:2570-2575`,
shadow-warning closure at `lib.rs:2479-2502`) plus four DESIGN.md
schema-fragment annotations. The discharge-time `refine_multi_candidate_residual`
is the only call site that needs the type-unification leg — the
synth-time twin `resolve_method_dispatch` is invoked with
`concrete_arg_type: None` and constructs the residual's metavar
*after* the dispatch call, so the rigid-var leg there has no
residual type to unify against (fresh metavar would trivially unify
with any declared-constraint type, degenerating to class-only). The
class-only filter at synth time is therefore semantically correct,
not drift; the carrier's Q1 "fix both" was reconsidered on closer
inspection.

**Tech Stack:** `crates/ailang-check/src/lib.rs` (synth + discharge
+ warning closure), `docs/DESIGN.md` (schema fragments).

---

## Files this plan creates or modifies

- Modify: `crates/ailang-check/src/lib.rs:2163-2168` — `refine_multi_candidate_residual` rigid-var branch: extend filter from class-only to class + type-unification via `constraint_type_matches`.
- Modify: `crates/ailang-check/src/lib.rs:2570-2575` — `qualifier_is_class_shape` predicate: accept bare-class qualifiers (PascalCase first char) in addition to module-qualified-class qualifiers (contains inner dot).
- Modify: `crates/ailang-check/src/lib.rs:2479-2502` — `emit_shadow_warning_if_class_method` closure: tighten emission to require at least one candidate class having a registry instance.
- Modify: `docs/DESIGN.md:2139` — `SuperclassRef.class` schema fragment annotation.
- Modify: `docs/DESIGN.md:2151-2152` — `InstanceDef.class` schema fragment annotation.
- Modify: `docs/DESIGN.md:2253` — `Type::Con.name` schema fragment annotation (ct.1 symmetric twin).
- Modify: `docs/DESIGN.md:2273` — `Constraint.class` schema fragment annotation.
- Test: `crates/ailang-check/src/lib.rs` (in-crate `mod tests` block) — three new RED-first unit tests for T1, T2, T3.

No new files. No new fixtures. No new integration tests (the existing
mq3 E2E suite already covers the warning-emission and dispatch paths
end-to-end; the unit tests pin the precise drift fixes).

---

## Task 1 — Rigid-var refinement type-unification leg

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:2163-2168`
- Test: `crates/ailang-check/src/lib.rs` (in-crate `mod tests` block)

The discharge-time `refine_multi_candidate_residual` (sig at
`lib.rs:2125-2176`) currently filters declared constraints on
`dc.class == c` only at line 2166. When a fn declares two
same-class-different-typevar constraints (the canonical example:
`forall a b. prelude.Show a, prelude.Show b => (a, b) -> String`,
or two distinct classes both declared on different typevars), the
filter cannot tell which typevar the residual is on, so both
declared constraints survive. The spec rule at
§"Constraint-discharge refinement" lines 130-138 says the filter
must ALSO unify `dc.type_` with the residual's `type_`. Use the
existing `constraint_type_matches` helper at
`lib.rs:2273-2283` — it's already the Var/Con recursive matcher
calibrated to the post-`subst.apply` residual shape (the doc
comment at 2266-2272 names this contract verbatim).

- [ ] **Step 1: Write the failing test in the in-crate `mod tests` block.**

Add to the existing `mod tests` block in `crates/ailang-check/src/lib.rs`
(near the other mq-prefixed dispatch tests, search for
`fn mq3_env_class_methods_tuple_keyed`):

```rust
#[test]
fn mq_tidy_rigid_var_filter_uses_type_unification() {
    use ailang_core::ast::Constraint;
    use std::collections::BTreeSet;

    // Two same-class declared constraints on different typevars,
    // candidate set has two classes. Without type-unification, the
    // class-only filter would keep both candidates because both
    // appear in declared constraints; the spec rule narrows to one.
    let mut candidates = BTreeSet::new();
    candidates.insert("prelude.Show".to_string());
    candidates.insert("userlib.Show".to_string());

    let residual = ResidualConstraint {
        class: "prelude.Show".to_string(),
        type_: Type::Var { name: "a".to_string() },
        method: "show".to_string(),
        candidates: Some(candidates),
    };

    // Active declared constraints: prelude.Show a (matches residual
    // type), userlib.Show b (does NOT match residual type).
    let declared = vec![
        Constraint {
            class: "prelude.Show".to_string(),
            type_: Type::Var { name: "a".to_string() },
        },
        Constraint {
            class: "userlib.Show".to_string(),
            type_: Type::Var { name: "b".to_string() },
        },
    ];

    let registry = std::collections::BTreeMap::new();
    let outcome = refine_multi_candidate_residual(&residual, &declared, &registry);

    assert_eq!(outcome, RefineOutcome::Resolved("prelude.Show".to_string()),
        "type-unification leg must drop userlib.Show because its declared type (Var b) does not match the residual type (Var a)");
}
```

- [ ] **Step 2: Run test to verify it fails.**

Run: `cargo test --workspace -p ailang-check mq_tidy_rigid_var_filter_uses_type_unification`

Expected: FAIL with `assertion failed` — the current class-only
filter returns `MissingConstraint` (because two survivors after
class-only filter), not `Resolved("prelude.Show")`.

- [ ] **Step 3: Apply the type-unification leg edit at lib.rs:2163-2168.**

Replace the rigid-var filter at `lib.rs:2163-2168`:

```rust
    // Rigid-var path: filter against declared constraints.
    let survivors: Vec<String> = candidates
        .iter()
        .filter(|c| declared_constraints.iter().any(|dc| &dc.class == *c))
        .cloned()
        .collect();
```

with:

```rust
    // Rigid-var path: filter against declared constraints requiring
    // BOTH class-name match AND type-unification with the residual's
    // type_ (per spec §"Constraint-discharge refinement" 130-138).
    // `constraint_type_matches` is the post-subst.apply Var/Con
    // recursive matcher; the residual's type_ has been `subst.apply`-d
    // by the discharge caller, so rigid-var identity (Var("a") vs
    // Var("b")) is a direct name comparison.
    let survivors: Vec<String> = candidates
        .iter()
        .filter(|c| {
            declared_constraints.iter().any(|dc| {
                &dc.class == *c && constraint_type_matches(&dc.type_, &residual.type_)
            })
        })
        .cloned()
        .collect();
```

- [ ] **Step 4: Run test to verify it passes.**

Run: `cargo test --workspace -p ailang-check mq_tidy_rigid_var_filter_uses_type_unification`

Expected: PASS.

- [ ] **Step 5: Run the existing dispatch + discharge tests to verify no regression.**

Run: `cargo test --workspace -p ailang-check mq3_ refine_multi_candidate dispatch_pin`

Expected: PASS for all matching tests. The single existing test that
exercises the rigid-var path (`mq2_refine_multi_candidate_residual_rigid_var_match`
or similar — search the in-crate tests) used a class-only-distinguishable
shape (different classes for different residuals); the type-unification
leg drops nothing on those inputs because the same typevar is on both
sides. Search:

Run: `grep -n "refine_multi_candidate_residual" crates/ailang-check/src/lib.rs crates/ailang-check/tests/`

Expected: existing tests stay green; the new test is the only one
exercising the same-class-different-typevar shape.

---

## Task 2 — Bare-class qualifier shape accepted

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:2570-2575`
- Test: `crates/ailang-check/src/lib.rs` (in-crate `mod tests` block)

The `qualifier_is_class_shape` predicate at `lib.rs:2570-2575`
currently requires the qualifier prefix to contain an inner dot:

```rust
let qualifier_is_class_shape = match &qualifier_opt {
    None => true,
    Some(q) => q.contains('.'),
};
```

This excludes same-module bare-class qualifiers like
`"Show.show"` (qualifier prefix `"Show"`, no inner dot). The
canonical-form rule per mq.1 says class refs are bare for
same-module and `<module>.<Class>` for cross-module — symmetric
on both sides. The current gate is asymmetric.

Discriminator between bare-class and bare-fn qualifiers: class
names start with uppercase (PascalCase per repo convention; see
the existing class refs in `examples/prelude.ail.json` — `Eq`,
`Ord` — and the mq-test fixtures — `Show`, `MyEq`). Bare fns
start with lowercase (e.g. `std_list.length`). The downstream
`resolve_method_dispatch` Step 3 at `lib.rs:2006-2012` already
accepts uniform `qualifier_prefix: Option<&str>` and the
`candidates.contains(q)` check naturally rejects qualifier
strings that don't match any candidate class — so admitting
bare-class qualifiers can't accidentally hit fn shapes (those
won't be in `candidates`).

- [ ] **Step 1: Write the failing test in the in-crate `mod tests` block.**

Add adjacent to the Task 1 test:

```rust
#[test]
fn mq_tidy_bare_class_qualifier_shape_accepted() {
    // Predicate function under test: extracted as a free helper for
    // testability, OR test the end-to-end behaviour by checking that
    // resolve_method_dispatch with a bare-class qualifier "Show" and
    // a candidate set including "prelude.Show" + "userlib.Show" picks
    // up "Show" as a class-shape qualifier and dispatches correctly
    // (it will UnknownClass because neither candidate equals "Show",
    // but the point is the gate accepts the shape).
    //
    // Simpler: directly test the predicate. The implementation will
    // introduce a free helper `qualifier_is_class_shape(&Option<String>)`
    // alongside the inline call.

    assert!(qualifier_is_class_shape(&None));
    assert!(qualifier_is_class_shape(&Some("Show".to_string())));
    assert!(qualifier_is_class_shape(&Some("prelude.Show".to_string())));

    // Bare fn qualifier (lowercase) is NOT class-shape — falls through
    // to the qualified-fn arm.
    assert!(!qualifier_is_class_shape(&Some("std_list".to_string())));
}
```

- [ ] **Step 2: Run test to verify it fails (compile error — function not yet extracted).**

Run: `cargo test --workspace -p ailang-check mq_tidy_bare_class_qualifier_shape_accepted`

Expected: FAIL — `cannot find function `qualifier_is_class_shape` in
this scope`. (The current implementation has the predicate inline at
`lib.rs:2570-2575`; the test forces the extraction-and-rename.)

- [ ] **Step 3: Extract the predicate as a free helper and broaden it.**

Add a free helper above the synth's Var-arm dispatch entry (near
`parse_method_qualifier` at `lib.rs:2236-2242`):

```rust
/// mq.tidy: predicate gating the synth Var-arm's class-method
/// dispatch entry on the qualifier shape. Accepts:
///   - bare-method form (qualifier absent), e.g. `"show"`.
///   - bare-class qualifier, e.g. `"Show.show"` — class names are
///     PascalCase per repo convention (first character uppercase).
///   - module-qualified class qualifier, e.g. `"prelude.Show.show"`.
/// Rejects qualifier shapes that look like cross-module-fn calls
/// (`"std_list.length"`): qualifier starts with lowercase, no
/// inner dot — falls through to the qualified-fn arm.
pub(crate) fn qualifier_is_class_shape(qualifier_opt: &Option<String>) -> bool {
    match qualifier_opt {
        None => true,
        Some(q) => {
            // Contains inner dot: module-qualified class
            // (`prelude.Show`).
            if q.contains('.') {
                return true;
            }
            // Single segment: class iff the first char is uppercase
            // (PascalCase convention).
            q.chars().next().map(|c| c.is_uppercase()).unwrap_or(false)
        }
    }
}
```

- [ ] **Step 4: Replace the inline predicate at lib.rs:2570-2575 with a call to the helper.**

Replace:

```rust
let qualifier_is_class_shape = match &qualifier_opt {
    None => true,
    Some(q) => q.contains('.'),
};
qualifier_is_class_shape
    && env.method_to_candidate_classes.contains_key(method_name)
```

with:

```rust
qualifier_is_class_shape(&qualifier_opt)
    && env.method_to_candidate_classes.contains_key(method_name)
```

- [ ] **Step 5: Run test to verify it passes.**

Run: `cargo test --workspace -p ailang-check mq_tidy_bare_class_qualifier_shape_accepted`

Expected: PASS.

- [ ] **Step 6: Run the existing qualifier-shape-affected tests to verify no regression.**

Run: `cargo test --workspace -p ailang-check parse_method_qualifier dispatch_pin synth_var_class_method`

Expected: PASS — the broader gate admits more shapes, but
`method_to_candidate_classes.contains_key(method_name)` still gates
behind real class-method presence; downstream `resolve_method_dispatch`
returns `UnknownClass` when the qualifier doesn't match any candidate
(test paths unchanged).

---

## Task 3 — `class-method-shadowed-by-fn` warning tightened

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:2479-2502`
- Test: `crates/ailang-check/src/lib.rs` (in-crate `mod tests` block)

The `emit_shadow_warning_if_class_method` closure at
`lib.rs:2479-2502` currently fires whenever
`env.method_to_candidate_classes.get(method_name)` is non-empty
— i.e. whenever ANY class declares the method. The spec rule at
§"Class-fn collisions" lines 161-162 says the warning should
fire only when a class candidate has an instance applicable to
the call. The full spec rule requires the arg type, which is
unavailable at the Var-arm closure call site (App-arm
unification has not run yet); per Boss Q2 decision, this tidy
lands the conservative tightening: require at least one
candidate class to have a registry entry (any instance, any
type).

The registry is `env.workspace_registry.entries: BTreeMap<(String,
String), RegistryEntry>` keyed by `(qualified_class, type_hash)`.
"At least one instance under candidate class C" = "any key
`(C, *) ∈ entries`".

- [ ] **Step 1: Write the failing test in the in-crate `mod tests` block.**

Add adjacent to the Task 2 test:

```rust
#[test]
fn mq_tidy_shadow_warning_suppressed_when_no_instance() {
    // Build a minimal Env where candidate class declares the method
    // but has NO registry instance. The warning closure should NOT
    // emit. Pre-mq.tidy it would emit unconditionally on
    // method_to_candidate_classes presence.
    //
    // Setup: one class `userlib.Foo` declares method `foo`; no
    // instance entries in workspace_registry.

    use std::collections::{BTreeMap, BTreeSet};

    let mut method_to_candidate_classes: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
    let mut foo_cands = BTreeSet::new();
    foo_cands.insert("userlib.Foo".to_string());
    method_to_candidate_classes.insert("foo".to_string(), foo_cands);

    let workspace_registry_entries: BTreeMap<(String, String), ()> = BTreeMap::new();

    // The predicate under test: "any candidate class C has any
    // (C, *) key in workspace_registry.entries". Extract this as a
    // free helper for testability:

    assert!(!any_candidate_class_has_instance(
        &method_to_candidate_classes,
        &workspace_registry_entries,
        "foo",
    ));

    // Now add an instance for userlib.Foo Int:
    let mut registry_with_inst: BTreeMap<(String, String), ()> = BTreeMap::new();
    registry_with_inst.insert(("userlib.Foo".to_string(), "Int_hash".to_string()), ());

    assert!(any_candidate_class_has_instance(
        &method_to_candidate_classes,
        &registry_with_inst,
        "foo",
    ));
}
```

- [ ] **Step 2: Run test to verify it fails (compile error — function not yet extracted).**

Run: `cargo test --workspace -p ailang-check mq_tidy_shadow_warning_suppressed_when_no_instance`

Expected: FAIL — `cannot find function `any_candidate_class_has_instance``.

- [ ] **Step 3: Extract the predicate as a free helper.**

Add a free helper near `parse_method_qualifier` and
`qualifier_is_class_shape`:

```rust
/// mq.tidy: predicate for the `class-method-shadowed-by-fn`
/// warning emission. The full spec rule (§"Class-fn collisions"
/// 161-162) requires a class candidate WITH AN INSTANCE FOR THE
/// ACTUAL ARG TYPE; the arg type is unavailable at the synth
/// Var-arm where the warning fires (App-arm unification has not
/// run yet). This conservative approximation requires only that
/// at least one candidate class has SOME instance in the
/// workspace registry — stricter than today's "any class
/// declares the method" (which fires even for class methods
/// with zero instances anywhere), looser than the full spec
/// rule. A future tighten can defer the warning emission to a
/// later pass where the arg type is known.
pub(crate) fn any_candidate_class_has_instance(
    method_to_candidate_classes: &std::collections::BTreeMap<String, std::collections::BTreeSet<String>>,
    workspace_registry_entries: &std::collections::BTreeMap<(String, String), ()>,
    method_name: &str,
) -> bool {
    let Some(cands) = method_to_candidate_classes.get(method_name) else {
        return false;
    };
    cands.iter().any(|c| {
        workspace_registry_entries
            .range((c.clone(), String::new())..)
            .next()
            .map(|((k, _), _)| k == c)
            .unwrap_or(false)
    })
}
```

The `range(..).next()` shape avoids scanning the full map: given
the `BTreeMap` ordering is lexicographic on the `(class,
type_hash)` tuple, the first entry whose key starts at
`(c, "")` is the first entry whose first component equals `c`
(if any) — O(log n) per class, O(|candidates| * log n) total.

- [ ] **Step 4: Update the warning closure at lib.rs:2479-2502 to call the helper.**

The closure today is:

```rust
let emit_shadow_warning_if_class_method =
    |name: &str, owner_module: &str, warnings: &mut Vec<crate::diagnostic::Diagnostic>| {
        let (method_name, _) = parse_method_qualifier(name);
        if let Some(cands) = env.method_to_candidate_classes.get(method_name) {
            ... emit diagnostic ...
        }
    };
```

The closure needs `workspace_registry.entries` access. The same
`registry_unit` view built later at `lib.rs:2599-2604` is the
right shape, but the closure runs before that point. Build the
view once near the closure definition:

```rust
let emit_shadow_warning_if_class_method =
    |name: &str, owner_module: &str, warnings: &mut Vec<crate::diagnostic::Diagnostic>| {
        let (method_name, _) = parse_method_qualifier(name);
        // mq.tidy: tighten emission per spec §"Class-fn collisions" —
        // fire only when at least one candidate class has a registry
        // instance (any type). Without this, the warning fires on
        // any class declaring the method, including class methods
        // with zero instances anywhere in the workspace.
        let registry_unit_view: std::collections::BTreeMap<(String, String), ()> = env
            .workspace_registry
            .entries
            .keys()
            .map(|k| (k.clone(), ()))
            .collect();
        if !any_candidate_class_has_instance(
            &env.method_to_candidate_classes,
            &registry_unit_view,
            method_name,
        ) {
            return;
        }
        if let Some(cands) = env.method_to_candidate_classes.get(method_name) {
            let mut candidate_list: Vec<String> = cands.iter().cloned().collect();
            candidate_list.sort();
            let d = crate::diagnostic::Diagnostic::warning(
                "class-method-shadowed-by-fn",
                format!(
                    "free fn `{name}` in module `{owner_module}` shadows class method `{method_name}` \
                     declared in classes {candidate_list:?}. \
                     To call the class method instead, write `<ClassQualifier>.{method_name} ...`.",
                ),
            )
            .with_def(in_def.to_string())
            .with_ctx(serde_json::json!({
                "name": name,
                "method": method_name,
                "fn_owner_module": owner_module,
                "candidate_classes": candidate_list,
            }));
            warnings.push(d);
        }
    };
```

Note that the `registry_unit_view` is rebuilt on every closure
invocation — the closure runs once per Var-arm; for typical
workspaces, registry entries are O(10-100), so the per-call cost
is bounded. A future tighten could hoist this view above the
closure if profiling shows the Var-arm hot.

- [ ] **Step 5: Run test to verify it passes.**

Run: `cargo test --workspace -p ailang-check mq_tidy_shadow_warning_suppressed_when_no_instance`

Expected: PASS.

- [ ] **Step 6: Run existing warning-fire tests to verify the positive case still fires.**

Run: `cargo test --workspace mq3_class_method_shadowed_by_fn_warning_fires mq3_class_eq_vs_fn_eq mq3_two_show shadow_warning`

Expected: PASS — the existing positive fixtures
(`mq3_class_eq_vs_fn_eq`, `typeclass_22b3::rewrite_walker_skips_locally_shadowed_class_method`)
all ship registry instances for the shadowed class, so the
tightened predicate continues to admit the warning emission.

- [ ] **Step 7: Run the full mq.3 E2E suite to verify no regression.**

Run: `cargo test --workspace -p ailang-cli mq3`

Expected: PASS — three mq3 multi-class E2E tests + the warning
suite remain green.

---

## Task 4 — DESIGN.md schema fragments cross-reference canonical-form rule

**Files:**
- Modify: `docs/DESIGN.md:2139` (SuperclassRef)
- Modify: `docs/DESIGN.md:2151-2152` (Instance class field)
- Modify: `docs/DESIGN.md:2253` (Type::Con name field — ct.1 twin)
- Modify: `docs/DESIGN.md:2273` (Constraint class field)

No test (doc-only).

- [ ] **Step 1: Read the canonical-form prose anchor.**

Read `docs/DESIGN.md` lines 1145-1170 (the "Class names" paragraph
where the canonical-form rule is named). Note the exact section
title and the line numbers — the cross-references should point at
the section title rather than line numbers (line numbers drift as
the document grows).

Run: `grep -n "Class names" docs/DESIGN.md | head -5`

Expected: at least one match around line 1156 (per recon) with the
section header containing "Class names" verbatim.

- [ ] **Step 2: Annotate SuperclassRef at DESIGN.md:2139.**

Current line (per recon):

```text
"superclass": null, // or { "class": "<id>", "type": "<param>" }
```

Replace with:

```text
"superclass": null, // or { "class": "<id>", "type": "<param>" } — "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names")
```

- [ ] **Step 3: Annotate InstanceDef at DESIGN.md:2151-2152.**

Locate the `"kind": "instance"` schema fragment around line 2151-2152.

Run: `awk 'NR>=2150 && NR<=2155' docs/DESIGN.md`

Expected: a block containing `"kind": "instance", "class": "<id>"`.

Replace the `"class": "<id>"` line with:

```text
  "class": "<id>",        // canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names")
```

(Trailing-comment style consistent with the SuperclassRef annotation;
exact whitespace per the surrounding block.)

- [ ] **Step 4: Annotate Type::Con at DESIGN.md:2253.**

Run: `awk 'NR>=2250 && NR<=2260' docs/DESIGN.md`

Expected: a block containing `Type::Con` schema fragment with a
`"name"` field.

Annotate the `"name"` line with a parenthetical that cross-references
the ct.1 canonical-form section (the structurally symmetric rule for
type names):

```text
  "name": "<id>",         // canonical form (bare for same-module, "<module>.<TypeName>" for cross-module; see §"Type names")
```

Note: the §"Type names" section is the ct.1 anchor that already
exists; this is the structural twin of the class-ref annotation.
Verify the section title by grepping for it before writing the
cross-reference text:

Run: `grep -n "Type names\|Canonical type names" docs/DESIGN.md | head -5`

If the section title is different (e.g. "Canonical type names"),
update the cross-reference text in the annotation to match.

- [ ] **Step 5: Annotate Constraint at DESIGN.md:2273.**

Locate the `Constraint` schema fragment around line 2273.

Run: `awk 'NR>=2270 && NR<=2280' docs/DESIGN.md`

Expected: a block containing `"constraints": [{ "class": "<id>", ... }]`.

Replace the `"class"` field annotation with:

```text
"constraints": [{ "class": "<id>", "type": "<id>" }, ...]   // "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names")
```

- [ ] **Step 6: Verify DESIGN.md still parses cleanly.**

Run: `head -1 docs/DESIGN.md && wc -l docs/DESIGN.md && grep -c "canonical form" docs/DESIGN.md`

Expected: file header unchanged, line count increased by ~4-8
lines (each annotation may have shifted a comment to a new line),
"canonical form" count increased by 4.

---

## Task 5 — Integration verification

**Files:** none modified; runs all tests + bench scripts.

- [ ] **Step 1: Run full workspace test suite.**

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

Expected: `passed: 548 failed: 0` (was 545 + 3 new RED-then-GREEN
tests from Tasks 1-3; Task 4 has no tests).

- [ ] **Step 2: Run bench/compile_check.py.**

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

Expected: `summary: 24 metrics; 0 regressed, 0 improved beyond tolerance, 24 stable` and exit code 0.

- [ ] **Step 3: Run bench/cross_lang.py.**

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

Expected: `summary: 25 metrics; 0 regressed, 0 improved beyond tolerance, 25 stable` and exit code 0.

- [ ] **Step 4: Run bench/check.py.**

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

Expected: `summary: 63 metrics; N regressed, M improved beyond tolerance, K stable` with N+M small (audit-mq established the noise envelope at metric identity shifting between runs across runs 1-4; 5th consecutive audit baseline-pristine convention applies if regressions land in the same noise class). If N is 0, that's a clean pass; if N is small (1-3) and metrics overlap with the audit-mq noise classes (`bench_list_sum.bump_s`, `bench_closure_chain.bump_s`, `latency.implicit_at_rc.*` max-tail), document in the per-iter journal as "noise envelope continues, baseline pristine". Tidy iter does NOT typically touch runtime metrics — the four drift fixes are all typecheck-side.

- [ ] **Step 5: Prelude roundtrip check.**

Run: `cargo run --bin ail -- check examples/prelude.ail.json`

Expected: `ok` and exit code 0. Sanity gate that the schema-fragment
annotations didn't break DESIGN.md → prelude consistency (annotations
are comment-only and don't touch the JSON, but verify the canonical
form on the prelude still works).

---

## Self-review

1. **Spec coverage:** All four actionable drift items from audit-mq
   are covered: T1 (high-1), T2 (high-2), T3 (medium-1), T4
   (medium-2). The two roadmap-backlog items ([low-1], [low-2]) and
   the acknowledged-debt item ([medium-3] `synth(...)` signature
   growth) are deliberately not in scope per the carrier — captured
   in audit-mq journal as deferred.

2. **Placeholder scan:** No "TBD", no "TODO", no "implement later",
   no "similar to Task N", no "add appropriate error handling".

3. **Type consistency:** `qualifier_is_class_shape` named once
   (helper + replacement), `any_candidate_class_has_instance` named
   once, `constraint_type_matches` referenced by its existing name
   per `lib.rs:2273`. `refine_multi_candidate_residual` and
   `resolve_method_dispatch` are referenced by their existing names.
   The carrier's Q1 "fix both call sites" was revised on closer
   inspection: only the discharge-time site has a residual type to
   unify against (synth-time uses a fresh metavar created AFTER the
   dispatch call). The plan documents this revision in the
   Architecture paragraph and only touches `refine_multi_candidate_residual`.

4. **Step granularity:** Each step is a single edit, test run, or
   verification command bounded at 2-5 minutes. No "implement the
   feature" steps.

5. **No commit steps:** No `git add` or `git commit` in any task.
   Implement leaves the work in the working tree; Boss commits at
   iter close.