AILang/crates/ailang-core/src/workspace.rs

//! Workspace loader: loads an entry module and recursively follows its
//! `imports`.
//!
//! Convention: an `import { module: "foo" }` is resolved relative to
//! the entry file's directory as `<root_dir>/foo.ail.json`. Module
//! names must match the file stem (the loader rejects mismatches).
//!
//! The single entry point is [`load_workspace`]; it returns a fully
//! populated [`Workspace`] or a structured [`WorkspaceLoadError`].
//! [`module_hash`] is the module-granularity counterpart to
//! [`crate::def_hash`] and is used both internally (to detect a module
//! re-loaded from disk with different content) and by the CLI.
//!
//! This module is responsible only for **finding** and consistently
//! **loading** all reachable modules. Cross-module typechecking lives
//! in `ailang-check`; codegen in `ailang-codegen`. Neither is run from
//! here.
//!
//! # Examples
//!
//! ```ignore
//! use ailang_core::load_workspace;
//! use std::path::Path;
//!
//! let ws = load_workspace(Path::new("examples/ws_main.ail.json"))?;
//! assert_eq!(ws.entry, "ws_main");
//! // All transitively imported modules are now in `ws.modules`.
//! for (name, m) in &ws.modules {
//!     println!("{name}: {} defs", m.defs.len());
//! }
//! # Ok::<(), ailang_core::workspace::WorkspaceLoadError>(())
//! ```

use crate::ast::{ClassDef, Def, InstanceDef, Module, Term, Type};
use crate::canonical;
use crate::{load_module, Error as CoreError};
use std::collections::{BTreeMap, BTreeSet, HashSet};
use std::path::{Path, PathBuf};

/// Fully loaded workspace.
///
/// `entry` names the entry module (module name, **not** a path). All
/// transitively reachable modules are contained in `modules` and indexed
/// by `Module.name`. `root_dir` is the directory the entry file lives
/// in; all imports are resolved relative to it.
///
/// Iter 22b.1 (Decision 11): `registry` is the workspace-global
/// instance registry, built at the end of [`load_workspace`] after the
/// DFS over imports completes. It is empty for any workspace whose
/// modules contain no [`crate::ast::Def::Instance`] defs.
#[derive(Debug, Clone)]
pub struct Workspace {
    /// Name of the entry module (the one passed to [`load_workspace`]).
    pub entry: String,
    /// Every module reachable from `entry`, indexed by module name.
    /// `BTreeMap` is used so iteration order is deterministic, which
    /// matters for downstream codegen and reporting.
    pub modules: BTreeMap<String, Module>,
    /// Directory the entry file lives in; all imports are resolved
    /// relative to it.
    pub root_dir: PathBuf,
    /// Iter 22b.1: workspace-global typeclass instance registry.
    pub registry: Registry,
}

/// Iter 22b.1: workspace-global instance registry (Decision 11).
///
/// Built at the end of [`load_workspace`] after all modules are
/// loaded. Keyed by `(class-name, canonical-type-hash)`; values are
/// the matching [`crate::ast::InstanceDef`] plus the name of the
/// module it was declared in. The hash key uses
/// [`canonical::type_hash`], so the key is stable against unrelated
/// whitespace / field-order differences in the source JSON.
///
/// 22b.1 enforces three coherence checks during build:
///
/// 1. **Coherence (orphan-freedom).** Every `instance C T` lives in
///    the module of `C` or in the module of `T` (per Decision 11
///    axis 3). Otherwise → [`WorkspaceLoadError::OrphanInstance`].
/// 2. **Uniqueness.** No two entries share a key. Otherwise →
///    [`WorkspaceLoadError::DuplicateInstance`].
/// 3. **Method completeness.** Each instance specifies a body for
///    every required (non-default) method of its class. Otherwise →
///    [`WorkspaceLoadError::MissingMethod`].
#[derive(Debug, Clone, Default)]
pub struct Registry {
    /// Map from `(class-name, type-hash)` to the registry entry.
    pub entries: BTreeMap<(String, String), RegistryEntry>,
    /// ct.1.5a: workspace-wide map from user-defined type-name to its
    /// defining module. Used by [`Self::normalize_type_for_lookup`] to
    /// rewrite a bare `Type::Con.name` to its always-qualified form
    /// before computing the registry key. Primitives are not present.
    /// Populated in [`build_registry`] from the same scan that builds
    /// the entry map.
    ///
    /// Note: keyed by bare type name only. If two modules each define a
    /// type with the same bare name (e.g. `type Foo` in both `M` and
    /// `N`), the second `insert` overwrites the first, and
    /// [`Self::normalize_type_for_lookup`] would collapse `M.Foo` and
    /// `N.Foo` to whichever module wins the race. Acceptable for the
    /// current corpus (all in-tree fixtures use distinct bare type
    /// names across modules); revisit if a future workspace breaks the
    /// assumption. Proper fix is to re-key as
    /// `(owning_module, bare_name) -> defining_module` and thread the
    /// calling module through every consumer site — out of ct.1's scope.
    pub type_def_module: BTreeMap<String, String>,
}

impl Registry {
    /// ct.1.5a: produce the canonical form of `t` for registry-key
    /// hashing. Bare-non-primitive `Type::Con` names get qualified to
    /// `<defining_module>.<name>`; already-qualified names stay; bare
    /// names whose defining module is unknown stay as-is.
    /// `Type::Fn`/`Type::Forall`/`Type::Var` recurse / pass through
    /// structurally.
    ///
    /// Every consumer that hashes an `inst.type_`-shaped expression to
    /// look it up in [`Self::entries`] must funnel through this
    /// helper, otherwise the registered-form and the queried-form
    /// disagree on whether the leading qualifier is present.
    pub fn normalize_type_for_lookup(&self, t: &Type) -> Type {
        normalize_type_for_registry(t, &self.type_def_module)
    }
}

/// One entry in the [`Registry`].
#[derive(Debug, Clone)]
pub struct RegistryEntry {
    /// The instance declaration itself.
    pub instance: InstanceDef,
    /// Name of the module the instance was declared in.
    pub defining_module: String,
}

/// Structured errors of the workspace loader.
///
/// `Cycle.path` is the chain of module names in which the cycle was
/// closed — the last element is the name already present in `visiting`.
#[derive(Debug, thiserror::Error)]
pub enum WorkspaceLoadError {
    /// File I/O failed while reading a module file (typically: file
    /// missing, permission denied).
    #[error("io error for {path}: {source}")]
    Io {
        path: PathBuf,
        #[source]
        source: std::io::Error,
    },

    /// File contents failed to parse as a [`Module`] or had the wrong
    /// schema tag. Wraps a [`CoreError`] (the single-module loader's
    /// error type).
    #[error("schema/parse error in {path}: {source}")]
    Schema {
        path: PathBuf,
        #[source]
        source: CoreError,
    },

    /// An `import { module: "foo" }` did not resolve to an existing
    /// file at the expected path.
    #[error("module `{name}` not found (expected at {expected_path})")]
    ModuleNotFound { name: String, expected_path: PathBuf },

