From e9e45c77affa635652505cc937b77b9349d18c8e Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 01:22:27 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20mq.2=20=E2=80=94=20Type-driven=20dispat?= =?UTF-8?q?ch=20mechanism,=209=20tasks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Installs the dispatch infrastructure without retiring MethodNameCollision yet: - 2 new CheckError variants (AmbiguousMethodResolution, UnknownClass) - NoInstance gains optional candidate_classes field - ResidualConstraint gains optional candidates: BTreeSet - Env gains workspace-flat method_to_candidate_classes index - New resolve_method_dispatch helper implementing the 5-step rule - Synth Var-arm rewritten to route through the helper - Constraint-discharge refines multi-candidate residuals (concrete-type path → registry filter; rigid-var path → declared-constraint filter) - Mono's residual-to-target mapping mirrors the discharge refinement End-to-end multi-class fixtures still gated by MethodNameCollision (iter mq.3); new path exercised in this iter only by 6 unit-test cases on resolve_method_dispatch + 3 each on refine and mono resolver. Boss decisions on recon open questions: residual extension via Option> field; index lives workspace-flat on Env; NoInstance.candidate_classes wired through to_diagnostic this iter; qualify_class_ref_in_check consolidation deferred per mq.1 known-debt. --- docs/plans/mq.2.md | 1665 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1665 insertions(+) create mode 100644 docs/plans/mq.2.md diff --git a/docs/plans/mq.2.md b/docs/plans/mq.2.md new file mode 100644 index 0000000..317ea6e --- /dev/null +++ b/docs/plans/mq.2.md @@ -0,0 +1,1665 @@ +# Iter mq.2 — Type-driven dispatch mechanism (installed, not yet exercised) — 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:** Install the type-driven dispatch infrastructure — new +`method_to_candidate_classes` workspace-flat index on `Env`, extended +`ResidualConstraint` carrying an optional candidate-class set, two new +`CheckError` variants (`AmbiguousMethodResolution` + `UnknownClass`), +additive `NoInstance.candidate_classes` field, rewritten synth Var-arm +class-method branch per Architecture's 5-step rule, constraint-discharge +refinement handling the multi-candidate residual, mono's residual +mapping handling the same. Exercised in this iter exclusively by unit +tests on the new dispatch-resolution helper; end-to-end multi-class +workspaces remain gated by `MethodNameCollision` until iter mq.3. + +**Architecture:** Synth's `Term::Var` arm at `lib.rs:2028` consults a +new workspace-flat `method_to_candidate_classes: BTreeMap>` (built in `build_check_env` alongside +the workspace-flat `class_methods` aggregation). For the bare-method +case the candidate set is either singleton (today's invariant) or +multi (future post-mq.3); both cases push a `ResidualConstraint` with +an optional `candidates` field. At fn-body-end discharge, multi- +candidate residuals are refined by either type-driven filter (concrete +`type_` against `(class, type_hash) ∈ Registry`) or constraint-driven +filter (rigid-var `type_` against active declared constraints). Single +survivor → discharge as today; multiple → `AmbiguousMethodResolution` +or `MissingConstraint` (rigid var); zero → `NoInstance` or +`MissingConstraint`. Mono's residual mapping mirrors the discharge +refinement to land a unique `MonoTarget::ClassMethod` per call site. + +**Tech Stack:** `ailang-check` (`lib.rs`, `mono.rs`, `diagnostic.rs`), +unit-test sibling crate (`crates/ailang-check/tests/method_dispatch_pin.rs`). + +**Pre-flight notes (from recon, settled by Boss):** +- Multi-candidate residual representation → extend `ResidualConstraint` + with `candidates: Option>` (None = single-class today + path; Some = multi-candidate post-mq.3 path). +- `method_to_candidate_classes` lives on `Env` (workspace-flat). Per- + module form skipped because candidate sets span the workspace by + definition. +- `NoInstance.candidate_classes` wired through `to_diagnostic` in this + iter (the field is added with rendering at the same time). +- `qualify_class_ref_in_check` consolidation deferred per mq.1 + known-debt entry; not in scope. +- Mq.1 invariant: synth Var-arm at `lib.rs:2028` already consumes + qualified `cm.class_name`; the rewrite in this plan does NOT + re-qualify anything, only restructures the resolution logic. + +--- + +## Task 1: Add `CheckError::AmbiguousMethodResolution` + `CheckError::UnknownClass` + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:355-622` (CheckError variants + code() + ctx()) +- Modify: `crates/ailang-check/src/diagnostic.rs:64-79` (module-doc code list) +- Test: inline in `crates/ailang-check/src/lib.rs` `mod tests` (Display + code() smoke) + +- [ ] **Step 1: Write RED tests for the new variants' code() and Display** + +Append inside the existing `mod tests` block at the bottom of +`crates/ailang-check/src/lib.rs`: + +```rust +/// mq.2.1: `AmbiguousMethodResolution` is the new check-time +/// diagnostic for multi-candidate residuals that survive type-driven +/// filtering at a monomorphic call site. Verifies the variant is +/// constructible, its `code()` returns the structured-diagnostic key, +/// and the Display surface names the candidate classes. +#[test] +fn mq2_ambiguous_method_resolution_display_and_code() { + let err = CheckError::AmbiguousMethodResolution { + method: "show".to_string(), + at_type: "Int".to_string(), + candidate_classes: vec![ + "prelude.Show".to_string(), + "userlib.Show".to_string(), + ], + }; + assert_eq!(err.code(), "ambiguous-method-resolution"); + let rendered = format!("{}", err); + assert!(rendered.contains("show"), "Display must echo method, got: {rendered}"); + assert!(rendered.contains("prelude.Show"), "Display must name candidate, got: {rendered}"); + assert!(rendered.contains("userlib.Show"), "Display must name candidate, got: {rendered}"); +} + +/// mq.2.1: `UnknownClass` is the new check-time diagnostic for an +/// explicit class qualifier in `Term::Var.name` that names a +/// qualified class not in the workspace. +#[test] +fn mq2_unknown_class_display_and_code() { + let err = CheckError::UnknownClass { + name: "unknownlib.Show".to_string(), + }; + assert_eq!(err.code(), "unknown-class"); + let rendered = format!("{}", err); + assert!(rendered.contains("unknownlib.Show"), "Display must echo the qualified name, got: {rendered}"); +} +``` + +- [ ] **Step 2: Run tests to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_ambiguous_method_resolution_display_and_code mq2_unknown_class_display_and_code` + +Expected: compile error (variants don't exist). + +- [ ] **Step 3: Add the two variants to `CheckError`** + +In `crates/ailang-check/src/lib.rs`, find the existing `NoInstance` +variant at lib.rs:567-572. Add two siblings immediately after: + +```rust +/// mq.2: a monomorphic call site ` x` with multiple +/// candidate classes (each declaring `` and each having an +/// instance for `x`'s concrete type) cannot be resolved unambiguously. +/// The LLM-author writes an explicit qualifier +/// (`. x`) to disambiguate. +#[error( + "method `{method}` at type `{at_type}` is ambiguous: classes \ + {candidate_classes:?} all declare it and provide an instance. \ + Disambiguate with `.{method}`." +)] +AmbiguousMethodResolution { + method: String, + at_type: String, + candidate_classes: Vec, +}, + +/// mq.2: an explicit class qualifier in `Term::Var.name` names a +/// qualified class that's not in the workspace registry. +#[error("class `{name}` is not declared in any module of this workspace")] +UnknownClass { + name: String, +}, +``` + +- [ ] **Step 4: Add code() table entries** + +Locate the `code()` impl on `CheckError` at lib.rs:617-620 (the +match arm table that returns the structured-diagnostic-key string). +Add two arms: + +```rust +CheckError::AmbiguousMethodResolution { .. } => "ambiguous-method-resolution", +CheckError::UnknownClass { .. } => "unknown-class", +``` + +- [ ] **Step 5: Add ctx() table entries** + +Locate the `ctx()` impl on `CheckError` at lib.rs:658-663 (the +match arm table that renders the structured-diagnostic context +JSON). Add two arms returning a `serde_json::Value`: + +```rust +CheckError::AmbiguousMethodResolution { method, at_type, candidate_classes } => { + serde_json::json!({ + "method": method, + "at_type": at_type, + "candidate_classes": candidate_classes, + }) +} +CheckError::UnknownClass { name } => { + serde_json::json!({ "name": name }) +} +``` + +(Match the exact return-type and shape of the existing `ctx()` arms +— the recon notes `MissingConstraint` and `NoInstance` arms at +lib.rs:658-663 as the pattern.) + +- [ ] **Step 6: Update `diagnostic.rs` module doc-comment** + +In `crates/ailang-check/src/diagnostic.rs:64-79` (the module-level +doc-comment listing stable diagnostic codes), add two entries to the +list (keep alphabetical or insertion-order with existing pattern): + +```rust +//! - `ambiguous-method-resolution` — mq.2: bare method call has +//! multiple candidate classes after type-driven filter. +//! - `unknown-class` — mq.2: explicit class qualifier names a class +//! not in the workspace registry. +``` + +- [ ] **Step 7: Run tests to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_ambiguous_method_resolution_display_and_code mq2_unknown_class_display_and_code` + +Expected: both PASS. + +- [ ] **Step 8: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. Only additive variants; no semantic change. + +--- + +## Task 2: Extend `CheckError::NoInstance` with optional `candidate_classes` + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:567-572` (NoInstance struct + Display) +- Modify: `crates/ailang-check/src/lib.rs:1697-1702` (existing NoInstance construction) +- Modify: `crates/ailang-check/src/lib.rs:658-663 + 718-728` (ctx() + Float-aware addendum) +- Test: inline in `crates/ailang-check/src/lib.rs` `mod tests` + +- [ ] **Step 1: Write a RED test for the extended Display** + +Append in `mod tests`: + +```rust +/// mq.2.2: `NoInstance` carries an optional `candidate_classes` +/// list (additive in mq.2). When non-empty, the Display surfaces +/// it; when empty, the Display is unchanged from pre-mq.2 form +/// (backwards compatible for single-class call sites). +#[test] +fn mq2_no_instance_with_candidate_classes_renders() { + let err = CheckError::NoInstance { + class: "prelude.Show".to_string(), + method: "show".to_string(), + at_type: "MyType".to_string(), + candidate_classes: vec!["prelude.Show".to_string()], + }; + let rendered = format!("{}", err); + assert!(rendered.contains("show"), "Display must echo method, got: {rendered}"); + assert!(rendered.contains("MyType"), "Display must echo type, got: {rendered}"); +} + +/// mq.2.2: empty `candidate_classes` keeps the existing single-class +/// Display shape — surface mentions the resolved class only. +#[test] +fn mq2_no_instance_empty_candidates_back_compat() { + let err = CheckError::NoInstance { + class: "prelude.Show".to_string(), + method: "show".to_string(), + at_type: "MyType".to_string(), + candidate_classes: vec![], + }; + let rendered = format!("{}", err); + assert!(rendered.contains("prelude.Show"), "Display must echo class, got: {rendered}"); +} +``` + +- [ ] **Step 2: Run tests to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_no_instance` + +Expected: compile error — `candidate_classes` field does not exist on `NoInstance`. + +- [ ] **Step 3: Add the field to `NoInstance`** + +In `crates/ailang-check/src/lib.rs:567-572`, find the `NoInstance` +variant. Add the optional field (as a `Vec` defaulting to +empty rather than `Option>` to keep construction simpler): + +```rust +/// `MissingConstraint`: when the residual type is concrete, the fn +/// — it can only be discharged by an existing instance. Without a +/// matching instance the call is rejected as `NoInstance`. mq.2 adds +/// the optional `candidate_classes` field: empty preserves the +/// pre-mq.2 single-class Display; non-empty surfaces the wider +/// candidate set when the bare-method dispatch path failed at the +/// concrete-type filter. +#[error( + "no instance found for class `{class}` at type `{at_type}` \ + (method `{method}` invoked here)" +)] +NoInstance { + class: String, + method: String, + at_type: String, + #[serde(default)] + candidate_classes: Vec, +}, +``` + +(If `#[serde(default)]` is not applicable because the variant isn't +serde-derived, omit it. Match the existing struct shape exactly.) + +- [ ] **Step 4: Update the single existing construction site** + +At lib.rs:1697-1702 (per recon), the existing single `NoInstance` +construction in `check_fn`'s residual-discharge loop. Add the empty +field: + +```rust +return Err(CheckError::NoInstance { + class: r.class.clone(), + method: r.method.clone(), + at_type: format_type_for_display(&r_ty_norm), + candidate_classes: vec![], +}); +``` + +Keep all other construction sites (if any are found via +`grep -n "NoInstance {" crates/ailang-check/src/`) updated the +same way — add `candidate_classes: vec![]` to each. + +- [ ] **Step 5: Update ctx() and Float-aware addendum** + +In `crates/ailang-check/src/lib.rs:658-663`, update the `NoInstance` +arm to include the new field in the rendered JSON. In lib.rs:718-728 +(the Float-aware addendum that branches on `class == "prelude.Eq" || +class == "prelude.Ord"`), no change needed — the addendum reads +`class` only. + +```rust +CheckError::NoInstance { class, method, at_type, candidate_classes } => { + let mut obj = serde_json::json!({ + "class": class, + "method": method, + "at_type": at_type, + }); + if !candidate_classes.is_empty() { + obj["candidate_classes"] = serde_json::json!(candidate_classes); + } + obj +} +``` + +- [ ] **Step 6: Run the mq.2.2 tests to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_no_instance` + +Expected: both PASS. + +- [ ] **Step 7: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. Additive field with empty default preserves all +existing semantics. + +--- + +## Task 3: Extend `ResidualConstraint` with `Option>` candidates + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:1737-1749` (ResidualConstraint struct) +- Modify: lib.rs construction sites for ResidualConstraint (grep for `ResidualConstraint {`) +- Test: inline in `crates/ailang-check/src/lib.rs` `mod tests` + +- [ ] **Step 1: Write a RED smoke test for the extended struct** + +Append in `mod tests`: + +```rust +/// mq.2.3: `ResidualConstraint` carries an optional candidate-class +/// set for the multi-candidate dispatch path. `None` preserves the +/// pre-mq.2 single-class semantics (the `class` field is the +/// resolved class). `Some(...)` carries the candidate set; the +/// `class` field's content is the first-of-set tentatively (or a +/// sentinel — implementer choice as long as the discharge path +/// reads from `candidates` when present). +#[test] +fn mq2_residual_constraint_candidates_field_exists() { + let single = ResidualConstraint { + class: "prelude.Eq".to_string(), + type_: Type::Con { name: "Int".to_string(), args: vec![] }, + method: "eq".to_string(), + candidates: None, + }; + assert!(single.candidates.is_none()); + + let mut multi_set = std::collections::BTreeSet::new(); + multi_set.insert("prelude.Show".to_string()); + multi_set.insert("userlib.Show".to_string()); + let multi = ResidualConstraint { + class: "prelude.Show".to_string(), + type_: Type::Con { name: "Int".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(multi_set.clone()), + }; + assert_eq!(multi.candidates, Some(multi_set)); +} +``` + +- [ ] **Step 2: Run test to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_residual_constraint_candidates_field_exists` + +Expected: compile error — `candidates` field does not exist. + +- [ ] **Step 3: Add the field to `ResidualConstraint`** + +At lib.rs:1737-1749, find the existing `ResidualConstraint` struct. +Add the field (with doc-comment): + +```rust +#[derive(Debug, Clone)] +pub(crate) struct ResidualConstraint { + pub class: String, + pub type_: Type, + pub method: String, + /// mq.2: candidate-class set for the multi-candidate dispatch + /// path. `None` ⇒ single-class semantics (pre-mq.2 behaviour); + /// the `class` field is the resolved class. `Some(set)` ⇒ + /// multi-candidate residual; discharge filters the set at fn- + /// body-end. When `Some`, the `class` field carries a tentative + /// value (typically the first set element) that discharge + /// overwrites on resolution. + pub candidates: Option>, +} +``` + +(Add `use std::collections::BTreeSet;` at the top of the file if not +already imported.) + +- [ ] **Step 4: Update existing `ResidualConstraint` construction sites to pass `candidates: None`** + +Run: `grep -n "ResidualConstraint {" crates/ailang-check/src/lib.rs` + +Each site must add the new field as `candidates: None,`. The known +sites from recon: `lib.rs:2051-2055` (synth Var-arm class-method push). +Verify with grep and update each. + +Example: + +```rust +residuals.push(ResidualConstraint { + class: cm.class_name.clone(), + type_: fresh, + method: name.clone(), + candidates: None, +}); +``` + +- [ ] **Step 5: Run the mq.2.3 test to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_residual_constraint_candidates_field_exists` + +Expected: PASS. + +- [ ] **Step 6: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. All existing residual constructions now pass +`candidates: None`, single-class discharge path unchanged. + +--- + +## Task 4: Build `method_to_candidate_classes` on `Env` in `build_check_env` + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:2904` (Env struct — add field) +- Modify: `crates/ailang-check/src/lib.rs:1291-1295` (build_check_env aggregation site) +- Test: inline in `crates/ailang-check/src/lib.rs` `mod tests` + +- [ ] **Step 1: Write a RED test for the new field** + +Append in `mod tests`: + +```rust +/// mq.2.4: `Env` carries a workspace-flat +/// `method_to_candidate_classes: BTreeMap>` +/// inverse map of `class_methods`. Today's `MethodNameCollision` +/// invariant guarantees each set is singleton; post-mq.3 the cardinality +/// > 1 case becomes legal. +#[test] +fn mq2_env_method_to_candidate_classes_built() { + // Build a minimal workspace with one class declaring one method. + let mut modules = BTreeMap::new(); + modules.insert( + "m".to_string(), + Module { + name: "m".to_string(), + imports: vec![], + defs: vec![Def::Class(ClassDef { + name: "MyShow".to_string(), + param: "a".to_string(), + superclass: None, + methods: vec![ClassMethod { + name: "myshow".to_string(), + ty: Type::Fn { + params: vec![Type::Var { name: "a".to_string() }], + param_modes: vec![ParamMode::Borrow], + ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }), + effects: vec![], + }, + default: None, + }], + doc: None, + })], + }, + ); + let ws = build_workspace_for_test(modules); // helper or inline equivalent + let env = build_check_env(&ws); + let candidates = env.method_to_candidate_classes.get("myshow") + .expect("method_to_candidate_classes must contain `myshow`"); + assert!(candidates.contains("m.MyShow"), "candidates: {candidates:?}"); + assert_eq!(candidates.len(), 1, "MethodNameCollision invariant: singleton"); +} +``` + +(If `build_workspace_for_test` does not exist, inline the workspace +construction using the same pattern as other in-file tests that +construct synthetic `Workspace` values. The implementer adapts to +the existing in-test workspace-construction pattern.) + +- [ ] **Step 2: Run test to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_env_method_to_candidate_classes_built` + +Expected: compile error — `method_to_candidate_classes` field does not exist on `Env`. + +- [ ] **Step 3: Add the field to `Env`** + +At lib.rs:2904 (per recon, the `Env` struct holds `class_methods`). +Add a sibling field immediately after: + +```rust +pub(crate) struct Env { + // ...existing fields... + pub(crate) class_methods: BTreeMap, + /// mq.2: workspace-flat inverse of `class_methods` — for each + /// method name, the set of qualified class names that declare + /// it. Today's `MethodNameCollision` invariant guarantees each + /// set is singleton; mq.3 lifts this and cardinality > 1 + /// becomes legal. Synth's `Term::Var` arm consults this index + /// per the 5-step rule (spec §Architecture). + pub(crate) method_to_candidate_classes: BTreeMap>, + // ...remaining fields... +} +``` + +(Insert at the exact line determined by `grep -n "pub(crate) class_methods" crates/ailang-check/src/lib.rs`.) + +- [ ] **Step 4: Populate the new field in `build_check_env`** + +At lib.rs:1291-1295 (per recon, the workspace-flat aggregation loop +that builds `env.class_methods`), add a parallel loop or extend the +existing one to populate `method_to_candidate_classes`: + +```rust +let mut method_to_candidate_classes: BTreeMap> = BTreeMap::new(); +for (_mod_name, mg) in &per_module_globals { + for (method_name, entry) in &mg.class_methods { + method_to_candidate_classes + .entry(method_name.clone()) + .or_default() + .insert(entry.class_name.clone()); + } +} +``` + +Pass `method_to_candidate_classes` into the `Env` constructor at the +end of `build_check_env`. Match the existing pattern that passes +`class_methods` into `Env`. + +- [ ] **Step 5: Run the mq.2.4 test to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_env_method_to_candidate_classes_built` + +Expected: PASS. + +- [ ] **Step 6: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. New field built but not yet consumed. + +--- + +## Task 5: New `resolve_method_dispatch` helper + six unit-test cases + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs` (add helper function near `ResidualConstraint`) +- Create: `crates/ailang-check/tests/method_dispatch_pin.rs` (six unit tests on the helper) + +- [ ] **Step 1: Write the six unit tests (RED-first)** + +Create `crates/ailang-check/tests/method_dispatch_pin.rs`: + +```rust +//! mq.2.5: pin tests on `resolve_method_dispatch` — the new +//! dispatch-resolution helper that synth's `Term::Var` arm consults +//! per the spec's 5-step rule. +//! +//! Six cases: +//! 1. Unique candidate. +//! 2. Multi + explicit qualifier matching one. +//! 3. Multi + explicit qualifier matching none → UnknownClass. +//! 4. Multi + type-driven filter narrows to one. +//! 5. Multi + constraint-driven filter narrows to one (rigid var case). +//! 6. Multi + true ambiguity → AmbiguousMethodResolution. + +use ailang_check::{resolve_method_dispatch, MethodDispatchOutcome}; +use ailang_check::ResidualConstraint; // if needed +use ailang_core::ast::Type; +use ailang_core::canonical; +use std::collections::{BTreeMap, BTreeSet}; + +fn registry_with(entries: &[(&str, &str)]) -> BTreeMap<(String, String), ()> { + // Returns a synthetic registry: keys are (qualified_class, type_hash_string) + // values are unit (instance presence flag). + let mut reg = BTreeMap::new(); + for (cls, ty_name) in entries { + let t = Type::Con { name: ty_name.to_string(), args: vec![] }; + let h = canonical::type_hash(&t); + reg.insert((cls.to_string(), h), ()); + } + reg +} + +fn candidates_of(classes: &[&str]) -> BTreeSet { + classes.iter().map(|s| s.to_string()).collect() +} + +/// Case 1: unique candidate → returns that class. +#[test] +fn case1_unique_candidate_resolves() { + let candidates = candidates_of(&["prelude.Eq"]); + let registry = registry_with(&[("prelude.Eq", "Int")]); + let arg_ty = Type::Con { name: "Int".to_string(), args: vec![] }; + let result = resolve_method_dispatch( + /*method*/ "eq", + /*qualifier_prefix*/ None, + /*candidates*/ &candidates, + /*concrete_arg_type*/ Some(&arg_ty), + /*declared_constraints*/ &[], + /*registry*/ ®istry, + ); + assert_eq!(result, MethodDispatchOutcome::Resolved("prelude.Eq".to_string())); +} + +/// Case 2: multi + explicit qualifier matching one → returns that class. +#[test] +fn case2_qualifier_matches_one() { + let candidates = candidates_of(&["prelude.Show", "userlib.Show"]); + let registry = registry_with(&[ + ("prelude.Show", "Int"), + ("userlib.Show", "Int"), + ]); + let arg_ty = Type::Con { name: "Int".to_string(), args: vec![] }; + let result = resolve_method_dispatch( + "show", + Some("userlib.Show"), + &candidates, + Some(&arg_ty), + &[], + ®istry, + ); + assert_eq!(result, MethodDispatchOutcome::Resolved("userlib.Show".to_string())); +} + +/// Case 3: multi + explicit qualifier matching none → UnknownClass. +#[test] +fn case3_qualifier_matches_none_unknown_class() { + let candidates = candidates_of(&["prelude.Show", "userlib.Show"]); + let registry = registry_with(&[("prelude.Show", "Int")]); + let arg_ty = Type::Con { name: "Int".to_string(), args: vec![] }; + let result = resolve_method_dispatch( + "show", + Some("nonexistent.Show"), + &candidates, + Some(&arg_ty), + &[], + ®istry, + ); + assert_eq!( + result, + MethodDispatchOutcome::UnknownClass("nonexistent.Show".to_string()), + ); +} + +/// Case 4: multi + type-driven filter narrows to one → returns that class. +#[test] +fn case4_type_driven_filter_narrows_to_one() { + let candidates = candidates_of(&["prelude.Show", "userlib.Show"]); + let registry = registry_with(&[("prelude.Show", "Int")]); // only prelude.Show has Show Int + let arg_ty = Type::Con { name: "Int".to_string(), args: vec![] }; + let result = resolve_method_dispatch( + "show", + None, + &candidates, + Some(&arg_ty), + &[], + ®istry, + ); + assert_eq!(result, MethodDispatchOutcome::Resolved("prelude.Show".to_string())); +} + +/// Case 5: multi + constraint-driven filter narrows to one (rigid var) → returns that class. +#[test] +fn case5_constraint_driven_filter_narrows_to_one() { + let candidates = candidates_of(&["prelude.Show", "userlib.Show"]); + let registry = registry_with(&[]); + let rigid_a = Type::Var { name: "a".to_string() }; + use ailang_core::ast::Constraint; + let declared = vec![Constraint { + class: "prelude.Show".to_string(), + type_: Type::Var { name: "a".to_string() }, + }]; + let result = resolve_method_dispatch( + "show", + None, + &candidates, + Some(&rigid_a), // rigid var, can't drive registry lookup + &declared, + ®istry, + ); + assert_eq!(result, MethodDispatchOutcome::Resolved("prelude.Show".to_string())); +} + +/// Case 6: multi + true ambiguity → AmbiguousMethodResolution. +#[test] +fn case6_true_ambiguity() { + let candidates = candidates_of(&["prelude.Show", "userlib.Show"]); + let registry = registry_with(&[ + ("prelude.Show", "Int"), + ("userlib.Show", "Int"), + ]); + let arg_ty = Type::Con { name: "Int".to_string(), args: vec![] }; + let result = resolve_method_dispatch( + "show", + None, + &candidates, + Some(&arg_ty), + &[], + ®istry, + ); + assert_eq!( + result, + MethodDispatchOutcome::Ambiguous { + method: "show".to_string(), + at_type: "Int".to_string(), + candidates: vec!["prelude.Show".to_string(), "userlib.Show".to_string()], + }, + ); +} +``` + +- [ ] **Step 2: Run tests to confirm RED** + +Run: `cargo test --workspace --test method_dispatch_pin` + +Expected: compile error — `resolve_method_dispatch` and +`MethodDispatchOutcome` are not exported. + +- [ ] **Step 3: Add the `MethodDispatchOutcome` type and the helper** + +In `crates/ailang-check/src/lib.rs`, near the `ResidualConstraint` +declaration (lib.rs:1737), add: + +```rust +/// mq.2: outcome of the dispatch-resolution helper. The synth Var-arm +/// consumer translates this enum into either a singleton +/// `ResidualConstraint` (Resolved) or a multi-candidate residual +/// (Multi) for discharge-time refinement, or a `CheckError` (Unknown +/// / Ambiguous). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum MethodDispatchOutcome { + /// Single class resolved unambiguously. + Resolved(String), + /// Explicit qualifier names a class not in the candidate set. + UnknownClass(String), + /// Bare-method call site survived both type-driven and constraint- + /// driven filters with >1 candidate. + Ambiguous { + method: String, + at_type: String, + candidates: Vec, + }, + /// Bare-method call site with multiple candidates that need + /// discharge-time refinement (rigid var type at synth time; + /// concrete type only available at discharge). + Multi { + method: String, + candidates: BTreeSet, + }, +} + +/// mq.2: resolve a method-call site per the spec's 5-step rule. +/// Pure function — no Env mutation, no residual emission. +/// +/// `qualifier_prefix` is the dot-stripped class prefix (e.g. +/// `"prelude.Show"` for a `Term::Var.name == "prelude.Show.show"`). +/// `None` = bare method form. +/// +/// `concrete_arg_type` is `Some` when synth's caller has the arg +/// type post-unification (App-arm); `None` when synth is at the +/// pre-App Var arm. When `None`, the helper does NOT apply type- +/// driven filtering at synth time. +/// +/// `declared_constraints` are the active forall-bound constraints +/// in scope at the call site; consulted for the rigid-var fallback. +/// +/// `registry` is the workspace registry keyed by `(qualified_class, +/// type_hash)` for instance-existence checks. +pub fn resolve_method_dispatch( + method: &str, + qualifier_prefix: Option<&str>, + candidates: &BTreeSet, + concrete_arg_type: Option<&Type>, + declared_constraints: &[ailang_core::ast::Constraint], + registry: &BTreeMap<(String, String), ()>, +) -> MethodDispatchOutcome { + // Step 3 (5-step rule): explicit qualifier present. + if let Some(q) = qualifier_prefix { + if candidates.contains(q) { + return MethodDispatchOutcome::Resolved(q.to_string()); + } + return MethodDispatchOutcome::UnknownClass(q.to_string()); + } + + // Step 4: bare-method form. + if candidates.len() == 1 { + return MethodDispatchOutcome::Resolved( + candidates.iter().next().cloned().unwrap(), + ); + } + + // Multi-candidate path. + // Type-driven filter first if arg type is concrete (non-Var). + let concrete = concrete_arg_type + .filter(|t| !matches!(t, Type::Var { .. })); + if let Some(t) = concrete { + let type_h = ailang_core::canonical::type_hash(t); + let survivors: BTreeSet = candidates + .iter() + .filter(|c| registry.contains_key(&((**c).clone(), type_h.clone()))) + .cloned() + .collect(); + if survivors.len() == 1 { + return MethodDispatchOutcome::Resolved( + survivors.into_iter().next().unwrap(), + ); + } + if survivors.len() > 1 { + let mut sorted: Vec = survivors.into_iter().collect(); + sorted.sort(); + let at_type = format_type_for_display(t); + return MethodDispatchOutcome::Ambiguous { + method: method.to_string(), + at_type, + candidates: sorted, + }; + } + // Zero survivors after type-driven filter: fall through to Multi + // (the discharge path raises NoInstance with candidates). + } + + // Constraint-driven filter (rigid-var case or no concrete arg). + let survivors: BTreeSet = candidates + .iter() + .filter(|c| { + declared_constraints + .iter() + .any(|dc| &dc.class == *c) + }) + .cloned() + .collect(); + if survivors.len() == 1 { + return MethodDispatchOutcome::Resolved( + survivors.into_iter().next().unwrap(), + ); + } + + // No filter narrowed; emit Multi for discharge-time refinement. + MethodDispatchOutcome::Multi { + method: method.to_string(), + candidates: candidates.clone(), + } +} + +/// mq.2 helper: render a Type as a short surface-shaped string for +/// diagnostic messages. +fn format_type_for_display(t: &Type) -> String { + match t { + Type::Con { name, args } if args.is_empty() => name.clone(), + _ => format!("{:?}", t), // implementer-acceptable fallback + } +} +``` + +Export `MethodDispatchOutcome` and `resolve_method_dispatch` as +`pub` (the test crate consumes them via `ailang_check::*`). + +- [ ] **Step 4: Run the six tests to confirm GREEN** + +Run: `cargo test --workspace --test method_dispatch_pin` + +Expected: all six PASS. + +- [ ] **Step 5: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. New helper exists, not yet called from synth (Task 6). + +--- + +## Task 6: Rewrite synth Var-arm class-method branch per 5-step rule + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:2028-2056` (synth Var-arm class-method branch) + +- [ ] **Step 1: Write a regression test (RED-first) that synth produces a single-candidate residual on a unique-method workspace** + +Append in `mod tests` in `crates/ailang-check/src/lib.rs`: + +```rust +/// mq.2.6: regression — synth's Var-arm class-method branch +/// preserves the pre-mq.2 behaviour on a unique-method workspace +/// (singleton candidate set). The residual carries +/// `candidates: None` and `class` = the qualified class name. +#[test] +fn mq2_synth_var_arm_singleton_preserves_single_class_residual() { + let mut modules = BTreeMap::new(); + modules.insert( + "m".to_string(), + Module { + name: "m".to_string(), + imports: vec![], + defs: vec![ + Def::Class(ClassDef { + name: "MyCls".to_string(), + param: "a".to_string(), + superclass: None, + methods: vec![ClassMethod { + name: "mymethod".to_string(), + ty: Type::Fn { + params: vec![Type::Var { name: "a".to_string() }], + param_modes: vec![ParamMode::Borrow], + ret: Box::new(Type::Con { name: "Unit".to_string(), args: vec![] }), + effects: vec![], + }, + default: None, + }], + doc: None, + }), + ], + }, + ); + let ws = build_workspace_for_test(modules); + let env = build_check_env(&ws); + + let mut residuals: Vec = Vec::new(); + let mut counter: u64 = 0; + let mut locals = BTreeMap::new(); + // synth_term with Term::Var { name: "mymethod" } — exact API may differ; + // implementer matches the existing in-test synth-invocation pattern. + let _ty = synth_term_for_test( + &Term::Var { name: "mymethod".to_string() }, + &env, + &mut residuals, + &mut counter, + &mut locals, + ); + + assert_eq!(residuals.len(), 1); + assert_eq!(residuals[0].class, "m.MyCls"); + assert_eq!(residuals[0].method, "mymethod"); + assert!(residuals[0].candidates.is_none(), + "single-candidate path: candidates must be None"); +} +``` + +(`build_workspace_for_test` and `synth_term_for_test` are in-test +helpers if they exist; otherwise the implementer inlines the +synth-invocation pattern from a neighbouring test.) + +- [ ] **Step 2: Run test to confirm GREEN (existing behaviour)** + +Run: `cargo test --workspace -p ailang-check mq2_synth_var_arm_singleton_preserves_single_class_residual` + +Expected: this test should PASS BEFORE the rewrite (existing behaviour +already produces single-class residual). The test is a regression +guard, not RED-first. + +If it fails, the test setup (`build_workspace_for_test`, +`synth_term_for_test`) is wrong — fix the in-test scaffolding. + +- [ ] **Step 3: Locate the existing class-method branch** + +At lib.rs:2028, the existing branch is: + +```rust +} else if let Some(cm) = env.class_methods.get(name) { + // Iter 22b.2 (Task 9): instantiate the class param with + // a fresh metavar; the body's unification at the call + // site fills it in, and the residual is the class + // constraint we owe at this use site. + // ... + let qualified_method_ty = + qualify_local_types(&cm.method_ty, &cm.defining_module, &owner_types); + let fresh = Subst::fresh(counter); + let mut mapping: BTreeMap = BTreeMap::new(); + mapping.insert(cm.class_param.clone(), fresh.clone()); + let inst_ty = substitute_rigids(&qualified_method_ty, &mapping); + residuals.push(ResidualConstraint { + class: cm.class_name.clone(), + type_: fresh, + method: name.clone(), + candidates: None, + }); + return Ok(inst_ty); +} +``` + +- [ ] **Step 4: Rewrite the branch per the 5-step rule** + +Replace the existing `else if let Some(cm) = env.class_methods.get(name)` +branch at lib.rs:2028 with a new branch keyed on +`method_to_candidate_classes`. The new branch handles both the +bare-method form (e.g. `"show"`) and the qualified form (e.g. +`"prelude.Show.show"`) — `parse_method_qualifier` extracts the method +name and optional class qualifier. + +```rust +} else if env + .method_to_candidate_classes + .contains_key(parse_method_qualifier(name).0) +{ + let (method_name, qualifier_prefix) = parse_method_qualifier(name); + let candidates = env + .method_to_candidate_classes + .get(method_name) + .expect("contains_key invariant"); + + // Synth runs at the Var arm before App-arm unification; concrete + // arg type is not yet known. The helper resolves on singleton + // candidates, explicit qualifier, or constraint-driven filter; + // otherwise emits Multi for discharge-time refinement. + let registry_unit: BTreeMap<(String, String), ()> = env + .registry_entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + let outcome = resolve_method_dispatch( + method_name, + qualifier_prefix.as_deref(), + candidates, + /*concrete_arg_type*/ None, + /*declared_constraints*/ &env.active_declared_constraints, + /*registry*/ ®istry_unit, + ); + + // Extract residual shape from outcome; on error variants, return + // early without touching the residual stack. + let (residual_class, residual_candidates) = match outcome { + MethodDispatchOutcome::Resolved(class) => (class, None), + MethodDispatchOutcome::Multi { candidates, method: _ } => { + let tentative = candidates + .iter() + .next() + .cloned() + .unwrap_or_default(); + (tentative, Some(candidates)) + } + MethodDispatchOutcome::UnknownClass(qname) => { + return Err(CheckError::UnknownClass { name: qname }); + } + MethodDispatchOutcome::Ambiguous { method, at_type, candidates } => { + return Err(CheckError::AmbiguousMethodResolution { + method, + at_type, + candidate_classes: candidates, + }); + } + }; + + // Look up the ClassMethodEntry by method name (workspace-flat). + // Today's invariant: any method name in method_to_candidate_classes + // corresponds to exactly one ClassMethodEntry in env.class_methods. + let cm = env.class_methods.get(method_name).expect( + "method_to_candidate_classes invariant: \ + method present implies class_methods entry", + ); + let owner_types = env + .module_types + .get(&cm.defining_module) + .cloned() + .unwrap_or_default(); + let qualified_method_ty = qualify_local_types( + &cm.method_ty, + &cm.defining_module, + &owner_types, + ); + let fresh = Subst::fresh(counter); + let mut mapping: BTreeMap = BTreeMap::new(); + mapping.insert(cm.class_param.clone(), fresh.clone()); + let inst_ty = substitute_rigids(&qualified_method_ty, &mapping); + residuals.push(ResidualConstraint { + class: residual_class, + type_: fresh, + method: method_name.to_string(), + candidates: residual_candidates, + }); + return Ok(inst_ty); +} +``` + +Add the qualifier-parsing helper near the existing `qualify_local_types` +helper (lib.rs scope): + +```rust +/// mq.2: split a `Term::Var.name` into `(method_name, optional_qualifier_prefix)` +/// at the last dot. `"prelude.Show.show"` → `("show", Some("prelude.Show"))`; +/// `"show"` → `("show", None)`. Always returns a method name (no +/// `Option` outer wrapper); a bare name passes through with `None` +/// qualifier. +fn parse_method_qualifier(name: &str) -> (&str, Option) { + if let Some(dot_idx) = name.rfind('.') { + (&name[dot_idx + 1..], Some(name[..dot_idx].to_string())) + } else { + (name, None) + } +} +``` + +Note on `env.registry_entries` and `env.active_declared_constraints`: +the implementer plumbs these accessors through `Env`. `registry_entries` +is the existing workspace registry (already on `Env` via the +workspace reference); `active_declared_constraints` is the current +fn's `Type::Forall.constraints` if synth is inside one, else `&[]` +(default-initialized at synth entry). + +Implementation notes for the `env.active_declared_constraints` and +`env.registry_unit_view` references: the implementer plumbs these +through `Env` (or `build_check_env`'s caller). If the registry is +already accessible on `Env` via a different name, use that name; the +helper accepts `&BTreeMap<(String, String), ()>` so the implementer +constructs a unit view (`.iter().map(|(k, _)| (k.clone(), ()))`) once +at synth-entry time. `active_declared_constraints` is the fn's +`Type::Forall.constraints` if synth is inside one, else `&[]`. + +- [ ] **Step 5: Run the regression test + the six unit tests** + +Run: `cargo test --workspace -p ailang-check mq2_synth_var_arm_singleton mq2_method_dispatch` +Run: `cargo test --workspace --test method_dispatch_pin` + +Expected: all PASS. The synth Var-arm now goes through the helper for +single-class residuals (regression-test PASS) and the six helper +unit tests are unaffected. + +- [ ] **Step 6: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. With `MethodNameCollision` still in place, the +multi-candidate path never fires in real workspaces; the resolver +returns `Resolved` on every singleton candidate set. + +- [ ] **Step 7: Run full cargo workspace test suite** + +Run: `cargo test --workspace` + +Expected: green. Downstream consumers (ail CLI, mono path) see the +same single-class residuals as pre-rewrite. + +--- + +## Task 7: Constraint-discharge refinement for multi-candidate residuals + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:1658-1710` (check_fn residual loop body) + +- [ ] **Step 1: Write a unit test for the multi-candidate concrete-type refinement path** + +Append in `mod tests`: + +```rust +/// mq.2.7: a multi-candidate residual with a concrete `type_` +/// resolved post-unification to `Int` is filtered against the +/// registry. Single survivor → discharged as that class. Multiple +/// survivors → AmbiguousMethodResolution. Zero → NoInstance with +/// candidate-classes populated. +#[test] +fn mq2_discharge_multi_candidate_concrete_type_single_survivor() { + // Synthetic: candidate set {prelude.Show, userlib.Show}; only + // prelude.Show has Show Int in the registry. Discharge resolves + // to prelude.Show. + 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(), // tentative + type_: Type::Con { name: "Int".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(candidates), + }; + let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new(); + let int_h = ailang_core::canonical::type_hash( + &Type::Con { name: "Int".to_string(), args: vec![] } + ); + registry.insert(("prelude.Show".to_string(), int_h), ()); + + let outcome = refine_multi_candidate_residual( + &residual, + /*declared_constraints*/ &[], + /*registry*/ ®istry, + ); + assert_eq!(outcome, RefineOutcome::Resolved("prelude.Show".to_string())); +} + +#[test] +fn mq2_discharge_multi_candidate_concrete_type_zero_survivors_no_instance() { + 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::Con { name: "MyType".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(candidates.clone()), + }; + let registry: BTreeMap<(String, String), ()> = BTreeMap::new(); + let outcome = refine_multi_candidate_residual(&residual, &[], ®istry); + match outcome { + RefineOutcome::NoInstance { candidate_classes, .. } => { + assert_eq!(candidate_classes.len(), 2); + } + other => panic!("expected NoInstance, got {other:?}"), + } +} + +#[test] +fn mq2_discharge_multi_candidate_concrete_type_multi_survivors_ambiguous() { + 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::Con { name: "Int".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(candidates.clone()), + }; + let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new(); + let int_h = ailang_core::canonical::type_hash( + &Type::Con { name: "Int".to_string(), args: vec![] } + ); + registry.insert(("prelude.Show".to_string(), int_h.clone()), ()); + registry.insert(("userlib.Show".to_string(), int_h), ()); + let outcome = refine_multi_candidate_residual(&residual, &[], ®istry); + match outcome { + RefineOutcome::Ambiguous { candidate_classes, .. } => { + assert_eq!(candidate_classes.len(), 2); + } + other => panic!("expected Ambiguous, got {other:?}"), + } +} +``` + +- [ ] **Step 2: Run tests to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_discharge_multi_candidate` + +Expected: compile error — `refine_multi_candidate_residual` and `RefineOutcome` do not exist. + +- [ ] **Step 3: Add `RefineOutcome` and `refine_multi_candidate_residual`** + +Near the helper from Task 5 in `crates/ailang-check/src/lib.rs`: + +```rust +/// mq.2: outcome of multi-candidate residual refinement at discharge +/// time. Consumed by `check_fn`'s residual loop and by mono's +/// residual-to-target mapping. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum RefineOutcome { + Resolved(String), + NoInstance { + method: String, + at_type: String, + candidate_classes: Vec, + }, + Ambiguous { + method: String, + at_type: String, + candidate_classes: Vec, + }, + /// Rigid-var residual with multiple constraint-set survivors. + MissingConstraint { + method: String, + candidate_classes: Vec, + }, +} + +/// mq.2: refine a multi-candidate residual at discharge time per the +/// spec's 5-step rule (constraint-discharge refinement subsection). +/// Caller is responsible for passing residuals whose `candidates` is +/// `Some(...)`; single-candidate residuals (`candidates: None`) bypass +/// this helper. +pub fn refine_multi_candidate_residual( + residual: &ResidualConstraint, + declared_constraints: &[ailang_core::ast::Constraint], + registry: &BTreeMap<(String, String), ()>, +) -> RefineOutcome { + let candidates = residual + .candidates + .as_ref() + .expect("refine_multi_candidate_residual called on single-candidate residual"); + + // Concrete-type path. + if !matches!(residual.type_, Type::Var { .. }) { + let type_h = ailang_core::canonical::type_hash(&residual.type_); + let survivors: Vec = candidates + .iter() + .filter(|c| registry.contains_key(&((**c).clone(), type_h.clone()))) + .cloned() + .collect(); + let at_type = format_type_for_display(&residual.type_); + return match survivors.len() { + 0 => RefineOutcome::NoInstance { + method: residual.method.clone(), + at_type, + candidate_classes: candidates.iter().cloned().collect(), + }, + 1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()), + _ => { + let mut sorted = survivors; + sorted.sort(); + RefineOutcome::Ambiguous { + method: residual.method.clone(), + at_type, + candidate_classes: sorted, + } + } + }; + } + + // Rigid-var path: filter against declared constraints. + let survivors: Vec = candidates + .iter() + .filter(|c| declared_constraints.iter().any(|dc| &dc.class == *c)) + .cloned() + .collect(); + match survivors.len() { + 1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()), + _ => RefineOutcome::MissingConstraint { + method: residual.method.clone(), + candidate_classes: candidates.iter().cloned().collect(), + }, + } +} +``` + +- [ ] **Step 4: Wire the refinement into `check_fn`'s residual-discharge loop** + +At lib.rs:1658-1710 (per recon, the residual loop body inside +`check_fn`), branch on `residual.candidates.is_some()` BEFORE the +existing single-class registry lookup. For multi-candidate residuals, +call `refine_multi_candidate_residual`, then either continue with the +resolved class or return the appropriate `CheckError`. + +Insertion site (just inside the residual `for r in residuals` loop, +before the existing single-class discharge): + +```rust +if r.candidates.is_some() { + let registry_unit: BTreeMap<(String, String), ()> = ws + .registry + .entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + match refine_multi_candidate_residual(r, &declared_constraints, ®istry_unit) { + RefineOutcome::Resolved(class) => { + // Overwrite r.class for the downstream discharge path. + // Discharge proceeds against (class, type_hash(r.type_)) below. + let resolved_class = class; + // ...continue with existing single-class discharge using `resolved_class`... + } + RefineOutcome::NoInstance { method, at_type, candidate_classes } => { + return Err(CheckError::NoInstance { + class: r.class.clone(), // tentative; candidate_classes is authoritative + method, + at_type, + candidate_classes, + }); + } + RefineOutcome::Ambiguous { method, at_type, candidate_classes } => { + return Err(CheckError::AmbiguousMethodResolution { + method, + at_type, + candidate_classes, + }); + } + RefineOutcome::MissingConstraint { method, candidate_classes } => { + return Err(CheckError::MissingConstraint { + class: candidate_classes.first().cloned().unwrap_or_default(), + method, + at_type: format_type_for_display(&r.type_), + }); + } + } + continue; +} +``` + +(The implementer adjusts the snippet to fit the actual control flow +of the existing residual loop. The key invariant: multi-candidate +residuals never reach the single-class discharge path; they either +resolve to a single class or emit a `CheckError`.) + +- [ ] **Step 5: Run discharge tests to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_discharge_multi_candidate` + +Expected: all three tests PASS. + +- [ ] **Step 6: Run full workspace test suite** + +Run: `cargo test --workspace` + +Expected: green. With `MethodNameCollision` still active, the +multi-candidate residual never appears in real workspaces; the new +discharge path is exercised only by these unit tests. + +--- + +## Task 8: Mono's residual mapping handles multi-candidate path + +**Files:** +- Modify: `crates/ailang-check/src/mono.rs:1178-1197` (collect_residuals_ordered residual-to-target mapping) + +- [ ] **Step 1: Write unit tests for mono's residual-class resolver** + +Append in `crates/ailang-check/src/mono.rs` `mod tests`: + +```rust +/// mq.2.8: mono's residual-class resolver refines multi-candidate +/// residuals via the same logic as discharge. A multi-candidate +/// residual with a concrete `type_` and a single registry-survivor +/// resolves to that class. +#[test] +fn mq2_mono_multi_candidate_resolves_to_single_class() { + let mut candidates = std::collections::BTreeSet::new(); + candidates.insert("prelude.Show".to_string()); + candidates.insert("userlib.Show".to_string()); + let residual = crate::ResidualConstraint { + class: "prelude.Show".to_string(), // tentative + type_: Type::Con { name: "Int".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(candidates), + }; + let mut registry_unit: std::collections::BTreeMap<(String, String), ()> = Default::default(); + let int_h = ailang_core::canonical::type_hash( + &Type::Con { name: "Int".to_string(), args: vec![] } + ); + registry_unit.insert(("prelude.Show".to_string(), int_h), ()); + + let resolved = resolve_residual_class_for_mono(&residual, ®istry_unit); + assert_eq!(resolved, Some("prelude.Show".to_string())); +} + +/// mq.2.8: single-class residual (candidates: None) flows through +/// unchanged. +#[test] +fn mq2_mono_single_class_residual_unchanged() { + let residual = crate::ResidualConstraint { + class: "prelude.Eq".to_string(), + type_: Type::Con { name: "Int".to_string(), args: vec![] }, + method: "eq".to_string(), + candidates: None, + }; + let registry_unit: std::collections::BTreeMap<(String, String), ()> = Default::default(); + let resolved = resolve_residual_class_for_mono(&residual, ®istry_unit); + assert_eq!(resolved, Some("prelude.Eq".to_string())); +} + +/// mq.2.8: multi-candidate residual that cannot refine (zero +/// registry survivors) returns None. +#[test] +fn mq2_mono_multi_candidate_no_survivors_returns_none() { + let mut candidates = std::collections::BTreeSet::new(); + candidates.insert("prelude.Show".to_string()); + candidates.insert("userlib.Show".to_string()); + let residual = crate::ResidualConstraint { + class: "prelude.Show".to_string(), + type_: Type::Con { name: "MyType".to_string(), args: vec![] }, + method: "show".to_string(), + candidates: Some(candidates), + }; + let registry_unit: std::collections::BTreeMap<(String, String), ()> = Default::default(); + let resolved = resolve_residual_class_for_mono(&residual, ®istry_unit); + assert_eq!(resolved, None); +} +``` + +- [ ] **Step 2: Run tests to confirm RED** + +Run: `cargo test --workspace -p ailang-check mq2_mono` + +Expected: compile error — `resolve_residual_class_for_mono` does not exist. + +- [ ] **Step 3: Adjust mono's residual-to-target mapping inline** + +At mono.rs:1178-1197 (per recon, where residuals get mapped to +`MonoTarget::ClassMethod`), the existing code reads: + +```rust +let registry_key = (r.class.clone(), ailang_core::canonical::type_hash(&t_ty_norm)); +let entry = ws.registry.entries.get(®istry_key); +match entry { + Some(entry) => MonoTarget::ClassMethod { /* ... */ }, + None => /* None-slot or error */, +} +``` + +(Exact shape varies; implementer reads the in-place lines.) + +Modify the existing site to refine the residual's class BEFORE +constructing the registry key. The refinement uses +`refine_multi_candidate_residual` from Task 7 (importable via +`crate::refine_multi_candidate_residual`), with `declared_constraints` +typically `&[]` here because mono runs post-typecheck on monomorphic +specializations — but the active declared constraints are still +plumbed in by `collect_residuals_ordered`'s caller and used for +correctness on the rigid-var path (which mono shouldn't normally +see in post-check, but the helper handles it for safety). + +The inline branch: + +```rust +// mq.2: refine multi-candidate residuals before mono target lookup. +// Single-class residuals (candidates: None) skip refinement and use +// r.class directly. +let resolved_class = if r.candidates.is_some() { + let registry_unit: BTreeMap<(String, String), ()> = ws + .registry + .entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + match crate::refine_multi_candidate_residual( + r, + /*declared_constraints*/ &[], + ®istry_unit, + ) { + crate::RefineOutcome::Resolved(c) => c, + // Ambiguous / NoInstance / MissingConstraint already fired + // at typecheck discharge (Task 7); reaching here means + // mono is processing a residual that check_fn should have + // rejected. Emit a None-slot defensively — the original + // CheckError already propagated to the user. + _ => return None, + } +} else { + r.class.clone() +}; + +let registry_key = (resolved_class.clone(), ailang_core::canonical::type_hash(&t_ty_norm)); +let entry = ws.registry.entries.get(®istry_key); +// ...existing match on `entry` continues unchanged, building +// MonoTarget::ClassMethod { class: resolved_class, ... } in the +// Some(entry) branch. +``` + +This replaces `r.class.clone()` with `resolved_class` in the +existing registry-key construction and in the `MonoTarget::ClassMethod +{ class: ... }` construction. Implementer makes the two-line edit +plus the prepended `let resolved_class = if r.candidates.is_some() { ... }` +block. + +For the unit test in Step 1 (`map_residual_to_mono_target` named +helper), the test calls into mono directly. Implementer either: (a) +extracts the `let resolved_class = ...` snippet into a small +`fn resolve_residual_class_for_mono(r, registry_unit) -> Option` +in mono.rs that the test can call, returning `Some(class)` for the +Resolved case and `None` for the abort cases; or (b) rewrites the +unit test to drive `collect_residuals_ordered` end-to-end on a +synthetic Workspace and assert the resulting MonoTarget. Path (a) is +simpler — five-line helper, single test consumer. + +If implementer picks path (a), the helper signature is: + +```rust +/// mq.2: resolve a residual's class for mono target construction. +/// Returns `Some(class)` for a discharge-ready residual (single-class +/// or refined-multi-candidate); `None` if the multi-candidate +/// residual cannot be refined (typecheck-side error already raised). +fn resolve_residual_class_for_mono( + r: &crate::ResidualConstraint, + registry_unit: &BTreeMap<(String, String), ()>, +) -> Option { + if r.candidates.is_some() { + match crate::refine_multi_candidate_residual(r, &[], registry_unit) { + crate::RefineOutcome::Resolved(c) => Some(c), + _ => None, + } + } else { + Some(r.class.clone()) + } +} +``` + +And the unit test from Step 1 is rewritten to call +`resolve_residual_class_for_mono` directly. The end-to-end mono +behaviour (`MonoTarget` construction) is then covered by the existing +mono test suite (which keeps passing because single-class residuals +flow through `Some(r.class.clone())` unchanged). + +- [ ] **Step 4: Run mono multi-candidate test to confirm GREEN** + +Run: `cargo test --workspace -p ailang-check mq2_mono_multi_candidate` + +Expected: PASS. + +- [ ] **Step 5: Run full ailang-check test suite** + +Run: `cargo test --workspace -p ailang-check` + +Expected: green. Pre-mq.2 mono behaviour preserved for single-candidate +residuals. + +--- + +## Task 9: Integration verification — full workspace + bench scripts + +**Files:** none modified; verification only. + +- [ ] **Step 1: Full `cargo test --workspace`** + +Run: `cargo test --workspace` + +Expected: green. All ~530 tests across 16 binary-test suites pass. + +- [ ] **Step 2: Run the six dispatch-pin tests directly** + +Run: `cargo test --workspace --test method_dispatch_pin` + +Expected: 6 PASS. + +- [ ] **Step 3: Verify no behavioural change on the prelude / existing fixtures** + +Run: `cargo run -p ail -- check examples/prelude.ail.json` +Expected: exit 0. + +Run: `cargo run -p ail -- check examples/mq1_xmod_constraint_class.ail.json` +Expected: exit 0. + +Run: `cargo run -p ail -- check examples/eq_ord_polymorphic.ail.json` +Expected: exit 0. + +- [ ] **Step 4: Bench scripts** + +Run: `python3 bench/check.py` +Expected: exit 0 OR audit-ratified — note in the journal whether +new variant additions shift any measured metric. + +Run: `python3 bench/compile_check.py` +Expected: exit 0 OR audit-ratified. + +Run: `python3 bench/cross_lang.py` +Expected: exit 0 OR audit-ratified. + +- [ ] **Step 5: Roundtrip-check the prelude** + +Run: `git diff -- examples/prelude.ail.json` + +Expected: no output (mq.2 is pure infrastructure addition; prelude is +unchanged). + +- [ ] **Step 6: Confirm the per-iter journal placeholder is staged** + +The implementer leaves `docs/journals/2026-05-13-iter-mq.2.md` (or the +date the iter actually finishes) in the working tree with a draft +entry covering: tasks ran, deviations from plan (if any), test counts, +bench outcomes, and notes on the `MethodNameCollision`-still-gates-real- +workspaces observation (the new dispatch path was exercised exclusively +by unit tests in this iter). Append a pointer line to +`docs/journals/INDEX.md`. The Boss commits.