From 4ed9096c87046b2e4445f4488ff6a68dbaeca235 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 11 May 2026 01:52:02 +0200 Subject: [PATCH] =?UTF-8?q?journal:=20ct.1=20canonical=20type=20names=20?= =?UTF-8?q?=E2=80=94=20validator=20+=20migration?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/JOURNAL.md | 155 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 155 insertions(+) diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 2ea4b8c..6e92bc3 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -14067,3 +14067,158 @@ Out of scope for this iter (covered by later 23.x): Workspace at iter-23.2 close: full `cargo test --workspace` green (416 tests, 0 failed). Cross-language and the three regression scripts not re-run for this iter; they run at milestone-23 close. + +## 2026-05-11 — Iteration ct.1: canonical type names — validator + migration + +First iteration of the canonical-type-names milestone. Spec at +`docs/specs/2026-05-10-canonical-type-names.md`. The milestone +formalises an unambiguous rule for `Type::Con` names in `.ail.json`: +within a file's module context (`"name"` at the top), bare = +local, qualified `.` = explicit cross-module, +and primitives stay bare. The bug-class that motivated the +milestone (iter 23.3 Task 4: bare cross-module references silently +mismatching when one side resolves through imports-fallback and +the other stays bare) becomes structurally impossible because +there's no bare cross-module form in canonical JSON. + +What ct.1 shipped: + +- **Validator** (`validate_canonical_type_names` in + `crates/ailang-core/src/workspace.rs`): walks every `Type::Con` + in Type position (incl. `Term::Lam.param_tys`, `Term::Lam.ret_ty`, + `Term::LetRec.ty`) and every `Term::Ctor.type_name` in Term + position. Three new `WorkspaceLoadError` variants: + `BareCrossModuleTypeRef` (with `candidates` from imports-in-order + + implicit prelude), `BadCrossModuleTypeRef` (qualified owner + unknown or doesn't declare the named type), `QualifiedClassName` + (one of four fields — `ClassDef.name`, `InstanceDef.class`, + `SuperclassRef.class`, `Constraint.class` — contains a `.`). + Wired into `load_workspace` between prelude injection and + `validate_classdefs` so the canonical-form diagnostic fires + before any downstream check that would have papered over the + malformed shape. + +- **Migration tool** (`ail migrate-canonical-types `): dev-only + CLI subcommand that walks `/*.ail.json`, rewrites bare + cross-module Type::Con + Term::Ctor.type_name references to their + qualified form via the first-match-in-imports-order disambiguation + rule (mirrors iter 23.1.3's typecheck-side imports-fallback on + the happy path; explicitly weaker than 23.1.3's `ambiguous-type` + diagnostic since this is one-shot tooling). Prelude treated as + implicit last-resort fallback. Idempotent. After ct.1.5 ran + the tool over `examples/`, exactly two fixtures shifted: + `ordering_match.ail.json` (Term::Ctor `Ordering` → + `prelude.Ordering`) and `test_22b1_dup_a.ail.json` (Type::Con + `MyInt` → `test_22b1_dup_b.MyInt`). + +- **Registry-side normalize-before-hash** (ct.1.5a discovery — + not in the original plan). The migration exposed a real semantic + gap: under the new canonical-form rule, a type defined in + module B is referenced bare-local in B (`Type::Con { name: + "MyInt" }`) but qualified `B.MyInt` when referenced from + elsewhere. The registry's `canonical::type_hash(&inst.type_)` + compares Type::Con name bytes verbatim, so two coherent + instances of the same type-def (one bare-local, one + qualified-cross-module) would hash differently and the + duplicate-instance detection would silently miss. Fix: + `Registry::normalize_type_for_lookup` qualifies bare-locals + via a `type_def_module: BTreeMap` lookup + before hashing. Four consumer call sites in `ailang-check` + (one in `lib.rs::no-instance` lookup, three in `mono.rs`) + funneled through the same method so the registered-form ↔ + queried-form contract is enforceable from one helper rather + than by grep. The defining-module-qualifier choice (vs. + owning-module) is documented as the right call for the + canonical-form-compliant corpus; a docstring on + `Registry.type_def_module` flags the latent bare-name- + collision-across-modules edge case as future-tidy debt + (would require re-keying the map to `(owning_module, bare_name)`). + +**The dead `KindMismatch` arm.** The fixture +`test_22b2_kind_mismatch.ail.json` uses `Type::Con { name: "f", +args: [Type::Var{a}] }` where `f` is meant to be the class param +in applied position — a malformed shape that pre-ct.1 fired +`KindMismatch`. Under ct.1's validator, that same shape is now +caught earlier as `BareCrossModuleTypeRef` (because `f` is bare, +non-primitive, and not a TypeDef anywhere). The +`validate_classdefs::walk_kind_mismatch` path becomes +structurally unreachable through well-formed schema. The +regression test was renamed to +`class_param_in_applied_position_fires_canonical_form_rejection` +and re-targeted to the new diagnostic; the kind-mismatch code +stays in the codebase as dead-but-defensive for now (cleanup +queued as future tidy). + +**Friction surfaced — CLI human-mode diagnostic surface.** While +writing the ct.1.8 E2E tester noticed that non-JSON `ail check` +does NOT route ct.1 errors through `workspace_error_to_diagnostic`; +human-mode stderr lacks the bracketed `[diagnostic-code]` prefix +that JSON mode carries (it goes via the `anyhow`/`thiserror` +Display impl as `Error: ` instead). Plausibly the same +asymmetry applies to other CLI subcommands that call +`load_workspace(&path)?` directly. Not a ct.1 bug — pre-existing +CLI architecture issue — queued as P2 follow-up in roadmap. + +**Plan vs. reality.** The plan's Task 5 ("run migration on +`examples/`") expected `cargo test --workspace` to be green right +after. It wasn't. The duplicate-instance test broke because the +registry hash didn't normalize. ct.1.5a (the registry-normalize +fix) was a mid-iteration scope expansion. Lesson: the plan named +the four obsolete typechecker / codegen mechanisms as ct.2/ct.3 +targets, but missed a fifth consumer site (the registry's +type-hash key) that's neither typechecker nor codegen — it's +workspace-load metadata. Future spec-writing for cross-cutting +canonical-form changes should explicitly enumerate ALL consumer +sites of the hashed/keyed AST shape. + +**4 obsolete mechanisms NOT cleaned up here.** Per spec, the +four imports-fallback / overlay mechanisms named in §"Mechanisms +made obsolete" (Pattern::Ctor imports-fallback, Term::Ctor synth +imports-fallback, `lookup_ctor_by_type` fallback, mono +`ctor_index` overlay) stay in place for ct.1 — they continue to +work on the migrated form (qualified bare → direct lookup +succeeds before fallback fires). Removal is ct.2 (typechecker) +and ct.3 (codegen+mono) work. + +Coverage at iter close: +- 17 new unit tests under `ct1_validator_*` / `ct1_fixture_*` / + `ct1_registry_*` / `ct1_5a_*` in + `crates/ailang-core/src/workspace.rs::mod tests`. +- 2 E2E tests in `crates/ail/tests/migrate_canonical_types.rs` + (Term::Ctor + Type::Con rewrite paths, idempotence). +- 5 E2E CLI tests in `crates/ail/tests/ct1_check_cli.rs` + (one per new diagnostic code through `--json` mode, one for + human-mode surface, one happy-path on `ordering_match`). +- 3 on-disk fixtures under `examples/test_ct1_*.ail.json` pin + the diagnostic surface against schema drift. +- Existing `iter22b1_duplicate_instance_fires_diagnostic` test + continues to pass on the migrated state (via the registry + normalize). `test_22b2_kind_mismatch`'s regression test + renamed + retargeted to `BareCrossModuleTypeRef`. + +Per-task commits: + +- `000b84d` iter ct.1.1: validator scaffolding + Type::Con canonical-form rules +- `3723495` iter ct.1.2: validator extends to Term::Ctor.type_name +- `9e2e843` iter ct.1.3: validator rejects qualified class-name fields +- `219908e` iter ct.1.3-followup: test for Constraint.class in ClassDef-method Forall +- `d45977f` iter ct.1.4: dev-only ail migrate-canonical-types subcommand +- `a73f7d3` iter ct.1.4-followup: type-con rewrite test + doc clarity +- `7872ccf` iter ct.1.5a: registry-side normalize-before-hash +- `5e653ff` iter ct.1.5a-followup: forall-constraints recursion + docstring + drop iteration-tag comments +- `d3280e9` iter ct.1.5: migrate bare cross-module type refs in examples/ +- `727d2c1` iter ct.1.6: wire validator into load_workspace; refresh kind-mismatch test +- `f22f88b` iter ct.1.7: on-disk fixture tests for canonical-form diagnostics +- `c1783e0` iter ct.1.8: E2E coverage for canonical-form diagnostic surface + happy path + +Out of scope (covered by later ct.x): +- Removal of 4 obsolete imports-fallback / overlay mechanisms (ct.2 typechecker, ct.3 codegen+mono). +- DESIGN.md amendments to Decision 2 (content-addressed defs) + hash-stability promises review (ct.4). +- Re-baseline of hash-pinned regression tests affected by the 2 migrated fixtures (ct.4). +- Form-B prose round-trip test extension for the qualifier-trim-on-print behaviour (ct.4). + +Workspace at iter-ct.1 close: full `cargo test --workspace` green +(roughly 440+ tests across crates, 0 failed). Cross-language and +the three regression scripts not re-run for this iter (no codegen- +shape change to existing fixtures beyond the surgical migration; +they run at canonical-type-names milestone close after ct.4).