//! Iter 22b.2 typeclass typecheck arms — integration tests.
//!
//! This file is shared by 22b.2 tasks: it exists from Task 8
//! (class methods register into module globals) and is extended by
//! Tasks 9 (`missing-constraint`) and 10 (`no-instance`).

use ailang_core::ast::Type;
use std::path::{Path, PathBuf};

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

/// Property protected: a class method declared in a `Def::Class` must be
/// reachable as a name in the module's `ModuleGlobals` so that pass-2
/// (`Term::Var { name: "show" }`) does not fire `unbound-var` for
/// well-formed class-method calls. The lookup must remember which class
/// the method belongs to so Task 9 can build the residual constraint at
/// the call site.
#[test]
fn class_method_is_in_module_globals() {
    let entry = examples_dir().join("test_22b2_class_method_lookup.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace must load");
    let globals = ailang_check::build_module_globals(&ws)
        .expect("globals build");
    let mod_globals = globals
        .get("test_22b2_class_method_lookup")
        .expect("module globals present");
    assert!(
        mod_globals.has_class_method("show"),
        "class method `show` must appear in module globals"
    );
    assert_eq!(
        mod_globals.class_method_class("show"),
        Some("Show"),
        "class method `show` must remember its class is `Show`"
    );
}

/// Property protected: the registered `ClassMethodEntry` carries the
/// full metadata Tasks 9 / 10 need — the defining module (so the
/// typecheck arms can find the matching `Registry` entries) and the
/// declared method signature (so a residual class constraint can be
/// built by instantiating the class param at the call site). The
/// fixture declares `class Show a { show: a -> Str }`, so the
/// recovered `method_ty` must be exactly `Type::Var "a" -> Type::Con
/// "Str"` with empty effects.
#[test]
fn class_method_entry_carries_full_metadata() {
    let entry = examples_dir().join("test_22b2_class_method_lookup.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace must load");
    let globals = ailang_check::build_module_globals(&ws)
        .expect("globals build");
    let mod_globals = globals
        .get("test_22b2_class_method_lookup")
        .expect("module globals present");
    let cm_entry = mod_globals
        .class_method("show")
        .expect("class method `show` must be registered");

    assert_eq!(
        cm_entry.defining_module, "test_22b2_class_method_lookup",
        "defining_module must point at the module that declared the class"
    );
    assert_eq!(
        cm_entry.class_param, "a",
        "class_param must be the class's single type parameter name"
    );

    match &cm_entry.method_ty {
        Type::Fn {
            params,
            ret,
            effects,
            ..
        } => {
            assert_eq!(
                params.len(),
                1,
                "method `show` must have exactly one parameter"
            );
            match &params[0] {
                Type::Var { name } => assert_eq!(
                    name, "a",
                    "param type must be the class param `a`, not `{}`",
                    name
                ),
                other => panic!(
                    "param type must be `Type::Var \"a\"`, got {:?}",
                    other
                ),
            }
            match ret.as_ref() {
                Type::Con { name, args } => {
                    assert_eq!(
                        name, "Str",
                        "return type must be `Str`, got `{}`",
                        name
                    );
                    assert!(
                        args.is_empty(),
                        "return type `Str` must take no args"
                    );
                }
                other => panic!(
                    "return type must be `Type::Con \"Str\"`, got {:?}",
                    other
                ),
            }
            assert!(
                effects.is_empty(),
                "method `show` must have empty effects, got {:?}",
                effects
            );
        }
        other => panic!(
            "method_ty must be `Type::Fn`, got {:?}",
            other
        ),
    }
}

/// Property protected: a polymorphic FnDef that calls a class method
/// (e.g. `show x` where `x: a`) but does not declare the matching class
/// constraint in its `Forall.constraints` MUST receive a
/// `missing-constraint` diagnostic. This is the principal soundness
/// guarantee of class-method calls inside polymorphic functions: every
/// dispatch point at a polymorphic type must be backed by an in-scope
/// constraint that the caller will eventually have to satisfy. Without
/// this check, monomorphisation in 22b.3 would have no way to know
/// which dictionary to thread.
#[test]
fn fn_calling_class_method_without_declared_constraint_fires_missing_constraint() {
    let entry = examples_dir().join("test_22b2_missing_constraint.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.iter().any(|d| d.code == "missing-constraint"),
        "expected missing-constraint; got: {:?}",
        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
    );
}

