diff --git a/bench/orchestrator-stats/2026-05-13-iter-mq.tidy.json b/bench/orchestrator-stats/2026-05-13-iter-mq.tidy.json
new file mode 100644
index 0000000..4d86948
--- /dev/null
+++ b/bench/orchestrator-stats/2026-05-13-iter-mq.tidy.json
@@ -0,0 +1,43 @@
+{
+  "iter_id": "mq.tidy",
+  "date": "2026-05-13",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 5,
+  "tasks_completed": 5,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 1,
+    "3": 0,
+    "4": 0,
+    "5": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 1,
+  "blocked_reason": null,
+  "tests_pre_iter": 545,
+  "tests_post_iter": 548,
+  "tests_added": 3,
+  "tests_added_names": [
+    "mq_tidy_rigid_var_filter_uses_type_unification",
+    "mq_tidy_bare_class_qualifier_shape_accepted",
+    "mq_tidy_shadow_warning_suppressed_when_no_instance"
+  ],
+  "trip_wire_fixtures_repaired": [
+    "mq3_class_method_shadowed_by_fn_warning_fires"
+  ],
+  "bench_compile_check_exit": 0,
+  "bench_cross_lang_exit": 0,
+  "bench_check_exit": 0,
+  "bench_check_noise_class_observations_consecutive": 6,
+  "files_touched": [
+    "crates/ailang-check/src/lib.rs",
+    "docs/DESIGN.md"
+  ],
+  "notes": {
+    "reloops_per_task.2": "T2 had one quality-phase re-loop: parse_method_qualifier docstring update added to keep helper documentation coherent with the broadened gate (treated as coherence-required edit, not unrequested extra).",
+    "review_loops_quality": "Single quality-phase re-loop on T2 for the docstring-coherence Minor; T3 trip-wire repair was implementer-phase (not a review-loop).",
+    "trip_wire_note": "mq3_class_method_shadowed_by_fn_warning_fires used Registry::default() (no instances); post-T3 spec-rule tightening correctly suppresses the warning, so fixture was updated to ship a clsmod.Show Int registry entry. Analogous to mq.3's typeclass_22b3 trip-wire pattern.",
+    "plan_step_5_inaccuracy": "Plan Task 5 Step 5 expected `cargo run --bin ail -- check examples/prelude.ail.json` to exit 0; actual behaviour is exit 1 (prelude is the loader's auto-injected module). Identical pre-edit; not a regression from this iter."
+  }
+}
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index ef6c0cf..a010ede 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -2160,10 +2160,20 @@ pub fn refine_multi_candidate_residual(
         };
     }
 
-    // Rigid-var path: filter against declared constraints.
+    // 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))
+        .filter(|c| {
+            declared_constraints.iter().any(|dc| {
+                &dc.class == *c && constraint_type_matches(&dc.type_, &residual.type_)
+            })
+        })
         .cloned()
         .collect();
     match survivors.len() {
@@ -2225,14 +2235,16 @@ pub(crate) fn qualify_class_ref_in_check(class_ref: &str, caller_module: &str) -
 ///
 /// - `"show"` → `("show", None)`
 /// - `"prelude.Show.show"` → `("show", Some("prelude.Show"))`
+/// - `"Show.show"` → `("show", Some("Show"))`
 /// - `"std_list.length"` → `("length", Some("std_list"))`
 ///
-/// Callers gate on the qualifier shape: a class qualifier is always
-/// qualified per mq.1's canonical-form rule, so a single-segment
-/// prefix (no dot) is structurally a module name and the caller falls
-/// through to the cross-module-fn path. A multi-segment prefix
-/// (`<module>.<Class>`) signals an explicit class qualifier on a
-/// class-method call site.
+/// Callers distinguish class qualifiers from cross-module-fn
+/// qualifiers via [`qualifier_is_class_shape`]: PascalCase
+/// single-segment prefixes (e.g. `"Show"`) and multi-segment
+/// prefixes (e.g. `"prelude.Show"`) are class qualifiers per
+/// mq.1's canonical-form rule; lowercase single-segment prefixes
+/// (e.g. `"std_list"`) are module names and the caller falls
+/// through to the cross-module-fn path.
 pub(crate) fn parse_method_qualifier(name: &str) -> (&str, Option<String>) {
     if let Some(dot_idx) = name.rfind('.') {
         (&name[dot_idx + 1..], Some(name[..dot_idx].to_string()))
@@ -2241,6 +2253,64 @@ pub(crate) fn parse_method_qualifier(name: &str) -> (&str, Option<String>) {
     }
 }
 
+/// 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)
+        }
+    }
+}
+
+/// 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: &BTreeMap<String, BTreeSet<String>>,
+    workspace_registry_entries: &BTreeMap<(String, String), ()>,
+    method_name: &str,
+) -> bool {
+    let Some(cands) = method_to_candidate_classes.get(method_name) else {
+        return false;
+    };
+    cands.iter().any(|c| {
+        // BTreeMap is ordered lexicographically on the tuple key;
+        // `range((c, "")..).next()` is the first entry whose first
+        // component is >= `c`. The check `k == c` rejects spillover
+        // into the next class. O(log n) per candidate.
+        workspace_registry_entries
+            .range((c.clone(), String::new())..)
+            .next()
+            .map(|((k, _), _)| k == c)
+            .unwrap_or(false)
+    })
+}
+
 /// Iter 22b.2 (Task 9): expand a list of declared class constraints
 /// with their one-step superclass closure (Decision 11). For every
 /// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
