journal: ct.1 canonical type names — validator + migration

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 `<owner>.<TypeName>` = 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 <dir>`): dev-only
+  CLI subcommand that walks `<dir>/*.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<String, String>` 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: <message>` 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).