Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

audit-mq: milestone close (module-qualified-class-names) — 4 drift items routing to mq.tidy

Browse Source 
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.
This commit is contained in:
Brummel
2026-05-13 02:29:03 +02:00
parent 99d3968656
commit f382931eb8
2 changed files with 196 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/journals/2026-05-13-audit-mq.md
+195
View File
@@ -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 (`<module>.<Class>.<method>`). 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 `<id>` 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<CheckError>` 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`.
docs/journals/INDEX.md
+1
View File
@@ -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, `<module>.<Class>` 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<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