@@ -2479,6 +2549,26 @@ pub(crate) fn synth(
             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: 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();
@@ -2567,11 +2657,7 @@ pub(crate) fn synth(
                 // `<module>.<Class>`), so we fall through to the
                 // qualified-fn arm below in that case.
                 let (method_name, qualifier_opt) = parse_method_qualifier(name);
-                let qualifier_is_class_shape = match &qualifier_opt {
-                    None => true,
-                    Some(q) => q.contains('.'),
-                };
-                qualifier_is_class_shape
+                qualifier_is_class_shape(&qualifier_opt)
                     && env.method_to_candidate_classes.contains_key(method_name)
             } {
                 // mq.2: type-driven dispatch entry. The Var arm runs
@@ -6220,11 +6306,30 @@ mod tests {
         let mut modules = BTreeMap::new();
         modules.insert("clsmod".into(), clsmod);
         modules.insert("fnmod".into(), fnmod);
+        // mq.tidy T3: post-tightening, the warning fires only when at
+        // least one candidate class has an instance in the workspace
+        // registry. Ship a `clsmod.Show Int` instance so the fixture
+        // continues to assert positive-fire behaviour under the
+        // post-tidy spec rule.
+        let mut registry = ailang_core::workspace::Registry::default();
+        let int_h = ailang_core::canonical::type_hash(&Type::int());
+        registry.entries.insert(
+            ("clsmod.Show".into(), int_h),
+            ailang_core::workspace::RegistryEntry {
+                instance: ailang_core::ast::InstanceDef {
+                    class: "clsmod.Show".into(),
+                    type_: Type::int(),
+                    methods: vec![],
+                    doc: None,
+                },
+                defining_module: "clsmod".into(),
+            },
+        );
         let ws = Workspace {
             entry: "fnmod".into(),
             modules,
             root_dir: std::path::PathBuf::from("."),
-            registry: ailang_core::workspace::Registry::default(),
+            registry,
         };
         let mut env = build_check_env(&ws);
         // Treat both modules as implicitly imported by `env.imports`
@@ -6302,4 +6407,102 @@ mod tests {
         assert!(env.class_methods.contains_key(&key),
                 "env.class_methods must contain {key:?}");
     }
+
+    /// mq.tidy T1: discharge-time rigid-var refinement must filter
+    /// declared constraints by BOTH class-name match AND
+    /// type-unification with the residual's `type_` (spec
+    /// §"Constraint-discharge refinement" lines 130-138). Two
+    /// same-class declared constraints on different typevars must
+    /// be discriminated by the residual's actual typevar identity.
+    #[test]
+    fn mq_tidy_rigid_var_filter_uses_type_unification() {
+        use ailang_core::ast::Constraint;
+
+        // Candidate set: two distinct classes both named "Show".
+        let mut candidates = BTreeSet::new();
+        candidates.insert("prelude.Show".to_string());
+        candidates.insert("userlib.Show".to_string());
+
+        // Residual on Var "a".
+        let residual = ResidualConstraint {
+            class: "prelude.Show".to_string(),
+            type_: Type::Var { name: "a".to_string() },
+            method: "show".to_string(),
+            candidates: Some(candidates),
+        };
+
+        // Declared: 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: BTreeMap<(String, String), ()> = 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)"
+        );
+    }
+
+    /// mq.tidy T2: the synth Var-arm's class-method dispatch entry
+    /// gates on a qualifier-shape predicate. The predicate must
+    /// accept three shapes — bare-method (None), bare-class
+    /// PascalCase qualifier (`"Show"`), module-qualified class
+    /// qualifier (`"prelude.Show"`) — and reject bare-fn
+    /// qualifiers (`"std_list"`, lowercase, no inner dot) which
+    /// belong to the cross-module-fn arm.
+    #[test]
+    fn mq_tidy_bare_class_qualifier_shape_accepted() {
+        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, no inner dot) — NOT class-shape.
+        assert!(!qualifier_is_class_shape(&Some("std_list".to_string())));
+    }
+
+    /// mq.tidy T3: the `class-method-shadowed-by-fn` warning fires
+    /// only when at least one candidate class has a registry
+    /// instance (any type) per spec §"Class-fn collisions" 161-162.
+    /// Without this conservative-tightening, the warning fires
+    /// unconditionally on `method_to_candidate_classes` presence,
+    /// including class methods with zero instances anywhere.
+    #[test]
+    fn mq_tidy_shadow_warning_suppressed_when_no_instance() {
+        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);
+
+        // Empty registry → no candidate class has an instance → false.
+        let empty_registry: BTreeMap<(String, String), ()> = BTreeMap::new();
+        assert!(!any_candidate_class_has_instance(
+            &method_to_candidate_classes,
+            &empty_registry,
+            "foo",
+        ));
+
+        // Add one instance for userlib.Foo → true.
+        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",
+        ));
+    }
 }
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index d23ed59..b3207ec 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -2136,7 +2136,7 @@ are real surface forms.
 { "kind": "class",
   "name": "<id>",          // class name (e.g. "Show")
   "param": "<id>",          // single class parameter, kind *
-  "superclass": null,       // or { "class": "<id>", "type": "<param>" }
+  "superclass": null,       // or { "class": "<id>", "type": "<param>" } — "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
   "methods": [
     { "name": "<id>",
       "type": Type,         // FnSig over the class param
@@ -2149,7 +2149,7 @@ are real surface forms.
 
 // instance (typeclass instance; see Decision 11)
 { "kind": "instance",
-  "class": "<id>",          // class being instantiated
+  "class": "<id>",          // class being instantiated; canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
   "type": Type,             // concrete type expression (never the class param)
   "methods": [
     { "name": "<id>", "body": Term }
@@ -2250,7 +2250,7 @@ Patterns are linear: each pattern variable may appear at most once.
 ```jsonc
 // Type-constructor application. `args` omitted when empty
 // (hash-stable when omitted, for non-parameterised cases like Int, Bool, ...).
-{ "k": "con", "name": "<id>", "args": [Type...] }
+{ "k": "con", "name": "<id>", "args": [Type...] }   // "name": canonical form (bare for same-module / primitives, "<module>.<TypeName>" for cross-module; see §"Type::Con name scoping" / ct.1)
 
 // Function type. Decision 10 added paramModes/retMode as
 // metadata on Type::Fn — they are NOT separate Type variants, so every
@@ -2270,7 +2270,7 @@ Patterns are linear: each pattern variable may appear at most once.
 // constraints (Decision 11); omitted when empty (hash-stable when omitted).
 { "k": "forall",
   "vars": ["<id>"...],
-  "constraints": [{ "class": "<id>", "type": "<id>" }, ...],
+  "constraints": [{ "class": "<id>", "type": "<id>" }, ...],   // "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
   "body": Type }
 ```
 
diff --git a/docs/journals/2026-05-13-iter-mq.tidy.md b/docs/journals/2026-05-13-iter-mq.tidy.md
new file mode 100644
index 0000000..aac987c
--- /dev/null
+++ b/docs/journals/2026-05-13-iter-mq.tidy.md
@@ -0,0 +1,219 @@
+# iter mq.tidy — Close 4 actionable drift items from audit-mq
+
+**Date:** 2026-05-13
+**Started from:** 64d3feeb972f4ddfe9bd48484585c69a457e7e1e
+**Status:** DONE
+**Tasks completed:** 5 of 5
+
+## Summary
+
+mq.tidy closes the four actionable drift items audit-mq surfaced
+(commit `f382931`), moving the module-qualified-class-names milestone
+from "structurally complete" to "drift-clean ready for next milestone".
+T1 extends the discharge-time `refine_multi_candidate_residual`
+rigid-var filter from class-only to class + type-unification via the
+existing `constraint_type_matches` helper, so two same-class declared
+constraints on different typevars are correctly discriminated by the
+residual's typevar identity (high-1). T2 extracts the inline
+`qualifier_is_class_shape` predicate as a free `pub(crate)` helper and
+broadens it to accept PascalCase single-segment qualifiers
+(`"Show.show"`) alongside module-qualified ones (`"prelude.Show.show"`)
+— same-module bare-class call sites are now reachable, symmetric to
+the canonical-form rule at the schema level (high-2). T3 introduces
+the `any_candidate_class_has_instance` predicate and gates the
+`class-method-shadowed-by-fn` warning closure on it, so class methods
+with zero registry instances anywhere no longer fire the warning;
+conservative approximation of the full spec rule per Boss Q2 (the arg
+type required for the strict version is unavailable at the Var-arm)
+(medium-1). T4 annotates the four Data Model schema fragments
+(`SuperclassRef`, `InstanceDef.class`, `Type::Con.name`,
+`Constraint.class`) with the canonical-form cross-reference, so a
+schema-section reader without the prose context no longer sees
+bare-only (medium-2).
+
+T5 verification: 548 tests green (was 545 pre-iter + 3 new
+mq_tidy_* unit tests). `bench/compile_check.py` exit 0 (24/24 stable
+after a one-run noise blip absorbed under tolerance on re-run).
+`bench/cross_lang.py` exit 0 (25/25 stable). `bench/check.py` exit 0
+both runs; metric-identity-migrating noise on the
+`latency.implicit_at_rc.*` max-tail cluster — 5th-consecutive audit
+observation per audit-mq's lineage, baseline pristine. The
+`mq3_class_method_shadowed_by_fn_warning_fires` in-crate test was a
+trip-wire: pre-tidy it used `Registry::default()` (no instances) and
+the warning fired anyway because the old gate didn't check instances;
+post-tidy it correctly suppresses, so the fixture was updated to ship
+a `clsmod.Show Int` registry instance — fixture-repair as a coherence
+consequence of the deliberately tightened spec rule. mq3 E2E (3 tests)
++ typeclass_22b3 (18 tests) all stay green; the E2E fixtures already
+ship instances for the shadowed class.
+
+## Per-task notes
+
+- **mq.tidy.1** — Rigid-var refinement type-unification leg.
+  `refine_multi_candidate_residual` filter at lib.rs:2163-2180 extends
+  from `dc.class == c` to `dc.class == c && constraint_type_matches(&dc.type_, &residual.type_)`.
+  New unit test `mq_tidy_rigid_var_filter_uses_type_unification` pins
+  the same-class-different-typevar discrimination
+  (`prelude.Show a` + `userlib.Show b` declared, residual on Var `a`
+  → `Resolved("prelude.Show")`, `userlib.Show` drops because its
+  declared type `Var b` doesn't unify with the residual's `Var a`).
+  Architecture decision per plan: only the discharge-time call site
+  needs the type-unification leg; the synth-time `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 filter). The class-only filter at synth time is therefore
+  semantically correct, not drift.
+
+- **mq.tidy.2** — Bare-class qualifier shape accepted. Inline
+  `qualifier_is_class_shape` predicate at the synth Var-arm dispatch
+  entry (originally lib.rs:2570-2575) extracted as a free
+  `pub(crate) fn qualifier_is_class_shape(&Option<String>) -> bool`
+  helper adjacent to `parse_method_qualifier`. Predicate body:
+  `None` → true (bare method); `Some(q)` with inner dot → true
+  (`<module>.<Class>`); `Some(q)` single-segment → first char
+  uppercase (PascalCase). Bare-fn qualifiers (`"std_list"`, lowercase)
+  correctly reject and fall through to the cross-module-fn arm.
+  Call site at the original location reduced to a one-liner. New
+  unit test `mq_tidy_bare_class_qualifier_shape_accepted` covers all
+  four shapes.
+
+- **mq.tidy.3** — `class-method-shadowed-by-fn` warning tightened.
+  New `pub(crate) fn any_candidate_class_has_instance(...)` helper
+  using BTreeMap range-scan (O(log n) per candidate, O(|candidates|
+  * log n) total) checks the workspace registry for at least one
+  instance under any candidate class. Warning closure at
+  lib.rs:2479-2502 (now ~2498-2540 post-T2-insertion-shift) builds
+  a `registry_unit_view: BTreeMap<(String, String), ()>` per
+  closure invocation and calls the helper before emitting. New
+  unit test `mq_tidy_shadow_warning_suppressed_when_no_instance`
+  pins both directions (empty registry → suppress; one instance
+  → fire). The existing `mq3_class_method_shadowed_by_fn_warning_fires`
+  in-crate test was a trip-wire — its fixture used
+  `Registry::default()` (no instances) and pre-tidy the warning
+  fired anyway because the old gate didn't check instances. Post-tidy
+  the spec rule correctly suppresses; fixture repaired by injecting
+  a `clsmod.Show Int` registry entry directly into `ws.registry.entries`
+  so the test continues to assert positive-fire behaviour under the
+  post-tidy rule. The three mq3 E2E fixtures (`mq3_class_eq_vs_fn_eq`
+  + `mq3_two_show_*`) already ship instances on the shadowed class,
+  so they stayed green without modification.
+
+- **mq.tidy.4** — DESIGN.md schema fragments. Four trailing-comment
+  annotations: `SuperclassRef` (`"superclass"` field at line 2139),
+  `InstanceDef.class` (line 2152), `Type::Con.name` (line 2253), and
+  `Constraint.class` (line 2273). Class-ref annotations cross-reference
+  §"Class names" / mq.1; the Type::Con annotation cross-references
+  §"Type::Con name scoping" / ct.1 (the actual section title — the
+  plan's "§Type names" / "Canonical type names" search did not match
+  exactly; used the canonical anchor title verified via grep). Doc
+  count of "canonical form" went from 1 → 5 (+4 as planned). All
+  annotations are inline trailing-comment appends; no line-count
+  change in DESIGN.md (2678 → 2678).
+
+- **mq.tidy.5** — Integration verification.
+  `cargo test --workspace --no-fail-fast` → 548 passed, 0 failed
+  (was 545 pre-iter + 3 new mq_tidy_* unit tests). `bench/compile_check.py`
+  exit 0; first run showed 1 regression
+  (`build_O0_ms.bench_list_sum_explicit` +5.43% within 20.0% tolerance,
+  classified `ok`; the summary's "1 regressed" count is a
+  false-positive on the first run, second run shows 0 regressed,
+  24/24 stable). `bench/cross_lang.py` exit 0 both runs, 25/25 stable.
+  `bench/check.py` exit 0 both runs; run 1 had 3 regressed / 3
+  improved (all `latency.implicit_at_rc.*` max-tail metrics — same
+  noise class the audit-mq journal documented across 4 consecutive
+  runs); run 2 had 0 regressed / 1 improved / 62 stable — exactly
+  the metric-identity-migration pattern the audit named as variance,
+  not signal. Baseline pristine per the conservative-call convention
+  (6th-consecutive observation now). Plan Step 5 (prelude roundtrip
+  via `cargo run --bin ail -- check examples/prelude.ail.json`)
+  returned exit 1 with "module name 'prelude' is reserved" — but
+  this is identical to pre-edit behaviour (verified via `git stash`),
+  not a regression from this iter. The plan's expectation was
+  inaccurate; the actual sanity gate (DESIGN.md doc edits do not
+  break prelude consistency) is satisfied by the workspace test
+  suite passing 548/548.
+
+## Concerns
+
+- **Plan Task 3 Step 6 anticipation was off for one in-crate test.**
+  The plan said: "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." This
+  was correct for those two fixtures (both E2E), but the in-crate
+  unit test `mq3_class_method_shadowed_by_fn_warning_fires` builds
+  its workspace with `Registry::default()` (zero instances) and
+  pre-tidy relied on the looser rule. Post-tidy it correctly
+  suppresses; the fixture was repaired inline by injecting a
+  `clsmod.Show Int` registry entry. This is exactly analogous to the
+  `typeclass_22b3::rewrite_walker_skips_locally_shadowed_class_method`
+  trip-wire mq.3 documented — same pattern, different test.
+  Fixture-repair as a coherence consequence of a deliberately
+  tightened spec rule; the test's intent ("warning fires when a
+  free fn shadows a class method") is unchanged.
+
+- **Plan Task 5 Step 5 prelude check expectation was off.** The plan
+  said `cargo run --bin ail -- check examples/prelude.ail.json`
+  expected `ok` exit 0; the actual behaviour is exit 1 with the
+  "module name 'prelude' is reserved (auto-injected by the loader)"
+  error. This is identical to pre-edit behaviour (verified via
+  `git stash`); the prelude file is the loader's auto-injected
+  module, not a workspace entry, so `ail check` against it has
+  always failed by design. The right sanity gate for "DESIGN.md
+  doc edits do not break prelude consistency" is the workspace
+  test pass (548/548), which exercises every workspace test that
+  uses the prelude. The plan's prescribed command can be removed
+  from future tidy plans.
+
+- **T2 docstring update on `parse_method_qualifier` was not
+  explicitly in the plan.** The plan asked for adding the new
+  `qualifier_is_class_shape` helper but did not enumerate the
+  paragraph update on `parse_method_qualifier`'s docstring. The
+  old docstring said "Callers gate on the qualifier shape: a class
+  qualifier is always qualified per mq.1's canonical-form rule" —
+  which the broadened gate directly contradicts (bare PascalCase
+  qualifiers now go to class-dispatch). Updating the existing
+  helper's documentation to reference the new helper and remove
+  the now-incorrect claim is strictly required to keep the helper's
+  documentation coherent with the requested behaviour change; it
+  is the docstring analog of "code edits strictly required to make
+  the requested changes compile." Defensible as a coherence
+  consequence, not unrequested scope creep.
+
+## Known debt
+
+- **bench/check.py max-tail noise envelope.** 6th-consecutive
+  observation of the `latency.implicit_at_rc.*` max-tail metric
+  identity migrating between runs. The conservative-call convention
+  has held the baseline pristine across 5 prior audits; this iter
+  adds run 6 to the lineage. A future audit may consider ratification
+  via `--update-baseline` if the pattern persists for another 2-3
+  audits; until then, the lineage is the documentation.
+
+- **mq.tidy did not deliver the [low-1] (Trajectory B + D E2E)
+  or [low-2] (mono env shape) roadmap-backlog items.** Same scope
+  as audit-mq's deferral; these wait for the multi-class workspace
+  shape to land downstream.
+
+- **mq.tidy did not refactor `synth(...)`'s 10-mut-ref signature.**
+  audit-mq's [medium-3] item was explicitly acknowledged-debt, not
+  in tidy scope. Same disposition; future iter may revisit if a
+  natural refactor opportunity arises.
+
+## Files touched
+
+Code:
+- crates/ailang-check/src/lib.rs
+
+Docs:
+- docs/DESIGN.md
+- docs/journals/2026-05-13-iter-mq.tidy.md (this file, new)
+
+No new test files; the three new mq_tidy_* unit tests are inline in
+`crates/ailang-check/src/lib.rs`'s `mod tests` block.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-13-iter-mq.tidy.json
diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md
index 154e694..4a8fd9c 100644
--- a/docs/journals/INDEX.md
+++ b/docs/journals/INDEX.md
@@ -46,3 +46,4 @@
 - 2026-05-13 — iter mq.2: type-driven dispatch mechanism installed (mechanism-before-exercise) — `Env.method_to_candidate_classes` workspace-flat inverse index built alongside `class_methods`; two new `CheckError` variants `AmbiguousMethodResolution` + `UnknownClass` (Display+code+ctx) plus additive `NoInstance.candidate_classes` field; `ResidualConstraint` extended with `candidates: Option<BTreeSet<String>>` (visibility bumped `pub(crate)` → `pub` for test-crate access); pure `resolve_method_dispatch` helper implementing the spec's 5-step rule (qualifier → singleton → type-driven filter → constraint-driven filter → `Multi` for discharge-time refinement); synth Var-arm class-method branch rewritten via `parse_method_qualifier` with inner-dot gate (qualifier must be `<module>.<Class>` form, single-dot names like `std_list.length` fall through to the existing qualified-fn path); `refine_multi_candidate_residual` wired into `check_fn` discharge using `expanded` (post-superclass-expansion constraints) for the rigid-var path; `resolve_residual_class_for_mono` wired into mono's `collect_residuals_ordered` residual-to-target mapping. With `MethodNameCollision` still gating real workspaces, the new multi-candidate branches are exercised exclusively by 15 unit tests: 6 in `tests/method_dispatch_pin.rs` covering the 5-step rule's six cases, 6 in `lib.rs` `mod tests` covering variants + field shapes + discharge refinement, 3 in `mono.rs` `mod tests` covering the mono helper. Real workspaces continue producing single-class residuals (`candidates: None`); every pre-mq.2 fixture typechecks unchanged. Plan-invented `format_type_for_display` replaced with `ailang_core::pretty::type_to_string` (one less duplicate). Synth-time `declared_constraints: &[]` is a deliberate gap documented as known debt — load-bearing only post-mq.3 for the rigid-var fallback (env-plumbing the active fn's constraints into the Var arm is a ~10-line edit slated for mq.3). 9/9 tasks, 539 tests green (was 520 at start of mq.2; +19 = 15 new + 4 pre-existing); `bench/compile_check.py` + `cross_lang.py` clean; `bench/check.py` 1 regression (latency noise, runtime cannot be touched by typecheck-side iter). `MethodNameCollision` retirement lands in mq.3 → 2026-05-13-iter-mq.2.md
 - 2026-05-13 — iter mq.3: `MethodNameCollision` retired + multi-class E2E + DESIGN.md sync — milestone close. Deletes `WorkspaceLoadError::MethodNameCollision` variant + `Origin` enum + per-def collision loop in `build_registry` (workspace.rs 596-681) + Display arm in `main.rs:1201`; the two in-workspace.rs pin tests relocate to `crates/ailang-check/tests/method_collision_pin.rs` with inverted assertions (loads cleanly + `env.method_to_candidate_classes["foo"]` has two qualified-class entries). Resolves both mq.2 known-debt items: (1) `Env.active_declared_constraints: Vec<Constraint>` plumbed pre-synth in `check_fn` so the post-superclass-expansion constraint set reaches the synth Var-arm's `resolve_method_dispatch` constraint-driven filter; (2) `ModuleGlobals.class_methods` + `Env.class_methods` re-keyed from `BTreeMap<MethodName, ClassMethodEntry>` to `BTreeMap<(QualifiedClass, MethodName), ClassMethodEntry>` with new `class_method_candidates(name) -> Vec<(&class, &entry)>` accessor; mono's two presence-check sites (`rewrite_mono_calls`, `interleave_slots`) switched to consult `method_to_candidate_classes` natively (method-keyed, preserves the presence-check signature shape). New `synth(...)` warnings channel via `warnings: &mut Vec<Diagnostic>` out-parameter threaded through 15+ recursive callsites + 5 external callers (check_fn, check_const, 3 in builtins.rs, 1 in lift.rs, 2 in mono.rs, 1 in `check`); new structured warning `class-method-shadowed-by-fn` (kebab-case code, structured ctx carrying `name`/`method`/`fn_owner_module`/`candidate_classes`) fires at all three fn-precedence branches (locals, same-module fn, implicit-import fn). Implicit-import-fn branch reordered ABOVE the class-method branch per spec §"Class-fn collisions" so fn-wins precedence is structural. Three new positive E2E fixtures + integration tests in `crates/ail/tests/mq3_multi_class_e2e.rs`: (a) `mq3_two_show_ambiguous` (two `Show` classes, both with `Show Int`, bare `show 42` → `AmbiguousMethodResolution`); (b) `mq3_two_show_qualified` (same workspace, `mq3_two_show_ambiguous_a.Show.show 42` → clean); (c) `mq3_class_eq_vs_fn_eq` (`class MyEq { myeq }` + `fn myeq` + bare `myeq 1 2` → fn wins, warning fires). DESIGN.md sync: class-names paragraph rewritten to point at mq.1 canonical-form + mq.3 dispatch model; `MethodNameCollision` bullet struck from "Workspace-load (registry-build) diagnostics" with forward-pointing note; `AmbiguousMethodResolution` / `UnknownClass` / `class-method-shadowed-by-fn` + `NoInstance.candidate_classes` added to "Typecheck diagnostics"; `AmbiguousInstance` paragraph reworded to distinguish registry-level (per-class coherence via `DuplicateInstance`) from call-site (cross-class method ambiguity, new diagnostic); new `### Method dispatch` subsection anchors the 5-step rule with `method_to_candidate_classes` as the load-bearing data structure, the class-fn precedence rule, and the post-mq.3 tuple-keyed `class_methods` shape. Roadmap P2 milestone → `[x]` with three-iter summary; milestone-24 `depends on:` line struck and entry annotated "ready for re-brainstorm". Plan defects fixed inline: `check_fn` signature is `Result<()>` not `Result<(CheckedFn, Vec<Diagnostic>)>` — adopted mut-ref-accumulator pattern matching existing `Vec<CheckError>` shape; `class_method_candidates` returns `Vec<(...)>` not `impl Iterator<...>` (the `use<'a, '_>` opaque-type-capture syntax not yet idiomatic in this crate); instance-method body shape draft was `Term::App` but existing-convention is `Term::Lam` with `paramTypes`/`retType` — three fixtures repaired inline. One existing E2E test (`crates/ail/tests/typeclass_22b3.rs:rewrite_walker_skips_locally_shadowed_class_method`) now correctly fires the new warning (the fixture intentionally shadows a class method); test's `assert!(diags.is_empty())` relaxed to filter the new warning with a naming comment. 9/9 tasks, 545 tests green (was 539; +6 net = 3 new mq.3.x lib + 2 method_collision_pin + 3 mq3_multi_class_e2e − 2 deleted workspace.rs pin tests); `bench/compile_check.py` + `cross_lang.py` exit 0; `bench/check.py` exit 1 with 2 noise-class regressions (3rd-consecutive `bench_list_sum.bump_s` persistence + max_us tail metric, both runtime-uncoupled-to-typecheck-iter); prelude zero-diff. Module-qualified-class-names milestone structurally closed → 2026-05-13-iter-mq.3.md
 - 2026-05-13 — audit-mq: milestone close (module-qualified-class-names) — architect drift report surfaces 4 actionable items routing to `mq.tidy` (2× [high]: rigid-var refinement type-unification leg missing in `refine_multi_candidate_residual` for `forall a b. Show a, Show b => ...` shapes; same-module bare-class qualifier `Show.show` unreachable because `qualifier_is_class_shape = q.contains('.')` excludes the no-dot case contradicting mq.1 canonical-form symmetry; 2× [medium]: `class-method-shadowed-by-fn` warning over-fires on locals shadowing prelude method names without class-candidate-for-arg-type check; DESIGN.md Data Model schema fragments don't carry the canonical-form rule for `InstanceDef.class` / `Constraint.class` / `SuperclassRef.class`), plus 1× [medium] acknowledged debt without fix (`synth(...)` 10-mut-ref-parameter growth — consistent with crate's existing accumulator pattern; refactor cost disproportionate to gain), plus 2× [low] roadmap-backlog (no E2E for Trajectories B + D; `collect_mono_targets` rebuilds env without `active_declared_constraints` — currently latent because mono residuals are concrete-type). Bench mixed: `compile_check.py` + `cross_lang.py` exit 0; `check.py` exit 1 across 4 consecutive re-runs with metric identity shifting between runs (3 → 1 → 1 → 0 regressions, different metrics each) — pattern consistent with 5th-consecutive audit noise-class observation since audit-cma; baseline pristine for 5th consecutive audit (the metric-migration-between-runs is itself attribution evidence variance not signal) → 2026-05-13-audit-mq.md
+- 2026-05-13 — iter mq.tidy: close 4 actionable drift items from audit-mq — T1 extends `refine_multi_candidate_residual`'s rigid-var filter at `lib.rs:2163-2168` from class-only (`dc.class == c`) to class + type-unification (`dc.class == c && constraint_type_matches(&dc.type_, &residual.type_)`) via the existing `constraint_type_matches` helper at `lib.rs:2273`, so `forall a b. prelude.Show a, userlib.Show b => (a, b) -> String`-shape declared-constraint sets correctly discriminate by which typevar the residual is on (high-1; spec §"Constraint-discharge refinement" 130-138). Plan revision noted at the architecture paragraph: synth-time `resolve_method_dispatch` is invoked with `concrete_arg_type: None` and constructs the residual metavar AFTER the dispatch call, so the rigid-var leg there has no residual type to unify against — class-only filter at synth time is semantically correct, not drift; fix lands only at the discharge-time site. T2 extracts the inline `qualifier_is_class_shape` predicate from synth Var-arm at `lib.rs:2570-2575` as a free `pub(crate) fn qualifier_is_class_shape(&Option<String>) -> bool` adjacent to `parse_method_qualifier`; broadened to accept PascalCase single-segment qualifiers (`"Show.show"`) alongside module-qualified ones (`"prelude.Show.show"`), so same-module bare-class call sites are now reachable — symmetric to mq.1's canonical-form rule at the schema level (high-2). Discriminator: class names start with uppercase per PascalCase convention; bare-fn qualifiers (`"std_list"`, lowercase) correctly reject and fall through to the cross-module-fn arm. T3 introduces `pub(crate) fn any_candidate_class_has_instance(...)` using a BTreeMap range-scan (O(|candidates| * log n)) and gates the `class-method-shadowed-by-fn` warning closure at `lib.rs:2479-2502` on it, so class methods with zero registry instances anywhere no longer fire the warning — conservative Boss-Q2-decision tightening of the spec rule (full rule would require the arg type, unavailable at the Var-arm before App-arm unification) (medium-1). T4 annotates four DESIGN.md Data Model schema fragments (`SuperclassRef` 2139, `InstanceDef.class` 2152, `Type::Con.name` 2253, `Constraint.class` 2273) with trailing-comment canonical-form cross-references — Type::Con annotation points at the actual existing section title `§"Type::Con name scoping"` (ct.1 anchor verified via grep, plan's text guess was off) (medium-2). Two trip-wires fixed inline: (a) `parse_method_qualifier` docstring updated to remove the now-incorrect "class qualifier is always qualified per mq.1" claim that the broadened gate directly contradicts — coherence-required not unrequested; (b) in-crate `mq3_class_method_shadowed_by_fn_warning_fires` test built workspace with `Registry::default()` (no instances) and pre-tidy fired anyway because old gate didn't check instances — post-tidy correctly suppresses, fixture repaired by injecting a `clsmod.Show Int` registry entry directly into `ws.registry.entries` (analogous to mq.3's `typeclass_22b3` trip-wire pattern). 5/5 tasks, 548 tests green (was 545 + 3 new `mq_tidy_*` unit tests); `bench/compile_check.py` exit 0 (24/24 stable after one-run noise blip absorbed under tolerance on re-run), `cross_lang.py` exit 0 (25/25 stable), `check.py` exit 0 both runs with metric-identity-migrating noise on `latency.implicit_at_rc.*` max-tail cluster — 6th-consecutive observation of the audit-mq-named noise envelope, baseline pristine. Plan Step 5 expectation `ail check examples/prelude.ail.json` exit 0 was inaccurate (actual: exit 1 "module name 'prelude' is reserved", identical to pre-edit, prelude is loader-auto-injected and never a workspace entry); 548/548 workspace test pass is the right sanity gate → 2026-05-13-iter-mq.tidy.md