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