diff --git a/docs/plans/2026-05-11-ct.2-typechecker-cleanup.md b/docs/plans/2026-05-11-ct.2-typechecker-cleanup.md
new file mode 100644
index 0000000..2f26d9e
--- /dev/null
+++ b/docs/plans/2026-05-11-ct.2-typechecker-cleanup.md
@@ -0,0 +1,1073 @@
+# Iteration ct.2: Typechecker Cleanup — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-10-canonical-type-names.md`
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Remove the two typechecker imports-fallback mechanisms that
+papered over bare cross-module type references, and wire
+`qualify_local_types` into the one remaining cross-module fn-lookup
+site that lacks it (class-method resolution).
+
+**Architecture:** Three sites in `crates/ailang-check/src/lib.rs`.
+Task 1 wires `qualify_local_types` into the `env.class_methods`
+channel (Term::Var path) so a class method whose declared type
+references a bare local Type::Con in its defining module is presented
+to the consumer's typecheck context as qualified — this closes the
+last cross-module fn-lookup boundary that lacks qualification. Tasks
+2 and 3 then delete the now-unreachable imports-fallback paths in
+`Pattern::Ctor` and `Term::Ctor` synth; both are replaced by direct
+type-driven lookup that uses the (post-ct.1) canonical
+`Type::Con.name` as its sole disambiguator. Order matters: Task 1
+first so that Tasks 2 and 3 do not break the class-method round-trip
+on the way through.
+
+**Tech Stack:** `crates/ailang-check/src/lib.rs` (only file touched
+in production code), `crates/ail/tests/mono_xmod_ctor_pattern.rs`
+(docstring refresh).
+
+---
+
+## Files this plan creates or modifies
+
+- Modify: `crates/ailang-check/src/lib.rs:1804-1818` — Term::Var
+ class-method channel: apply `qualify_local_types` to `cm.method_ty`
+ with `cm.defining_module` as owner.
+- Modify: `crates/ailang-check/src/lib.rs:2418-2422` —
+ `qualify_local_types`'s `Type::Forall` arm: recurse into
+ `constraints[].type_` (mirror of ct.1.5a-followup's fix to
+ `normalize_type_for_registry`).
+- Modify: `crates/ailang-check/src/lib.rs:2450-2522` — `Pattern::Ctor`
+ lookup: switch from `ctor_index.get(ctor)` + imports-fallback to
+ type-driven lookup keyed on the `expected: Type::Con` name.
+- Modify: `crates/ailang-check/src/lib.rs:1943-2027` — `Term::Ctor`
+ synth lookup: delete the bare-name imports-fallback else-branch;
+ leave qualified-and-local paths unchanged.
+- Modify: `crates/ailang-check/src/lib.rs` (unit tests near
+ lines 3582-3970): retarget or delete legacy fallback regression
+ tests; add new tests for canonical-form invariants.
+- Modify: `crates/ail/tests/mono_xmod_ctor_pattern.rs` — refresh
+ the module-level docstring (mentions the flat `ctor_index` and
+ imports-fallback by line number; both are gone post-Task 2).
+
+No files are created. No files are deleted.
+
+---
+
+## Task 1: Wire qualify_local_types into class-method channel
+
+The Term::Var resolution path at `lib.rs:1800-1854` has four
+branches: `locals`, `env.globals`, `env.class_methods`, qualified
+`prefix.suffix`. The qualified branch already runs
+`qualify_local_types` (line 1850). The `env.class_methods` branch
+does not — it pulls `cm.method_ty` and runs `substitute_rigids` for
+the class param, but the rest of the method type stays in the
+defining module's bare-local namespace.
+
+Post-ct.1, this is the structural gap that explains the
+iter 23.3 Task 4 failure: prelude's `compare : a → a → Ordering`
+returns a bare `Ordering` when called from a user module. The
+user module's `Pattern::Ctor LT` against that bare scrutinee no
+longer resolves because the post-ct.1 canonical form expects the
+scrutinee to be `prelude.Ordering`.
+
+**Also fix (same task, single commit):** the `Type::Forall` arm of
+`qualify_local_types` itself does not recurse into
+`constraints[].type_`. Symmetric to the ct.1.5a-followup fix to
+`normalize_type_for_registry`. A class method's signature is
+typically `Forall. Fn[..]` — the constraints carry types too
+(`a` here, but more generally any Type), and any bare-local Type::Con
+in them must be qualified.
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs:1804-1818` (the
+ `env.class_methods` branch in `synth`).
+- Modify: `crates/ailang-check/src/lib.rs:2418-2422` (the
+ `Type::Forall` arm in `qualify_local_types`).
+- Test: `crates/ailang-check/src/lib.rs` `mod tests` (append three
+ new tests next to the existing iter 15a / iter 23.1 tests).
+
+- [ ] **Step 1: Write the RED test for the class-method cross-module qualifier gap**
+
+Append to `crates/ailang-check/src/lib.rs` `mod tests`, immediately
+after `user_module_can_pattern_match_on_prelude_ordering_bare`
+(currently around line 3970):
+
+```rust
+/// ct.2 Task 1: a class method whose declared return type is a
+/// bare local Type::Con in the defining module (e.g.
+/// `compare : a -> a -> Ordering` declared inside `prelude`) must
+/// be presented to a consumer module's typecheck context with the
+/// return type qualified (`prelude.Ordering`). Without this, the
+/// consumer's `Pattern::Ctor LT` against the scrutinee no longer
+/// resolves once the post-ct.1 canonical form removes the
+/// imports-fallback that previously papered over the mismatch.
+#[test]
+fn ct2_class_method_cross_module_qualifies_return_type() {
+ // Defining module declares `Ordering` locally and a class
+ // `Ord` with a method `compare : a -> a -> Ordering`. The
+ // `Ordering` Type::Con is bare-local in the class method's ty,
+ // which is canonical post-ct.1 (bare = local to defining module).
+ let prelude = Module {
+ schema: SCHEMA.into(),
+ name: "p".into(),
+ imports: vec![],
+ defs: vec![
+ Def::Type(TypeDef {
+ name: "Ordering".into(),
+ vars: vec![],
+ ctors: vec![
+ Ctor { name: "LT".into(), fields: vec![] },
+ Ctor { name: "EQ".into(), fields: vec![] },
+ Ctor { name: "GT".into(), fields: vec![] },
+ ],
+ doc: None,
+ drop_iterative: false,
+ }),
+ Def::Class(ailang_core::ast::ClassDef {
+ name: "Ord".into(),
+ param: "a".into(),
+ superclass: None,
+ methods: vec![ailang_core::ast::ClassMethod {
+ name: "compare".into(),
+ ty: Type::Forall {
+ vars: vec!["a".into()],
+ constraints: vec![],
+ body: Box::new(Type::Fn {
+ params: vec![
+ Type::Var { name: "a".into() },
+ Type::Var { name: "a".into() },
+ ],
+ ret: Box::new(Type::Con {
+ name: "Ordering".into(),
+ args: vec![],
+ }),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ }),
+ },
+ default: None,
+ }],
+ doc: None,
+ }),
+ Def::Instance(ailang_core::ast::InstanceDef {
+ class: "Ord".into(),
+ type_: Type::int(),
+ methods: vec![ailang_core::ast::InstanceMethod {
+ name: "compare".into(),
+ body: Term::Lam {
+ params: vec!["x".into(), "y".into()],
+ param_tys: vec![Type::int(), Type::int()],
+ ret_ty: Box::new(Type::Con {
+ name: "Ordering".into(),
+ args: vec![],
+ }),
+ effects: vec![],
+ body: Box::new(Term::Ctor {
+ type_name: "Ordering".into(),
+ ctor: "EQ".into(),
+ args: vec![],
+ }),
+ },
+ }],
+ doc: None,
+ }),
+ ],
+ };
+ // Consumer module imports prelude and calls `compare` (bare).
+ // The return type seen by the consumer must be `p.Ordering`,
+ // not bare `Ordering` — otherwise the match arm below fails to
+ // typecheck because the Pattern::Ctor lookup is type-driven and
+ // would not find `LT` in any TypeDef named bare `Ordering` in
+ // the consumer's local types.
+ let consumer = Module {
+ schema: SCHEMA.into(),
+ name: "u".into(),
+ imports: vec![Import { module: "p".into(), alias: None }],
+ defs: vec![fn_def(
+ "use_compare",
+ Type::Fn {
+ params: vec![],
+ ret: Box::new(Type::int()),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ },
+ vec![],
+ Term::Match {
+ scrutinee: Box::new(Term::App {
+ callee: Box::new(Term::Var { name: "compare".into() }),
+ args: vec![
+ Term::Lit { lit: Literal::Int { value: 1 } },
+ Term::Lit { lit: Literal::Int { value: 2 } },
+ ],
+ tail: false,
+ }),
+ arms: vec![
+ Arm {
+ pat: Pattern::Ctor {
+ ctor: "LT".into(),
+ fields: vec![],
+ },
+ body: Term::Lit { lit: Literal::Int { value: 1 } },
+ },
+ Arm {
+ pat: Pattern::Ctor {
+ ctor: "EQ".into(),
+ fields: vec![],
+ },
+ body: Term::Lit { lit: Literal::Int { value: 2 } },
+ },
+ Arm {
+ pat: Pattern::Ctor {
+ ctor: "GT".into(),
+ fields: vec![],
+ },
+ body: Term::Lit { lit: Literal::Int { value: 3 } },
+ },
+ ],
+ },
+ )],
+ };
+ let mut modules = BTreeMap::new();
+ modules.insert("p".into(), prelude);
+ modules.insert("u".into(), consumer);
+ let ws = Workspace {
+ entry: "u".into(),
+ modules,
+ root_dir: std::path::PathBuf::from("."),
+ registry: ailang_core::workspace::Registry::default(),
+ };
+ let diags = check_workspace(&ws);
+ assert!(
+ diags.is_empty(),
+ "consumer module must typecheck cleanly when calling a class \
+ method whose return type is bare-local in its defining \
+ module; the class-method channel must apply \
+ qualify_local_types just like the qualified Term::Var path \
+ does. Got diagnostics: {:?}",
+ diags
+ );
+}
+```
+
+- [ ] **Step 2: Run RED test to verify it fails**
+
+Run: `cargo test --workspace -p ailang-check ct2_class_method_cross_module_qualifies_return_type`
+
+Expected: FAIL. The current diagnostic is a `PatternTypeMismatch`
+or `UnknownCtorInPattern` against bare `Ordering` (the exact
+variant depends on the lookup order; either way it is NOT empty).
+
+- [ ] **Step 3: Add the RED test for the Forall constraints recursion gap**
+
+Append next to the test from Step 1:
+
+```rust
+/// ct.2 Task 1: `qualify_local_types`'s `Type::Forall` arm must
+/// recurse into `constraints[].type_`. A class method whose
+/// declared type is `Forall{Ord a}. Fn[..]` carries the
+/// constraint type `Type::Var { name: "a" }` — fine — but a
+/// hypothetical `Forall{Show p.Foo}. Fn[..]` would carry a
+/// bare-local `Foo` if the defining module is `p`, and the
+/// consumer must see `p.Foo` after the cross-module qualifier
+/// runs. Symmetric to the ct.1.5a-followup fix on
+/// `normalize_type_for_registry`.
+#[test]
+fn ct2_qualify_local_types_recurses_into_forall_constraints() {
+ use crate::qualify_local_types;
+ let mut local_types: IndexMap = IndexMap::new();
+ local_types.insert("Foo".into(), ailang_core::ast::TypeDef {
+ name: "Foo".into(),
+ vars: vec![],
+ ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
+ doc: None,
+ drop_iterative: false,
+ });
+ let input = Type::Forall {
+ vars: vec!["a".into()],
+ constraints: vec![ailang_core::ast::Constraint {
+ class: "Show".into(),
+ type_: Type::Con { name: "Foo".into(), args: vec![] },
+ }],
+ body: Box::new(Type::Fn {
+ params: vec![Type::Var { name: "a".into() }],
+ ret: Box::new(Type::int()),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ }),
+ };
+ let out = qualify_local_types(&input, "p", &local_types);
+ match out {
+ Type::Forall { constraints, .. } => {
+ assert_eq!(constraints.len(), 1, "constraint count preserved");
+ match &constraints[0].type_ {
+ Type::Con { name, .. } => assert_eq!(
+ name, "p.Foo",
+ "constraint Type::Con must be qualified by qualify_local_types"
+ ),
+ other => panic!("expected Type::Con, got {:?}", other),
+ }
+ }
+ other => panic!("expected Type::Forall, got {:?}", other),
+ }
+}
+```
+
+- [ ] **Step 4: Run the second RED test to verify it fails**
+
+Run: `cargo test --workspace -p ailang-check ct2_qualify_local_types_recurses_into_forall_constraints`
+
+Expected: FAIL. The constraint's `Foo` stays bare in the output.
+
+- [ ] **Step 5: Apply the production fix — class-methods qualifier**
+
+Edit `crates/ailang-check/src/lib.rs:1804-1818`. Replace the
+`env.class_methods` branch body with:
+
+```rust
+ } else if let Some(cm) = env.class_methods.get(name) {
+ // Iter 22b.2 (Task 9): instantiate the class param with
+ // a fresh metavar; the body's unification at the call
+ // site fills it in, and the residual is the class
+ // constraint we owe at this use site.
+ //
+ // ct.2 Task 1: a class method's declared type lives in
+ // its defining module's bare-local namespace.
+ // qualify_local_types runs symmetrically with the
+ // Term::Var qualified path below so the consumer's
+ // typecheck context sees the method's return /
+ // parameter Type::Cons fully qualified.
+ let owner_types = env
+ .module_types
+ .get(&cm.defining_module)
+ .cloned()
+ .unwrap_or_default();
+ let qualified_method_ty =
+ qualify_local_types(&cm.method_ty, &cm.defining_module, &owner_types);
+ let fresh = Subst::fresh(counter);
+ let mut mapping: BTreeMap = BTreeMap::new();
+ mapping.insert(cm.class_param.clone(), fresh.clone());
+ let inst_ty = substitute_rigids(&qualified_method_ty, &mapping);
+ residuals.push(ResidualConstraint {
+ class: cm.class_name.clone(),
+ type_: fresh,
+ method: name.clone(),
+ });
+ return Ok(inst_ty);
+```
+
+- [ ] **Step 6: Apply the production fix — Forall constraints recursion**
+
+Edit `crates/ailang-check/src/lib.rs:2418-2422`. Replace the
+`Type::Forall` arm of `qualify_local_types` with:
+
+```rust
+ Type::Forall { vars, constraints, body } => Type::Forall {
+ vars: vars.clone(),
+ constraints: constraints
+ .iter()
+ .map(|c| ailang_core::ast::Constraint {
+ class: c.class.clone(),
+ type_: qualify_local_types(&c.type_, owner_module, local_types),
+ })
+ .collect(),
+ body: Box::new(qualify_local_types(body, owner_module, local_types)),
+ },
+```
+
+- [ ] **Step 7: Run both new tests to verify they pass**
+
+Run: `cargo test --workspace -p ailang-check ct2_class_method_cross_module_qualifies_return_type ct2_qualify_local_types_recurses_into_forall_constraints`
+
+Expected: PASS (both).
+
+- [ ] **Step 8: Run the full check workspace test suite to confirm no regressions**
+
+Run: `cargo test --workspace -p ailang-check`
+
+Expected: all pass (no count regression; the two new tests are the
+only additions).
+
+- [ ] **Step 9: Run the full workspace test suite**
+
+Run: `cargo test --workspace`
+
+Expected: all pass.
+
+- [ ] **Step 10: Commit**
+
+```bash
+git add crates/ailang-check/src/lib.rs
+git commit -m "iter ct.2.1: qualify_local_types on class-method channel + Forall constraints recursion"
+```
+
+---
+
+## Task 2: Pattern::Ctor type-driven lookup; delete imports-fallback
+
+Post-ct.1, every `Pattern::Ctor`'s scrutinee has a canonical
+`Type::Con.name` (bare = local TypeDef, qualified = explicit
+cross-module). The current lookup at `lib.rs:2488-2523` first
+consults `env.ctor_index` (a per-module local map, populated by
+`check_in_workspace`'s overlay at `lib.rs:1257-1284`), then falls
+back to scanning `env.module_types` for any imported module whose
+type defs contain a ctor by this name.
+
+The fallback is the iter 15a imports-fallback. It is now
+unreachable in well-formed inputs: a bare-local pattern ctor is
+matched against a bare-local TypeDef (and `env.ctor_index` has the
+local hit); a cross-module pattern ctor is matched against a
+qualified TypeDef. There is no third case.
+
+The cleanest replacement is type-driven: derive the TypeDef from
+`expected` (the scrutinee type) and look up the ctor by name within
+that TypeDef. This sidesteps `env.ctor_index` entirely for the
+Pattern::Ctor path (the index remains for other uses, including
+duplicate-ctor detection at workspace build).
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs:2450-2585` (the
+ `Pattern::Ctor` arm of `type_check_pattern`).
+- Modify: `crates/ailang-check/src/lib.rs` `mod tests`:
+ - Rename `cross_module_pat_ctor_fallback_resolves` →
+ `cross_module_pat_ctor_typedriven_resolves`; update docstring.
+ - Delete `cross_module_pat_ctor_ambiguous_errors` (ambiguity no
+ longer arises — the lookup is anchored to a single TypeDef).
+- Modify: `crates/ail/tests/mono_xmod_ctor_pattern.rs` (docstring
+ only — body still passes because the scrutinee is qualified).
+
+- [ ] **Step 1: Write the RED test for the new type-driven lookup**
+
+Append to `crates/ailang-check/src/lib.rs` `mod tests`:
+
+```rust
+/// ct.2 Task 2: a `Pattern::Ctor` against a scrutinee of type
+/// `Type::Con { name: "p.T", .. }` looks up the TypeDef in
+/// `env.module_types["p"]["T"]` and finds the ctor by name within
+/// it — no `env.ctor_index` consult, no imports-walk. This pins the
+/// new lookup strategy.
+#[test]
+fn ct2_pattern_ctor_type_driven_lookup_cross_module() {
+ let lib = Module {
+ schema: SCHEMA.into(),
+ name: "lib".into(),
+ imports: vec![],
+ defs: vec![Def::Type(TypeDef {
+ name: "Box".into(),
+ vars: vec!["a".into()],
+ ctors: vec![Ctor {
+ name: "MkBox".into(),
+ fields: vec![Type::Var { name: "a".into() }],
+ }],
+ doc: None,
+ drop_iterative: false,
+ })],
+ };
+ let consumer = Module {
+ schema: SCHEMA.into(),
+ name: "use_lib".into(),
+ imports: vec![Import { module: "lib".into(), alias: None }],
+ defs: vec![fn_def(
+ "open",
+ Type::Fn {
+ params: vec![Type::Con {
+ name: "lib.Box".into(),
+ args: vec![Type::int()],
+ }],
+ ret: Box::new(Type::int()),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ },
+ vec!["b"],
+ Term::Match {
+ scrutinee: Box::new(Term::Var { name: "b".into() }),
+ arms: vec![Arm {
+ pat: Pattern::Ctor {
+ ctor: "MkBox".into(),
+ fields: vec![Pattern::Var { name: "x".into() }],
+ },
+ body: Term::Var { name: "x".into() },
+ }],
+ },
+ )],
+ };
+ let mut modules = BTreeMap::new();
+ modules.insert("lib".into(), lib);
+ modules.insert("use_lib".into(), consumer);
+ let ws = Workspace {
+ entry: "use_lib".into(),
+ modules,
+ root_dir: std::path::PathBuf::from("."),
+ registry: ailang_core::workspace::Registry::default(),
+ };
+ let diags = check_workspace(&ws);
+ assert!(diags.is_empty(), "expected green; got {diags:?}");
+}
+
+/// ct.2 Task 2: when the scrutinee carries a Type::Con name that
+/// doesn't resolve to any TypeDef (workspace-wide), the pattern
+/// lookup must fail closed. The post-ct.1 validator catches this
+/// shape earlier for canonical inputs; this test pins the residual
+/// runtime guard against constructed (non-loaded) AST.
+#[test]
+fn ct2_pattern_ctor_fails_closed_when_scrutinee_type_unknown() {
+ let consumer = Module {
+ schema: SCHEMA.into(),
+ name: "u".into(),
+ imports: vec![],
+ defs: vec![fn_def(
+ "f",
+ Type::Fn {
+ params: vec![Type::Con {
+ name: "Nonexistent".into(),
+ args: vec![],
+ }],
+ ret: Box::new(Type::int()),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ },
+ vec!["x"],
+ Term::Match {
+ scrutinee: Box::new(Term::Var { name: "x".into() }),
+ arms: vec![Arm {
+ pat: Pattern::Ctor {
+ ctor: "Whatever".into(),
+ fields: vec![],
+ },
+ body: Term::Lit { lit: Literal::Int { value: 0 } },
+ }],
+ },
+ )],
+ };
+ let mut modules = BTreeMap::new();
+ modules.insert("u".into(), consumer);
+ let ws = Workspace {
+ entry: "u".into(),
+ modules,
+ root_dir: std::path::PathBuf::from("."),
+ registry: ailang_core::workspace::Registry::default(),
+ };
+ let diags = check_workspace(&ws);
+ assert!(
+ !diags.is_empty(),
+ "expected at least one diagnostic for unknown scrutinee \
+ type, got none"
+ );
+}
+```
+
+- [ ] **Step 2: Run the new tests to verify they pass with current behaviour**
+
+Run: `cargo test --workspace -p ailang-check ct2_pattern_ctor_type_driven_lookup_cross_module ct2_pattern_ctor_fails_closed_when_scrutinee_type_unknown`
+
+Expected: BOTH PASS (the first via the current imports-fallback,
+the second via the current `expected: Type::Con` shape check).
+This is the GREEN-now-pin-then-refactor pattern — the tests are
+invariants that must hold AFTER the refactor too.
+
+- [ ] **Step 3: Replace the Pattern::Ctor lookup body**
+
+Edit `crates/ailang-check/src/lib.rs:2485-2523`. Replace the lines
+that resolve `resolved_type_name`, `resolved_td`, and
+`resolved_owning_module` (the `if let Some(cref) = env.ctor_index
+.get(ctor) ... else { ... hits ... match hits.len() { ... } }`
+block) with a single type-driven lookup:
+
+```rust
+ // ct.2 Task 2: Pattern::Ctor lookup is type-driven post-ct.1.
+ // The scrutinee's Type::Con name is canonical (bare = local
+ // TypeDef, qualified = explicit cross-module). Derive the
+ // TypeDef from `expected` and find the ctor by name within
+ // it; no env.ctor_index consult, no imports-walk.
+ let (resolved_type_name, resolved_td, resolved_owning_module) =
+ match expected {
+ Type::Con { name, args: _ } => {
+ if let Some((owner, suffix)) = name.split_once('.') {
+ let td = env
+ .module_types
+ .get(owner)
+ .and_then(|tys| tys.get(suffix))
+ .cloned()
+ .ok_or_else(|| {
+ CheckError::PatternTypeMismatch {
+ ctor: ctor.clone(),
+ ty: ailang_core::pretty::type_to_string(expected),
+ }
+ })?;
+ (name.clone(), td, Some(owner.to_string()))
+ } else {
+ let td = env.types.get(name).cloned().ok_or_else(|| {
+ CheckError::PatternTypeMismatch {
+ ctor: ctor.clone(),
+ ty: ailang_core::pretty::type_to_string(expected),
+ }
+ })?;
+ (name.clone(), td, None)
+ }
+ }
+ _ => {
+ return Err(CheckError::PatternTypeMismatch {
+ ctor: ctor.clone(),
+ ty: ailang_core::pretty::type_to_string(expected),
+ });
+ }
+ };
+ // Validate the ctor exists in the resolved TypeDef.
+ if !resolved_td.ctors.iter().any(|c| &c.name == ctor) {
+ return Err(CheckError::UnknownCtorInPattern(ctor.clone()));
+ }
+```
+
+The subsequent code (the `scrutinee_args` extraction, the
+`cdef`/`qualified_fields` logic) stays as is — it already consumes
+`resolved_type_name`, `resolved_td`, `resolved_owning_module`. The
+only structural change is replacing the resolution prologue; the
+binding logic is unchanged.
+
+The previously needed `scrutinee_args` re-extraction (lines
+2527-2535) becomes a redundant double-check on `expected`; collapse
+it into a direct extraction from the resolved Type::Con form. Edit
+those lines to:
+
+```rust
+ // expected is already validated as Type::Con above.
+ let scrutinee_args: Vec = match expected {
+ Type::Con { args, .. } => args.clone(),
+ _ => unreachable!("matched above"),
+ };
+```
+
+- [ ] **Step 4: Retarget the legacy iter 15a path 3 test**
+
+Edit `crates/ailang-check/src/lib.rs` test at line ~3582-3619.
+Rename `cross_module_pat_ctor_fallback_resolves` to
+`cross_module_pat_ctor_typedriven_resolves` and update the
+docstring:
+
+```rust
+ /// Iter 15a (post-ct.2): a bare `Pattern::Ctor` (e.g. `MkBox x`)
+ /// against a scrutinee of type `lib.Box` resolves through
+ /// the type-driven lookup keyed on `expected.name`. Previously
+ /// this exercised an imports-fallback; post-ct.2 the lookup is
+ /// anchored to the scrutinee's qualified TypeDef directly.
+ #[test]
+ fn cross_module_pat_ctor_typedriven_resolves() {
+```
+
+Body unchanged — the test still passes because the scrutinee type
+is `lib.Box` (qualified), the new lookup finds
+`env.module_types["lib"]["Box"]`, and `MkBox` exists inside it.
+
+- [ ] **Step 5: Delete the ambiguity test**
+
+Edit `crates/ailang-check/src/lib.rs` at line ~3621-3699 — delete
+the `cross_module_pat_ctor_ambiguous_errors` test entirely. The
+ambiguity it exercised (bare `Mk` matching two imports) is
+structurally impossible post-ct.2: the lookup is anchored to the
+scrutinee's single TypeDef, which uniquely determines the ctor by
+name within it. The `CheckError::AmbiguousCtor` variant may remain
+dead-but-defensive (do not delete the variant in this iter — it is
+left to a later tidy).
+
+- [ ] **Step 6: Refresh the mono_xmod_ctor_pattern docstring**
+
+Edit `crates/ail/tests/mono_xmod_ctor_pattern.rs` lines 1-52 (the
+module-level docstring). Replace the body of the doc-block (keeping
+the same `//!` prefix style) with:
+
+```rust
+//! Regression: the workspace-monomorphisation pass must not mis-resolve
+//! a cross-module constructor pattern. The mono pass re-runs `synth` on
+//! every fn body to recover residual class constraints; that env is built
+//! by `mono::build_workspace_env`, which delegates to `crate::build_check_env`
+//! and produces a workspace-flat `ctor_index` and `types` map.
+//!
+//! Post-ct.2, `Pattern::Ctor` lookup is type-driven — it consults the
+//! scrutinee's canonical `Type::Con.name` to find the TypeDef directly
+//! in `env.module_types`, then validates the ctor name within it. The
+//! mono pass's flat `ctor_index` is no longer consulted by this path;
+//! the per-module overlay (lib.rs:1247-1258) is now decorative for the
+//! pattern path and remains only for duplicate-type / duplicate-ctor
+//! detection at the workspace-build prologue.
+//!
+//! This test pins the cross-module pattern shape against a minimal
+//! 2-module fixture (`test_mono_ctor_main` + `test_mono_ctor_listmod`).
+//! Pre-ct.2 the bug surfaced as `PatternTypeMismatch { ctor: "Cons",
+//! ty: "test_mono_ctor_listmod.List" }` because the mono env
+//! resolved `Cons` to bare `List` via the flat index. Post-ct.2 the
+//! lookup is type-driven and `expected.name == "test_mono_ctor_listmod.List"`
+//! directly indexes the right TypeDef.
+//!
+//! Surfaced by iter 23.2 Task 3, which adds `class Eq a` + Eq Int/Bool/Str
+//! instances to `examples/prelude.ail.json`, flipping the
+//! `workspace_has_typeclasses` gate so every workspace exercises the
+//! mono pass.
+```
+
+- [ ] **Step 7: Run the full workspace test suite**
+
+Run: `cargo test --workspace`
+
+Expected: all pass. The deleted `cross_module_pat_ctor_ambiguous_errors`
+reduces the test count by 1; the renamed test continues to pass;
+`mono_pass_handles_xmod_ctor_pattern` continues to pass with the
+refreshed docstring.
+
+- [ ] **Step 8: Commit**
+
+```bash
+git add crates/ailang-check/src/lib.rs crates/ail/tests/mono_xmod_ctor_pattern.rs
+git commit -m "iter ct.2.2: Pattern::Ctor type-driven lookup; delete imports-fallback"
+```
+
+---
+
+## Task 3: Term::Ctor synth direct lookup; delete imports-fallback
+
+Post-ct.1, every `Term::Ctor.type_name` is canonical. The current
+synth path at `lib.rs:1964-2028` has three branches:
+
+1. Qualified `module.Type`: resolves via `env.imports.get(prefix)` and
+ `env.module_types.get(target_module).and_then(|tys| tys.get(suffix))`.
+2. Local hit: `env.types.get(type_name)`.
+3. Bare imports-fallback (iter 23.1.3): scan `env.imports.values()`
+ for a module whose `module_types` contains the bare name; pick
+ single hit, error on zero or multiple.
+
+Post-ct.1, branch 3 is unreachable: a bare `type_name` in canonical
+form means *local to this module*, which is branch 2. The validator
+catches the legacy bare-cross-module shape at load time. The
+imports-fallback's only remaining role is as a defensive guard
+against ill-formed AST constructed in tests — which is not a
+defensible reason to keep it (per spec acceptance criterion 3 and
+the project's "no defensive guards against canonical-form
+violations" stance).
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs:1943-2087` (the
+ `Term::Ctor` arm of `synth`).
+- Modify: `crates/ailang-check/src/lib.rs` `mod tests`:
+ - Delete `cross_module_term_ctor_ambiguous_type_errors`
+ (ambiguity unreachable post-ct.2).
+ - Delete `user_module_can_pattern_match_on_prelude_ordering_bare`
+ (its invariant — bare cross-module `type_name` works through
+ imports-fallback — is exactly what we are removing).
+ - Add `ct2_term_ctor_bare_cross_module_fails_closed` pinning the
+ new behaviour.
+
+- [ ] **Step 1: Write the RED test for the new fail-closed behaviour**
+
+Append to `crates/ailang-check/src/lib.rs` `mod tests`:
+
+```rust
+/// ct.2 Task 3: a bare `Term::Ctor.type_name` that does not resolve
+/// to a local TypeDef must error with `UnknownType` (or
+/// `UnknownCtor`, depending on which check fires first). The
+/// imports-fallback that previously synthesised a qualified result
+/// from an arbitrary imported module is gone. The
+/// post-ct.1 validator catches this shape at load time for
+/// canonical inputs; this test pins the residual runtime guard
+/// against constructed (non-loaded) AST.
+#[test]
+fn ct2_term_ctor_bare_cross_module_fails_closed() {
+ let prelude = Module {
+ schema: SCHEMA.into(),
+ name: "p".into(),
+ imports: vec![],
+ defs: vec![Def::Type(TypeDef {
+ name: "Ordering".into(),
+ vars: vec![],
+ ctors: vec![
+ Ctor { name: "LT".into(), fields: vec![] },
+ Ctor { name: "EQ".into(), fields: vec![] },
+ Ctor { name: "GT".into(), fields: vec![] },
+ ],
+ doc: None,
+ drop_iterative: false,
+ })],
+ };
+ // Consumer imports prelude but writes BARE `Ordering` in
+ // Term::Ctor — this is a stale-canonical-form construction.
+ let consumer = Module {
+ schema: SCHEMA.into(),
+ name: "u".into(),
+ imports: vec![Import { module: "p".into(), alias: None }],
+ defs: vec![fn_def(
+ "stale",
+ Type::Fn {
+ params: vec![],
+ ret: Box::new(Type::Con {
+ name: "p.Ordering".into(),
+ args: vec![],
+ }),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ },
+ vec![],
+ Term::Ctor {
+ type_name: "Ordering".into(),
+ ctor: "LT".into(),
+ args: vec![],
+ },
+ )],
+ };
+ let mut modules = BTreeMap::new();
+ modules.insert("p".into(), prelude);
+ modules.insert("u".into(), consumer);
+ let ws = Workspace {
+ entry: "u".into(),
+ modules,
+ root_dir: std::path::PathBuf::from("."),
+ registry: ailang_core::workspace::Registry::default(),
+ };
+ let diags = check_workspace(&ws);
+ assert!(
+ diags.iter().any(|d| d.code == "unknown-type"),
+ "expected unknown-type diagnostic for bare cross-module \
+ Term::Ctor; got {diags:?}"
+ );
+}
+
+/// ct.2 Task 3: a qualified `Term::Ctor.type_name`
+/// (`p.Ordering` / `LT`) continues to resolve cleanly through the
+/// qualified branch. This is the canonical form post-ct.1 and the
+/// hot path for every Term::Ctor in a migrated fixture.
+#[test]
+fn ct2_term_ctor_qualified_cross_module_resolves() {
+ let prelude = Module {
+ schema: SCHEMA.into(),
+ name: "p".into(),
+ imports: vec![],
+ defs: vec![Def::Type(TypeDef {
+ name: "Ordering".into(),
+ vars: vec![],
+ ctors: vec![
+ Ctor { name: "LT".into(), fields: vec![] },
+ Ctor { name: "EQ".into(), fields: vec![] },
+ Ctor { name: "GT".into(), fields: vec![] },
+ ],
+ doc: None,
+ drop_iterative: false,
+ })],
+ };
+ let consumer = Module {
+ schema: SCHEMA.into(),
+ name: "u".into(),
+ imports: vec![Import { module: "p".into(), alias: None }],
+ defs: vec![fn_def(
+ "lt",
+ Type::Fn {
+ params: vec![],
+ ret: Box::new(Type::Con {
+ name: "p.Ordering".into(),
+ args: vec![],
+ }),
+ effects: vec![],
+ param_modes: vec![],
+ ret_mode: ParamMode::Implicit,
+ },
+ vec![],
+ Term::Ctor {
+ type_name: "p.Ordering".into(),
+ ctor: "LT".into(),
+ args: vec![],
+ },
+ )],
+ };
+ let mut modules = BTreeMap::new();
+ modules.insert("p".into(), prelude);
+ modules.insert("u".into(), consumer);
+ let ws = Workspace {
+ entry: "u".into(),
+ modules,
+ root_dir: std::path::PathBuf::from("."),
+ registry: ailang_core::workspace::Registry::default(),
+ };
+ let diags = check_workspace(&ws);
+ assert!(diags.is_empty(), "expected green; got {diags:?}");
+}
+```
+
+- [ ] **Step 2: Run the new tests to verify state**
+
+Run: `cargo test --workspace -p ailang-check ct2_term_ctor_bare_cross_module_fails_closed ct2_term_ctor_qualified_cross_module_resolves`
+
+Expected:
+- `ct2_term_ctor_qualified_cross_module_resolves`: PASS (qualified
+ branch already exists).
+- `ct2_term_ctor_bare_cross_module_fails_closed`: FAIL — the
+ current imports-fallback resolves `Ordering` to `p.Ordering`
+ and the ret-type unifies, so no diagnostic fires.
+
+- [ ] **Step 3: Apply the production fix — delete the imports-fallback else-branch**
+
+Edit `crates/ailang-check/src/lib.rs:1962-2028`. Replace the
+entire `let td = if ... else if let Some(td) = env.types.get(type_name) ... else { ... }`
+chain with a two-branch form (qualified or local; no imports
+fallback). The simplified form:
+
+```rust
+ // ct.2 Task 3: Term::Ctor lookup is direct post-ct.1.
+ // Canonical type_name: bare = local TypeDef, qualified =
+ // explicit cross-module. The imports-fallback (iter
+ // 23.1.3) is gone — bare cross-module refs are rejected
+ // upstream by the workspace validator (ct.1).
+ let owning_module: Option;
+ let result_type_name: String = type_name.clone();
+ let td = if type_name.matches('.').count() == 1 {
+ let (prefix, suffix) = type_name.split_once('.').expect("checked");
+ let target_module = match env.imports.get(prefix) {
+ Some(m) => m.clone(),
+ None => {
+ return Err(CheckError::UnknownModule {
+ module: prefix.to_string(),
+ });
+ }
+ };
+ let td = env.module_types
+ .get(&target_module)
+ .and_then(|tys| tys.get(suffix))
+ .cloned()
+ .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
+ owning_module = Some(target_module);
+ td
+ } else if let Some(td) = env.types.get(type_name) {
+ owning_module = None;
+ td.clone()
+ } else {
+ return Err(CheckError::UnknownType(type_name.clone()));
+ };
+```
+
+(The change: the third `else { let mut hits: Vec<...> ...; match
+hits.len() { ... } }` branch is replaced by a single
+`return Err(CheckError::UnknownType(type_name.clone()))`. The
+`result_type_name` variable, previously mutable to allow the
+fallback to upgrade it to a qualified form, becomes a plain `let`
+since it is never rewritten now.)
+
+The subsequent code (cdef lookup, qualified_fields, mapping,
+type_args construction) stays as is.
+
+- [ ] **Step 4: Run the new tests to verify the bare path now fails closed**
+
+Run: `cargo test --workspace -p ailang-check ct2_term_ctor_bare_cross_module_fails_closed ct2_term_ctor_qualified_cross_module_resolves`
+
+Expected: BOTH PASS.
+
+- [ ] **Step 5: Delete the legacy iter 23.1 imports-fallback tests**
+
+Edit `crates/ailang-check/src/lib.rs`:
+- Delete `cross_module_term_ctor_ambiguous_type_errors` (line
+ range ~3805-3885). The ambiguity it exercises (bare `T`
+ matching two imports → `ambiguous-type`) is structurally
+ unreachable; the bare path is fail-closed with
+ `unknown-type` directly.
+- Delete `user_module_can_pattern_match_on_prelude_ordering_bare`
+ (line range ~3887-3970). Its invariant — bare `type_name:
+ "Ordering"` in a user module typechecks cleanly through the
+ imports-fallback — is the exact behaviour ct.2 removes.
+
+The `CheckError::AmbiguousType` enum variant remains
+dead-but-defensive in this iter (a later tidy can remove it).
+
+- [ ] **Step 6: Run the full workspace test suite**
+
+Run: `cargo test --workspace`
+
+Expected: all pass. Two tests deleted, two added; net -0 from
+ct.2.3's lens. End-to-end pipeline (examples/ workspace,
+prose round-trips, IR snapshots) unaffected because every migrated
+fixture carries qualified `Term::Ctor.type_name` post-ct.1.
+
+- [ ] **Step 7: Commit**
+
+```bash
+git add crates/ailang-check/src/lib.rs
+git commit -m "iter ct.2.3: Term::Ctor synth direct lookup; delete imports-fallback"
+```
+
+---
+
+## Closing checks
+
+After all three tasks land:
+
+- [ ] **Step C1: Bench-script smoke run**
+
+Run: `bash bench/run.sh` (no comparison vs baseline — just a
+smoke that the binary still produces).
+
+Expected: exit 0 (or whatever the audit-bench-exit-code policy
+allows — see `skills/audit/SKILL.md`).
+
+- [ ] **Step C2: Confirm the four obsolete mechanisms catalogue**
+
+After ct.2 closes, two of the four mechanisms named in
+`docs/specs/2026-05-10-canonical-type-names.md` ct.1 JOURNAL
+entry are gone:
+- ✅ `Pattern::Ctor` imports-fallback (was lib.rs:2486-2521).
+- ✅ `Term::Ctor` synth imports-fallback (was lib.rs:1979-2025).
+- ⏳ `lookup_ctor_by_type` codegen imports-fallback — ct.3.
+- ⏳ `apply_per_module_ctor_index_overlay` in mono — ct.3.
+
+No action required in this iter — just a checkpoint for the JOURNAL
+entry below.
+
+- [ ] **Step C3: JOURNAL entry**
+
+Append to `docs/JOURNAL.md`:
+
+```markdown
+## 2026-05-11 — Iteration ct.2: typechecker cleanup
+
+Three tasks landed in the canonical-type-names milestone's
+typechecker-cleanup iteration:
+
+- **ct.2.1**: wired `qualify_local_types` into the
+ `env.class_methods` channel of `Term::Var` resolution, closing
+ the last cross-module fn-lookup boundary that did not run the
+ qualifier. Also fixed a latent gap in
+ `qualify_local_types`'s `Type::Forall` arm: it now recurses into
+ `constraints[].type_`, symmetric to the ct.1.5a-followup fix on
+ `normalize_type_for_registry`. This is the actionable side of
+ the spec's "audit `qualify_local_types` for uniform application
+ at all cross-module fn-lookup sites" — only one site was
+ missing.
+- **ct.2.2**: deleted the `Pattern::Ctor` imports-fallback (iter
+ 15a); replaced with type-driven lookup keyed on
+ `expected: Type::Con`'s canonical name. The
+ `cross_module_pat_ctor_ambiguous_errors` test deleted (ambiguity
+ unreachable post-refactor; lookup is anchored to a single
+ TypeDef). The `mono_xmod_ctor_pattern.rs` regression test still
+ passes — its scrutinee carries the qualified type and the new
+ lookup finds the TypeDef directly.
+- **ct.2.3**: deleted the `Term::Ctor` synth imports-fallback
+ (iter 23.1.3). Bare cross-module `type_name` now fails closed
+ with `UnknownType`; the post-ct.1 workspace validator catches
+ the shape at load time for canonical inputs.
+
+Remaining obsolete mechanisms (ct.3 scope): the codegen
+`lookup_ctor_by_type` imports-fallback (iter 23.1.4) and the mono
+`apply_per_module_ctor_index_overlay` (iter 23.2 fix `84dcc46`).
+
+`cargo test --workspace` green at iteration close. Three tests
+added (one per task's invariant), three tests deleted (the iter
+15a path 4 ambiguity test, the iter 23.1 ambiguous-type test, the
+iter 23.1 bare-prelude-Ordering test); net zero in test count
+across deletes and additions.
+```
+
+- [ ] **Step C4: Commit the JOURNAL entry**
+
+```bash
+git add docs/JOURNAL.md
+git commit -m "journal: ct.2 typechecker cleanup"
+```