    /// The `name` field in a loaded module file disagrees with the
    /// file-stem-derived name the loader expected (i.e. the
    /// `<name>.ail.json` convention is broken).
    #[error(
        "module name in file ({name_in_file:?}) does not match expected name from path ({name_from_path:?})"
    )]
    ModuleNameMismatch {
        name_in_file: String,
        name_from_path: String,
    },

    /// An import cycle was detected. `path` is the chain of module
    /// names in which the cycle was closed — the last element is the
    /// name that was already on the visit stack.
    #[error("import cycle detected: {}", path.join(" -> "))]
    Cycle { path: Vec<String> },

    /// A module was reachable through two import paths, and its
    /// on-disk content (compared via [`module_hash`]) differs between
    /// the two reads. This typically means the file changed mid-load.
    #[error(
        "module `{name}` was loaded twice with differing content (hashes differ)"
    )]
    ModuleHashMismatch { name: String },

    /// Iter 22b.1: an [`crate::ast::Def::Instance`] was declared in a
    /// module that is neither the class's defining module nor the
    /// instance type's defining module. Coherence violation per
    /// Decision 11 axis 3 ("orphan-freedom"). The lookup is hard:
    /// AILang does not provide a `--allow-orphans` flag.
    #[error(
        "orphan instance: `instance {class} {type_repr}` declared in module `{defining_module}`, \
        but neither `{class}` (in `{class_module}`) nor `{type_repr}` (in `{type_module}`) lives there"
    )]
    OrphanInstance {
        class: String,
        type_repr: String,
        defining_module: String,
        class_module: String,
        type_module: String,
    },

    /// Iter 22b.1: two [`crate::ast::Def::Instance`]s share the same
    /// `(class, canonical-type-hash)` key. Coherence requires
    /// uniqueness; the registry has no way to disambiguate at
    /// resolution time. Per Decision 11 there is no
    /// `AmbiguousInstance` diagnostic — coherence makes the lookup
    /// unambiguous by construction, and a duplicate is a workspace
    /// configuration error, not a per-call-site one.
    #[error(
        "duplicate instance: `instance {class} {type_repr}` declared in both `{first_module}` and `{second_module}`"
    )]
    DuplicateInstance {
        class: String,
        type_repr: String,
        first_module: String,
        second_module: String,
    },

    /// Iter 22b.1: an [`crate::ast::Def::Instance`] does not specify
    /// a body for a required (non-default) method of its class.
    /// Default-bearing methods may be inherited; non-default
    /// (abstract-required) methods must be specified by every
    /// instance. Per Decision 11 §"Defaults and superclasses".
    #[error(
        "instance `{class} {type_repr}` is missing a body for method `{method}` (no default)"
    )]
    MissingMethod {
        class: String,
        type_repr: String,
        method: String,
    },

    /// Iter 22b.2: class-schema validation. The class parameter
    /// appears in applied position (e.g. as the head of a
    /// `Type::Con { name == param, args.len() > 0 }`) inside a method
    /// signature. Decision 11 axis 5 forbids HKTs — class params are
    /// kind `*` only.
    #[error(
        "kind mismatch in class `{class}`: parameter `{param}` is used in applied position \
        inside method `{method}` (Decision 11 axis 5: class params are kind `*` only)"
    )]
    KindMismatch {
        class: String,
        param: String,
        method: String,
        defining_module: String,
    },

    /// Iter 22b.2: class-schema validation. A class's `superclass.type`
    /// does not equal its own `param`. Decision 11 single-superclass
    /// model requires the superclass to be applied to the same param
    /// (e.g. `class Ord a extends Eq a`, not `extends Eq b`).
    #[error(
        "class `{class}` declares superclass `{superclass} {got_type}`, but its own parameter is `{expected_param}` \
        — superclass `type` must equal class `param`"
    )]
    InvalidSuperclassParam {
        class: String,
        superclass: String,
        expected_param: String,
        got_type: String,
    },

    /// Iter 22b.2: class-schema validation. A class method's
    /// signature contains a constraint referencing a type variable
    /// that is neither bound by the method's `Forall.vars` nor equal
    /// to the class's `param`.
    #[error(
        "in class `{class}` method `{method}`: constraint `{constraint_class} {var}` references unbound type variable `{var}`"
    )]
    UnboundConstraintTypeVar {
        class: String,
        method: String,
        constraint_class: String,
        var: String,
    },

    /// Iter 22b.2: an instance specifies a body for a method name
    /// that the corresponding class does not declare. Symmetric to
    /// `MissingMethod` but in the opposite direction.
    #[error(
        "instance `{class} {type_repr}` provides body for method `{method}`, but class `{class}` does not declare it"
    )]
    OverridingNonExistentMethod {
        class: String,
        type_repr: String,
        method: String,
    },

    /// Iter 22b.2: a class-method name collides with another
    /// class-method or with a top-level fn. `kind` is
    /// `"class-class"` or `"class-fn"`.
    #[error(
        "method name `{method}` collides ({kind}): defined in `{first_origin}` and `{second_origin}`"
    )]
    MethodNameCollision {
        method: String,
        kind: &'static str,
        first_origin: String,
        second_origin: String,
    },

    /// Iter 22b.2: an instance `C T` was declared, but `C`'s
    /// superclass `S` does not have an instance for the same type
    /// `T`. Decision 11 single-superclass model requires `instance S
    /// T` to exist whenever `instance C T` exists.
    #[error(
        "instance `{class} {type_repr}` requires superclass instance `{superclass} {type_repr}`, but none was found"
    )]
    MissingSuperclassInstance {
        class: String,
        superclass: String,
        type_repr: String,
    },

    /// Iter 23.1: a user module attempted to use the reserved
    /// module name `prelude`. The prelude is auto-injected by
    /// the loader, so a user module of the same name would
    /// collide silently. Reject explicitly.
    #[error("module name {name:?} is reserved (auto-injected by the loader)")]
    ReservedModuleName { name: String },

    /// 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<String>,
    },

    /// ct.1: a qualified `Type::Con` of the form `<owner>.<type>`
    /// was encountered, but `<owner>` is not a known module in the
    /// workspace, or `<owner>` is known but declares no TypeDef
    /// named `<type>`.
    #[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,
    },
}

/// Hash over the canonical bytes of a complete module.
///
/// Parallel to `def_hash`, but at module level. The workspace loader
/// uses this to verify double-loads; the CLI uses it to emit a stable
/// per-module identifier.
pub fn module_hash(m: &Module) -> String {
    let bytes = canonical::to_bytes(m);
    let h = blake3::hash(&bytes);
    h.to_hex().as_str()[..16].to_string()
}

/// Iter 23.1: the prelude module is embedded into the binary at
/// compile time so the loader needs no on-disk resolution. The
/// canonical source-of-truth file remains
/// `examples/prelude.ail.json` (the file the LLM-author edits).
const PRELUDE_JSON: &str = include_str!(
    "../../../examples/prelude.ail.json"
);

/// Iter 23.1: parse the embedded prelude source into a `Module`.
/// Panics on parse failure — the prelude is build-time-validated;
/// a failure here means the embedded file is malformed and is a
/// build-correctness bug, not a runtime concern.
fn load_prelude() -> Module {
    serde_json::from_str(PRELUDE_JSON)
        .expect("examples/prelude.ail.json must parse as a Module")
}

/// Load entry module plus all transitively reachable modules.
///
/// Algorithm: DFS over `imports`, with two sets:
/// - `loaded` (= `modules` map): modules whose subtree is already fully
///   processed. On a re-hit only hash consistency is checked.
/// - `visiting`: stack of modules whose DFS descent is still running.
///   A hit here = cycle.
pub fn load_workspace(entry_path: &Path) -> Result<Workspace, WorkspaceLoadError> {
    let entry_path = entry_path.to_path_buf();
    let root_dir = entry_path
        .parent()
        .map(Path::to_path_buf)
        .unwrap_or_else(|| PathBuf::from("."));

    // Load entry module + check name<->filename convention.
    let entry_module = load_one(&entry_path)?;
    let expected_entry_name = module_name_from_path(&entry_path);
    if entry_module.name != expected_entry_name {
        return Err(WorkspaceLoadError::ModuleNameMismatch {
            name_in_file: entry_module.name.clone(),
            name_from_path: expected_entry_name,
        });
    }

    let entry_name = entry_module.name.clone();

    let mut modules: BTreeMap<String, Module> = BTreeMap::new();
    let mut visiting: Vec<String> = Vec::new();
    let mut visiting_set: HashSet<String> = HashSet::new();

    visit(
        entry_module,
        &root_dir,
        &mut modules,
        &mut visiting,
        &mut visiting_set,
    )?;

    // Iter 23.1: inject the prelude module. It is implicitly
    // part of every workspace, so the user's import graph
    // does not name it. A user module that happens to be named
    // "prelude" would collide here; reject explicitly so the
    // failure is informative rather than silent.
    if modules.contains_key("prelude") {
        return Err(WorkspaceLoadError::ReservedModuleName {
            name: "prelude".to_string(),
        });
    }
    let prelude = load_prelude();
    modules.insert("prelude".to_string(), prelude);

    // 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)?;

    // Iter 22b.2: class-schema validation runs before registry
    // construction so that ill-kinded class definitions are rejected
    // before any instance against them is registered.
    validate_classdefs(&modules)?;

    // Iter 22b.1: build the workspace-global instance registry. Three
    // coherence checks fire here (Orphan / Duplicate / Missing-method);
    // any violation is surfaced as a `WorkspaceLoadError`, not as a
    // per-call-site diagnostic.
    let registry = build_registry(&modules)?;

    Ok(Workspace {
        entry: entry_name,
        modules,
        root_dir,
        registry,
    })
}