/// Property protected: when a polymorphic FnDef declares the matching
/// class constraint in its `Forall.constraints`, the call to the class
/// method typechecks clean — the residual constraint produced at the
/// call site is satisfied by the in-scope declared constraint, and no
/// diagnostic fires. This is the positive counterpart to the
/// missing-constraint check: declaring `Show a =>` makes `show x`
/// well-formed inside the body.
#[test]
fn fn_with_correct_constraint_typechecks_green() {
    let entry = examples_dir().join("test_22b2_constraint_declared.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.is_empty(),
        "expected no diagnostics; got: {:?}",
        diagnostics
    );
}

/// Property protected: superclass-walk in `expand_declared_constraints`
/// covers the residual class produced by calling a superclass's method
/// from within a function constrained on the subclass. Concretely: the
/// fn declares `Ord a =>` and calls `eq` (an `Eq` method); the residual
/// `(Eq, a)` is satisfied because `Ord` extends `Eq`, so the expanded
/// declared set must include `(Eq, a)`. Without the superclass walk the
/// fn would spuriously fire `missing-constraint`. This is the positive
/// fixture for Decision 11's one-step superclass closure.
#[test]
fn fn_calling_superclass_method_via_subclass_constraint_typechecks_green() {
    let entry = examples_dir()
        .join("test_22b2_constraint_declared_via_superclass.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.is_empty(),
        "expected no diagnostics; superclass walk should have covered Eq via Ord; got: {:?}",
        diagnostics
    );
}

/// Property protected: the superclass walk goes from subclass to
/// superclass only — never the other direction. A fn that declares
/// `Eq a =>` and calls `lt` (an `Ord` method) must still fire
/// `missing-constraint` because `Ord` is a *sub*class of `Eq`, not a
/// superclass; the declared `(Eq, a)` does not cover the residual
/// `(Ord, a)`. Without this asymmetry, declaring the superclass would
/// spuriously satisfy any subclass residual.
#[test]
fn fn_with_superclass_constraint_calling_subclass_method_fires_missing_constraint() {
    let entry = examples_dir()
        .join("test_22b2_missing_constraint_subclass.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.iter().any(|d| d.code == "missing-constraint"),
        "expected missing-constraint; superclass walk should NOT cover sub-direction; got: {:?}",
        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
    );
}

/// Property protected: a (monomorphic) fn that calls a class method at a
/// fully-concrete type for which no `instance C T` exists in the workspace
/// MUST receive a `no-instance` diagnostic. This is the dual of
/// `missing-constraint`: when the residual class constraint resolves to a
/// concrete type, the fn cannot push the obligation to a caller via a
/// `Forall.constraints` annotation — it can only be discharged by an
/// existing instance. Without this check, monomorphisation in 22b.3 would
/// have nothing to specialise to. Fixture: `main` calls `show 42` (so the
/// residual is `(Show, Int)`) without any `instance Show Int` declared in
/// the workspace.
#[test]
fn fn_calling_class_method_at_type_without_instance_fires_no_instance() {
    let entry = examples_dir().join("test_22b2_no_instance.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.iter().any(|d| d.code == "no-instance"),
        "expected no-instance; got: {:?}",
        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
    );
}

/// Property protected: the positive counterpart to `no-instance` — when a
/// monomorphic fn calls a class method at a fully-concrete type AND a
/// matching `instance C T` exists in the workspace, the call typechecks
/// green. The concrete-residual path must look up `(class, type_hash(T))`
/// in `env.workspace_registry` and find a hit, so no diagnostic fires.
/// This guards against registry-keying or threading bugs that would
/// otherwise sneak past the negative-only test: a registry that is empty
/// at typecheck time, or keyed under the wrong shape, would silently fire
/// `no-instance` even when the instance is present. Fixture: `main` calls
/// `show 42` with `instance Show Int` declared in the same workspace.
#[test]
fn fn_calling_class_method_at_type_with_instance_typechecks_green() {
    let entry = examples_dir().join("test_22b2_instance_present.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.is_empty(),
        "expected no diagnostics — instance Show Int is present, registry lookup must hit; got: {:?}",
        diagnostics
    );
}

