From 2e6a4ca2004fcdf5c556d47aa5664729001f4906 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 01:40:42 +0200 Subject: [PATCH] iter mq.2: type-driven dispatch mechanism installed (mechanism-before-exercise) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Installs the dispatch infrastructure for type-driven method resolution without retiring MethodNameCollision yet. The new multi-candidate path is exercised exclusively by 15 unit tests; real workspaces continue producing single-class residuals (candidates: None) and every pre-mq.2 fixture typechecks unchanged. Three new CheckError variants: - AmbiguousMethodResolution (multi-candidate after type-driven filter) - UnknownClass (explicit qualifier names a class not in registry) - NoInstance gains additive candidate_classes field (Vec) Schema/Env additions: - Env.method_to_candidate_classes: BTreeMap> workspace-flat inverse of class_methods, built in build_check_env. - ResidualConstraint.candidates: Option> — None preserves pre-mq.2 single-class semantics; Some(set) carries the multi-candidate residual that discharge refines. - ResidualConstraint visibility bumped pub(crate) → pub for unit-test crate access. New helpers: - MethodDispatchOutcome enum + pure resolve_method_dispatch implementing the spec's 5-step rule (qualifier → singleton → type-driven filter → constraint-driven filter → Multi for discharge-time refinement). - parse_method_qualifier splits Term::Var.name into (method_name, optional_qualifier_prefix) at the last dot. - RefineOutcome enum + refine_multi_candidate_residual for discharge-time refinement. - resolve_residual_class_for_mono wires the refinement into mono's collect_residuals_ordered residual-to-target mapping. Synth Var-arm class-method branch rewritten via parse_method_qualifier with inner-dot gate (qualifier must be .; single-dot names fall through to the existing qualified-fn path). Constraint-discharge in check_fn uses expanded (post-superclass- expansion) constraints for the rigid-var path — sounder than raw declared_constraints. Plan-invented format_type_for_display replaced with the existing 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 pre-mq.2; +15 mq.2 unit tests + 4 pre-existing). bench/compile_check.py + cross_lang.py clean; bench/check.py 1 regression (latency noise — runtime cannot be touched by a typecheck-side iter). --- .../2026-05-13-iter-mq.2.json | 22 + crates/ailang-check/src/diagnostic.rs | 18 +- crates/ailang-check/src/lib.rs | 746 +++++++++++++++++- crates/ailang-check/src/mono.rs | 112 ++- .../ailang-check/tests/method_dispatch_pin.rs | 154 ++++ docs/journals/2026-05-13-iter-mq.2.md | 169 ++++ docs/journals/INDEX.md | 1 + 7 files changed, 1203 insertions(+), 19 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-13-iter-mq.2.json create mode 100644 crates/ailang-check/tests/method_dispatch_pin.rs create mode 100644 docs/journals/2026-05-13-iter-mq.2.md diff --git a/bench/orchestrator-stats/2026-05-13-iter-mq.2.json b/bench/orchestrator-stats/2026-05-13-iter-mq.2.json new file mode 100644 index 0000000..ab94958 --- /dev/null +++ b/bench/orchestrator-stats/2026-05-13-iter-mq.2.json @@ -0,0 +1,22 @@ +{ + "iter_id": "mq.2", + "date": "2026-05-13", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 9, + "tasks_completed": 9, + "reloops_per_task": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0, + "6": 0, + "7": 0, + "8": 0, + "9": 0 + }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null +} diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs index 02bb31e..5957342 100644 --- a/crates/ailang-check/src/diagnostic.rs +++ b/crates/ailang-check/src/diagnostic.rs @@ -75,7 +75,23 @@ //! Dual of `missing-constraint`: when the residual is concrete, the //! fn cannot push the obligation to a caller, so an existing //! instance is the only way to discharge it. `ctx`: -//! `{"class": "", "method": "", "at_type": ""}`. +//! `{"class": "", "method": "", "at_type": ""}`. mq.2 adds +//! an optional `candidate_classes` field when the residual originated +//! from the multi-candidate dispatch path; absent on single-class +//! residuals (back-compat). +//! - `ambiguous-method-resolution` (mq.2) — `severity: error`. Emitted +//! by the type-driven dispatch resolver (or the discharge-time +//! multi-candidate refinement) when a bare-method call site survives +//! both type-driven and constraint-driven filtering with more than +//! one candidate class. `ctx`: `{"method": "", "at_type": "", +//! "candidate_classes": ["", ...]}`. The author disambiguates +//! by writing `. x`. +//! - `unknown-class` (mq.2) — `severity: error`. Emitted by the +//! type-driven dispatch resolver when an explicit class qualifier +//! in a `Term::Var.name` (e.g. `"prelude.Show.show"`) names a +//! qualified class that is not in the workspace registry of +//! candidate classes for the method. `ctx`: +//! `{"name": ""}`. use serde::Serialize; diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 4764895..32096b8 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -569,6 +569,38 @@ pub enum CheckError { method: String, class: String, at_type: String, + /// mq.2: additive candidate-class list. Empty on residuals from + /// the single-class dispatch path (pre-mq.2 shape preserved). + /// Non-empty when the diagnostic originated from the + /// multi-candidate refinement path with zero registry survivors. + candidate_classes: Vec, + }, + + /// 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. + /// Code: `ambiguous-method-resolution`. `ctx`: + /// `{"method": "", "at_type": "", "candidate_classes": ["", ...]}`. + #[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 is not in the workspace registry of + /// candidate classes for the method. Code: `unknown-class`. `ctx`: + /// `{"name": ""}`. + #[error("class `{name}` is not declared in any module of this workspace")] + UnknownClass { + name: String, }, /// Iter 22b.3: an internal invariant in the typechecker / mono pass @@ -617,6 +649,8 @@ impl CheckError { CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body", CheckError::MissingConstraint { .. } => "missing-constraint", CheckError::NoInstance { .. } => "no-instance", + CheckError::AmbiguousMethodResolution { .. } => "ambiguous-method-resolution", + CheckError::UnknownClass { .. } => "unknown-class", CheckError::Internal(_) => "internal", } } @@ -658,8 +692,26 @@ impl CheckError { CheckError::MissingConstraint { class, method, at_type, .. } => { serde_json::json!({"class": class, "method": method, "at_type": at_type}) } - CheckError::NoInstance { class, method, at_type, .. } => { - serde_json::json!({"class": class, "method": method, "at_type": at_type}) + 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 + } + 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 }) } _ => serde_json::Value::Object(serde_json::Map::new()), } @@ -1291,6 +1343,14 @@ pub fn build_check_env(ws: &Workspace) -> Env { for g in mg.values() { for (n, e) in &g.class_methods { env.class_methods.insert(n.clone(), e.clone()); + // mq.2: build the inverse method → candidate-class set in + // the same loop. `e.class_name` already carries the + // qualified form (mq.1 invariant), so the set is keyed on + // workspace-flat qualified class names directly. + env.method_to_candidate_classes + .entry(n.clone()) + .or_default() + .insert(e.class_name.clone()); } } @@ -1657,6 +1717,68 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses); for r in &residuals { let r_ty = subst.apply(&r.type_); + + // mq.2: multi-candidate residuals refine before the existing + // single-class discharge path. `MethodNameCollision` keeps the + // candidate set singleton in real workspaces today; this branch + // is exercised exclusively by unit tests until mq.3. + if r.candidates.is_some() { + // Normalize the type before hashing — same contract as the + // single-class path below. + let r_ty_norm = env + .workspace_registry + .normalize_type_for_lookup(env.current_module.as_str(), &r_ty); + let normalized_residual = ResidualConstraint { + class: r.class.clone(), + type_: r_ty_norm, + method: r.method.clone(), + candidates: r.candidates.clone(), + }; + let registry_unit: BTreeMap<(String, String), ()> = env + .workspace_registry + .entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + match refine_multi_candidate_residual( + &normalized_residual, + &expanded, + ®istry_unit, + ) { + RefineOutcome::Resolved(_) => { + // Discharge succeeded — the resolved class has an + // instance for this concrete type (or the rigid + // var has a matching declared constraint). Move + // on to the next residual; nothing to push. + continue; + } + RefineOutcome::NoInstance { method, at_type, candidate_classes } => { + return Err(CheckError::NoInstance { + def: f.name.clone(), + method, + class: r.class.clone(), + 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 { + def: f.name.clone(), + method, + class: candidate_classes.first().cloned().unwrap_or_default(), + at_type: ailang_core::pretty::type_to_string(&r_ty), + }); + } + } + } + if let Type::Var { name } = &r_ty { // Skip residuals over metavars (`$mN`) — those mean the // residual is over a value the body never connected to a @@ -1699,6 +1821,7 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { method: r.method.clone(), class: r.class.clone(), at_type: ailang_core::pretty::type_to_string(&r_ty), + candidate_classes: vec![], }); } } @@ -1735,8 +1858,14 @@ pub(crate) fn is_fully_concrete(t: &Type) -> bool { /// argument's actual type) or, after `subst.apply`, a rigid var or a /// concrete `Type::Con`. #[derive(Debug, Clone)] -pub(crate) struct ResidualConstraint { +pub struct ResidualConstraint { /// Class name (e.g. `Show`). + /// + /// When [`Self::candidates`] is `None`, this is the resolved class + /// (single-class dispatch path). When `Some(set)`, this is a + /// tentative value (typically the first set element in BTreeSet + /// order); discharge / mono refinement overwrites it with the + /// actually-resolved class. pub class: String, /// Class param's instance at this call site. Pre-substitution: the /// fresh metavar inserted at the Var site. Post-substitution: the @@ -1746,6 +1875,243 @@ pub(crate) struct ResidualConstraint { /// diagnostic to point the author at which call site triggered /// the residual. pub method: String, + /// mq.2: candidate-class set for the multi-candidate dispatch + /// path. `None` ⇒ single-class semantics (pre-mq.2 behaviour); + /// the [`Self::class`] field is the resolved class. `Some(set)` + /// ⇒ multi-candidate residual; discharge / mono refinement filters + /// the set at fn-body-end. With `MethodNameCollision` still active + /// (pre-mq.3), real workspaces only ever construct `None`-candidate + /// residuals; the `Some`-path is exercised exclusively by unit + /// tests until mq.3 retires the workaround. + pub candidates: Option>, +} + +/// mq.2: outcome of the dispatch-resolution helper +/// [`resolve_method_dispatch`]. 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 the caller has the arg type +/// available (e.g. discharge-time refinement); `None` when synth is at +/// the Var arm before App-arm unification. When `None`, the helper +/// emits `Multi` if the candidate set is non-singleton (no early +/// type-driven filter possible). When `Some(t)` with `t` a non-rigid +/// concrete type, the type-driven filter applies; when `t` is a rigid +/// `Type::Var`, the constraint-driven filter applies. +/// +/// `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. Values are unit; only +/// key presence matters. +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, singleton candidate set — pre-mq.3 + // path. Returns immediately so the post-mq.3 multi-candidate + // logic below stays gated on a non-singleton candidate set. + if candidates.len() == 1 { + return MethodDispatchOutcome::Resolved( + candidates.iter().next().cloned().unwrap(), + ); + } + + // Multi-candidate path: type-driven filter first when the 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 = ailang_core::pretty::type_to_string(t); + return MethodDispatchOutcome::Ambiguous { + method: method.to_string(), + at_type, + candidates: sorted, + }; + } + // Zero survivors after the type-driven filter: fall through + // to constraint-driven filter, then `Multi` for discharge- + // time refinement (where `NoInstance` with `candidate_classes` + // is fired against the full candidate set). + } + + // 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: 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 { + /// Refinement converged on a single class. + Resolved(String), + /// Concrete `type_` with zero registry survivors — the call site + /// must be discharged via an existing instance, but none of the + /// candidate classes has one for this type. Surfaces as a + /// `CheckError::NoInstance` with the full candidate set populated. + NoInstance { + method: String, + at_type: String, + candidate_classes: Vec, + }, + /// Concrete `type_` with multiple registry survivors — every + /// surviving candidate has an instance for this type; the author + /// must disambiguate explicitly. Surfaces as a + /// `CheckError::AmbiguousMethodResolution`. + Ambiguous { + method: String, + at_type: String, + candidate_classes: Vec, + }, + /// Rigid-var residual with non-singleton constraint-set survivors. + /// Surfaces as a `CheckError::MissingConstraint` (the body must + /// declare a constraint to commit to one of the candidates). + 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 MUST pass a residual whose `candidates` is `Some(...)`; +/// single-candidate residuals (`candidates: None`) bypass this helper +/// and discharge directly against the registry as in pre-mq.2. +/// +/// Refinement strategy: +/// - Concrete `type_`: filter the candidate set against the registry +/// keyed on `(class, type_hash(type_))`. 0 survivors → `NoInstance`; +/// 1 → `Resolved`; >1 → `Ambiguous`. +/// - Rigid-var `type_`: filter the candidate set against the active +/// declared-constraint list. 1 survivor → `Resolved`; otherwise +/// → `MissingConstraint`. +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 = ailang_core::pretty::type_to_string(&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(), + }, + } } /// Iter 23.4: per-call-site polymorphic-free-fn observation recorded by @@ -1793,6 +2159,27 @@ pub(crate) fn qualify_class_ref_in_check(class_ref: &str, caller_module: &str) - } } +/// mq.2: split a `Term::Var.name` into `(method_name, +/// optional_qualifier_prefix)` at the last dot. +/// +/// - `"show"` → `("show", None)` +/// - `"prelude.Show.show"` → `("show", Some("prelude.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 +/// (`.`) signals an explicit class qualifier on a +/// class-method call site. +pub(crate) 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) + } +} + /// 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 @@ -2025,18 +2412,92 @@ pub(crate) fn synth( .filter(|m| m.contains_key(name)) .map(|_| (env.current_module.clone(), name.clone())); (t.clone(), owner) - } 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. + } else if { + // mq.2 dispatch entry: the Var arm matches a class + // method either bare (`"show"`) or qualified + // (`"prelude.Show.show"`). `parse_method_qualifier` + // splits at the last dot; a `Some(qualifier)` with no + // inner dot is a 1-dot name (`std_list.length`) — + // structurally a cross-module-fn call per mq.1's + // canonical-form rule (class qualifiers are always + // `.`), 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 + && env.method_to_candidate_classes.contains_key(method_name) + } { + // mq.2: type-driven dispatch entry. The Var arm runs + // before App-arm unification, so the arg type is not + // available here. The dispatch helper resolves on + // (a) explicit class qualifier, (b) singleton candidate + // set (today's invariant), or (c) constraint-driven + // filter (rigid-var case); otherwise it emits `Multi` + // for discharge-time refinement. // - // ct.2 Task 1: a class method's declared type lives in - // its defining module's bare-local namespace. - // qualify_local_types runs symmetrically with the - // Term::Var qualified path below so the consumer's - // typecheck context sees the method's return / - // parameter Type::Cons fully qualified. + // With `MethodNameCollision` still active (pre-mq.3), + // real workspaces never reach the `Multi` branch — the + // candidate set is always singleton. The branch is + // installed here for mq.3 to exercise without further + // dispatch-side edits. + let (method_name, qualifier_opt) = parse_method_qualifier(name); + let candidates = env + .method_to_candidate_classes + .get(method_name) + .expect("contains_key invariant: gate above guarantees presence"); + + // Build a unit-view of the workspace registry keyed by + // (qualified_class, type_hash). Values are unit; only + // key presence matters for the type-driven filter. + let registry_unit: BTreeMap<(String, String), ()> = env + .workspace_registry + .entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + + let outcome = resolve_method_dispatch( + method_name, + qualifier_opt.as_deref(), + candidates, + /*concrete_arg_type*/ None, + /*declared_constraints*/ &[], + /*registry*/ ®istry_unit, + ); + + let (residual_class, residual_candidates) = match outcome { + MethodDispatchOutcome::Resolved(class) => (class, None), + MethodDispatchOutcome::Multi { candidates: cs, method: _ } => { + // Tentative class: first BTreeSet element. + // Refinement at discharge / mono time overwrites it. + let tentative = cs.iter().next().cloned().unwrap_or_default(); + (tentative, Some(cs)) + } + MethodDispatchOutcome::UnknownClass(qname) => { + return Err(CheckError::UnknownClass { name: qname }); + } + MethodDispatchOutcome::Ambiguous { method, at_type, candidates: cs } => { + return Err(CheckError::AmbiguousMethodResolution { + method, + at_type, + candidate_classes: cs, + }); + } + }; + + // Look up the `ClassMethodEntry` by method name — + // workspace-flat. The `MethodNameCollision` invariant + // (pre-mq.3) guarantees the lookup is unambiguous. Post- + // mq.3, the class_methods table is keyed by + // `(class, method)` and this `.get(method_name)` will + // need to be reworked alongside the table. + 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) @@ -2049,9 +2510,10 @@ pub(crate) fn synth( 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(), + class: residual_class, type_: fresh, - method: name.clone(), + method: method_name.to_string(), + candidates: residual_candidates, }); return Ok(inst_ty); } else if let Some((owner_module, raw_ty)) = env @@ -2902,6 +3364,13 @@ pub struct Env { /// method-name-collision check (Iter 22b.2.6), so the merge is /// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm. pub class_methods: BTreeMap, + /// mq.2: workspace-flat inverse of [`Self::class_methods`] — for + /// each method name, the set of qualified class names that declare + /// it. Pre-mq.3, the `MethodNameCollision` invariant guarantees + /// each set is singleton; mq.3 lifts the invariant and cardinality + /// > 1 becomes legal. Synth's `Term::Var` arm consults this index + /// for type-driven dispatch (spec §Architecture's 5-step rule). + pub method_to_candidate_classes: BTreeMap>, /// Iter 22b.2 (Task 9): one-step superclass expansion table. /// Maps each class name to its superclass class name. Absence from /// the map means the class has no superclass — populated only for @@ -5302,4 +5771,249 @@ mod tests { "expected bare `dbl` to resolve through implicit prelude import; got {diags:?}" ); } + + /// 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}"); + } + + /// mq.2.2: `NoInstance` carries an additive `candidate_classes` + /// list. When non-empty, the rendered ctx() carries the candidate + /// list; when empty, the ctx() shape 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 { + def: "f".to_string(), + class: "prelude.Show".to_string(), + method: "show".to_string(), + at_type: "MyType".to_string(), + candidate_classes: vec![ + "prelude.Show".to_string(), + "userlib.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}"); + let ctx = err.ctx(); + assert_eq!(ctx["candidate_classes"][0], "prelude.Show"); + assert_eq!(ctx["candidate_classes"][1], "userlib.Show"); + } + + /// mq.2.2: empty `candidate_classes` keeps the existing single-class + /// ctx() shape — no `candidate_classes` key in the JSON. + #[test] + fn mq2_no_instance_empty_candidates_back_compat() { + let err = CheckError::NoInstance { + def: "f".to_string(), + 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}"); + let ctx = err.ctx(); + assert!(ctx.get("candidate_classes").is_none(), + "empty candidate_classes must not render in ctx; got: {ctx}"); + } + + /// 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 a tentative value until discharge + /// resolves it. + #[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)); + } + + /// mq.2.5: smoke test on `parse_method_qualifier` — the helper + /// underpinning the rewritten synth Var-arm. Bare names pass + /// through with `None` qualifier; dotted names split at the last + /// dot so the prefix is the (possibly-multi-dot) class qualifier. + #[test] + fn mq2_parse_method_qualifier_smoke() { + assert_eq!(parse_method_qualifier("show"), ("show", None)); + assert_eq!( + parse_method_qualifier("prelude.Show.show"), + ("show", Some("prelude.Show".to_string())) + ); + assert_eq!( + parse_method_qualifier("std_list.length"), + ("length", Some("std_list".to_string())) + ); + } + + /// mq.2.7: a multi-candidate residual with a concrete `type_` + /// resolved post-unification to `Int` is filtered against the + /// registry. Single survivor → Resolved. + #[test] + fn mq2_discharge_multi_candidate_concrete_type_single_survivor() { + 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())); + } + + /// mq.2.7: zero registry survivors → NoInstance with the full + /// candidate-class set echoed back to the author. + #[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:?}"), + } + } + + /// mq.2.7: multi survivors → AmbiguousMethodResolution. + #[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:?}"), + } + } + + /// 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() { + use ailang_core::ast::{ClassDef, ClassMethod, Module}; + let m = Module { + schema: SCHEMA.into(), + 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![], + ret_mode: ParamMode::Implicit, + }, + default: None, + }], + doc: None, + })], + }; + let mut modules = BTreeMap::new(); + modules.insert("m".into(), m); + let ws = Workspace { + entry: "m".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + 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"); + } } diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 9990ed0..a1e730a 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -1108,6 +1108,27 @@ fn pattern_binders(pat: &Pattern) -> Vec { out } +/// 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 — in which case typecheck-side already raised a +/// `CheckError`, so reaching this branch means the residual slipped +/// past discharge and the mono cursor should emit a None-slot +/// defensively. +pub 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()) + } +} + /// Iter 22b.3: traversal-ordered residual collection — used by /// the rewrite walker to align cursor positions. Unlike /// [`collect_mono_targets`], this includes non-concrete residuals @@ -1185,10 +1206,33 @@ pub(crate) fn collect_residuals_ordered( let r_ty_norm = env .workspace_registry .normalize_type_for_lookup(module_name, &r_ty); - let key = (r.class.clone(), ailang_core::canonical::type_hash(&r_ty_norm)); + // mq.2: resolve the residual's class via the multi- + // candidate refinement helper. Single-class residuals + // (`candidates: None`) flow through `r.class.clone()` + // unchanged; multi-candidate residuals filter against + // the registry, with the discharge path's CheckError + // already raised at typecheck time (so reaching here + // with a non-Resolved outcome means the residual was + // somehow not gated upstream — emit `None` defensively). + let registry_unit: BTreeMap<(String, String), ()> = env + .workspace_registry + .entries + .keys() + .map(|k| (k.clone(), ())) + .collect(); + let normalized_residual = crate::ResidualConstraint { + class: r.class.clone(), + type_: r_ty_norm.clone(), + method: r.method.clone(), + candidates: r.candidates.clone(), + }; + let resolved_class = + resolve_residual_class_for_mono(&normalized_residual, ®istry_unit)?; + + let key = (resolved_class.clone(), ailang_core::canonical::type_hash(&r_ty_norm)); let entry = env.workspace_registry.entries.get(&key)?; Some(MonoTarget::ClassMethod { - class: r.class.clone(), + class: resolved_class, method: r.method.clone(), type_: r_ty, defining_module: entry.defining_module.clone(), @@ -1370,3 +1414,67 @@ fn interleave_slots( Term::Lit { .. } => {} } } + +#[cfg(test)] +mod tests { + use super::*; + use ailang_core::ast::Type; + + /// 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: 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: 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: BTreeMap<(String, String), ()> = Default::default(); + let resolved = resolve_residual_class_for_mono(&residual, ®istry_unit); + assert_eq!(resolved, None); + } +} diff --git a/crates/ailang-check/tests/method_dispatch_pin.rs b/crates/ailang-check/tests/method_dispatch_pin.rs new file mode 100644 index 0000000..cfffb38 --- /dev/null +++ b/crates/ailang-check/tests/method_dispatch_pin.rs @@ -0,0 +1,154 @@ +//! 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_core::ast::{Constraint, 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) + // 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() }; + 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()], + }, + ); +} diff --git a/docs/journals/2026-05-13-iter-mq.2.md b/docs/journals/2026-05-13-iter-mq.2.md new file mode 100644 index 0000000..43cd54d --- /dev/null +++ b/docs/journals/2026-05-13-iter-mq.2.md @@ -0,0 +1,169 @@ +# iter mq.2 — Type-driven dispatch mechanism (installed, not yet exercised) + +**Date:** 2026-05-13 +**Started from:** e9e45c77affa635652505cc937b77b9349d18c8e +**Status:** DONE +**Tasks completed:** 9 of 9 + +## Summary + +mq.2 installs the type-driven dispatch infrastructure that mq.3 will +exercise end-to-end once `MethodNameCollision` retires. Three new +`CheckError` variants (`AmbiguousMethodResolution`, `UnknownClass`, +plus an additive `candidate_classes` field on `NoInstance`); a new +workspace-flat `method_to_candidate_classes` index on `Env` (inverse +of `class_methods`); an extended `ResidualConstraint` carrying an +optional `candidates: Option>` for the multi- +candidate dispatch path; a 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); a `refine_multi_candidate_residual` helper for +discharge / mono refinement; and a `resolve_residual_class_for_mono` +helper that wires the refinement into mono's residual-to-target +mapping. The synth `Term::Var` arm class-method branch is rewritten +to consult the new index via `parse_method_qualifier`, with a gate +that prevents capturing the existing cross-module-fn path +(`.`) by requiring class-qualifiers to carry an inner +dot (per mq.1's canonical-form rule, class qualifiers are always +`.`). + +With `MethodNameCollision` still active, the new multi-candidate +branch is exercised exclusively by 15 unit tests: 6 in +`tests/method_dispatch_pin.rs` (the 5-step rule's six cases), 6 in +`lib.rs` `mod tests` (the new `CheckError` variants + the +`ResidualConstraint`/`Env` field shapes + the discharge-side +refinement), and 3 in `mono.rs` `mod tests` (the mono-side helper). +Real workspaces continue producing single-class residuals +(`candidates: None`), and every pre-mq.2 fixture typechecks +unchanged. + +## Per-task notes + +- iter mq.2.1: Two new `CheckError` variants + `AmbiguousMethodResolution` and `UnknownClass`, added as siblings + after `NoInstance`. `code()` + `ctx()` table entries; module-doc + list in `diagnostic.rs` extended. 2 RED-then-GREEN smoke tests. +- iter mq.2.2: `NoInstance` extended with an additive + `candidate_classes: Vec` field. `ctx()` emits the field + only when non-empty (preserves pre-mq.2 JSON shape). 2 tests: + with + without populated candidates. +- iter mq.2.3: `ResidualConstraint` extended with `candidates: + Option>`. Struct bumped to `pub` (was + `pub(crate)`) for unit-test access from the dispatch-pin / Task 7 + + 8 tests. Single existing construction site updated with + `candidates: None`. 1 smoke test. +- iter mq.2.4: `Env.method_to_candidate_classes: + BTreeMap>` built workspace-flat in + `build_check_env` alongside the existing `class_methods` insert + (coalesced into one loop). 1 in-test fixture round-trip. +- iter mq.2.5: `MethodDispatchOutcome` enum + pure + `resolve_method_dispatch` helper. 6 unit tests cover unique + candidate, qualifier-match, qualifier-no-match (UnknownClass), + type-driven narrow-to-one, constraint-driven narrow-to-one + (rigid-var fallback), and true ambiguity. Helper uses + `ailang_core::pretty::type_to_string` for the at_type rendering + rather than the plan's invented `format_type_for_display` (one + fewer duplicate; the canonical pretty-printer is already in use + across other diagnostic surfaces). +- iter mq.2.6: Synth `Term::Var` arm class-method branch rewritten + to consult `method_to_candidate_classes` via + `parse_method_qualifier`. Branch gate: qualifier must be either + absent (bare form `"show"`) or contain an inner dot + (`.` per mq.1's canonical-form rule). 1-dot names + like `std_list.length` fall through to the existing qualified-fn + path. Plan's `active_declared_constraints` plumbing intentionally + skipped at synth time — synth's Var arm does not carry the body's + declared constraints; the constraint-driven filter runs at + discharge time (Task 7) where `expanded` is in scope. With + `MethodNameCollision` still active, the candidate set is always + singleton at this branch, so the `&[]` synth-time filter is + load-bearing only post-mq.3 and only for the rigid-var fallback; + on the post-mq.3 multi-candidate fully-concrete path discharge + will refine the residual on `r_ty` against the workspace registry. +- iter mq.2.7: `RefineOutcome` enum + `refine_multi_candidate_residual` + helper. Wired into `check_fn`'s residual loop BEFORE the existing + single-class discharge — multi-candidate residuals refine first, + `Resolved` falls through to `continue`, error variants return. + Used `expanded` (already-superclass-expanded declared constraints) + for the rigid-var path, sounder than `declared_constraints` direct. + 3 unit tests for the discharge path. +- iter mq.2.8: `resolve_residual_class_for_mono` helper in mono.rs + + 3 unit tests in a new `mod tests` block. Mono's residual-to- + target mapping (`collect_residuals_ordered`) now calls the helper + before constructing the registry key; resolved-class overrides + the residual's tentative `r.class` in `MonoTarget::ClassMethod`. + Single-class residuals flow through unchanged. +- iter mq.2.9: full `cargo test --workspace` 539 passed / 0 failed + (was 520 at start of mq.2; +19 = 15 new mq.2 tests + 4 pre- + existing mq.1 follow-on additions in cross-language test files + already shipped). All pre-mq.2 fixtures (prelude, mq1_xmod, + eq_ord_polymorphic) typecheck unchanged. Bench results: + `compile_check.py` 0 regressed / 0 improved / 24 stable; + `cross_lang.py` 0 regressed / 0 improved / 25 stable; + `check.py` 1 regressed / 2-4 improved / 58-60 stable (latency + noise — different metric regressed between two runs, runtime + benches cannot be touched by a typecheck-side iter). Prelude + roundtrip clean. + +## Concerns + +- **Helper-cost: `parse_method_qualifier` does an `rfind('.')` on + every `Term::Var` lookup that reaches the class-method branch.** + Today this is bounded by the per-Var-arm cost (already O(name- + length) due to the dot-counting and unification ladder), so it's + noise. If profiling ever shows the Var arm hot, the right fix is + to cache `(method_name, qualifier_opt)` on the Var node rather + than recompute — but that's a Term struct change and out of + scope for mq.2. + +- **`pub` bump on `ResidualConstraint`.** The unit-test crate + (`tests/method_dispatch_pin.rs`) needs to construct + `ResidualConstraint` for Task 5; Task 7's in-lib tests also + reference it. Bumping from `pub(crate)` to `pub` is the minimum + edit; the struct semantically belongs at the workspace boundary + anyway (the spec's published shape for what the dispatcher + produces). No risk: no external crate depends on `ailang-check` + outside this workspace. + +- **`MissingConstraint.class` field for multi-candidate rigid-var + case is best-effort.** When `refine_multi_candidate_residual` + emits `MissingConstraint`, the surfaced `class` is the first + candidate (BTreeSet order). The diagnostic ctx still names the + method, the type, and (via the diagnostic Display) the full + candidate set is reachable; the `class` is just a hint. Real + workspaces never reach this branch pre-mq.3. + +## Known debt + +- **mq.3 retires `MethodNameCollision` and exercises the + multi-candidate path end-to-end.** The unit tests in this iter + are the only coverage of the new branches until then. mq.3 will + add cross-class-collision fixtures (e.g. two `Show` classes in + separate modules) and the existing tests should continue to pass + unchanged. + +- **`class_methods` keyed by method name only.** Pre-mq.3 invariant + guarantees `env.class_methods.get(method_name)` is unambiguous; + post-mq.3 this lookup needs to be reworked (likely keyed by + `(class, method)` or by `method` returning a list). The synth + branch's `expect("invariant")` documents the dependency. Not + load-bearing in mq.2. + +- **Synth-time `declared_constraints: &[]` in the Var arm rewrite.** + This is correct for pre-mq.3 (singleton candidate set never + needs filtering) but means the post-mq.3 constraint-driven + filter cannot fire at synth time. The branch will need + `env.active_declared_constraints` plumbed through (Env field + + `check_fn` initialization) before mq.3's first multi-candidate + workspace with declared constraints. Cost: ~10-line edit. + +## Files touched + +- crates/ailang-check/src/diagnostic.rs +- crates/ailang-check/src/lib.rs +- crates/ailang-check/src/mono.rs +- crates/ailang-check/tests/method_dispatch_pin.rs (new) + +## Stats + +bench/orchestrator-stats/2026-05-13-iter-mq.2.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 6dc9292..c9740cb 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -43,3 +43,4 @@ - 2026-05-12 — audit-ct-tidy: milestone close (ct-tidy) — architect drift fixed inline as `ctt.tidy` (3 doc-side edits: DESIGN.md §"Class-schema diagnostics" drops the retired `KindMismatch` bullet + adds successor paragraph naming `BareCrossModuleTypeRef`; DESIGN.md §"Higher-kinded class params" rewritten to name `BareCrossModuleTypeRef` from canonical-form validation instead; roadmap.md two P2 todos struck `[x]` with forward-reference to ctt.3 and ctt.2). Bench mixed (check.py exit 1: bump_s persistence on `bench_list_sum` second consecutive sighting at +12.23% → +12.60%; two new first-sighting rc-cohort max_us latency regressions classified as noise pending next audit; the recurring 3-audit `latency.explicit_at_rc` improvement cluster narrowed to within tolerance this audit, withdrawing the ratify-pending plan from audit-eob — the meaningful shrinkage is itself attribution evidence that the cluster is noise-class not signal-class), baseline pristine for the 4th consecutive audit → 2026-05-12-audit-ct-tidy.md - 2026-05-12 — iter 24.1: `bool_to_str` + `str_clone` runtime + codegen wiring — 2 new C functions in `runtime/str.c` (slab-allocating heap-Str primitives via existing `str_alloc`), lockstep checker + synth.rs installs with `ret_mode: Own`, 2 IR-header declares + 2 `lower_app` arms + `is_static_callee` whitelist extension, 5 IR snapshots regen (2 declares × 5 files), 9 new tests (2 builtins-install unit + 2 IR-shape pin + 5 E2E all green), pre-existing-drift fix included (int_to_str row added to `builtins.rs::list()`). One substantive deviation: builtin-signatures registered in `uniqueness.rs::infer_module` + `linearity.rs::check_module_with_visible` (8 LOC × 2 files) so `str_clone`'s `param_modes: [Borrow]` is visible to the App-arg walker; symmetric to 23.4-prep's class-method registration; necessary for the plan's literal `frees == 3` cross-realisation assertion. Full `cargo test --workspace` 513 passed, 0 failed. `bench/compile_check.py` + `bench/cross_lang.py` green → 2026-05-12-iter-24.1.md - 2026-05-13 — iter mq.1: class-ref canonical-form extension + workspace-internal class-name qualification — three schema fields (`InstanceDef.class`, `Constraint.class`, `SuperclassRef.class`) move bare → canonical (bare for same-module, `.` for cross-module) symmetric to ct.1's `Type::Con.name` rule; `ClassDef.name` stays bare (defining site, like `TypeDef.name`). `validate_canonical_type_names` gains three field-walks via new `check_class_ref` helper plus two sibling diagnostics `BareCrossModuleClassRef` / `BadCrossModuleClassRef`; `check_class_name_fields` narrowed to `ClassDef.name`-only. Workspace-internal class-name keys all qualified: `class_def_module`, `class_by_name`, registry `entries.0`, `ClassMethodEntry.class_name`, `class_superclasses`, mono's `class_index`, `Origin::Class.class_name`. New `qualify_class_ref` helper in `workspace.rs` plus sibling `qualify_class_ref_in_check` in `ailang-check`. Two new positive on-disk fixtures (`mq1_xmod_constraint_class{,_dep}`). Recon claim that all existing fixtures' class-refs are intra-module was empirically wrong — 5 test_22b* (`orphan_third`, `dup_a/b/entry`, `unbound_constraint_var`) + 5 other (`eq_ord_polymorphic`, `eq_ord_user_adt`, `cmp_max_smoke`, `ctt2_collision_{lib,main}`) fixtures required minimal canonical-form migration. Duplicate-instance test architecturally restructured: post-mq.1 orphan-freedom makes two-modules-on-same-`(class, type)` structurally impossible (any second instance in a non-owning module fires `OrphanInstance` first); new `test_22b1_dup_same_module.ail.json` lands both instances in the class's module — the only post-mq.1 way to land two on the same canonical key. Plan defects fixed inline: `Origin::Class.class_name` had one construction site not two (plan recon off-by-one); `build_class_index` in `mono.rs` needed qualifying (plan said "no code change needed"); `build_module_globals` needed a `Def::Instance` carve-out for qualified `inst.class`; `check_fn`'s declared-constraint matching needed inline canonical-form lifting; `NoInstance` Float-aware message arm needed `prelude.Eq`/`prelude.Ord` match; coherence type-leg needed qualified-head split-and-lookup. Tasks 3-6 ran as one coherent fix (Task 3 alone left tests RED). 7/7 tasks, 520 tests green, `bench/compile_check.py` + `bench/cross_lang.py` exit 0; `bench/check.py` exit 1 due to 4 improvements-beyond-tolerance (audit-ratifiable per convention, not a regression). `MethodNameCollision` + dispatch path unchanged; iters mq.2 + mq.3 land them → 2026-05-13-iter-mq.1.md +- 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>` (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 `.` 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