diff --git a/docs/plans/2026-05-11-ct.1-validator-and-migration.md b/docs/plans/2026-05-11-ct.1-validator-and-migration.md new file mode 100644 index 0000000..97daa83 --- /dev/null +++ b/docs/plans/2026-05-11-ct.1-validator-and-migration.md @@ -0,0 +1,1883 @@ +# ct.1 — Canonical Type Names: Validator + Migration — Implementation Plan + +> **Parent spec:** `docs/specs/2026-05-10-canonical-type-names.md` (Components row ct.1) +> +> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` +> to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Land the `.ail.json` schema validator that enforces the +canonical-type-names rule (bare = primitive or local-to-this-file; +qualified = `.` for cross-module refs; qualified +class-name fields rejected), plus the one-shot migration tool that +rewrites the two stale `examples/` fixtures relying on the old +imports-fallback into the canonical form. After ct.1 the workspace +loader rejects bare cross-module Type::Con refs with a clear +diagnostic listing import-derived candidates. + +**Architecture:** The validator lives in +`crates/ailang-core/src/workspace.rs` as `validate_canonical_type_names` +and runs at the end of `load_workspace`, after the prelude is injected +but before `validate_classdefs` / `build_registry` — so a stale bare +cross-module ref fires the *new* diagnostic instead of a downstream +one. Type::Con walking is shared with Term::Ctor.type_name (the +rules are identical: the field carries a Type::Con name). Class-name +fields use a simpler check (reject any `'.'`-containing string in +the 4 fields named by the spec). + +The migration tool is a hidden CLI subcommand `ail migrate-canonical-types ` +that walks every `*.ail.json` under ``, parses each as a Module, +and rewrites bare cross-module Type::Con names by scanning the import +graph in declaration order (mirroring iter 23.1.3's +`Term::Ctor`-synth imports-fallback so the rewrite never silently +shifts which type a fixture resolves to). The prelude is treated as +an implicit last-resort fallback (matches iter 23.2.4's implicit- +prelude behaviour). Idempotent: re-running over a canonical workspace +is a no-op. The tool is dev-only and not documented in +`docs/DESIGN.md` — it has one job, runs once at ct.1 close, and is +preserved as a regression aid (CI re-runs it and asserts no diff). + +**Tech Stack:** `crates/ailang-core/src/workspace.rs` (validator + +3 new diagnostic variants), `crates/ail/src/main.rs` (migration +subcommand), `examples/*.ail.json` (2 fixtures rewritten, 3 new test +fixtures), `crates/ail/tests/` (one E2E test for migration +idempotence). + +--- + +**Files this plan creates or modifies:** + +- Modify: `crates/ailang-core/src/workspace.rs` — add 3 variants to + `WorkspaceLoadError` (`BareCrossModuleTypeRef`, + `BadCrossModuleTypeRef`, `QualifiedClassName`); add + `validate_canonical_type_names`; call from `load_workspace` after + prelude injection. +- Modify: `crates/ail/src/main.rs` — add `Cmd::MigrateCanonicalTypes` + subcommand handler. +- Migrate: `examples/ordering_match.ail.json` — `"type":"Ordering"` + → `"type":"prelude.Ordering"` (1 occurrence in `Term::Ctor`). +- Migrate: `examples/test_22b1_dup_a.ail.json` — + `"name":"MyInt"` (in `Type::Con` inside `InstanceDef.type_`) → + `"name":"test_22b1_dup_b.MyInt"`. +- Modify: `examples/test_22b2_kind_mismatch.ail.json` — unchanged; + but the regression test that loads it must be updated (see Task 6). +- Create: `examples/test_ct1_bare_xmod_rejected.ail.json` — fixture + exercising the new diagnostic on a bare Ordering reference. +- Create: `examples/test_ct1_bad_qualifier.ail.json` — fixture + exercising `BadCrossModuleTypeRef` on `Mystery.Type`. +- Create: `examples/test_ct1_qualified_class_rejected.ail.json` — + fixture exercising `QualifiedClassName` on + `InstanceDef.class`. +- Modify: `crates/ailang-core/src/workspace.rs::mod tests` — new + unit tests per spec §Testing strategy; update the kind-mismatch + test to expect `BareCrossModuleTypeRef` instead of `KindMismatch` + (validator fires first). + +--- + +## Task 1: New error variants + `validate_canonical_type_names` scaffolding + Type::Con validation + +**Subject:** add 3 diagnostic variants and the validator function; +implement the Type::Con rule end-to-end. Term::Ctor and class-name +checks land in Tasks 2 and 3. + +**Files:** +- Modify: `crates/ailang-core/src/workspace.rs` — error enum (after + line 291, the existing `ReservedModuleName` variant); fn body + appended at end of `impl`-block region (`~line 720` after + `walk_kind_mismatch`). +- Test: `crates/ailang-core/src/workspace.rs::mod tests` — six new + unit tests covering the cases enumerated in spec §Testing strategy. + +- [ ] **Step 1: Write the failing tests** + +Append to `crates/ailang-core/src/workspace.rs::mod tests`, after the +existing tests. These tests construct a synthetic Module in-memory +(via `serde_json::json!` → `serde_json::from_value`) and run the +validator directly so they do not depend on file-system fixtures: + +```rust +/// ct.1: a `Type::Con` whose `name` is a primitive (`Int` / `Bool` / +/// `Str` / `Unit` / `Float`) must be accepted bare. The five +/// primitive names are the only legal bare-non-local Type::Con names +/// under the canonical-form rule. +#[test] +fn ct1_validator_accepts_primitive_type_cons() { + let modules = single_module_with_type_con("m", "Int"); + validate_canonical_type_names(&modules).expect("Int must be accepted"); + let modules = single_module_with_type_con("m", "Float"); + validate_canonical_type_names(&modules).expect("Float must be accepted"); +} + +/// ct.1: a bare Type::Con whose `name` matches a local TypeDef in +/// the same module must be accepted (the canonical-form rule: bare = +/// local). +#[test] +fn ct1_validator_accepts_bare_local_type_con() { + let modules = single_module_with_local_type_and_ref("m", "Foo"); + validate_canonical_type_names(&modules) + .expect("local Foo must be accepted"); +} + +/// ct.1: a bare Type::Con whose `name` is neither a primitive nor a +/// local TypeDef must fire `BareCrossModuleTypeRef`. With no imports, +/// the candidates list is empty. +#[test] +fn ct1_validator_rejects_bare_xmod_no_imports() { + let modules = single_module_with_type_con("m", "Ordering"); + let err = validate_canonical_type_names(&modules) + .expect_err("Ordering must be rejected"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { + assert_eq!(module, "m"); + assert_eq!(name, "Ordering"); + assert!(candidates.is_empty(), + "no imports => no candidates; got {candidates:?}"); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } +} + +/// ct.1: a bare Type::Con whose `name` resolves to one imported +/// module's TypeDef must fire `BareCrossModuleTypeRef` with that +/// qualified form in `candidates` (so the diagnostic can suggest the +/// fix). +#[test] +fn ct1_validator_rejects_bare_xmod_with_import_candidate() { + let mut modules = BTreeMap::new(); + modules.insert("other".to_string(), module_with_type_def("other", "Ordering")); + modules.insert("m".to_string(), module_with_import_and_type_con("m", "other", "Ordering")); + let err = validate_canonical_type_names(&modules) + .expect_err("Ordering must be rejected with candidate"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, .. } => { + assert_eq!(name, "Ordering"); + assert_eq!(candidates, vec!["other.Ordering".to_string()]); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } +} + +/// ct.1: a qualified Type::Con `.` where `` is a +/// known module AND `` is one of its TypeDefs must be accepted. +#[test] +fn ct1_validator_accepts_qualified_xmod_ref() { + let mut modules = BTreeMap::new(); + modules.insert("other".to_string(), module_with_type_def("other", "Ordering")); + modules.insert("m".to_string(), module_with_import_and_type_con("m", "other", "other.Ordering")); + validate_canonical_type_names(&modules) + .expect("other.Ordering must be accepted"); +} + +/// ct.1: a qualified Type::Con `.` where `` is +/// NOT a known module must fire `BadCrossModuleTypeRef`. Symmetric +/// case: `` known but no TypeDef `` in it. +#[test] +fn ct1_validator_rejects_bad_qualified_ref() { + let modules = single_module_with_type_con("m", "Mystery.Type"); + let err = validate_canonical_type_names(&modules) + .expect_err("Mystery.Type must be rejected"); + match err { + WorkspaceLoadError::BadCrossModuleTypeRef { module, name } => { + assert_eq!(module, "m"); + assert_eq!(name, "Mystery.Type"); + } + other => panic!("expected BadCrossModuleTypeRef, got {other:?}"), + } +} + +/// ct.1: a Type::Con embedded inside a `Term::Lam.param_tys` is a +/// Type-position occurrence, just inside a Term tree. The validator +/// must walk into Lam-internal types so an LLM author can't smuggle +/// a bare cross-module ref past it by hiding it in a lambda +/// annotation. +#[test] +fn ct1_validator_walks_lam_embedded_types() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] }, + "params": [], + "body": { + "t": "lam", + "params": ["x"], + "paramTypes": [{ "k": "con", "name": "Ordering" }], + "retType": { "k": "con", "name": "Unit" }, + "effects": [], + "body": { "t": "lit", "lit": { "kind": "unit" } } + } + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("Lam-embedded Ordering must be rejected"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { name, .. } => { + assert_eq!(name, "Ordering"); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } +} +``` + +Plus three small `fn` helpers in the same `mod tests`: + +```rust +fn module_with_type_def(name: &str, type_name: &str) -> Module { + serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": name, + "imports": [], + "defs": [ + { "kind": "type", "name": type_name, "ctors": [] } + ], + })).unwrap() +} + +fn single_module_with_type_con(name: &str, type_con: &str) -> BTreeMap { + // Module with a single fn whose return type is Type::Con { name: type_con }. + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": name, + "imports": [], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] }, + "params": [], + "body": { "t": "lit", "lit": { "kind": "unit" } } + }], + })).unwrap(); + let mut map = BTreeMap::new(); + map.insert(name.to_string(), m); + map +} + +fn single_module_with_local_type_and_ref(name: &str, type_name: &str) -> BTreeMap { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": name, + "imports": [], + "defs": [ + { "kind": "type", "name": type_name, "ctors": [] }, + { "kind": "fn", "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_name }, "effects": [] }, + "params": [], + "body": { "t": "lit", "lit": { "kind": "unit" } } } + ], + })).unwrap(); + let mut map = BTreeMap::new(); + map.insert(name.to_string(), m); + map +} + +fn module_with_import_and_type_con(name: &str, import: &str, type_con: &str) -> Module { + serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": name, + "imports": [{ "module": import }], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": type_con }, "effects": [] }, + "params": [], + "body": { "t": "lit", "lit": { "kind": "unit" } } + }], + })).unwrap() +} +``` + +- [ ] **Step 2: Run the tests to verify they fail** + +Run: `cargo test --workspace -p ailang-core ct1_validator_` +Expected: FAIL — all six tests fail with "cannot find function `validate_canonical_type_names`". + +- [ ] **Step 3: Add the three new error variants to `WorkspaceLoadError`** + +In `crates/ailang-core/src/workspace.rs`, append after the +`ReservedModuleName` variant (line ~291): + +```rust + /// ct.1 (canonical-type-names): a `Type::Con` whose `name` is + /// neither a primitive nor a local TypeDef of the owning module + /// was encountered. Under the canonical-form rule, bare = + /// local; a bare cross-module ref is a schema violation. + /// `candidates` lists the qualified forms found by scanning the + /// owning module's imports in declaration order. + #[error( + "module `{module}` contains bare type name `{name}` that does not resolve to a local type. \ + AILang's `.ail.json` requires cross-module type references to be qualified. \ + Candidates from imports: {candidates:?}. Run `ail migrate-canonical-types` to fix legacy fixtures." + )] + BareCrossModuleTypeRef { + module: String, + name: String, + candidates: Vec, + }, + + /// ct.1: a qualified `Type::Con` of the form `.` + /// was encountered, but `` is not a known module in the + /// workspace, or `` is known but declares no TypeDef + /// named ``. + #[error( + "module `{module}` references qualified type `{name}` but the owner module is not known \ + or does not declare a type by that name" + )] + BadCrossModuleTypeRef { + module: String, + name: String, + }, + + /// ct.1: a class-reference field (`InstanceDef.class`, + /// `SuperclassRef.class`, `Constraint.class`, or + /// `ClassDef.name`) contains a `.` — under this milestone class + /// names are NOT module-qualified (see DESIGN spec §"Out of + /// scope: Class names"). The schema rejects qualified forms so + /// half-migrated files cannot silently load. + #[error( + "module `{module}` contains qualified class name `{name}` in field `{field}`. \ + Class names are not module-qualified in this milestone; \ + keep the bare form." + )] + QualifiedClassName { + module: String, + name: String, + field: &'static str, + }, +``` + +- [ ] **Step 4: Add the validator function (Type::Con + primitive rules only)** + +First, extend the existing top-of-file `use` line in +`crates/ailang-core/src/workspace.rs` from + +```rust +use crate::ast::{ClassDef, Def, InstanceDef, Module, Type}; +``` + +to + +```rust +use crate::ast::{ClassDef, Def, InstanceDef, Module, Term, Type}; +``` + +(the new `Term` import is needed by `walk_term_embedded_types` below). + +Then append at the end of `crates/ailang-core/src/workspace.rs`, after +`walk_kind_mismatch` and before `fn type_head_name`: + +```rust +/// ct.1: the five primitive type names that are always bare under +/// the canonical-form rule. Kept in sync with `Type::int`, +/// `Type::bool_`, `Type::str_`, `Type::unit`, `Type::float` in +/// `crate::ast`. +fn is_primitive_type_name(name: &str) -> bool { + matches!(name, "Int" | "Bool" | "Str" | "Unit" | "Float") +} + +/// ct.1: enforce the canonical-form rule on every `Type::Con` and +/// `Term::Ctor.type_name` reference in every loaded module. Runs +/// after prelude injection and before class-schema validation, so a +/// stale bare cross-module ref fires the canonical-form diagnostic +/// rather than a downstream one. +/// +/// Rule per spec §Architecture: +/// 1. Qualified `.`: `` must be a known module, +/// `` must be one of its TypeDefs. Else `BadCrossModuleTypeRef`. +/// 2. Bare primitive (`Int`/`Bool`/`Str`/`Unit`/`Float`): accepted. +/// 3. Bare non-primitive: must be a TypeDef in the owning module. +/// Else `BareCrossModuleTypeRef` with `candidates` = qualified +/// forms found by scanning the owning module's imports. +pub(crate) fn validate_canonical_type_names( + modules: &BTreeMap, +) -> Result<(), WorkspaceLoadError> { + // Pre-pass: for each module, build a `BTreeSet` of local + // TypeDef names. Used for both the owning-module local lookup + // and the per-import owner lookup. + let mut local_types: BTreeMap> = BTreeMap::new(); + for (mod_name, m) in modules { + let mut s = BTreeSet::new(); + for def in &m.defs { + if let Def::Type(t) = def { + s.insert(t.name.clone()); + } + } + local_types.insert(mod_name.clone(), s); + } + + for (mod_name, m) in modules { + // Imports in declaration order — used for both the + // qualified-`` known-module check and the bare-non-primitive + // candidates list. + let import_names: Vec<&str> = m.imports.iter().map(|i| i.module.as_str()).collect(); + + // Walk every Type in this module's defs and check each Type::Con name. + for def in &m.defs { + walk_def_types(def, &mut |t: &Type| { + if let Type::Con { name, .. } = t { + check_type_con_name( + name, mod_name, &local_types, &import_names, + )?; + } + Ok(()) + })?; + } + } + + Ok(()) +} + +/// ct.1: apply the canonical-form rule to one `Type::Con.name` +/// (also reused for `Term::Ctor.type_name` in Task 2). +fn check_type_con_name( + name: &str, + owning_module: &str, + local_types: &BTreeMap>, + import_names: &[&str], +) -> Result<(), WorkspaceLoadError> { + if let Some((prefix, suffix)) = name.split_once('.') { + // Rule 1: qualified. + let owner_types = local_types + .get(prefix) + .ok_or_else(|| WorkspaceLoadError::BadCrossModuleTypeRef { + module: owning_module.to_string(), + name: name.to_string(), + })?; + if !owner_types.contains(suffix) { + return Err(WorkspaceLoadError::BadCrossModuleTypeRef { + module: owning_module.to_string(), + name: name.to_string(), + }); + } + return Ok(()); + } + // Bare. + if is_primitive_type_name(name) { + return Ok(()); // Rule 2. + } + // Rule 3: must be local. + if local_types + .get(owning_module) + .map(|s| s.contains(name)) + .unwrap_or(false) + { + return Ok(()); + } + // Bare cross-module — collect candidates from imports in declaration order. + // Prelude is implicit: scan it last as a fallback candidate (mirrors + // iter 23.2.4's implicit-prelude behaviour in codegen). + let mut candidates: Vec = Vec::new(); + for imp in import_names { + if local_types + .get(*imp) + .map(|s| s.contains(name)) + .unwrap_or(false) + { + candidates.push(format!("{imp}.{name}")); + } + } + if !import_names.contains(&"prelude") + && local_types + .get("prelude") + .map(|s| s.contains(name)) + .unwrap_or(false) + { + candidates.push(format!("prelude.{name}")); + } + Err(WorkspaceLoadError::BareCrossModuleTypeRef { + module: owning_module.to_string(), + name: name.to_string(), + candidates, + }) +} + +/// ct.1: walk every `Type` reachable from a single `Def`, calling +/// `f` on each. Recurses into `Type::Fn.params/ret`, `Type::Con.args`, +/// `Type::Forall.constraints/body`, plus the obvious top-level fields +/// of each `Def` variant AND every Type annotation embedded in a Term +/// (`Term::Lam.param_tys`, `Term::Lam.ret_ty`, `Term::LetRec.ty`) — +/// because those are Type-position occurrences too. Term::Ctor name +/// walking is a separate concern handled in Task 2 since that field +/// is a `String`, not a `Type`. +fn walk_def_types(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&Type) -> Result<(), WorkspaceLoadError>, +{ + match def { + Def::Fn(fd) => { + walk_type(&fd.ty, f)?; + walk_term_embedded_types(&fd.body, f) + } + Def::Const(cd) => { + walk_type(&cd.ty, f)?; + walk_term_embedded_types(&cd.value, f) + } + Def::Type(td) => { + for c in &td.ctors { + for fty in &c.fields { + walk_type(fty, f)?; + } + } + Ok(()) + } + Def::Class(cd) => { + for cm in &cd.methods { + walk_type(&cm.ty, f)?; + if let Some(body) = &cm.default { + walk_term_embedded_types(body, f)?; + } + } + Ok(()) + } + Def::Instance(id) => { + walk_type(&id.type_, f)?; + for im in &id.methods { + walk_term_embedded_types(&im.body, f)?; + } + Ok(()) + } + } +} + +/// ct.1: walk a `Term` and call `f` on every Type annotation embedded +/// in it (Lam.param_tys, Lam.ret_ty, LetRec.ty). Recurses through +/// every Term sub-position. Does NOT fire on `Term::Ctor.type_name` +/// (that's a `String`, not a `Type`; handled by `walk_def_terms` in +/// Task 2). +fn walk_term_embedded_types(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&Type) -> Result<(), WorkspaceLoadError>, +{ + match t { + Term::Lit { .. } | Term::Var { .. } => Ok(()), + Term::App { callee, args, .. } => { + walk_term_embedded_types(callee, f)?; + for a in args { walk_term_embedded_types(a, f)?; } + Ok(()) + } + Term::Let { value, body, .. } => { + walk_term_embedded_types(value, f)?; + walk_term_embedded_types(body, f) + } + Term::LetRec { ty, body, in_term, .. } => { + walk_type(ty, f)?; + walk_term_embedded_types(body, f)?; + walk_term_embedded_types(in_term, f) + } + Term::If { cond, then, else_ } => { + walk_term_embedded_types(cond, f)?; + walk_term_embedded_types(then, f)?; + walk_term_embedded_types(else_, f) + } + Term::Do { args, .. } => { + for a in args { walk_term_embedded_types(a, f)?; } + Ok(()) + } + Term::Ctor { args, .. } => { + for a in args { walk_term_embedded_types(a, f)?; } + Ok(()) + } + Term::Match { scrutinee, arms } => { + walk_term_embedded_types(scrutinee, f)?; + for arm in arms { + walk_term_embedded_types(&arm.body, f)?; + } + Ok(()) + } + Term::Lam { param_tys, ret_ty, body, .. } => { + for pt in param_tys { walk_type(pt, f)?; } + walk_type(ret_ty, f)?; + walk_term_embedded_types(body, f) + } + Term::Seq { lhs, rhs } => { + walk_term_embedded_types(lhs, f)?; + walk_term_embedded_types(rhs, f) + } + Term::Clone { value } => walk_term_embedded_types(value, f), + Term::ReuseAs { source, body } => { + walk_term_embedded_types(source, f)?; + walk_term_embedded_types(body, f) + } + } +} + +/// ct.1: recursive walk of a `Type`, calling `f` at every node. +fn walk_type(t: &Type, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&Type) -> Result<(), WorkspaceLoadError>, +{ + f(t)?; + match t { + Type::Con { args, .. } => { + for a in args { + walk_type(a, f)?; + } + Ok(()) + } + Type::Fn { params, ret, .. } => { + for p in params { + walk_type(p, f)?; + } + walk_type(ret, f) + } + Type::Forall { body, constraints, .. } => { + for c in constraints { + walk_type(&c.type_, f)?; + } + walk_type(body, f) + } + Type::Var { .. } => Ok(()), + } +} +``` + +- [ ] **Step 5: Run the tests to verify they pass** + +Run: `cargo test --workspace -p ailang-core ct1_validator_` +Expected: PASS — all six tests green. + +- [ ] **Step 6: Run the workspace's full test suite to confirm no regressions** + +Run: `cargo build --workspace && cargo test --workspace -p ailang-core` +Expected: PASS. The validator is NOT yet wired into `load_workspace`, +so existing fixtures continue to load. + +- [ ] **Step 7: Commit** + +```bash +git add crates/ailang-core/src/workspace.rs +git commit -m "iter ct.1.1: validator scaffolding + Type::Con canonical-form rules" +``` + +--- + +## Task 2: Extend the validator to walk `Term::Ctor.type_name` + +**Subject:** the canonical-form rule on `Type::Con.name` is identical +to the rule on `Term::Ctor.type_name` — both fields name a TypeDef. +This task plumbs the existing `check_type_con_name` through Term +walking so a `Term::Ctor { type: "Ordering", ... }` inside a fn body +also fires the diagnostic. + +**Files:** +- Modify: `crates/ailang-core/src/workspace.rs` — add `walk_def_terms` + + `walk_term_types_and_ctor_names`; call from + `validate_canonical_type_names`. +- Test: append one new unit test exercising the Term::Ctor path. + +- [ ] **Step 1: Write the failing test** + +Append to `crates/ailang-core/src/workspace.rs::mod tests`: + +```rust +/// ct.1: a `Term::Ctor` whose `type_name` is a bare cross-module ref +/// must fire `BareCrossModuleTypeRef`. Symmetric to the Type::Con +/// rule but the field lives on Term, not Type. +#[test] +fn ct1_validator_rejects_bare_term_ctor_type_name() { + let mut modules = BTreeMap::new(); + modules.insert("prelude".to_string(), + module_with_type_def("prelude", "Ordering")); + // Module `m` has no imports, no local Ordering, but a Term::Ctor + // referencing bare `Ordering`. + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] }, + "params": [], + "body": { + "t": "ctor", + "type": "Ordering", + "ctor": "LT", + "args": [] + } + }], + })).unwrap(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("bare Term::Ctor type must be rejected"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { + assert_eq!(module, "m"); + assert_eq!(name, "Ordering"); + assert_eq!(candidates, vec!["prelude.Ordering".to_string()], + "prelude is implicit-fallback"); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } +} +``` + +- [ ] **Step 2: Run the test to verify it fails** + +Run: `cargo test --workspace -p ailang-core ct1_validator_rejects_bare_term_ctor` +Expected: FAIL — Term::Ctor walking is not yet implemented, so the +validator does not visit `body.ctor.type` and the call returns Ok(()). + +- [ ] **Step 3: Add Term walking to the validator** + +Extend `validate_canonical_type_names` in +`crates/ailang-core/src/workspace.rs` (immediately after the +`walk_def_types` call for Type-side coverage, in the per-def loop): + +```rust + walk_def_terms(def, &mut |type_name: &str| { + check_type_con_name( + type_name, mod_name, &local_types, &import_names, + ) + })?; +``` + +Add these helpers after `walk_type`: + +```rust +/// ct.1: walk every `Term::Ctor.type_name` reachable from a single +/// `Def`, plus every `Type` embedded in `Term::Lam` annotations, +/// calling `f` on the type_name strings and (separately) on the +/// embedded types. Used to enforce the canonical-form rule on +/// term-side type references. +fn walk_def_terms(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + match def { + Def::Fn(fd) => walk_term(&fd.body, f), + Def::Const(cd) => walk_term(&cd.value, f), + Def::Type(_) => Ok(()), + Def::Class(cd) => { + for cm in &cd.methods { + if let Some(body) = &cm.default { + walk_term(body, f)?; + } + } + Ok(()) + } + Def::Instance(id) => { + for im in &id.methods { + walk_term(&im.body, f)?; + } + Ok(()) + } + } +} + +/// ct.1: recursive walk of a `Term`, calling `f` on every +/// `Term::Ctor.type_name`. Embedded `Type` annotations (Lam param / +/// return types, LetRec types) ride the `walk_def_types` path via +/// the fn-signature's Type::Forall — but Lam-internal types live on +/// `Term`, not `Def`, so walk them here. +fn walk_term(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + use crate::ast::{Pattern, Term}; + match t { + Term::Lit { .. } | Term::Var { .. } => Ok(()), + Term::App { callee, args, .. } => { + walk_term(callee, f)?; + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Let { value, body, .. } => { + walk_term(value, f)?; + walk_term(body, f) + } + Term::LetRec { body, in_term, .. } => { + walk_term(body, f)?; + walk_term(in_term, f) + } + Term::If { cond, then, else_ } => { + walk_term(cond, f)?; + walk_term(then, f)?; + walk_term(else_, f) + } + Term::Do { args, .. } => { + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Ctor { type_name, args, .. } => { + f(type_name)?; + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Match { scrutinee, arms } => { + walk_term(scrutinee, f)?; + for arm in arms { + walk_pattern(&arm.pat, f)?; + walk_term(&arm.body, f)?; + } + Ok(()) + } + Term::Lam { body, .. } => walk_term(body, f), + Term::Seq { lhs, rhs } => { + walk_term(lhs, f)?; + walk_term(rhs, f) + } + Term::Clone { value } => walk_term(value, f), + Term::ReuseAs { source, body } => { + walk_term(source, f)?; + walk_term(body, f) + } + } +} + +/// ct.1: Pattern::Ctor carries a `ctor` name (matches against a +/// scrutinee's TypeDef) but NOT a type_name field — the type is +/// inferred from the scrutinee. So Pattern walking only recurses; +/// no canonical-form check fires here. +fn walk_pattern(p: &crate::ast::Pattern, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + use crate::ast::Pattern; + match p { + Pattern::Wild | Pattern::Var { .. } | Pattern::Lit { .. } => Ok(()), + Pattern::Ctor { fields, .. } => { + for sub in fields { + walk_pattern(sub, f)?; + } + Ok(()) + } + } +} +``` + +(The `Term` import at the top of `workspace.rs` was already added in +Task 1 Step 4; no further import changes are needed here.) + +- [ ] **Step 4: Run the test to verify it passes** + +Run: `cargo test --workspace -p ailang-core ct1_validator_rejects_bare_term_ctor` +Expected: PASS. + +- [ ] **Step 5: Run the full crate test suite** + +Run: `cargo test --workspace -p ailang-core` +Expected: PASS — the validator is still not wired into `load_workspace`, +so existing fixtures continue to load. + +- [ ] **Step 6: Commit** + +```bash +git add crates/ailang-core/src/workspace.rs +git commit -m "iter ct.1.2: validator extends to Term::Ctor.type_name" +``` + +--- + +## Task 3: Class-name field rejection (4 fields) + +**Subject:** reject any `.` in `ClassDef.name`, `InstanceDef.class`, +`SuperclassRef.class`, and `Constraint.class`. Per spec §"Out of +scope: Class names", class names are NOT module-qualified in this +milestone; the validator catches half-migrated files where these +fields slipped through. + +**Files:** +- Modify: `crates/ailang-core/src/workspace.rs` — extend + `validate_canonical_type_names` with a class-name pass. +- Test: append one unit test per field (4 tests). + +- [ ] **Step 1: Write the failing tests** + +Append to `crates/ailang-core/src/workspace.rs::mod tests`: + +```rust +/// ct.1: a qualified `ClassDef.name` (e.g. `other.Eq`) must fire +/// `QualifiedClassName`. Class names stay bare in this milestone. +#[test] +fn ct1_validator_rejects_qualified_classdef_name() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "class", + "name": "other.MyEq", + "param": "a", + "methods": [] + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("qualified ClassDef.name must be rejected"); + match err { + WorkspaceLoadError::QualifiedClassName { module, name, field } => { + assert_eq!(module, "m"); + assert_eq!(name, "other.MyEq"); + assert_eq!(field, "ClassDef.name"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } +} + +/// ct.1: a qualified `InstanceDef.class` must fire +/// `QualifiedClassName`. +#[test] +fn ct1_validator_rejects_qualified_instancedef_class() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "instance", + "class": "other.MyEq", + "type": { "k": "con", "name": "Int" }, + "methods": [] + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("qualified InstanceDef.class must be rejected"); + match err { + WorkspaceLoadError::QualifiedClassName { name, field, .. } => { + assert_eq!(name, "other.MyEq"); + assert_eq!(field, "InstanceDef.class"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } +} + +/// ct.1: a qualified `SuperclassRef.class` must fire +/// `QualifiedClassName`. +#[test] +fn ct1_validator_rejects_qualified_superclassref_class() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "class", + "name": "MyOrd", + "param": "a", + "superclass": { "class": "other.MyEq", "type": "a" }, + "methods": [] + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("qualified SuperclassRef.class must be rejected"); + match err { + WorkspaceLoadError::QualifiedClassName { name, field, .. } => { + assert_eq!(name, "other.MyEq"); + assert_eq!(field, "SuperclassRef.class"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } +} + +/// ct.1: a qualified `Constraint.class` (inside a `Type::Forall`) +/// must fire `QualifiedClassName`. +#[test] +fn ct1_validator_rejects_qualified_constraint_class() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { + "k": "forall", + "vars": ["a"], + "constraints": [ + { "class": "other.MyEq", "type": { "k": "var", "name": "a" } } + ], + "body": { + "k": "fn", "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Unit" }, "effects": [] + } + }, + "params": ["x"], + "body": { "t": "lit", "lit": { "kind": "unit" } } + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("qualified Constraint.class must be rejected"); + match err { + WorkspaceLoadError::QualifiedClassName { name, field, .. } => { + assert_eq!(name, "other.MyEq"); + assert_eq!(field, "Constraint.class"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } +} +``` + +- [ ] **Step 2: Run the tests to verify they fail** + +Run: `cargo test --workspace -p ailang-core ct1_validator_rejects_qualified_` +Expected: FAIL — class-name fields are not yet checked; all four return Ok(()). + +- [ ] **Step 3: Add class-name field check to the validator** + +Extend `validate_canonical_type_names`'s per-def loop in +`crates/ailang-core/src/workspace.rs` (immediately after the +`walk_def_terms` call): + +```rust + check_class_name_fields(def, mod_name)?; +``` + +And add the new fn after `walk_pattern`: + +```rust +/// ct.1: reject any `.` in the four class-reference fields. +/// `ClassDef.name`, `InstanceDef.class`, `SuperclassRef.class`, +/// `Constraint.class`. Per spec §"Out of scope: Class names": class +/// names are NOT module-qualified in this milestone, so any +/// qualified form indicates a half-migrated file. +fn check_class_name_fields( + def: &Def, + owning_module: &str, +) -> Result<(), WorkspaceLoadError> { + fn fire( + owning_module: &str, + name: &str, + field: &'static str, + ) -> WorkspaceLoadError { + WorkspaceLoadError::QualifiedClassName { + module: owning_module.to_string(), + name: name.to_string(), + field, + } + } + match def { + Def::Class(cd) => { + if cd.name.contains('.') { + return Err(fire(owning_module, &cd.name, "ClassDef.name")); + } + if let Some(sc) = &cd.superclass { + if sc.class.contains('.') { + return Err(fire(owning_module, &sc.class, "SuperclassRef.class")); + } + } + for m in &cd.methods { + if let Type::Forall { constraints, .. } = &m.ty { + for c in constraints { + if c.class.contains('.') { + return Err(fire(owning_module, &c.class, "Constraint.class")); + } + } + } + } + Ok(()) + } + Def::Instance(id) => { + if id.class.contains('.') { + return Err(fire(owning_module, &id.class, "InstanceDef.class")); + } + Ok(()) + } + Def::Fn(fd) => { + if let Type::Forall { constraints, .. } = &fd.ty { + for c in constraints { + if c.class.contains('.') { + return Err(fire(owning_module, &c.class, "Constraint.class")); + } + } + } + Ok(()) + } + Def::Const(_) | Def::Type(_) => Ok(()), + } +} +``` + +- [ ] **Step 4: Run the tests to verify they pass** + +Run: `cargo test --workspace -p ailang-core ct1_validator_rejects_qualified_` +Expected: PASS — all four tests green. + +- [ ] **Step 5: Run the full crate test suite** + +Run: `cargo test --workspace -p ailang-core` +Expected: PASS. + +- [ ] **Step 6: Commit** + +```bash +git add crates/ailang-core/src/workspace.rs +git commit -m "iter ct.1.3: validator rejects qualified class-name fields" +``` + +--- + +## Task 4: Migration subcommand `ail migrate-canonical-types ` + +**Subject:** add the dev-only CLI subcommand that walks `/*.ail.json`, +rewrites bare cross-module Type::Con and Term::Ctor.type_name +references to their qualified form using the first-match-in-imports-order +disambiguation rule (with prelude as implicit last-resort). Idempotent. + +**Files:** +- Modify: `crates/ail/src/main.rs` — new variant `Cmd::MigrateCanonicalTypes { dir: PathBuf }` + + handler. +- Modify: `crates/ailang-core/src/workspace.rs` — expose + `walk_def_types_mut` + `walk_def_terms_mut` as `pub(crate)` so the + CLI can mutate. (Implementer may instead choose to write the rewrite + inline in main.rs using `serde_json::Value` editing — both are valid; + the implementer picks the cleaner one. The plan prefers the AST-mutating + variant for type-safety.) +- Test: `crates/ail/tests/migrate_canonical_types.rs` (new) — + E2E test that builds a synthetic workspace in a tempdir, runs the + migration, and asserts the rewritten files are byte-stable on a + second run (idempotence). + +- [ ] **Step 1: Write the failing E2E test** + +Create `crates/ail/tests/migrate_canonical_types.rs`: + +```rust +//! ct.1: E2E test for `ail migrate-canonical-types `. +//! +//! Builds a synthetic workspace in a tempdir with one fixture that +//! has a bare cross-module Type::Con ref, runs the migration, then +//! asserts: (a) the rewritten fixture's `Term::Ctor.type_name` is +//! now qualified; (b) running migration again produces no diff +//! (idempotence). + +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn tmp_dir(tag: &str) -> PathBuf { + let d = std::env::temp_dir().join(format!( + "ailang_migrate_test_{tag}_{}", + std::process::id() + )); + let _ = fs::remove_dir_all(&d); + fs::create_dir_all(&d).unwrap(); + d +} + +fn ail_bin() -> PathBuf { + // CARGO_BIN_EXE_ is set by cargo when building integration tests. + PathBuf::from(env!("CARGO_BIN_EXE_ail")) +} + +#[test] +fn migrate_canonical_types_rewrites_bare_xmod_term_ctor() { + let dir = tmp_dir("rewrites_bare_xmod"); + // Defining module: `other` declares `type Foo`. + let other_path = dir.join("other.ail.json"); + fs::write(&other_path, serde_json::to_vec_pretty(&serde_json::json!({ + "schema": "ailang/v0", + "name": "other", + "imports": [], + "defs": [{ "kind": "type", "name": "Foo", "ctors": [{ "name": "MkFoo", "fields": [] }] }], + })).unwrap()).unwrap(); + // Consumer module: imports `other`, uses bare `Foo` Term::Ctor. + let main_path = dir.join("main.ail.json"); + let bare_module = serde_json::json!({ + "schema": "ailang/v0", + "name": "main", + "imports": [{ "module": "other" }], + "defs": [{ + "kind": "fn", "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] }, + "params": [], + "body": { "t": "ctor", "type": "Foo", "ctor": "MkFoo", "args": [] } + }], + }); + fs::write(&main_path, serde_json::to_vec_pretty(&bare_module).unwrap()).unwrap(); + + // Run migration. + let status = Command::new(ail_bin()) + .args(["migrate-canonical-types", dir.to_str().unwrap()]) + .status() + .expect("ail binary must launch"); + assert!(status.success(), "migration exited non-zero"); + + // Inspect rewritten consumer. + let after: serde_json::Value = serde_json::from_slice( + &fs::read(&main_path).unwrap() + ).unwrap(); + let ctor_type = after["defs"][0]["body"]["type"].as_str().unwrap(); + assert_eq!(ctor_type, "other.Foo", + "Term::Ctor.type must be qualified after migration"); + + // Idempotence: run migration again, capture bytes, compare. + let bytes_before = fs::read(&main_path).unwrap(); + let status2 = Command::new(ail_bin()) + .args(["migrate-canonical-types", dir.to_str().unwrap()]) + .status() + .expect("ail binary must launch"); + assert!(status2.success(), "second migration exited non-zero"); + let bytes_after = fs::read(&main_path).unwrap(); + assert_eq!(bytes_before, bytes_after, "migration must be idempotent"); +} +``` + +- [ ] **Step 2: Run the test to verify it fails** + +Run: `cargo build --workspace && cargo test --workspace -p ail migrate_canonical_types_rewrites_bare_xmod_term_ctor` +Expected: FAIL — the `migrate-canonical-types` subcommand does not +yet exist; the binary will print an unrecognised-subcommand error. + +- [ ] **Step 3: Add the subcommand** + +In `crates/ail/src/main.rs`, add to the `enum Cmd` (anywhere is fine; +after `MergeProse` is conventional): + +```rust + /// ct.1 (dev-only): rewrite every `*.ail.json` under `` so + /// that bare cross-module `Type::Con` and `Term::Ctor.type_name` + /// references gain their owning module's qualifier. Idempotent. + /// Uses the first-match-in-imports-order disambiguation rule + /// (matches iter 23.1.3's imports-fallback) so the rewrite never + /// silently changes which type a fixture resolves to. Prelude is + /// treated as an implicit last-resort fallback. + MigrateCanonicalTypes { + /// Directory containing `*.ail.json` to migrate (typically + /// `examples/`). + dir: PathBuf, + }, +``` + +In the `match cli.cmd { ... }` block in `fn main`, add the handler. +The implementation walks every `*.ail.json` under `dir`, parses each +as a `Module`, applies the rewrite per-file, and writes back via +canonical JSON. Implementation skeleton: + +```rust + Cmd::MigrateCanonicalTypes { dir } => { + use ailang_core::ast::{Def, Module, Term, Type}; + use ailang_core::canonical; + use std::collections::{BTreeMap, BTreeSet}; + use std::fs; + + // Pass 1: load every *.ail.json in `dir` into a map by + // module name (NOT via load_workspace — these fixtures + // may currently fail validation). + let mut modules: BTreeMap = BTreeMap::new(); + for entry in fs::read_dir(&dir)? { + let entry = entry?; + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("json") { + continue; + } + let bytes = fs::read(&path)?; + let m: Module = match serde_json::from_slice(&bytes) { + Ok(m) => m, + Err(_) => continue, // not a Module (e.g. snapshot files) + }; + modules.insert(m.name.clone(), (path, m)); + } + + // Include the embedded prelude (so the implicit fallback + // matches the loader's behaviour). + let prelude_json: &str = include_str!( + "../../../examples/prelude.ail.json" + ); + let prelude: Module = serde_json::from_str(prelude_json) + .expect("embedded prelude must parse"); + if !modules.contains_key("prelude") { + modules.insert("prelude".to_string(), + (PathBuf::new(), prelude)); + } + + // Pre-pass: per-module local-types index. + let mut local_types: BTreeMap> = BTreeMap::new(); + for (name, (_, m)) in &modules { + let mut s = BTreeSet::new(); + for d in &m.defs { + if let Def::Type(t) = d { + s.insert(t.name.clone()); + } + } + local_types.insert(name.clone(), s); + } + + // Pass 2: rewrite each module's bare cross-module refs. + // Skip the prelude entry (synthetic, no path to write to). + let mut rewritten = 0usize; + for (mod_name, (path, m)) in modules.iter_mut() { + if mod_name == "prelude" && path.as_os_str().is_empty() { + continue; + } + let import_names: Vec = + m.imports.iter().map(|i| i.module.clone()).collect(); + let owning = mod_name.clone(); + + // Walk types + terms and mutate Type::Con.name + + // Term::Ctor.type_name. The mutation rule mirrors + // the validator's `check_type_con_name` but, on bare + // non-primitive non-local hits, rewrites instead of + // erroring. + let mut changed = false; + for def in &mut m.defs { + rewrite_def(def, &owning, &local_types, &import_names, &mut changed); + } + if changed { + let bytes = serde_json::to_vec_pretty(m)?; + fs::write(path, bytes)?; + println!("migrated: {}", path.display()); + rewritten += 1; + } + } + println!("done. {} file(s) rewritten.", rewritten); + Ok(()) + } +``` + +Plus the helper `fn rewrite_def(...)` at module-bottom of +`crates/ail/src/main.rs`: + +```rust +/// ct.1 migration helper: rewrite bare cross-module Type::Con names +/// and Term::Ctor.type_name to their qualified form. Sets +/// `*changed` to `true` if any rewrite happened. +fn rewrite_def( + def: &mut ailang_core::ast::Def, + owning_module: &str, + local_types: &std::collections::BTreeMap>, + import_names: &[String], + changed: &mut bool, +) { + use ailang_core::ast::{Def, Type, Term}; + + fn rewrite_name( + name: &mut String, + owning_module: &str, + local_types: &std::collections::BTreeMap>, + import_names: &[String], + changed: &mut bool, + ) { + if name.contains('.') { return; } + if matches!(name.as_str(), "Int" | "Bool" | "Str" | "Unit" | "Float") { return; } + if local_types.get(owning_module).map(|s| s.contains(name)).unwrap_or(false) { + return; + } + // Bare cross-module — find owner via imports-in-order, with prelude as fallback. + let owner: Option<&str> = import_names.iter() + .map(|s| s.as_str()) + .find(|imp| local_types.get(*imp).map(|s| s.contains(name)).unwrap_or(false)) + .or_else(|| { + if local_types.get("prelude").map(|s| s.contains(name)).unwrap_or(false) { + Some("prelude") + } else { + None + } + }); + if let Some(owner) = owner { + *name = format!("{owner}.{name}"); + *changed = true; + } + // If no owner found, leave bare — validator will reject later. + } + + fn rewrite_type( + t: &mut Type, + owning_module: &str, + local_types: &std::collections::BTreeMap>, + import_names: &[String], + changed: &mut bool, + ) { + match t { + Type::Con { name, args } => { + rewrite_name(name, owning_module, local_types, import_names, changed); + for a in args { + rewrite_type(a, owning_module, local_types, import_names, changed); + } + } + Type::Fn { params, ret, .. } => { + for p in params { rewrite_type(p, owning_module, local_types, import_names, changed); } + rewrite_type(ret, owning_module, local_types, import_names, changed); + } + Type::Forall { body, constraints, .. } => { + for c in constraints { + rewrite_type(&mut c.type_, owning_module, local_types, import_names, changed); + } + rewrite_type(body, owning_module, local_types, import_names, changed); + } + Type::Var { .. } => {} + } + } + + fn rewrite_term( + t: &mut Term, + owning_module: &str, + local_types: &std::collections::BTreeMap>, + import_names: &[String], + changed: &mut bool, + ) { + match t { + Term::Lit { .. } | Term::Var { .. } => {} + Term::App { callee, args, .. } => { + rewrite_term(callee, owning_module, local_types, import_names, changed); + for a in args { rewrite_term(a, owning_module, local_types, import_names, changed); } + } + Term::Let { value, body, .. } => { + rewrite_term(value, owning_module, local_types, import_names, changed); + rewrite_term(body, owning_module, local_types, import_names, changed); + } + Term::LetRec { ty, body, in_term, .. } => { + rewrite_type(ty, owning_module, local_types, import_names, changed); + rewrite_term(body, owning_module, local_types, import_names, changed); + rewrite_term(in_term, owning_module, local_types, import_names, changed); + } + Term::If { cond, then, else_ } => { + rewrite_term(cond, owning_module, local_types, import_names, changed); + rewrite_term(then, owning_module, local_types, import_names, changed); + rewrite_term(else_, owning_module, local_types, import_names, changed); + } + Term::Do { args, .. } => { + for a in args { rewrite_term(a, owning_module, local_types, import_names, changed); } + } + Term::Ctor { type_name, args, .. } => { + rewrite_name(type_name, owning_module, local_types, import_names, changed); + for a in args { rewrite_term(a, owning_module, local_types, import_names, changed); } + } + Term::Match { scrutinee, arms } => { + rewrite_term(scrutinee, owning_module, local_types, import_names, changed); + for arm in arms { + rewrite_term(&mut arm.body, owning_module, local_types, import_names, changed); + } + } + Term::Lam { param_tys, ret_ty, body, .. } => { + for pt in param_tys { rewrite_type(pt, owning_module, local_types, import_names, changed); } + rewrite_type(ret_ty, owning_module, local_types, import_names, changed); + rewrite_term(body, owning_module, local_types, import_names, changed); + } + Term::Seq { lhs, rhs } => { + rewrite_term(lhs, owning_module, local_types, import_names, changed); + rewrite_term(rhs, owning_module, local_types, import_names, changed); + } + Term::Clone { value } => rewrite_term(value, owning_module, local_types, import_names, changed), + Term::ReuseAs { source, body } => { + rewrite_term(source, owning_module, local_types, import_names, changed); + rewrite_term(body, owning_module, local_types, import_names, changed); + } + } + } + + match def { + Def::Fn(fd) => { + rewrite_type(&mut fd.ty, owning_module, local_types, import_names, changed); + rewrite_term(&mut fd.body, owning_module, local_types, import_names, changed); + } + Def::Const(cd) => { + rewrite_type(&mut cd.ty, owning_module, local_types, import_names, changed); + rewrite_term(&mut cd.value, owning_module, local_types, import_names, changed); + } + Def::Type(td) => { + for c in &mut td.ctors { + for fty in &mut c.fields { + rewrite_type(fty, owning_module, local_types, import_names, changed); + } + } + } + Def::Class(cd) => { + for cm in &mut cd.methods { + rewrite_type(&mut cm.ty, owning_module, local_types, import_names, changed); + if let Some(body) = &mut cm.default { + rewrite_term(body, owning_module, local_types, import_names, changed); + } + } + } + Def::Instance(id) => { + rewrite_type(&mut id.type_, owning_module, local_types, import_names, changed); + for im in &mut id.methods { + rewrite_term(&mut im.body, owning_module, local_types, import_names, changed); + } + } + } +} +``` + +- [ ] **Step 4: Run the test to verify it passes** + +Run: `cargo test --workspace -p ail migrate_canonical_types_rewrites_bare_xmod_term_ctor` +Expected: PASS — the migration rewrites the bare ref, and the second +run leaves bytes unchanged. + +- [ ] **Step 5: Commit** + +```bash +git add crates/ail/src/main.rs crates/ail/tests/migrate_canonical_types.rs +git commit -m "iter ct.1.4: dev-only ail migrate-canonical-types subcommand" +``` + +--- + +## Task 5: Run migration on `examples/` — single bulk commit + +**Subject:** apply the migration tool to the in-tree fixtures. The +fixture survey identified two files that today rely on the +imports-fallback for bare cross-module Type::Con / Term::Ctor refs: + +- `examples/ordering_match.ail.json` — `Term::Ctor.type_name` = + `"Ordering"` (bare, owner is implicit prelude). +- `examples/test_22b1_dup_a.ail.json` — `Type::Con.name` = `"MyInt"` + (bare, owner is imported `test_22b1_dup_b`). + +The migration tool rewrites both to their qualified form. No other +in-tree fixture should change (intra-module-only fixtures are +bit-stable per spec §Migration impact). + +**Files:** +- Run: `cargo run --bin ail -- migrate-canonical-types examples/` +- Migrate (auto-rewritten): `examples/ordering_match.ail.json`, + `examples/test_22b1_dup_a.ail.json`. + +- [ ] **Step 1: Run the migration on `examples/`** + +Run: `cargo run --bin ail -- migrate-canonical-types examples/` +Expected stdout: two lines `migrated: examples/...`, followed by +`done. 2 file(s) rewritten.` If a different count appears, **stop +and diagnose**: extra rewrites mean the survey missed a fixture, or +the tool is over-eager. + +- [ ] **Step 2: Inspect the diff** + +Run: `git diff examples/` +Expected: exactly two files changed; each diff is a single-string +substitution: + +- `ordering_match.ail.json`: `"type": "Ordering"` → `"type": "prelude.Ordering"` + (1 occurrence inside `Term::Ctor`). +- `test_22b1_dup_a.ail.json`: `"name": "MyInt"` → `"name": "test_22b1_dup_b.MyInt"` + (1 occurrence inside `Type::Con`). + +Plus any reformatting `serde_json::to_vec_pretty` introduces. If the +reformatting introduces unrelated whitespace churn that obscures the +substantive change, the implementer may use `jq --indent 2` or a +minimal post-pass to preserve original formatting — but the rewrite +itself MUST round-trip the AST, not the bytes, so some byte-level +churn is acceptable. + +- [ ] **Step 3: Verify both migrated fixtures still load + work** + +Run: `cargo test --workspace` +Expected: PASS — the typechecker's existing imports-fallback paths +continue to handle the qualified form (they already do, per iter +23.1.3's documentation). The validator is NOT yet wired (that lands +in Task 6), so the migration is just a pre-emptive shape change at +this point. + +- [ ] **Step 4: Commit** + +```bash +git add examples/ordering_match.ail.json examples/test_22b1_dup_a.ail.json +git commit -m "iter ct.1.5: migrate bare cross-module type refs in examples/" +``` + +--- + +## Task 6: Wire validator into `load_workspace` + update kind-mismatch test expectation + +**Subject:** wire `validate_canonical_type_names` into `load_workspace` +(immediately after prelude injection, before `validate_classdefs`). +Update the existing kind-mismatch regression test, whose fixture +uses `Type::Con { name: "f" }` as the class param — the new +validator now catches this shape as a `BareCrossModuleTypeRef` +BEFORE `validate_classdefs` runs. Verify full `cargo test +--workspace` green. + +**Files:** +- Modify: `crates/ailang-core/src/workspace.rs::load_workspace` — + add a call to `validate_canonical_type_names` after the prelude + insertion, before `validate_classdefs`. +- Modify: `crates/ailang-core/src/workspace.rs::tests::class_param_in_applied_position_fires_kind_mismatch` + — update to expect `BareCrossModuleTypeRef { name: "f", .. }` + instead of `KindMismatch`. Rename the test to reflect what it + actually pins: `class_param_in_applied_position_fires_canonical_form_rejection`. + The `KindMismatch` diagnostic path becomes structurally + unreachable through well-formed schema; leave the existing + `validate_classdefs` code in place for now (cleanup is out of + scope for ct.1 — eligible for a follow-up tidy later). + +- [ ] **Step 1: Wire the validator** + +In `crates/ailang-core/src/workspace.rs::load_workspace`, after the +existing `modules.insert("prelude".to_string(), prelude);` and +before `validate_classdefs(&modules)?;`, add: + +```rust + // ct.1: enforce the canonical-form rule on Type::Con and + // Term::Ctor.type_name. Runs before class-schema validation + // so a stale bare cross-module ref fires the canonical-form + // diagnostic instead of a downstream one. + validate_canonical_type_names(&modules)?; +``` + +- [ ] **Step 2: Update the kind-mismatch test expectation** + +In `crates/ailang-core/src/workspace.rs::mod tests`, replace the +existing `class_param_in_applied_position_fires_kind_mismatch` test +with: + +```rust + /// ct.1: a class whose parameter `f` appears as a `Type::Con` + /// name (the malformed-but-historically-test-fixture shape used + /// to trigger `KindMismatch` pre-ct.1) is now caught earlier by + /// the canonical-type-names validator: `f` is bare, + /// non-primitive, and not a TypeDef in the owning module, so + /// `BareCrossModuleTypeRef` fires before `validate_classdefs` + /// gets a chance to run. The `KindMismatch` path stays in the + /// codebase as dead-but-defensive code; a future tidy may + /// retire it. + #[test] + fn class_param_in_applied_position_fires_canonical_form_rejection() { + let entry = std::path::PathBuf::from( + "../../examples/test_22b2_kind_mismatch.ail.json", + ); + let err = load_workspace(&entry) + .expect_err("must fire canonical-form rejection"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { module, name, .. } => { + assert_eq!(module, "test_22b2_kind_mismatch"); + assert_eq!(name, "f"); + } + other => panic!( + "expected BareCrossModuleTypeRef (validator now fires first), got {other:?}", + ), + } + } +``` + +- [ ] **Step 3: Run the workspace test suite** + +Run: `cargo test --workspace -p ailang-core` +Expected: PASS. + +If any other test fails because its fixture now trips the validator, +the implementer must: + +1. **Stop and survey.** A failing test outside the kind-mismatch one + is a signal that the migration in Task 5 missed a fixture. +2. **Don't adapt the test to the bug** — re-run the migration tool + on the failing fixture, confirm it picks the right qualifier, and + include the rewrite in this task's commit. +3. **If the migration tool can't fix it** (e.g. the bare ref names a + type that doesn't exist in any imported or prelude module), the + fixture is malformed schema; that's a separate diagnosis. Report + `BLOCKED` and escalate to the orchestrator. + +- [ ] **Step 4: Run the full workspace test suite (all crates)** + +Run: `cargo build --workspace && cargo test --workspace` +Expected: PASS — `ailang-check`, `ailang-codegen`, `ail`'s E2E suite, +all green. + +- [ ] **Step 5: Commit** + +```bash +git add crates/ailang-core/src/workspace.rs +git commit -m "iter ct.1.6: wire validator into load_workspace; refresh kind-mismatch test" +``` + +--- + +## Task 7: Three new fixture tests for the diagnostic surface + +**Subject:** the unit tests in Tasks 1-3 use synthetic in-memory +modules. For the diagnostic shape to be observable via the `ail +check` CLI path (and for fieldtest-style end-to-end pinning), three +on-disk fixtures land here. Each fixture is paired with a test in +`crates/ailang-core/src/workspace.rs::mod tests`. + +**Files:** +- Create: `examples/test_ct1_bare_xmod_rejected.ail.json` — bare + `Ordering` Term::Ctor without imports. +- Create: `examples/test_ct1_bad_qualifier.ail.json` — qualified + `Mystery.Type` with `Mystery` not a known module. +- Create: `examples/test_ct1_qualified_class_rejected.ail.json` — + qualified `prelude.Eq` in an `InstanceDef.class` field. +- Modify: `crates/ailang-core/src/workspace.rs::mod tests` — three + new fixture-loading tests. + +- [ ] **Step 1: Create fixture 1 — bare cross-module ref** + +Create `examples/test_ct1_bare_xmod_rejected.ail.json`: + +```json +{ + "schema": "ailang/v0", + "name": "test_ct1_bare_xmod_rejected", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "main", + "type": { + "k": "fn", + "params": [], + "ret": { "k": "con", "name": "Unit" }, + "effects": ["IO"] + }, + "params": [], + "body": { + "t": "ctor", + "type": "Ordering", + "ctor": "LT", + "args": [] + } + } + ] +} +``` + +- [ ] **Step 2: Create fixture 2 — bad qualifier** + +Create `examples/test_ct1_bad_qualifier.ail.json`: + +```json +{ + "schema": "ailang/v0", + "name": "test_ct1_bad_qualifier", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "f", + "type": { + "k": "fn", + "params": [], + "ret": { "k": "con", "name": "Mystery.Type" }, + "effects": [] + }, + "params": [], + "body": { "t": "lit", "lit": { "kind": "unit" } } + } + ] +} +``` + +- [ ] **Step 3: Create fixture 3 — qualified class name** + +Create `examples/test_ct1_qualified_class_rejected.ail.json`: + +```json +{ + "schema": "ailang/v0", + "name": "test_ct1_qualified_class_rejected", + "imports": [], + "defs": [ + { + "kind": "instance", + "class": "prelude.Eq", + "type": { "k": "con", "name": "Int" }, + "methods": [] + } + ] +} +``` + +- [ ] **Step 4: Add three on-disk fixture tests** + +Append to `crates/ailang-core/src/workspace.rs::mod tests`: + +```rust +/// ct.1: on-disk fixture for `BareCrossModuleTypeRef`. Bare +/// `Ordering` Term::Ctor with no imports; the validator catches it +/// after prelude injection (so the candidate list contains +/// `prelude.Ordering`). +#[test] +fn ct1_fixture_bare_xmod_rejected() { + let entry = examples_dir().join("test_ct1_bare_xmod_rejected.ail.json"); + let err = load_workspace(&entry).expect_err("must reject bare Ordering"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { + assert_eq!(module, "test_ct1_bare_xmod_rejected"); + assert_eq!(name, "Ordering"); + assert_eq!(candidates, vec!["prelude.Ordering".to_string()]); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } +} + +/// ct.1: on-disk fixture for `BadCrossModuleTypeRef`. Qualified +/// `Mystery.Type` with `Mystery` not a known module. +#[test] +fn ct1_fixture_bad_qualifier() { + let entry = examples_dir().join("test_ct1_bad_qualifier.ail.json"); + let err = load_workspace(&entry).expect_err("must reject Mystery.Type"); + match err { + WorkspaceLoadError::BadCrossModuleTypeRef { module, name } => { + assert_eq!(module, "test_ct1_bad_qualifier"); + assert_eq!(name, "Mystery.Type"); + } + other => panic!("expected BadCrossModuleTypeRef, got {other:?}"), + } +} + +/// ct.1: on-disk fixture for `QualifiedClassName`. Qualified +/// `prelude.Eq` in an `InstanceDef.class` field — the schema +/// rejects this so half-migrated files cannot silently load. +#[test] +fn ct1_fixture_qualified_class_rejected() { + let entry = examples_dir().join("test_ct1_qualified_class_rejected.ail.json"); + let err = load_workspace(&entry).expect_err("must reject prelude.Eq"); + match err { + WorkspaceLoadError::QualifiedClassName { module, name, field } => { + assert_eq!(module, "test_ct1_qualified_class_rejected"); + assert_eq!(name, "prelude.Eq"); + assert_eq!(field, "InstanceDef.class"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } +} +``` + +- [ ] **Step 5: Run the new fixture tests** + +Run: `cargo test --workspace -p ailang-core ct1_fixture_` +Expected: PASS — all three on-disk fixture tests green. + +- [ ] **Step 6: Run the full workspace test suite** + +Run: `cargo build --workspace && cargo test --workspace` +Expected: PASS. + +- [ ] **Step 7: Commit** + +```bash +git add crates/ailang-core/src/workspace.rs examples/test_ct1_*.ail.json +git commit -m "iter ct.1.7: on-disk fixture tests for canonical-form diagnostics" +``` + +--- + +## Coverage check (Step-5 self-review post-write) + +| Spec § | Task | +|-------------------------|------| +| Validator rule 1 (qualified) | Task 1 (Type::Con) + Task 2 (Term::Ctor) | +| Validator rule 2 (primitive) | Task 1 | +| Validator rule 3 (bare local + bare-xmod rejection) | Task 1 + Task 2 | +| Class-name field rejection | Task 3 | +| Migration tool (imports-order disambiguation) | Task 4 | +| Migration on `examples/` (2 fixtures) | Task 5 | +| Wire into `load_workspace` + kind-mismatch test refresh | Task 6 | +| On-disk fixture tests | Task 7 | +| `cargo test --workspace` green | Task 6 + Task 7 (re-verified) | + +Out of scope per spec, NOT in ct.1: removal of the 4 obsolete +mechanisms (Pattern::Ctor imports-fallback, Term::Ctor synth +imports-fallback, lookup_ctor_by_type fallback, mono ctor_index +overlay). Those land in ct.2 and ct.3. The validator gates the +canonical form; the cleanup follows once we know nothing depends +on the fallbacks at consumer sites. + +DESIGN.md amendments are ct.4, not ct.1.