/// Iter 22b.1: build the workspace-global typeclass instance registry.
///
/// Two passes:
///
/// 1. Scan every loaded module to build a "where is X defined" lookup
///    for class names and type names — needed for the coherence
///    (orphan) check below.
/// 2. For each [`crate::ast::Def::Instance`] in declaration order,
///    apply the three checks (coherence / uniqueness / method
///    completeness) and insert the entry on success.
///
/// Iteration is over the modules `BTreeMap` (alphabetical by name) so
/// the order in which collisions are detected is deterministic across
/// runs. Within a module, defs are scanned in source order.
fn build_registry(
    modules: &BTreeMap<String, Module>,
) -> Result<Registry, WorkspaceLoadError> {
    // Pass 1: collect "where is X defined" maps, plus a class lookup
    // by name (needed for the method-completeness check).
    let mut class_def_module: BTreeMap<String, String> = BTreeMap::new();
    let mut type_def_module: BTreeMap<String, String> = BTreeMap::new();
    let mut class_by_name: BTreeMap<String, &ClassDef> = BTreeMap::new();
    for (mod_name, m) in modules {
        for def in &m.defs {
            match def {
                Def::Class(c) => {
                    class_def_module.insert(c.name.clone(), mod_name.clone());
                    class_by_name.insert(c.name.clone(), c);
                }
                Def::Type(t) => {
                    type_def_module.insert(t.name.clone(), mod_name.clone());
                }
                _ => {}
            }
        }
    }

    // Iter 22b.2: method-name-collision pre-pass. Bare-name resolution
    // (`foo x` rather than `A.foo x`) requires that a method name
    // appears in at most one origin across the whole workspace. We
    // walk every `Def::Class` and `Def::Fn` once, building a
    // `method_origins` map; the first repeat fires the diagnostic.
    // The `kind` field distinguishes class-method ↔ class-method from
    // class-method ↔ top-level-fn; fn-fn collisions are a separate
    // concern surfaced by `CheckError::DuplicateDef` in `ailang-check`,
    // not here.
    //
    // Origins are kept structural (the `Origin` enum below) so the
    // `kind` discriminator is a `match` on variants rather than a
    // string-prefix check on a display form.
    enum Origin {
        Class { class_name: String, module: String },
        Fn { name: String, module: String },
    }
    impl Origin {
        fn format(&self) -> String {
            match self {
                Origin::Class { class_name, module } => {
                    format!("class {class_name} (in {module})")
                }
                Origin::Fn { name, module } => format!("fn {name} (in {module})"),
            }
        }
    }

    let mut method_origins: BTreeMap<String, Origin> = BTreeMap::new();
    for (mod_name, m) in modules {
        for def in &m.defs {
            match def {
                Def::Class(c) => {
                    for method in &c.methods {
                        let origin = Origin::Class {
                            class_name: c.name.clone(),
                            module: mod_name.clone(),
                        };
                        if let Some(prior) = method_origins.get(&method.name) {
                            let kind = match prior {
                                Origin::Class { .. } => "class-class",
                                Origin::Fn { .. } => "class-fn",
                            };
                            return Err(WorkspaceLoadError::MethodNameCollision {
                                method: method.name.clone(),
                                kind,
                                first_origin: prior.format(),
                                second_origin: origin.format(),
                            });
                        }
                        method_origins.insert(method.name.clone(), origin);
                    }
                }
                Def::Fn(f) => {
                    let origin = Origin::Fn {
                        name: f.name.clone(),
                        module: mod_name.clone(),
                    };
                    if let Some(prior) = method_origins.get(&f.name) {
                        // Only fire on class-fn collisions here. fn-fn
                        // collisions (two `Def::Fn` with the same name)
                        // are `CheckError::DuplicateDef`'s job in
                        // `ailang-check`; firing here with `kind:
                        // "class-fn"` would misreport.
                        if matches!(prior, Origin::Class { .. }) {
                            return Err(WorkspaceLoadError::MethodNameCollision {
                                method: f.name.clone(),
                                kind: "class-fn",
                                first_origin: prior.format(),
                                second_origin: origin.format(),
                            });
                        }
                        // prior is a fn: skip; do not overwrite.
                    } else {
                        method_origins.insert(f.name.clone(), origin);
                    }
                }
                _ => {}
            }
        }
    }

    // Pass 2: register each instance, with coherence / uniqueness /
    // method-completeness checks.
    let mut entries: BTreeMap<(String, String), RegistryEntry> = BTreeMap::new();
    for (mod_name, m) in modules {
        for def in &m.defs {
            if let Def::Instance(inst) = def {
                let type_repr = type_head_name(&inst.type_);

                // Coherence (orphan-freedom): instance's module must
                // equal the class's module or the type's module. A
                // class declared inside the same module as the
                // instance always satisfies the first leg; a
                // user-defined type declared in the instance's module
                // satisfies the second. Primitives have no
                // user-defined module — instances on primitives
                // therefore must live in the class's module.
                let class_mod = class_def_module
                    .get(&inst.class)
                    .cloned()
                    .unwrap_or_else(|| "<unknown-class>".into());
                let type_mod = type_def_module
                    .get(&type_repr)
                    .cloned()
                    .unwrap_or_else(|| "<primitive-or-unknown>".into());
                let coherent = mod_name == &class_mod || mod_name == &type_mod;
                if !coherent {
                    return Err(WorkspaceLoadError::OrphanInstance {
                        class: inst.class.clone(),
                        type_repr,
                        defining_module: mod_name.clone(),
                        class_module: class_mod,
                        type_module: type_mod,
                    });
                }

                // Uniqueness: a `(class, type-hash)` key must appear
                // at most once across the whole workspace. ct.1.5a: the
                // type expression is normalised to its always-qualified
                // form before hashing so a bare-local declaration in
                // the type's defining module and a qualified-cross-module
                // declaration from elsewhere produce the same key (both
                // refer to the same type under the canonical-form rule).
                let type_hash = canonical::type_hash(
                    &normalize_type_for_registry(&inst.type_, &type_def_module),
                );
                let key = (inst.class.clone(), type_hash);
                if let Some(prior) = entries.get(&key) {
                    return Err(WorkspaceLoadError::DuplicateInstance {
                        class: inst.class.clone(),
                        type_repr,
                        first_module: prior.defining_module.clone(),
                        second_module: mod_name.clone(),
                    });
                }

                // Method completeness: every non-default method of
                // the class must have a body in this instance.
                // Defaults may be inherited (no body required).
                // Missing class declaration is deferred to 22b.2's
                // typecheck arms — for 22b.1 we skip the
                // completeness check rather than firing a separate
                // diagnostic.
                if let Some(class_def) = class_by_name.get(&inst.class) {
                    let provided: BTreeSet<&str> =
                        inst.methods.iter().map(|m| m.name.as_str()).collect();
                    for class_method in &class_def.methods {
                        if class_method.default.is_none()
                            && !provided.contains(class_method.name.as_str())
                        {
                            return Err(WorkspaceLoadError::MissingMethod {
                                class: inst.class.clone(),
                                type_repr,
                                method: class_method.name.clone(),
                            });
                        }
                    }

                    // Symmetric to MissingMethod: an instance must
                    // not specify a body for a method name the class
                    // never declared. Decision 11 forbids ad-hoc
                    // additions to a class's method set at the
                    // instance site.
                    let declared: BTreeSet<&str> =
                        class_def.methods.iter().map(|m| m.name.as_str()).collect();
                    for inst_method in &inst.methods {
                        if !declared.contains(inst_method.name.as_str()) {
                            return Err(WorkspaceLoadError::OverridingNonExistentMethod {
                                class: inst.class.clone(),
                                type_repr: type_repr.clone(),
                                method: inst_method.name.clone(),
                            });
                        }
                    }
                }

                entries.insert(
                    key,
                    RegistryEntry {
                        instance: inst.clone(),
                        defining_module: mod_name.clone(),
                    },
                );
            }
        }
    }

    // Iter 22b.2: superclass-instance completeness. For every entry,
    // walk the class's superclass chain and require an entry for each
    // step at the same type-hash.
    for (key, entry) in entries.iter() {
        let (class_name, type_hash) = key;
        let type_repr = type_head_name(&entry.instance.type_);
        // Iter 22b.2 leaves superclass-cycle detection to a future arm;
        // here we just terminate the walk.
        let mut visited: BTreeSet<&str> = BTreeSet::new();
        let mut current = class_by_name.get(class_name.as_str()).copied();
        while let Some(c) = current {
            if !visited.insert(c.name.as_str()) {
                break;
            }
            if let Some(sc) = &c.superclass {
                let sc_key = (sc.class.clone(), type_hash.clone());
                if !entries.contains_key(&sc_key) {
                    return Err(WorkspaceLoadError::MissingSuperclassInstance {
                        class: class_name.clone(),
                        superclass: sc.class.clone(),
                        type_repr: type_repr.clone(),
                    });
                }
                current = class_by_name.get(sc.class.as_str()).copied();
            } else {
                break;
            }
        }
    }

    Ok(Registry {
        entries,
        type_def_module,
    })
}

