From f382931eb805c8fb030a2635773b7c6780352ee7 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 02:29:03 +0200 Subject: [PATCH] =?UTF-8?q?audit-mq:=20milestone=20close=20(module-qualifi?= =?UTF-8?q?ed-class-names)=20=E2=80=94=204=20drift=20items=20routing=20to?= =?UTF-8?q?=20mq.tidy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Architect drift review surfaces: - 2x [high]: rigid-var refinement misses type-unification leg (refine_multi_candidate_residual filters declared constraints on class only, breaks 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 (contradicts mq.1 canonical-form symmetry). - 2x [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 class-ref fields (only the prose at 1156-1162 does). - 1x [medium] acknowledged debt without fix: synth(...) grown to 10 mut-ref parameters — refactor cost disproportionate to gain. - 2x [low] roadmap backlog: Trajectories B + D have unit-test coverage only; collect_mono_targets rebuilds env without active_declared_constraints (currently latent). Bench: compile_check.py + cross_lang.py exit 0; check.py exit 1 across 4 consecutive re-runs with metric identity shifting between runs — 5th-consecutive audit observation of the same noise envelope. Baseline pristine. Resolution: mq.tidy iter covers 4 actionable items; 3 deferred. --- docs/journals/2026-05-13-audit-mq.md | 195 +++++++++++++++++++++++++++ docs/journals/INDEX.md | 1 + 2 files changed, 196 insertions(+) create mode 100644 docs/journals/2026-05-13-audit-mq.md diff --git a/docs/journals/2026-05-13-audit-mq.md b/docs/journals/2026-05-13-audit-mq.md new file mode 100644 index 0000000..3b825c6 --- /dev/null +++ b/docs/journals/2026-05-13-audit-mq.md @@ -0,0 +1,195 @@ +# audit-mq — milestone close (module-qualified-class-names) + +**Date:** 2026-05-13 +**Milestone:** module-qualified-class-names +**Iters covered:** mq.1 (`0eb3323`) → mq.2 (`2e6a4ca`) → mq.3 (`99d3968`) +**Range from previous close:** `0dcdaab..99d3968` (audit-ct-tidy → mq.3) +**Status:** drift_found — `mq.tidy` queued + +## Summary + +The module-qualified-class-names milestone landed in three iters: +mq.1 lifted the canonical-form rule to the three class-ref schema +fields and qualified all workspace-internal class-name keys; mq.2 +installed the type-driven dispatch mechanism without exercising it +end-to-end; mq.3 retired `WorkspaceLoadError::MethodNameCollision`, +re-keyed `class_methods` to a `(class, method)` tuple, plumbed +`Env.active_declared_constraints`, added the +`class-method-shadowed-by-fn` warning, and shipped three positive +E2E fixtures exercising trajectories C (ambiguous), E (explicit +qualifier), and the class-fn shadow case. + +Architect drift review surfaces seven items: two [high] (rigid-var +refinement type-unification leg missing; same-module bare-class +qualifier shape unreachable), three [medium] (warning over-fires on +unrelated locals shadowing prelude method names; DESIGN.md Data +Model schema fragments don't reflect the canonical-form rule for +class-refs; `synth(...)` has grown to 10 mut-ref parameters), and +two [low] backlog items (trajectories B + D covered by unit tests +only — no E2E fixture; `collect_mono_targets` rebuilds env without +`active_declared_constraints`, currently latent). + +Bench: `check.py` exit 1 across four consecutive runs with metric +identity shifting between runs (3 → 1 → 1 → 0 regressions across +re-runs, different metrics each time; one run showed only +improvements). Pattern is consistent with 5th-consecutive audit +noise-class observation. `compile_check.py` exit 0 (24/24 stable); +`cross_lang.py` exit 0 (25/25 stable). Baseline left pristine per +the 5th-consecutive conservative-call convention; see Bench notes +below. + +Resolution path: `mq.tidy` iteration covers the four actionable +drift items (two [high] + two [medium]). The 5th [medium] +(`synth(...)` signature growth) is acknowledged as accepted +post-mq.3 cost and not fixed — refactoring `synth(...)` would +ripple through 15+ recursive callsites and 5 external callers, +disproportionate to the readability gain. The two [low] items +join the roadmap backlog. + +## Architect drift items + +### [high-1] Rigid-var refinement misses type-unification leg + +**Path:** `crates/ailang-check/src/lib.rs:2163-2168` + +The `refine_multi_candidate_residual` rigid-var branch filters +declared constraints on `dc.class == c` only. Spec §"Constraint- +discharge refinement" (line 130-138) requires the filter to also +unify the declared constraint's `type_` with the residual's +`type_`. Two same-class declared constraints on different typevars +(`forall a b. Show a, Show b => (a, b) -> String` style) cannot +currently be discriminated; the filter returns the first match +regardless of which typevar the residual actually came from. No +unit test pins the type-unification leg. + +**Outcome:** fix in `mq.tidy`. + +### [high-2] Same-module bare-class qualifier shape unreachable + +**Path:** `crates/ailang-check/src/lib.rs:2570-2575` + +`qualifier_is_class_shape = q.contains('.')` makes same-module bare- +class qualifiers (`Show.show`) unreachable; the gate only admits +cross-module class qualifiers (`..`). This +contradicts the canonical-form rule's symmetry — bare class refs +are legal at every other class-ref schema field (per mq.1's rule). +Trajectory E E2E coverage is cross-module-only as a consequence. + +**Outcome:** fix in `mq.tidy`. + +### [medium-1] `class-method-shadowed-by-fn` over-fires + +**Path:** `crates/ailang-check/src/lib.rs:2479-2502` + +The warning fires whenever any class declares the method, not +when a class candidate for the actual arg type exists per spec +§"Class-fn collisions" (line 161-162). Will spam on unrelated +locals shadowing prelude method names (e.g. `let show = …` inside +an arbitrary body where `show` has no Show-context). + +**Outcome:** fix in `mq.tidy`. + +### [medium-2] DESIGN.md Data Model schema fragments don't reflect canonical-form rule for class-refs + +**Path:** `docs/DESIGN.md:2139, 2152, 2273` + +Data Model schema fragments for `InstanceDef`, `Constraint`, +`SuperclassRef` describe class-ref `` without flagging the +canonical-form rule. Only the prose at lines 1156-1162 carries the +rule. A schema-section reader without the prose context sees +bare-only. + +**Outcome:** fix in `mq.tidy` (doc-only). + +### [medium-3] `synth(...)` signature growth (accepted) + +**Path:** `crates/ailang-check/src/lib.rs:2415` + +`synth(...)` now carries 10 mut-ref parameters (added `warnings` +in mq.3). Two re-entries (`mono.rs:614`, `lift.rs:700`) discard +the warnings channel by convention. + +**Outcome:** acknowledged debt, NOT fixed in `mq.tidy`. Rationale: +refactoring `synth(...)` (e.g. into a `SynthCtx` struct carrying +the mut-refs) would ripple through 15+ recursive callsites and 5 +external callers, with the only payoff a marginal readability +gain. The mut-ref pattern is consistent with the rest of the +crate (`check_in_workspace`'s `Vec` accumulator), so +this is project-style rather than drift. + +### [low-1] Trajectories B + D no E2E + +**Paths:** spec §"Data flow" trajectories B (type-driven narrow- +to-one) + D (rigid-var narrow-to-one) are covered by unit tests +only — `tests/method_dispatch_pin.rs` 5-step rule tests. No +on-disk fixture exercises either path end-to-end. + +**Outcome:** roadmap backlog (P3). Single-class-per-method +workspaces don't exercise these branches; the real coverage gap +opens when downstream code starts producing the multi-class +shapes the unit tests already pin. + +### [low-2] `collect_mono_targets` rebuilds env without `active_declared_constraints` + +**Path:** `crates/ailang-check/src/mono.rs:574-625` + +Structural divergence from `check_fn`'s env setup. Currently +latent: mono's residuals are concrete-type so the rigid-var +filter never runs. Env-shape invariant unpinned. + +**Outcome:** roadmap backlog (P3). Test that pins the invariant +(`env.active_declared_constraints` populated consistently +wherever `Env` is built) belongs with the [low-1] E2E work for +trajectory D. + +## Bench + +- `bench/check.py`: exit 1 across four consecutive re-runs with + metric identity shifting between runs: + - Run 1: 1 regression (`latency.implicit_at_rc.p99_over_median`), + 5 improvements (across `bench_list_sum.gc_over_bump` + + `bench_closure_chain.gc_over_bump` + 3 + `latency.explicit_at_rc.*` metrics). + - Run 2: 3 regressions (`bench_list_sum.bump_s` 3rd-consecutive + sighting + 2 `latency.implicit_at_rc.*` max-tail), 3 + improvements (same `latency.explicit_at_rc` cluster). + - Run 3: 1 regression (different metric again), 5 improvements. + - Run 4: 0 regressions, 2 improvements + (`bench_list_sum.gc_over_bump` + + `bench_closure_chain.gc_over_bump`). + - Pattern: metric identity is not stable; the recurring + `bench_list_sum.bump_s` 3rd-consecutive sighting per mq.3 + journal lineage shows up in 1 of 4 runs only. Audit-ct-tidy + (2026-05-12), audit-eob (2026-05-12), audit-ms (2026-05-12), + audit-cma (2026-05-12) all left baseline pristine on the same + `latency.explicit_at_rc` improvement cluster reappearing + across milestones — this is the 5th consecutive audit + observation of the same noise envelope. + - Conservative call: baseline pristine for 5th consecutive + audit. The latency cluster has narrowed-then-widened-then- + narrowed across audits, which is itself attribution evidence + that this is variance, not signal. If signal were present + the metric would not migrate between runs at this rate. +- `bench/compile_check.py`: exit 0; 24/24 stable. +- `bench/cross_lang.py`: exit 0; 25/25 stable. + +No `--update-baseline` invocation this audit. + +## Resolution + +- `mq.tidy` iter to land four drift fixes: `[high-1]`, `[high-2]`, + `[medium-1]`, `[medium-2]`. Routes through `planner` → + `implement`. +- `[medium-3]` (`synth(...)` signature growth): acknowledged + debt, no action. +- `[low-1]` (Trajectory B + D E2E) + `[low-2]` (mono env shape): + roadmap backlog P3. Same scope — single follow-up iter when the + multi-class workspace shape lands. + +## Files touched + +- `docs/journals/2026-05-13-audit-mq.md` (new, this file) +- `docs/journals/INDEX.md` (one new line) + +No production code or test edits in this audit; all +recommendations land in `mq.tidy`. diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 3fe50d9..154e694 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -45,3 +45,4 @@ - 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 - 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` 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` 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` 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)>` — adopted mut-ref-accumulator pattern matching existing `Vec` 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