plan: mq.tidy — 4 drift items from audit-mq, 5 tasks

Rigid-var refinement type-unification leg in refine_multi_candidate_residual
(high-1); same-module bare-class qualifier shape accepted (high-2);
class-method-shadowed-by-fn warning tightened to require an instance
in workspace_registry (medium-1); DESIGN.md Data Model schema fragments
cross-reference the canonical-form rule (medium-2).

Q1 revised from carrier "fix both sites" to "fix only discharge-time"
after code inspection: synth-time resolve_method_dispatch is invoked
with concrete_arg_type: None and the residual's metavar is constructed
AFTER the dispatch call, so the rigid-var leg has no residual type to
unify against — class-only filter is semantically correct there.

Q2 conservative tightening: filter via "any candidate class has any
registry instance" instead of deferring to App-arm via pending-warning
list (full spec rule).
This commit is contained in:
2026-05-13 02:36:18 +02:00
parent f382931eb8
commit 64d3feeb97
+712
View File
@@ -0,0 +1,712 @@
# Iter mq.tidy — Implementation Plan
> **Parent spec:** `docs/specs/2026-05-13-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.