/// Iter 22b.2: class-schema validation. Runs before `build_registry`.
/// Three diagnostics fire from here: `kind-mismatch`,
/// `invalid-superclass-param`, `constraint-references-unbound-type-var`.
fn validate_classdefs(
    modules: &BTreeMap<String, Module>,
) -> Result<(), WorkspaceLoadError> {
    for (mod_name, m) in modules {
        for def in &m.defs {
            if let Def::Class(c) = def {
                for method in &c.methods {
                    walk_kind_mismatch(&method.ty, &c.param)
                        .map_err(|()| WorkspaceLoadError::KindMismatch {
                            class: c.name.clone(),
                            param: c.param.clone(),
                            method: method.name.clone(),
                            defining_module: mod_name.clone(),
                        })?;
                }
                if let Some(sc) = &c.superclass {
                    if sc.type_ != c.param {
                        return Err(WorkspaceLoadError::InvalidSuperclassParam {
                            class: c.name.clone(),
                            superclass: sc.class.clone(),
                            expected_param: c.param.clone(),
                            got_type: sc.type_.clone(),
                        });
                    }
                }
                for method in &c.methods {
                    if let Type::Forall { vars, constraints, .. } = &method.ty {
                        let mut bound: BTreeSet<&str> =
                            vars.iter().map(String::as_str).collect();
                        bound.insert(c.param.as_str());
                        for constr in constraints {
                            if let Type::Var { name } = &constr.type_ {
                                if !bound.contains(name.as_str()) {
                                    return Err(WorkspaceLoadError::UnboundConstraintTypeVar {
                                        class: c.name.clone(),
                                        method: method.name.clone(),
                                        constraint_class: constr.class.clone(),
                                        var: name.clone(),
                                    });
                                }
                            }
                        }
                    }
                }
            }
        }
    }
    Ok(())
}

/// Walks a `Type` looking for any `Type::Con { name == param, args
/// non-empty }`. The class param is kind `*`; appearing as a
/// constructor with arguments is a kind-mismatch.
fn walk_kind_mismatch(t: &Type, param: &str) -> Result<(), ()> {
    match t {
        Type::Con { name, args } => {
            if name == param && !args.is_empty() {
                return Err(());
            }
            for a in args {
                walk_kind_mismatch(a, param)?;
            }
            Ok(())
        }
        Type::Fn { params, ret, .. } => {
            for p in params {
                walk_kind_mismatch(p, param)?;
            }
            walk_kind_mismatch(ret, param)
        }
        Type::Forall { body, .. } => walk_kind_mismatch(body, param),
        Type::Var { .. } => Ok(()),
    }
}

/// 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.5a: normalize a `Type` by qualifying every bare-non-primitive
/// `Type::Con.name` to its always-qualified form
/// (`<defining_module>.<name>`). Primitives stay bare; already-qualified
/// names stay as-is; bare names whose defining module is unknown stay
/// as-is (downstream diagnostics will catch them). `Type::Fn` /
/// `Type::Forall` / `Type::Var` recurse / pass through structurally.
///
/// Used by [`build_registry`] for registry-key canonicalisation so the
/// duplicate-instance check survives the asymmetric "bare = local,
/// qualified = cross-module" canonical-form rule: an instance declared
/// bare-local in the type's defining module and an equivalent one
/// declared qualified-cross-module from elsewhere produce the same
/// registry key.
///
/// The qualifier is the type's *defining* module (looked up in
/// `type_def_module`), not the instance's owning module. The two
/// coincide under a canonical-form-compliant workspace (bare implies
/// local-to-defining-module), but using the defining-module lookup is
/// robust against pre-`validate_canonical_type_names`-wired fixtures
/// that may still carry bare cross-module refs.
fn normalize_type_for_registry(
    t: &Type,
    type_def_module: &BTreeMap<String, String>,
) -> Type {
    match t {
        Type::Con { name, args } => {
            let new_name = if name.contains('.') || is_primitive_type_name(name) {
                name.clone()
            } else if let Some(owner) = type_def_module.get(name) {
                format!("{owner}.{name}")
            } else {
                // Unknown bare non-primitive — leave as-is. Either it is
                // a class-param Type::Var miscoded as a Con (which is a
                // separate well-formedness problem) or a stale ref that
                // downstream diagnostics will catch.
                name.clone()
            };
            Type::Con {
                name: new_name,
                args: args
                    .iter()
                    .map(|a| normalize_type_for_registry(a, type_def_module))
                    .collect(),
            }
        }
        Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
            params: params
                .iter()
                .map(|p| normalize_type_for_registry(p, type_def_module))
                .collect(),
            param_modes: param_modes.clone(),
            ret: Box::new(normalize_type_for_registry(ret, type_def_module)),
            ret_mode: *ret_mode,
            effects: effects.clone(),
        },
        Type::Forall { vars, constraints, body } => Type::Forall {
            vars: vars.clone(),
            constraints: constraints
                .iter()
                .map(|c| crate::ast::Constraint {
                    class: c.class.clone(),
                    type_: normalize_type_for_registry(&c.type_, type_def_module),
                })
                .collect(),
            body: Box::new(normalize_type_for_registry(body, type_def_module)),
        },
        Type::Var { name } => Type::Var { name: name.clone() },
    }
}

