iter mq.3: retire MethodNameCollision + multi-class E2E + DESIGN.md sync

Closes the module-qualified-class-names milestone. Deletes the
workspace-load workaround; the two-libraries case now resolves via
type-driven dispatch at the call site with explicit qualifier as the
LLM-author's disambiguation tool. Resolves both mq.2 known-debt items
(active_declared_constraints plumbing, (class,method) re-key). New
synth warnings channel emits class-method-shadowed-by-fn at all three
fn-precedence branches per spec section Class-fn collisions. Three new
E2E fixtures + integration tests cover the ambiguous, qualified, and
class-fn-shadow trajectories. DESIGN.md class-names paragraph rewritten,
new section Method dispatch added. Roadmap P2 marked done, milestone-24
unblocked for re-brainstorm.

9/9 tasks. 545 tests green. bench/compile_check.py + cross_lang.py
exit 0; bench/check.py exit 1 (2 noise-class regressions, runtime
uncoupled to typecheck iter).

docs/DESIGN.md

@@ -1153,11 +1153,23 @@ qualified references whose owner is unknown are also a violation
 (`WorkspaceLoadError::BadCrossModuleTypeRef`). The same rule
 applies to `Term::Ctor.type_name`.
 
-Class names (`ClassDef.name`, `InstanceDef.class`,
-`SuperclassRef.class`, `Constraint.class`) are NOT module-scoped
-under this rule; they remain workspace-flat with
-`MethodNameCollision` enforced at load. Class-name scoping is a
-future milestone with its own DESIGN amendment.
+Class names follow the canonical-form rule (mq.1): bare for
+same-module references, `<module>.<Class>` for cross-module
+references — symmetric to `Type::Con.name`'s rule from ct.1.
+Three schema fields carry class references in this form:
+`InstanceDef.class`, `Constraint.class`, and `SuperclassRef.class`.
+`ClassDef.name` itself stays bare (defining-site context, like
+`TypeDef.name`).
+
+Method dispatch is type-driven post-mq.3 (see §"Method dispatch"
+below): synth resolves a `Term::Var { name: "show" }` by consulting
+the workspace's method-to-candidate-class index, filtering by
+argument type (concrete) or by declared constraint (rigid-var), and
+routing the residual through the registry at fn-body-end discharge.
+Method-name collisions across classes are now structurally legal —
+they resolve at the call site via type-driven dispatch with explicit
+qualifier (`<module>.<Class>.<method>`) as the LLM-author's
+disambiguation tool.
 
 The legacy `(con T)` form is treated as `(own T)` semantically.
 
@@ -1727,8 +1739,12 @@ wording is fixed; the categories and their triggers are:
 - `MissingMethod` — instance omits a required method.
 - `OverridingNonExistentMethod` — instance specifies a method not in
   the class.
-- `MethodNameCollision` — same method name across two in-scope
-  classes, or between a class method and a top-level function.
+
+(`MethodNameCollision` was retired at iter mq.3. Cross-class method
+sharing is now structurally legal; ambiguity surfaces at the call
+site via `AmbiguousMethodResolution` or, for class-fn name overlap,
+via the `class-method-shadowed-by-fn` warning. See §"Method
+dispatch" below.)
 
 **Class-schema diagnostics** (validation of class declarations):
 
@@ -1749,10 +1765,75 @@ at iter ctt.3.
 - `MissingConstraint` — body's residual constraint is not covered
   by declared (and superclass-expanded) constraints.
 - `NoInstance` — fully concrete constraint has no registry entry.
+  mq.2 adds an optional `candidate_classes` field surfacing the
+  multi-candidate set when the bare-method dispatch path's filter
+  collapses to zero registry survivors.
+- `AmbiguousMethodResolution` (mq.2) — a monomorphic `Term::Var`
+  call site survives both type-driven and constraint-driven filters
+  with more than one candidate class. LLM-author writes the explicit
+  qualifier form `<module>.<Class>.<method>` to disambiguate.
+- `UnknownClass` (mq.2) — an explicit class qualifier in
+  `Term::Var.name` names a qualified class that is not in the
+  workspace's candidate-class index for the method.
+- `class-method-shadowed-by-fn` (mq.3, warning) — a `Term::Var`
+  resolved via fn lookup precedence (locals → caller-module-fn →
+  imported-fn) while a class method of the same name also exists
+  in the workspace. Fn resolution proceeds; the warning surfaces
+  the shadow so the LLM-author can disambiguate via explicit
+  class-qualified call if the shadow was unintentional.
 
-There is no `AmbiguousInstance` diagnostic. Coherence (W2) makes
-every `(class, type)` key globally unique; resolution is therefore
-deterministic by construction.
+There is no `AmbiguousInstance` diagnostic at the registry level —
+coherence (`DuplicateInstance` at registry build, W2) makes
+per-`(class, type)` ambiguity structurally impossible. Cross-class
+method ambiguity is a separate concern resolved at the call site
+via `AmbiguousMethodResolution` (see §"Method dispatch" below).
+
+### Method dispatch
+
+Post-mq.3, dispatch is two-mode:
+
+**Polymorphic call sites** (inside a fn body with `forall` +
+constraint set): the constraint names the class via the qualified
+`Constraint.class` field (canonical-form per mq.1). Synth's
+residual carries the class name directly; constraint-discharge at
+fn-body-end matches against the workspace registry by
+`(class, type_hash)` key.
+
+**Monomorphic call sites**: synth consults the workspace-flat
+`Env.method_to_candidate_classes: BTreeMap<MethodName,
+BTreeSet<QualifiedClassName>>` index, then runs the 5-step
+dispatch rule:
+
+1. Parse the `Term::Var.name` for an optional class qualifier
+   (last-dot-segment is the method name; everything before is the
+   qualified class).
+2. If `method_to_candidate_classes` has no entry for the method
+   name, fall through to the existing Var-arm branches (free fn
+   lookup, dot-qualified cross-module).
+3. Qualifier present: filter candidates to the named class. Empty
+   result fires `UnknownClass`. Singleton survivor proceeds.
+4. Qualifier empty (bare-method form): singleton candidate proceeds
+   directly; multiple candidates yield a multi-candidate residual
+   for discharge-time refinement.
+5. At discharge, refinement runs: concrete `type_` filters
+   candidates via the workspace registry; rigid-var `type_` filters
+   via the active fn's declared constraints
+   (`env.active_declared_constraints`). Single survivor discharges;
+   multiple survivors fire `AmbiguousMethodResolution` (concrete) or
+   `MissingConstraint` (rigid-var); zero survivors fire `NoInstance`
+   (concrete) or `MissingConstraint` (rigid-var).
+
+The `method_to_candidate_classes` index is the load-bearing data
+structure for this routing — its construction in `build_check_env`
+inverts the per-module `class_methods` maps (themselves tuple-keyed
+by `(qualified-class, method)` post-mq.3) to a workspace-flat
+method-name-to-class-set map.
+
+Class-fn collisions resolve at the call site, not at workspace load
+time: the fn lookup precedence (locals → caller-module-fn →
+imported-fn) runs ahead of the class-method branch. When both
+sides have a match, the fn wins and a `class-method-shadowed-by-fn`
+warning surfaces the shadow.
 
 ### What the typeclass design explicitly does NOT support