AILang/docs/plans/0026-ct.2-typechecker-cleanup.md

Iteration ct.2: Typechecker Cleanup — Implementation Plan

Parent spec: docs/specs/0007-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<a>. 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):

/// 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:

/// ct.2 Task 1: `qualify_local_types`'s `Type::Forall` arm must
/// recurse into `constraints[].type_`. A class method whose
/// declared type is `Forall<a>{Ord a}. Fn[..]` carries the
/// constraint type `Type::Var { name: "a" }` — fine — but a
/// hypothetical `Forall<a>{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<String, ailang_core::ast::TypeDef> = 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:

            } 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<String, Type> = 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:

        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

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:

/// 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:

            // 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:

            // expected is already validated as Type::Con above.
            let scrutinee_args: Vec<Type> = 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:

    /// Iter 15a (post-ct.2): a bare `Pattern::Ctor` (e.g. `MkBox x`)
    /// against a scrutinee of type `lib.Box<Int>` 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<Int> (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:

//! 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<Int>" }` 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

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:

/// 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:

            // 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<String>;
            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

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/0007-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:

## 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

git add docs/JOURNAL.md
git commit -m "journal: ct.2 typechecker cleanup"