/// 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 `<owner>.<type>`: `<owner>` must be a known module,
///    `<type>` 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<String, Module>,
) -> Result<(), WorkspaceLoadError> {
    // Pre-pass: for each module, build a `BTreeSet<String>` of local
    // TypeDef names. Used for both the owning-module local lookup
    // and the per-import owner lookup.
    let mut local_types: BTreeMap<String, BTreeSet<String>> = 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-`<owner>` 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(())
            })?;
            walk_def_terms(def, &mut |type_name: &str| {
                check_type_con_name(
                    type_name, mod_name, &local_types, &import_names,
                )
            })?;
            check_class_name_fields(def, mod_name)?;
        }
    }

    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<String, BTreeSet<String>>,
    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<String> = 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<F>(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<F>(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<F>(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(()),
    }
}

/// ct.1: walk every `Term::Ctor.type_name` reachable from a single
/// `Def`, calling `f` on the type_name strings. Used to enforce the
/// canonical-form rule on term-side type references.
fn walk_def_terms<F>(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` /
/// `walk_term_embedded_types` path — but `Term::Ctor.type_name` is
/// a `String`, not a `Type`, so it lives here.
fn walk_term<F>(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError>
where
    F: FnMut(&str) -> Result<(), WorkspaceLoadError>,
{
    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<F>(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(())
        }
    }
}

/// 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(()),
    }
}

/// Iter 22b.1: extract the head-constructor name of a type, for the
/// "where is this type defined" lookup and for diagnostic-message
/// rendering.
///
/// For `Type::Con { name, .. }` (the only legal head shape for a
/// non-orphan instance) returns `name`. Other variants (`Var`,
/// `Forall`, `Fn`) are not legal as instance heads — Decision 11
/// requires a concrete type expression at the instance head — so we
/// emit a stable fallback string. The fallback prevents diagnostic
/// rendering from panicking on a malformed fixture; the "real"
/// rejection of non-concrete instance heads will arrive as a
/// schema-validation diagnostic in 22b.2.
fn type_head_name(t: &Type) -> String {
    match t {
        Type::Con { name, .. } => name.clone(),
        Type::Var { name } => format!("<var:{name}>"),
        Type::Forall { .. } => "<forall>".into(),
        Type::Fn { .. } => "<fn>".into(),
    }
}

fn visit(
    module: Module,
    root_dir: &Path,
    modules: &mut BTreeMap<String, Module>,
    visiting: &mut Vec<String>,
    visiting_set: &mut HashSet<String>,
) -> Result<(), WorkspaceLoadError> {
    let name = module.name.clone();

    // Already fully loaded? Then do nothing. Hash consistency is checked
    // on re-encounter via imports (see below in the loop).
    if modules.contains_key(&name) {
        return Ok(());
    }

    // Cycle: same name currently on the DFS stack.
    if visiting_set.contains(&name) {
        let mut path = visiting.clone();
        path.push(name);
        return Err(WorkspaceLoadError::Cycle { path });
    }

    visiting.push(name.clone());
    visiting_set.insert(name.clone());

    // Process imports recursively.
    let imports = module.imports.clone();
    for imp in &imports {
        let imp_path = root_dir.join(format!("{}.ail.json", imp.module));

        if let Some(existing) = modules.get(&imp.module) {
            // Already fully loaded — check hash consistency, in case the
            // file on disk has changed.
            let on_disk = match load_one(&imp_path) {
                Ok(m) => m,
                Err(WorkspaceLoadError::Io { .. }) => continue,
                Err(e) => return Err(e),
            };
            if module_hash(existing) != module_hash(&on_disk) {
                return Err(WorkspaceLoadError::ModuleHashMismatch {
                    name: imp.module.clone(),
                });
            }
            continue;
        }

        if visiting_set.contains(&imp.module) {
            let mut path = visiting.clone();
            path.push(imp.module.clone());
            return Err(WorkspaceLoadError::Cycle { path });
        }

        if !imp_path.exists() {
            return Err(WorkspaceLoadError::ModuleNotFound {
                name: imp.module.clone(),
                expected_path: imp_path,
            });
        }

        let imported = load_one(&imp_path)?;
        if imported.name != imp.module {
            return Err(WorkspaceLoadError::ModuleNameMismatch {
                name_in_file: imported.name,
                name_from_path: imp.module.clone(),
            });
        }
        visit(imported, root_dir, modules, visiting, visiting_set)?;
    }

    visiting.pop();
    visiting_set.remove(&name);
    modules.insert(name, module);

    Ok(())
}

fn load_one(path: &Path) -> Result<Module, WorkspaceLoadError> {
    match load_module(path) {
        Ok(m) => Ok(m),
        Err(CoreError::Io(e)) => Err(WorkspaceLoadError::Io {
            path: path.to_path_buf(),
            source: e,
        }),
        Err(e) => Err(WorkspaceLoadError::Schema {
            path: path.to_path_buf(),
            source: e,
        }),
    }
}

fn module_name_from_path(p: &Path) -> String {
    let file = p.file_name().and_then(|s| s.to_str()).unwrap_or("");
    // Convention: `<name>.ail.json`.
    if let Some(stripped) = file.strip_suffix(".ail.json") {
        return stripped.to_string();
    }
    // Fallback: strip only the last extension.
    Path::new(file)
        .file_stem()
        .and_then(|s| s.to_str())
        .unwrap_or(file)
        .to_string()
}

#[cfg(test)]
mod tests {
    use super::*;
    use std::fs;

    fn write_module(dir: &Path, name: &str, imports: &[&str]) -> PathBuf {
        let imports_json: Vec<serde_json::Value> = imports
            .iter()
            .map(|m| serde_json::json!({ "module": m }))
            .collect();
        let module = serde_json::json!({
            "schema": crate::SCHEMA,
            "name": name,
            "imports": imports_json,
            "defs": [],
        });
        let path = dir.join(format!("{name}.ail.json"));
        fs::write(&path, serde_json::to_vec_pretty(&module).unwrap()).unwrap();
        path
    }

    fn tmp_dir(tag: &str) -> PathBuf {
        let d = std::env::temp_dir().join(format!(
            "ailang_workspace_test_{tag}_{}",
            std::process::id()
        ));
        let _ = fs::remove_dir_all(&d);
        fs::create_dir_all(&d).unwrap();
        d
    }

    #[test]
    fn loads_example_workspace_happy_path() {
        // Uses the canonical example files under `examples/`. This
        // test documents that the loader relies on the committed
        // workspace example.
        let manifest_dir = env!("CARGO_MANIFEST_DIR");
        let workspace_root =
            Path::new(manifest_dir).parent().unwrap().parent().unwrap();
        let entry = workspace_root.join("examples").join("ws_main.ail.json");

        let ws = load_workspace(&entry).expect("load workspace");
        assert_eq!(ws.entry, "ws_main");
        assert!(ws.modules.contains_key("ws_main"));
        assert!(ws.modules.contains_key("ws_lib"));
        // Iter 23.1: the loader auto-injects the `prelude` module,
        // so the count is the user's two modules plus prelude.
        assert_eq!(ws.modules.len(), 3);
    }

    #[test]
    fn loads_workspace_auto_injects_prelude() {
        // Iter 23.1: the prelude module is implicitly part of every
        // workspace, regardless of whether the user's modules import
        // it. Loading any well-formed workspace must result in
        // `ws.modules["prelude"]` being present with the Ordering
        // type def.
        let manifest_dir = env!("CARGO_MANIFEST_DIR");
        let workspace_root =
            Path::new(manifest_dir).parent().unwrap().parent().unwrap();
        let entry = workspace_root.join("examples").join("ws_main.ail.json");

        let ws = load_workspace(&entry).expect("load workspace");
        assert!(
            ws.modules.contains_key("prelude"),
            "prelude module must be auto-injected; modules present: {:?}",
            ws.modules.keys().collect::<Vec<_>>()
        );
        let prelude = &ws.modules["prelude"];
        assert_eq!(prelude.name, "prelude");
        assert!(
            prelude.defs.iter().any(|d| matches!(
                d,
                crate::ast::Def::Type(t) if t.name == "Ordering"
            )),
            "prelude must contain Ordering type def"
        );

        // Iter 23.2: prelude also ships the `Eq` class plus three
        // primitive instances (Eq Int, Eq Bool, Eq Str).
        assert!(
            prelude.defs.iter().any(|d| matches!(
                d,
                crate::ast::Def::Class(c) if c.name == "Eq"
            )),
            "prelude must contain Eq class def"
        );
        let eq_instance_types: Vec<&str> = prelude
            .defs
            .iter()
            .filter_map(|d| match d {
                crate::ast::Def::Instance(i) if i.class == "Eq" => {
                    if let crate::ast::Type::Con { name, .. } = &i.type_ {
                        Some(name.as_str())
                    } else {
                        None
                    }
                }
                _ => None,
            })
            .collect();
        assert!(
            eq_instance_types.contains(&"Int"),
            "prelude must contain `instance Eq Int`; saw Eq instances on: {eq_instance_types:?}"
        );
        assert!(
            eq_instance_types.contains(&"Bool"),
            "prelude must contain `instance Eq Bool`; saw Eq instances on: {eq_instance_types:?}"
        );
        assert!(
            eq_instance_types.contains(&"Str"),
            "prelude must contain `instance Eq Str`; saw Eq instances on: {eq_instance_types:?}"
        );

        // Iter 23.3: prelude also ships the `Ord` class plus three
        // primitive instances (Ord Int, Ord Bool, Ord Str). Ord
        // extends Eq (Decision 11 single-superclass closure), so its
        // shape is the same as Eq's instance set; the loader uses the
        // superclass walk to verify the Eq instances exist.
        assert!(
            prelude.defs.iter().any(|d| matches!(
                d,
                crate::ast::Def::Class(c) if c.name == "Ord"
            )),
            "prelude must contain Ord class def"
        );
        let ord_instance_types: Vec<&str> = prelude
            .defs
            .iter()
            .filter_map(|d| match d {
                crate::ast::Def::Instance(i) if i.class == "Ord" => {
                    if let crate::ast::Type::Con { name, .. } = &i.type_ {
                        Some(name.as_str())
                    } else {
                        None
                    }
                }
                _ => None,
            })
            .collect();
        assert!(
            ord_instance_types.contains(&"Int"),
            "prelude must contain `instance Ord Int`; saw: {ord_instance_types:?}"
        );
        assert!(
            ord_instance_types.contains(&"Bool"),
            "prelude must contain `instance Ord Bool`; saw: {ord_instance_types:?}"
        );
        assert!(
            ord_instance_types.contains(&"Str"),
            "prelude must contain `instance Ord Str`; saw: {ord_instance_types:?}"
        );
    }

    #[test]
    fn user_module_named_prelude_is_rejected() {
        // Iter 23.1: the loader auto-injects a module named "prelude",
        // so a user module that also claims that name would collide
        // silently. The collision is caught explicitly with
        // `ReservedModuleName`.
        let dir = tmp_dir("prelude_collision");
        write_module(&dir, "prelude", &[]);
        let entry = dir.join("prelude.ail.json");

        let err = load_workspace(&entry).expect_err("must reject user prelude");
        match err {
            WorkspaceLoadError::ReservedModuleName { name } => {
                assert_eq!(name, "prelude");
            }
            other => panic!(
                "expected ReservedModuleName, got: {other:?}"
            ),
        }
    }

    #[test]
    fn detects_import_cycle() {
        let dir = tmp_dir("cycle");
        write_module(&dir, "a", &["b"]);
        write_module(&dir, "b", &["a"]);
        let entry = dir.join("a.ail.json");

        let err = load_workspace(&entry).expect_err("must error on cycle");
        match err {
            WorkspaceLoadError::Cycle { path } => {
                assert!(path.contains(&"a".to_string()));
                assert!(path.contains(&"b".to_string()));
            }
            other => panic!("expected Cycle, got {other:?}"),
        }
    }

    #[test]
    fn module_not_found_yields_structured_error() {
        let dir = tmp_dir("notfound");
        write_module(&dir, "main", &["does_not_exist"]);
        let entry = dir.join("main.ail.json");

        let err = load_workspace(&entry).expect_err("must error on missing module");
        match err {
            WorkspaceLoadError::ModuleNotFound { name, expected_path } => {
                assert_eq!(name, "does_not_exist");
                assert!(expected_path.ends_with("does_not_exist.ail.json"));
            }
            other => panic!("expected ModuleNotFound, got {other:?}"),
        }
    }

    /// Iter 22b.1: a workspace whose own modules contain no
    /// `Def::Instance` defs produces no non-prelude registry entries.
    /// This is the happy-path baseline for the registry-build pass —
    /// every pre-22b workspace falls into this case. With the
    /// auto-loaded prelude (iter 23.2) the registry is no longer
    /// strictly empty, so the invariant is now "no entries whose
    /// `defining_module` is anything other than `prelude`".
    #[test]
    fn iter22b1_workspace_with_no_classes_has_empty_registry() {
        let manifest_dir = env!("CARGO_MANIFEST_DIR");
        let workspace_root =
            Path::new(manifest_dir).parent().unwrap().parent().unwrap();
        let entry = workspace_root.join("examples").join("sum.ail.json");

        let ws = load_workspace(&entry).expect("sum.ail.json loads");
        assert!(
            ws.registry.entries.values().all(|e| e.defining_module == "prelude"),
            "pre-22b fixture has no class/instance defs of its own; \
             all registry entries must come from the auto-injected prelude. \
             got non-prelude entries: {:?}",
            ws.registry.entries.values()
                .filter(|e| e.defining_module != "prelude")
                .map(|e| &e.defining_module)
                .collect::<Vec<_>>()
        );
    }

    fn examples_dir() -> PathBuf {
        let manifest_dir = env!("CARGO_MANIFEST_DIR");
        Path::new(manifest_dir)
            .parent()
            .unwrap()
            .parent()
            .unwrap()
            .join("examples")
    }

    /// Iter 22b.1: a coherent instance (in the class's module)
    /// loads cleanly and produces one registry entry from the
    /// fixture itself. With the auto-loaded prelude (iter 23.2)
    /// the registry also contains the prelude's own entries; the
    /// invariant is filtered to fixture-only entries.
    #[test]
    fn iter22b1_instance_in_class_module_loads_clean() {
        let entry = examples_dir().join("test_22b1_orphan_class.ail.json");
        let ws = load_workspace(&entry).expect("coherent instance loads");
        let fixture_entries: Vec<_> = ws.registry.entries.iter()
            .filter(|(_, e)| e.defining_module != "prelude")
            .collect();
        assert_eq!(fixture_entries.len(), 1);
        let (key, entry) = fixture_entries[0];
        assert_eq!(&key.0, "Show");
        assert_eq!(entry.defining_module, "test_22b1_orphan_class");
        assert_eq!(entry.instance.class, "Show");
    }

    /// Iter 22b.1: an instance declared in a module that is neither
    /// the class's module nor the type's module fires `OrphanInstance`.
    /// The fixture imports `test_22b1_orphan_third_classmod` (which
    /// owns `class Show`) and the entry module declares `instance
    /// Show Int` itself — but the entry is not the class's module
    /// and `Int` is primitive, so neither leg of coherence is
    /// satisfied.
    #[test]
    fn iter22b1_orphan_instance_fires_diagnostic() {
        let entry = examples_dir().join("test_22b1_orphan_third.ail.json");
        let err = load_workspace(&entry).expect_err("must fire orphan");
        match err {
            WorkspaceLoadError::OrphanInstance {
                class,
                type_repr,
                defining_module,
                ..
            } => {
                assert_eq!(class, "Show");
                assert_eq!(type_repr, "Int");
                assert_eq!(defining_module, "test_22b1_orphan_third");
            }
            other => panic!("expected OrphanInstance, got {other:?}"),
        }
    }

    /// Iter 22b.1: two instances of the same `(class, type)` pair
    /// declared from coherent positions (one in the class's module,
    /// one in the type's module) collide on the registry's
    /// uniqueness check. Setup per the JOURNAL hint:
    /// - module A defines `class Show` and declares
    ///   `instance Show MyInt` (legal, A is class's module).
    /// - module B defines `type MyInt` and declares
    ///   `instance Show MyInt` (legal, B is type's module).
    /// - entry module imports both A and B.
    /// The build_registry pass sees both instances under the same
    /// `(Show, hash-of-MyInt)` key and fires `DuplicateInstance`.
    #[test]
    fn iter22b1_duplicate_instance_fires_diagnostic() {
        let entry = examples_dir().join("test_22b1_dup_entry.ail.json");
        let err = load_workspace(&entry).expect_err("must fire duplicate");
        match err {
            WorkspaceLoadError::DuplicateInstance {
                class,
                type_repr,
                first_module,
                second_module,
            } => {
                assert_eq!(class, "Show");
                assert_eq!(type_repr, "MyInt");
                assert_ne!(first_module, second_module);
                let modules: BTreeSet<&str> =
                    [first_module.as_str(), second_module.as_str()].iter().copied().collect();
                assert!(modules.contains("test_22b1_dup_a"));
                assert!(modules.contains("test_22b1_dup_b"));
            }
            other => panic!("expected DuplicateInstance, got {other:?}"),
        }
    }

    /// Iter 22b.1: an instance that omits a required (non-default)
    /// method of its class fires `MissingMethod`. The fixture's
    /// `class TEq` declares `teq` and `ne` as both non-default; the
    /// instance only specifies `ne`, leaving `teq` missing.
    /// (Class is `TEq` rather than `Eq` to avoid colliding with the
    /// auto-loaded prelude's `class Eq`.)
    #[test]
    fn iter22b1_missing_method_fires_diagnostic() {
        let entry = examples_dir().join("test_22b1_missing_method.ail.json");
        let err = load_workspace(&entry).expect_err("must fire missing-method");
        match err {
            WorkspaceLoadError::MissingMethod {
                class,
                type_repr,
                method,
            } => {
                assert_eq!(class, "TEq");
                assert_eq!(type_repr, "Int");
                assert_eq!(method, "teq");
            }
            other => panic!("expected MissingMethod, got {other:?}"),
        }
    }

    /// 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:?}",
            ),
        }
    }

    /// Iter 22b.2: a class whose `superclass.type` differs from its
    /// own `param` (e.g. `class Ord a extends Eq b`) must fire
    /// `InvalidSuperclassParam`. Decision 11 axis 1 ("single
    /// superclass, applied to the same param") makes the only legal
    /// shape `extends Eq a` when the parent class has `param: "a"`.
    #[test]
    fn superclass_with_wrong_param_fires_invalid_superclass_param() {
        let entry = std::path::PathBuf::from(
            "../../examples/test_22b2_invalid_superclass_param.ail.json",
        );
        let err = load_workspace(&entry)
            .expect_err("must fire invalid-superclass-param");
        match err {
            WorkspaceLoadError::InvalidSuperclassParam {
                class, superclass, expected_param, got_type,
            } => {
                assert_eq!(class, "Ord");
                assert_eq!(superclass, "Eq");
                assert_eq!(expected_param, "a");
                assert_eq!(got_type, "b");
            }
            other => panic!("expected InvalidSuperclassParam, got {other:?}"),
        }
    }

    /// Iter 22b.2: an instance that specifies a body for a method
    /// name the class never declared must fire
    /// `OverridingNonExistentMethod`. Symmetric counterpart to
    /// `MissingMethod`: the latter fires when the class declares a
    /// non-default method that the instance omits; this one fires
    /// when the instance provides a body the class did not ask for.
    /// Decision 11 forbids ad-hoc additions to a class's method set
    /// at the instance site.
    /// (Class is `TEq` rather than `Eq` to avoid colliding with the
    /// auto-loaded prelude's `class Eq`.)
    #[test]
    fn instance_overriding_nonexistent_method_fires() {
        let entry = std::path::PathBuf::from(
            "../../examples/test_22b2_overriding_nonexistent.ail.json",
        );
        let err = load_workspace(&entry)
            .expect_err("must fire overriding-non-existent-method");
        match err {
            WorkspaceLoadError::OverridingNonExistentMethod {
                class, type_repr, method,
            } => {
                assert_eq!(class, "TEq");
                assert_eq!(type_repr, "Int");
                assert_eq!(method, "ne");
            }
            other => panic!("expected OverridingNonExistentMethod, got {other:?}"),
        }
    }

    /// Iter 22b.2: a class method's `Type::Forall` whose `constraints`
    /// reference a type variable that is neither bound by `Forall.vars`
    /// nor equal to the class's `param` must fire
    /// `UnboundConstraintTypeVar`. The fixture's `class Foo a` declares
    /// method `foo` with `forall a. (Bar z) => a -> Unit`; `z` is
    /// bound nowhere, so the constraint is unsatisfiable by
    /// construction.
    #[test]
    fn constraint_with_unbound_var_fires_unbound_constraint_type_var() {
        let entry = std::path::PathBuf::from(
            "../../examples/test_22b2_unbound_constraint_var.ail.json",
        );
        let err = load_workspace(&entry)
            .expect_err("must fire constraint-references-unbound-type-var");
        match err {
            WorkspaceLoadError::UnboundConstraintTypeVar {
                class, method, var, ..
            } => {
                assert_eq!(class, "Foo");
                assert_eq!(method, "foo");
                assert_eq!(var, "z");
            }
            other => panic!("expected UnboundConstraintTypeVar, got {other:?}"),
        }
    }

    /// Iter 22b.2: two classes that declare a method with the same
    /// name must fire `MethodNameCollision` with `kind == "class-class"`.
    /// Decision 11 keeps method names workspace-unique so that bare
    /// method-name resolution (`foo x` rather than `A.foo x`) is
    /// unambiguous; if two classes both export `foo`, the registry has
    /// no way to choose between them at a use site.
    #[test]
    fn class_class_method_name_collision_fires() {
        let entry = examples_dir()
            .join("test_22b2_method_name_collision_class_class.ail.json");
        let err = load_workspace(&entry)
            .expect_err("must fire method-name-collision");
        match err {
            WorkspaceLoadError::MethodNameCollision {
                method,
                kind,
                first_origin,
                second_origin,
            } => {
                assert_eq!(method, "foo");
                assert_eq!(kind, "class-class");
                assert!(
                    first_origin.starts_with("class A"),
                    "first_origin = {first_origin:?}",
                );
                assert!(
                    second_origin.starts_with("class B"),
                    "second_origin = {second_origin:?}",
                );
            }
            other => panic!("expected MethodNameCollision, got {other:?}"),
        }
    }

    /// Iter 22b.2: a class-method name that collides with a top-level
    /// `fn` of the same name must fire `MethodNameCollision` with
    /// `kind == "class-fn"`. Same rationale as the class-class case:
    /// bare-name resolution must be unambiguous, and a class method
    /// shadowing (or being shadowed by) a free function silently is
    /// the worst possible failure mode.
    #[test]
    fn class_fn_method_name_collision_fires() {
        let entry = examples_dir()
            .join("test_22b2_method_name_collision_class_fn.ail.json");
        let err = load_workspace(&entry)
            .expect_err("must fire method-name-collision");
        match err {
            WorkspaceLoadError::MethodNameCollision {
                method,
                kind,
                first_origin,
                second_origin,
            } => {
                assert_eq!(method, "greet");
                assert_eq!(kind, "class-fn");
                assert!(
                    first_origin.starts_with("class Greet"),
                    "first_origin = {first_origin:?}",
                );
                assert!(
                    second_origin.starts_with("fn greet"),
                    "second_origin = {second_origin:?}",
                );
            }
            other => panic!("expected MethodNameCollision, got {other:?}"),
        }
    }

    /// Iter 22b.2: an instance `C T` whose class `C` declares a
    /// superclass `S` requires that `instance S T` also exist in the
    /// workspace. The fixture declares `class TEq a`, `class TOrd a
    /// extends TEq a`, and `instance TOrd Int` — but no `instance TEq
    /// Int` — so registry build must fire
    /// `MissingSuperclassInstance`. Decision 11 single-superclass
    /// model requires `instance S T` whenever `instance C T` exists.
    /// (Classes are `TEq` / `TOrd` rather than `Eq` / `Ord` to avoid
    /// colliding with the auto-loaded prelude's `class Eq`.)
    #[test]
    fn instance_without_superclass_instance_fires() {
        let entry = examples_dir().join("test_22b2_missing_superclass_instance.ail.json");
        let err = load_workspace(&entry)
            .expect_err("must fire missing-superclass-instance");
        match err {
            WorkspaceLoadError::MissingSuperclassInstance {
                class, superclass, type_repr,
            } => {
                assert_eq!(class, "TOrd");
                assert_eq!(superclass, "TEq");
                assert_eq!(type_repr, "Int");
            }
            other => panic!("expected MissingSuperclassInstance, got {other:?}"),
        }
    }

    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<String, Module> {
        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<String, Module> {
        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()
    }

    /// 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 `<owner>.<type>` where `<owner>` is a
    /// known module AND `<type>` 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 `<owner>.<type>` where `<owner>` is
    /// NOT a known module must fire `BadCrossModuleTypeRef`. Symmetric
    /// case: `<owner>` known but no TypeDef `<type>` 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:?}"),
        }
    }

    /// 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:?}"),
        }
    }

    /// 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:?}"),
        }
    }

    /// ct.1.5a: registry-side duplicate detection survives the
    /// asymmetric canonical-form representation. Two coherent instances
    /// on the same type-def, one declared bare-local (in the type's
    /// defining module) and one declared qualified-cross-module (in the
    /// class's defining module), must collide on the registry's
    /// `(class, type-hash)` key.
    ///
    /// This is the regression that broke during the ct.1.5 migration
    /// dry-run: after migrating `test_22b1_dup_a.ail.json` to qualified
    /// `test_22b1_dup_b.MyInt`, the unmigrated `test_22b1_dup_b.ail.json`
    /// (which keeps bare `MyInt` because the type IS local there)
    /// produced a different type-hash, and the duplicate detection
    /// silently missed.
    ///
    /// The fixture is constructed in-memory rather than from disk so
    /// the test stays focused on the registry behaviour rather than the
    /// migration tool. Class `TShow` is named distinctly from the
    /// prelude's `Eq`/`Show` to avoid collisions with the auto-loaded
    /// prelude — but `build_registry` here is called directly on a flat
    /// `BTreeMap` (no auto-prelude injection), so the choice is purely
    /// belt-and-braces.
    #[test]
    fn ct1_registry_duplicate_detection_survives_mixed_canonical_form() {
        // Module `cls`: declares `class TShow a` (custom name to avoid
        // any future prelude collision) and the qualified-cross-module
        // instance `instance TShow other.MyInt`.
        let cls: Module = serde_json::from_value(serde_json::json!({
            "schema": crate::SCHEMA,
            "name": "cls",
            "imports": [{ "module": "other" }],
            "defs": [
                {
                    "kind": "class",
                    "name": "TShow",
                    "param": "a",
                    "methods": [
                        { "name": "tshow",
                          "type": { "k": "fn",
                                    "params": [{ "k": "var", "name": "a" }],
                                    "ret": { "k": "con", "name": "Str" },
                                    "effects": [] } }
                    ]
                },
                {
                    "kind": "instance",
                    "class": "TShow",
                    "type": { "k": "con", "name": "other.MyInt" },
                    "methods": [
                        { "name": "tshow",
                          "body": { "t": "lit", "lit": { "kind": "str", "value": "cls-side" } } }
                    ]
                }
            ],
        })).unwrap();

        // Module `other`: declares `type MyInt` and the bare-local
        // instance `instance TShow MyInt`. Imports `cls` for shape
        // coherence (the dependency direction needed to bring `class
        // TShow` into scope under the actual loader).
        let other: Module = serde_json::from_value(serde_json::json!({
            "schema": crate::SCHEMA,
            "name": "other",
            "imports": [{ "module": "cls" }],
            "defs": [
                { "kind": "type", "name": "MyInt", "ctors": [{ "name": "MkMyInt", "fields": [] }] },
                {
                    "kind": "instance",
                    "class": "TShow",
                    "type": { "k": "con", "name": "MyInt" },
                    "methods": [
                        { "name": "tshow",
                          "body": { "t": "lit", "lit": { "kind": "str", "value": "other-side" } } }
                    ]
                }
            ],
        })).unwrap();

        let mut modules = BTreeMap::new();
        modules.insert("cls".to_string(), cls);
        modules.insert("other".to_string(), other);

        let err = build_registry(&modules).expect_err(
            "registry build must fire DuplicateInstance for mixed canonical-form"
        );
        match err {
            WorkspaceLoadError::DuplicateInstance {
                class, first_module, second_module, ..
            } => {
                assert_eq!(class, "TShow");
                let mods: BTreeSet<&str> =
                    [first_module.as_str(), second_module.as_str()].into_iter().collect();
                assert!(mods.contains("cls"),
                    "got {first_module}, {second_module}");
                assert!(mods.contains("other"),
                    "got {first_module}, {second_module}");
            }
            other => panic!("expected DuplicateInstance, got {other:?}"),
        }
    }

    /// ct.1.5a follow-up: `normalize_type_for_registry` must recurse into
    /// `Type::Forall.constraints[].type_` just like it does into
    /// `Type::Forall.body`. A bare `Type::Con` nested inside a Forall
    /// constraint that lives in a different module must be rewritten to
    /// its qualified form, otherwise the registry key for a constrained
    /// polymorphic type would disagree between bare-local and
    /// qualified-cross-module call sites — the same divergence
    /// `ct1_registry_duplicate_detection_survives_mixed_canonical_form`
    /// guards against at the outer level.
    #[test]
    fn ct1_5a_normalize_recurses_into_forall_constraints() {
        let mut type_def_module: BTreeMap<String, String> = BTreeMap::new();
        type_def_module.insert("MyInt".to_string(), "other".to_string());

        // Forall a. (TShow MyInt) => a -> a
        // The constraint's type carries a bare `MyInt` that should be
        // rewritten to `other.MyInt`.
        let input = Type::Forall {
            vars: vec!["a".to_string()],
            constraints: vec![crate::ast::Constraint {
                class: "TShow".to_string(),
                type_: Type::Con {
                    name: "MyInt".to_string(),
                    args: vec![],
                },
            }],
            body: Box::new(Type::Fn {
                params: vec![Type::Var { name: "a".to_string() }],
                param_modes: vec![],
                ret: Box::new(Type::Var { name: "a".to_string() }),
                ret_mode: Default::default(),
                effects: vec![],
            }),
        };

        let out = normalize_type_for_registry(&input, &type_def_module);

        match out {
            Type::Forall { constraints, .. } => {
                assert_eq!(constraints.len(), 1);
                match &constraints[0].type_ {
                    Type::Con { name, .. } => {
                        assert_eq!(
                            name, "other.MyInt",
                            "constraint type was not normalised; got {name}"
                        );
                    }
                    other => panic!("expected Type::Con, got {other:?}"),
                }
            }
            other => panic!("expected Type::Forall, got {other:?}"),
        }
    }

    /// ct.1: a qualified `Constraint.class` nested inside a
    /// `ClassDef.methods[].ty.Forall.constraints` must fire
    /// `QualifiedClassName`. Distinct from the `Def::Fn` site: the
    /// `Def::Class` branch of `check_class_name_fields` has its own
    /// per-method Forall walk that needs independent coverage.
    #[test]
    fn ct1_validator_rejects_qualified_constraint_class_in_classdef_method() {
        let m: Module = serde_json::from_value(serde_json::json!({
            "schema": crate::SCHEMA,
            "name": "m",
            "imports": [],
            "defs": [{
                "kind": "class",
                "name": "Foo",
                "param": "a",
                "methods": [{
                    "name": "m",
                    "type": {
                        "k": "forall",
                        "vars": ["b"],
                        "constraints": [
                            { "class": "other.MyEq", "type": { "k": "var", "name": "b" } }
                        ],
                        "body": {
                            "k": "fn",
                            "params": [{ "k": "var", "name": "b" }],
                            "ret": { "k": "con", "name": "Unit" },
                            "effects": []
                        }
                    }
                }]
            }],
        })).unwrap();
        let mut modules = BTreeMap::new();
        modules.insert("m".to_string(), m);
        let err = validate_canonical_type_names(&modules)
            .expect_err("qualified Constraint.class in ClassDef-method Forall 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:?}"),
        }
    }

    /// 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:?}"),
        }
    }
}