/// Property protected: class-method symbols declared in module A are
/// reachable from a fn in module B that imports A — i.e. the workspace-
/// wide merge of `module_globals.class_methods` into `Env.class_methods`
/// (per `check_in_workspace`) is what call-site resolution actually
/// consults. Without this merge, a `Term::Var { name: "show" }` in B would
/// fire `unbound-var`. The discriminator: when B's `main` calls `show 42`
/// at a fully-concrete type and A has NO matching instance, the diagnostic
/// must be `no-instance` (proving the class method resolved cross-module),
/// NOT `unbound-var` (which would mean cross-module class-method lookup
/// failed silently). Fixture: A = `test_22b2_xmod_classmod_noinst` declares
/// `class Show a`; B = `test_22b2_xmod_no_instance` calls `show 42`.
#[test]
fn cross_module_class_method_resolves_and_fires_no_instance() {
    let entry = examples_dir().join("test_22b2_xmod_no_instance.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    let codes: Vec<&str> = diagnostics.iter().map(|d| d.code.as_str()).collect();
    assert!(
        codes.contains(&"no-instance"),
        "expected no-instance (proving cross-module class-method resolution); got: {:?}",
        codes
    );
    assert!(
        !codes.contains(&"unbound-var"),
        "must NOT fire unbound-var — class method `show` from module A is in scope in module B; got: {:?}",
        codes
    );
}

/// Property protected: a polymorphic fn in module B calling a class method
/// declared in module A (without declaring the matching constraint) MUST
/// fire `missing-constraint`. This pins the cross-module class-superclass
/// expansion path: B's `Forall.constraints` is empty, A's `class Show a`
/// is in `Env.class_methods` via the workspace merge, and the residual
/// `(Show, a)` collected at the `show x` call site must reach `check_fn`'s
/// missing-constraint arm. Without the cross-module merge, the call would
/// produce `unbound-var`; with the merge but a broken superclass-table
/// merge, the residual could be spuriously satisfied. Fixture: A =
/// `test_22b2_xmod_classmod_noinst`; B = `test_22b2_xmod_missing_constraint`
/// declares `forall a. (a) -> Str` and calls `show x`.
#[test]
fn cross_module_polymorphic_fn_without_constraint_fires_missing_constraint() {
    let entry = examples_dir().join("test_22b2_xmod_missing_constraint.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.iter().any(|d| d.code == "missing-constraint"),
        "expected missing-constraint across modules; got: {:?}",
        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
    );
}

/// Property protected: cross-module instance lookup for the no-instance
/// arm. Module A declares `class Show a` AND `instance Show Int`; module
/// B imports A and calls `show 42`. The call must typecheck clean — the
/// workspace registry built at load time over all modules must include A's
/// `instance Show Int`, and B's `check_fn` must find it under
/// `(class="Show", type_hash(Int))`. Without cross-module registry
/// population, B would spuriously fire `no-instance` at a type for which
/// an instance demonstrably exists. Fixture: A =
/// `test_22b2_xmod_classmod`; B = `test_22b2_xmod_instance_present`.
#[test]
fn cross_module_instance_satisfies_concrete_call() {
    let entry = examples_dir().join("test_22b2_xmod_instance_present.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    assert!(
        diagnostics.is_empty(),
        "expected clean typecheck — A's instance Show Int must be in the workspace registry visible from B; got: {:?}",
        diagnostics
    );
}

/// Property protected: `check_workspace` aggregates diagnostics across
/// distinct fns rather than stopping at the first failing fn. When two
/// independent polymorphic fns each call `show x` without declaring `Show
/// a`, the resulting diagnostic vec must contain TWO `missing-constraint`
/// entries — one per fn — with the right `def` field on each. Without
/// per-def aggregation in the `for def in &m.defs` loop of
/// `check_in_workspace`, an editor consuming the diagnostics list would
/// see only the first failure, hiding the second from the author until
/// the first is fixed. Fixture has `describe_first` and `describe_second`,
/// both ill-formed in the same way; both must surface.
#[test]
fn two_fns_each_missing_constraint_produce_two_diagnostics() {
    let entry = examples_dir().join("test_22b2_two_fns_missing_constraint.ail.json");
    let ws = ailang_core::workspace::load_workspace(&entry)
        .expect("workspace loads");
    let diagnostics = ailang_check::check_workspace(&ws);
    let mc: Vec<&ailang_check::Diagnostic> = diagnostics
        .iter()
        .filter(|d| d.code == "missing-constraint")
        .collect();
    assert_eq!(
        mc.len(),
        2,
        "expected two missing-constraint diagnostics (one per fn); got: {:?}",
        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
    );
    let defs: std::collections::BTreeSet<&str> = mc
        .iter()
        .filter_map(|d| d.def.as_deref())
        .collect();
    assert!(
        defs.contains("describe_first"),
        "expected diagnostic for `describe_first`; got defs: {:?}",
        defs
    );
    assert!(
        defs.contains("describe_second"),
        "expected diagnostic for `describe_second`; got defs: {:?}",
        defs
    );
}
