audit-ct-tidy: close milestone ct-tidy via ctt.tidy
This commit is contained in:
+13
-5
@@ -1732,13 +1732,18 @@ wording is fixed; the categories and their triggers are:
|
||||
|
||||
**Class-schema diagnostics** (validation of class declarations):
|
||||
|
||||
- `KindMismatch` — class param appears in applied position in any
|
||||
method signature (e.g., `f a` where `f` is the class param).
|
||||
- `InvalidSuperclassParam` — superclass `type` differs from the
|
||||
class's own `param`.
|
||||
- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a
|
||||
type variable not bound by the surrounding `forall`.
|
||||
|
||||
A class param appearing in applied position (e.g., `f a` where `f`
|
||||
is the class param) is rejected earlier by the canonical-form
|
||||
validator as `BareCrossModuleTypeRef` — `f` is a bare,
|
||||
non-primitive name not declared as a `TypeDef` in the owning
|
||||
module — so the dedicated `KindMismatch` diagnostic was retired
|
||||
at iter ctt.3.
|
||||
|
||||
**Typecheck diagnostics** (per function body):
|
||||
|
||||
- `MissingConstraint` — body's residual constraint is not covered
|
||||
@@ -1758,9 +1763,12 @@ axis-5 (kind `*` only) covers the space.
|
||||
|
||||
- **Multi-parameter classes** (`class Foo a b where ...`). Schema
|
||||
rejects: `ClassDef.param` is a string, not a list.
|
||||
- **Higher-kinded class params** (`class Functor f`). Diagnostic
|
||||
S1 (`KindMismatch`) at class declaration if any method applies
|
||||
the param.
|
||||
- **Higher-kinded class params** (`class Functor f`). Rejected at
|
||||
workspace-load time: `BareCrossModuleTypeRef` from canonical-form
|
||||
validation fires before class-schema validation if any method
|
||||
body uses the param as a `Type::Con` head — bare non-primitive
|
||||
names must be declared as a `TypeDef` in the owning module, and
|
||||
a class param is not.
|
||||
- **Higher-rank polymorphism** (`forall a. (forall b. b -> b) -> a`).
|
||||
Already rejected at parse time per the typeclass-conversation
|
||||
rationale recorded in JOURNAL; constraint-bearing
|
||||
|
||||
@@ -0,0 +1,163 @@
|
||||
# audit-ct-tidy — Milestone close: ct-tidy (closing iter ctt.3)
|
||||
|
||||
**Date:** 2026-05-12
|
||||
**Milestone:** ct-tidy (ctt.1 + ctt.2 + ctt.3)
|
||||
**Status:** Closed, three doc-drift items fixed inline (`ctt.tidy`)
|
||||
|
||||
## Architect drift review
|
||||
|
||||
`ailang-architect` reported `drift_found` across the commit range
|
||||
`805bba3..0d3f44b`. Code-side changes match DESIGN.md /
|
||||
spec / iters; three doc-side drift items surfaced (two high,
|
||||
one low; one medium is acceptable per spec).
|
||||
|
||||
**[high — spec acceptance]** `docs/DESIGN.md:1735-1736` —
|
||||
`KindMismatch` listed as a live class-schema diagnostic. Stale
|
||||
since ctt.3.
|
||||
|
||||
**[high — spec acceptance]** `docs/DESIGN.md:1761-1763` —
|
||||
`KindMismatch` cited as the rejection mechanism for
|
||||
higher-kinded class params. Stale since ctt.3.
|
||||
|
||||
**[high — spec acceptance]** `docs/roadmap.md:91-97` — the
|
||||
`KindMismatch` retire todo unchecked with no forward-reference
|
||||
to ctt.3. Spec acceptance criterion called for strikes on the
|
||||
relevant todo lines; ctt.3 struck none.
|
||||
|
||||
**[medium — record-keeping]** `examples/test_22b2_kind_mismatch.ail.json`
|
||||
keeps the retired-diagnostic-name in its filename. Spec is silent
|
||||
(acceptable as-is); rename is a future candidate, not in this
|
||||
audit's scope.
|
||||
|
||||
**[low — numerical drift]** Spec claim "`grep type_def_module`
|
||||
returns 13 hits" is now 18 hits post-ctt.2. Intent honoured (every
|
||||
consumer threaded); numerical figure is historical.
|
||||
|
||||
### Tidy fixes applied inline (`ctt.tidy`)
|
||||
|
||||
All three high-severity items addressed in this audit commit
|
||||
(Boss-mechanical edits — three doc edits, no separate plan /
|
||||
implement dispatch warranted):
|
||||
|
||||
1. `docs/DESIGN.md:1733-1740` — dropped the `KindMismatch` bullet
|
||||
from the class-schema diagnostics list; added a successor
|
||||
paragraph naming `BareCrossModuleTypeRef` as the structural
|
||||
rejection path for the malformed class-param-in-applied-position
|
||||
shape; cross-references iter ctt.3.
|
||||
|
||||
2. `docs/DESIGN.md:1761-1763` — rewrote the "Higher-kinded class
|
||||
params" bullet under "What this typeclass design explicitly does
|
||||
NOT support" to name `BareCrossModuleTypeRef` from canonical-form
|
||||
validation instead of `KindMismatch` at class declaration.
|
||||
|
||||
3. `docs/roadmap.md:91-97` — struck `[x]` with a forward-reference
|
||||
to ctt.3 (canonical-form-rejection test stays green asserting
|
||||
`BareCrossModuleTypeRef`). Adjacent ctt.2 todo at lines 98-105
|
||||
also struck (mechanical follow-up — ctt.2 closed the re-key it
|
||||
tracks).
|
||||
|
||||
Medium / low items skipped: filename rename + spec numerical claim
|
||||
both fall outside ctt.tidy's scope (spec acceptance was on
|
||||
intent-honour, not figure-precision; filename rename is a future
|
||||
candidate the spec already permits as-is).
|
||||
|
||||
## Bench-regression check
|
||||
|
||||
Sequence run as Boss (the `&&` chain tripped at `check.py`'s exit
|
||||
1; `compile_check.py` and `cross_lang.py` then ran separately):
|
||||
|
||||
- `check.py`: **exit 1** — 63 metrics; 3 regressed, 3 improved
|
||||
beyond tolerance, 57 stable.
|
||||
- Regressions:
|
||||
- `bench_list_sum.bump_s` +12.23% (tol 10%) —
|
||||
**second consecutive sighting** (audit-eob first-sighted
|
||||
this at +12.60%, this audit at +12.23%).
|
||||
- `latency.explicit_at_rc.max_us` +44.31% (tol 25%) —
|
||||
**first sighting**, rc-cohort tail-latency.
|
||||
- `latency.implicit_at_rc.max_us` +35.07% (tol 30%) —
|
||||
**first sighting**, rc-cohort tail-latency.
|
||||
- Improvements:
|
||||
- `bench_list_sum.gc_over_bump` -10.40% — mirror of the
|
||||
bump_s regression (gc/bump ratio falls because bump rose).
|
||||
- `bench_closure_chain.gc_over_bump` -15.05% — new improvement.
|
||||
- `bench_list_sum_explicit.gc_over_bump` -8.30% — new improvement.
|
||||
- `compile_check.py`: exit 0; 24 metrics, all stable within ±25%.
|
||||
- `cross_lang.py`: exit 0; 25 metrics, all stable within ±15%.
|
||||
|
||||
### Classification
|
||||
|
||||
**bump_s persistence** (`bench_list_sum.bump_s`): second
|
||||
consecutive sighting (audit-eob → audit-ct-tidy) at near-identical
|
||||
magnitude (+12.60% → +12.23%). The audit-eob classification was
|
||||
"first-sighting rule — observe in the next audit; if it persists,
|
||||
investigate". This audit IS that next audit, and it persists.
|
||||
|
||||
ctt.* milestone made zero codegen-relevant edits (the three iters
|
||||
touched env-overlay doc + check-side registry key shape +
|
||||
workspace-load-time diagnostic deletion). No plausible attribution
|
||||
to ctt.*. The persistence is real but uncaptured — the underlying
|
||||
cause predates this milestone and is independent of the work in
|
||||
the audit window.
|
||||
|
||||
Conservative call (same standing rule as previous three audits):
|
||||
**do not** baseline-update. The persistence is now documented
|
||||
across two audits; if it persists into the next audit
|
||||
unchanged, ratify-without-attribution becomes the right call
|
||||
(at three consecutive sightings the noise hypothesis is
|
||||
unsupported). The latency tail-cluster regressions are first
|
||||
sightings — observe.
|
||||
|
||||
**Latency max_us regressions** (`explicit_at_rc.max_us`,
|
||||
`implicit_at_rc.max_us`): first sighting in any recent audit.
|
||||
Both metrics are rc-cohort tail-latency (the extreme-outlier
|
||||
window). The bench harness runs ~50ms workloads; a single
|
||||
outlier of +183µs (explicit) or +167µs (implicit) absolute
|
||||
moves the max_us proportionally. ctt.* made zero codegen edits,
|
||||
so the noise hypothesis is the most parsimonious explanation
|
||||
on first sighting.
|
||||
|
||||
Conservative call: first-sighting rule — **do not**
|
||||
baseline-update; observe in the next audit.
|
||||
|
||||
**Recurring latency.explicit_at_rc improvement cluster**: the
|
||||
three-audit-long improvement cluster on `p99_us` / `p99_9_us` /
|
||||
`p99_over_median` (previously at ~-37%, classified as
|
||||
ratify-candidate after one more audit at audit-eob) now reports
|
||||
within tolerance this audit:
|
||||
- `p99_us` -24.87% (tol 25%) — stable (was: improvement)
|
||||
- `p99_over_median` -24.10% (tol 25%) — stable (was: improvement)
|
||||
- `p99_9_us` not flagged (within tolerance)
|
||||
|
||||
The cluster has narrowed from ~-37% improvements to ~-24%
|
||||
near-tolerance stable. The improvements partially reverted —
|
||||
the metrics are still on the improvement side, but no longer
|
||||
beyond tolerance. The audit-eob recommendation ("if the cluster
|
||||
persists into the next two audits unchanged, ratify; if it
|
||||
shifts or shrinks meaningfully, that is itself the attribution
|
||||
signal") has fired: the cluster shrank meaningfully this audit.
|
||||
This is itself attribution-evidence — the underlying cause is
|
||||
variable rather than persistent. The ratify-pending plan is
|
||||
withdrawn; the cluster is now noise-class, not signal-class.
|
||||
|
||||
**Baseline left pristine on every script** for the fourth
|
||||
consecutive audit. No `--update-baseline` invocation.
|
||||
|
||||
## Status
|
||||
|
||||
Closed. Ct-tidy milestone fully landed:
|
||||
|
||||
- env-overlay shape ratified (ctt.1: DESIGN.md `## Env construction`
|
||||
section + DuplicateCtor pinning test + 2 P2 todos closed).
|
||||
- `Registry.type_def_module` re-keyed to `(owning_module, bare_name)`
|
||||
with `caller_module` threaded through every consumer (ctt.2:
|
||||
3-module fixture + regression test).
|
||||
- `KindMismatch` retired (ctt.3: variant + helper + dispatch +
|
||||
Display arm deleted; test stays green via canonical-form
|
||||
successor `BareCrossModuleTypeRef`).
|
||||
- DESIGN.md tracks all three iters' anchors (ctt.tidy in this audit:
|
||||
class-schema diagnostics list updated, higher-kinded params bullet
|
||||
updated, ctt.3 retirement marker pattern).
|
||||
- Roadmap reflects closure (ctt.tidy: two P2 todos struck `[x]`).
|
||||
|
||||
Working tree exits audit clean. main HEAD advances by exactly
|
||||
this audit commit.
|
||||
@@ -40,3 +40,4 @@
|
||||
- 2026-05-12 — iter ctt.1: env-overlay shape ratification — new DESIGN.md top-level section `## Env construction` anchors the `env.types` (owning) / `env.ctor_index` (reverse-index) split with the semantic rationale, plus the intentional check-side / mono-side asymmetry (mono-side narrowed at ct.3.2, check-side retains both halves because in-band `DuplicateCtor` consumes the per-module `env.ctor_index` rebuild); new behavioural-pin test `crates/ailang-check/tests/duplicate_ctor_pin.rs` ratifies the consumer; two P2 roadmap todos struck `[x]` (overlay shape question, per-module overlay narrowing); 3/3 tasks first-shot, zero review re-loops, no production-code edits → 2026-05-12-iter-ctt.1.md
|
||||
- 2026-05-12 — iter ctt.2: `Registry.type_def_module` re-key from `BTreeMap<String, String>` to `BTreeMap<(String, String), String>` keyed by `(owning_module, bare_name)`; new `caller_module: &str` parameter threads through `normalize_type_for_registry` + `Registry::normalize_type_for_lookup`; four `ailang-check` consumer sites (lib.rs:1640, mono.rs:121/624/1175) pass the correct module-context (env.current_module / defining_module / module_name) per the plan's Design Notes; new regression test plus three-module fixture (`ctt2_collision_{cls,lib,main}.ail.json`) exercises the cross-module bare-name collision shape that pre-ctt.2 silently overwrote; RED-failure observed as `OrphanInstance` rather than the plan's predicted `DuplicateInstance` because the pass-2 coherence check (workspace.rs:656-659) is also a bare-name consumer and fires earlier; both consumers fixed by the same re-key; plan's verbatim two-module fixture had two structural defects (two-way imports → Cycle, qualified `InstanceDef.class` → QualifiedClassName) that the implementer-phase repair handled by introducing the third cls-module; spec-intent (RED-first against bare-name collision) preserved; `cargo test --workspace` green (16 binary-test suites, ~600 tests, zero failures) → 2026-05-12-iter-ctt.2.md
|
||||
- 2026-05-12 — iter ctt.3: `KindMismatch` retire — pure deletion across 3 files (workspace.rs: variant + dispatch + helper + "dead-but-defensive" doc; main.rs: Display arm; lib.rs: 22b.1 archaeology comment). Existing test `class_param_in_applied_position_fires_canonical_form_rejection` stays green unchanged (asserts `BareCrossModuleTypeRef` on the malformed fixture — the canonical-form-validator successor path). Two adjacent textual-consistency edits ride along (validate_classdefs doc-comment "Three → Two", lib.rs archaeology comment gains a ctt.3 retirement marker). One mid-deletion mechanical fix: dispatch-loop deletion orphaned `mod_name` binding → rewrote `for (mod_name, m) in modules` to `for m in modules.values()` (same body type, mechanical). 2/2 tasks, ~600 tests green across 16 binary-test suites → 2026-05-12-iter-ctt.3.md
|
||||
- 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
|
||||
|
||||
+3
-3
@@ -88,14 +88,14 @@ context. Pick the next milestone from P1.)_
|
||||
the JSON path carries is missing. Plausibly applies to every CLI
|
||||
subcommand that calls `load_workspace(&path)?` directly.
|
||||
- context: JOURNAL 2026-05-11 ("Iteration ct.1") — surfaced by ct.1.8 tester.
|
||||
- [ ] **\[todo\]** Retire dead `KindMismatch` arm — `validate_classdefs`'s
|
||||
- [x] **\[todo\]** Retire dead `KindMismatch` arm — `validate_classdefs`'s
|
||||
`walk_kind_mismatch` path is structurally unreachable through
|
||||
well-formed schema post-ct.1 (the canonical-form validator catches
|
||||
the malformed `Type::Con { name: param }` shape earlier). The
|
||||
enum variant + `walk_kind_mismatch` helper stay as dead-but-defensive
|
||||
code; a future tidy can delete both.
|
||||
- context: JOURNAL 2026-05-11 ("Iteration ct.1").
|
||||
- [ ] **\[todo\]** Re-key `Registry.type_def_module` to handle
|
||||
- context: JOURNAL 2026-05-11 ("Iteration ct.1"); closed by iter ctt.3 — variant + helper + dispatch + Display arm all deleted; canonical-form-rejection test stays green asserting `BareCrossModuleTypeRef`.
|
||||
- [x] **\[todo\]** Re-key `Registry.type_def_module` to handle
|
||||
bare-name-collision-across-modules — `BTreeMap<String, String>` keyed
|
||||
by bare type name silently overwrites when two modules each define
|
||||
`type Foo`; `normalize_type_for_registry` would then collapse `M.Foo`
|
||||
|
||||
Reference in New Issue
Block a user