// ============================================================================
// Phase A — Bundle 2 — A2 Verification
//
// Nominal types are distinct from their wrapped representations at the
// typechecker level. No new code in pfcl-typechecker is required — these
// tests prove that the existing `Type::Con(name, args)` discrimination
// already gives us nominal-type semantics for free.
//
// What these tests prove:
//
//   1. `Type::Con("Celsius", [])` ≠ `Type::Con("Float", [])` under unify
//      (Mismatch error), even though Celsius wraps Float at the catalog
//      level.
//   2. Two nominal types over the same representation (Celsius vs.
//      Fahrenheit, both wrapping Float) are distinct under unify.
//   3. `Type::Con("Celsius", [])` unifies with `Type::Var(?)` and binds
//      the var to Celsius — nominal types are first-class in the
//      polymorphic vocabulary.
//   4. Parametric nominal types (`Tagged<Bytes, EdPubKey>` vs
//      `Tagged<Bytes, X25519PubKey>`) are distinct: the phantom tag
//      argument carries through unification.
//   5. PartialEq derive on `Type` agrees with unify on identity.
//
// Reference: `Nominal_Types_Design.md` §4 Rule N1 (construction is
// explicit) and Rule N7 (synthesis respects nominal identity).
// ============================================================================

use pfcl_typechecker::types::{Type, TypeVar};
use pfcl_typechecker::unify::{unify, TypeErrorKind};

// ---------------------------------------------------------------------------
// Helper: build named nominal types as `Type::Con(name, [])`.
//
// At the typechecker level we don't carry the `wraps` relationship — it's
// erased. A nominal type's representation in `Type` is just its name.
// The catalog's nominal-type registry knows the wrap relationship
// separately (used by lint Pass 10 once it ships).
// ---------------------------------------------------------------------------

fn nominal(name: &str) -> Type {
    Type::Con(name.to_string(), Vec::new())
}

fn tagged(repr: Type, phantom: Type) -> Type {
    // The parametric nominal `Tagged<a, k>` instantiated with concrete `a`
    // and `k`. Modeled as `Type::Con("Tagged", [a, k])`.
    Type::Con("Tagged".to_string(), vec![repr, phantom])
}

// ---------------------------------------------------------------------------
// 1. Celsius is distinct from Float
// ---------------------------------------------------------------------------

#[test]
fn celsius_does_not_unify_with_float() {
    let celsius = nominal("Celsius");
    let float = Type::float();
    let err = unify(&celsius, &float).expect_err(
        "Celsius (wraps Float) must NOT unify with bare Float — nominal types are distinct",
    );
    match err.kind {
        TypeErrorKind::Mismatch { expected, actual } => {
            // The error reports a mismatch between exactly the two types
            // we tried to unify, with names preserved.
            assert_eq!(expected, celsius);
            assert_eq!(actual, float);
        }
        other => panic!("expected Mismatch error, got {:?}", other),
    }
}

#[test]
fn float_does_not_unify_with_celsius_either_direction() {
    // Unify is symmetric for this case — order shouldn't matter.
    let celsius = nominal("Celsius");
    let float = Type::float();
    assert!(unify(&float, &celsius).is_err());
    assert!(unify(&celsius, &float).is_err());
}

// ---------------------------------------------------------------------------
// 2. Celsius is distinct from Fahrenheit (both wrap Float)
// ---------------------------------------------------------------------------

#[test]
fn celsius_does_not_unify_with_fahrenheit() {
    // The canonical synthesis-precision test: two nominal types over
    // identical underlying representation must remain distinct.
    let celsius = nominal("Celsius");
    let fahrenheit = nominal("Fahrenheit");
    let err = unify(&celsius, &fahrenheit).expect_err(
        "Celsius and Fahrenheit must NOT unify — both wrap Float but are nominally distinct",
    );
    match err.kind {
        TypeErrorKind::Mismatch { .. } => {}
        other => panic!("expected Mismatch error, got {:?}", other),
    }
}

#[test]
fn many_pairwise_unit_distinctness() {
    // Smoke-test a wider net to prove the discrimination scales.
    let unit_names = [
        "Celsius",
        "Fahrenheit",
        "Kelvin",
        "Meters",
        "Feet",
        "Kilograms",
        "Pounds",
        "Seconds",
    ];
    for (i, a) in unit_names.iter().enumerate() {
        for b in unit_names.iter().skip(i + 1) {
            let ta = nominal(a);
            let tb = nominal(b);
            assert!(
                unify(&ta, &tb).is_err(),
                "{} should not unify with {}",
                a,
                b
            );
        }
    }
}

// ---------------------------------------------------------------------------
// 3. Same-name nominal types unify reflexively (Rule N3)
// ---------------------------------------------------------------------------

#[test]
fn celsius_unifies_with_celsius() {
    let c1 = nominal("Celsius");
    let c2 = nominal("Celsius");
    let subst = unify(&c1, &c2).expect("identical nominal types must unify");
    // Identity-unification yields the empty substitution.
    assert!(subst.is_empty());
}

#[test]
fn t_to_t_composes_freely_for_same_nominal() {
    // Rule N3 from the design doc: `T → T` composes with another `T → T`.
    // Models that by unifying two function types of the same nominal arrow.
    let arr1 = Type::fun1(nominal("Celsius"), nominal("Celsius"));
    let arr2 = Type::fun1(nominal("Celsius"), nominal("Celsius"));
    let subst = unify(&arr1, &arr2).expect("identical T→T arrows must unify");
    assert!(subst.is_empty());
}

#[test]
fn cross_nominal_arrows_do_not_unify() {
    // Rule N4: `Celsius → Float` must not unify with `Fahrenheit → Float`.
    // The mismatch happens in the input position.
    let to_float_from_c = Type::fun1(nominal("Celsius"), Type::float());
    let to_float_from_f = Type::fun1(nominal("Fahrenheit"), Type::float());
    assert!(unify(&to_float_from_c, &to_float_from_f).is_err());
}

// ---------------------------------------------------------------------------
// 4. Nominal types bind type variables (parametric machinery is intact)
// ---------------------------------------------------------------------------

#[test]
fn type_var_binds_to_celsius() {
    // A type variable can be bound to a nominal type, just like to any
    // other Type::Con. This is the polymorphic-substitution case relied
    // on by `List<a>` instantiated with `a = Celsius`.
    let a = TypeVar(0);
    let var = Type::Var(a);
    let celsius = nominal("Celsius");
    let subst = unify(&var, &celsius).expect("type var must unify with nominal type");
    assert_eq!(subst.lookup(a), Some(&celsius));
}

#[test]
fn type_var_binds_to_celsius_right_side_too() {
    // Variable on the right (the other branch of unify).
    let a = TypeVar(0);
    let var = Type::Var(a);
    let celsius = nominal("Celsius");
    let subst = unify(&celsius, &var).expect("nominal-then-var must still unify");
    assert_eq!(subst.lookup(a), Some(&celsius));
}

#[test]
fn list_of_a_instantiates_to_list_of_celsius() {
    // `List<a>` unified with `List<Celsius>` must bind `a := Celsius`.
    let a = TypeVar(7);
    let list_a = Type::list(Type::Var(a));
    let list_celsius = Type::list(nominal("Celsius"));
    let subst = unify(&list_a, &list_celsius).expect("List<a> must unify with List<Celsius>");
    assert_eq!(subst.lookup(a), Some(&nominal("Celsius")));
}

// ---------------------------------------------------------------------------
// 5. Parametric nominal: Tagged<a, k> with phantom tag
// ---------------------------------------------------------------------------

#[test]
fn ed25519_public_key_distinct_from_x25519_public_key() {
    // The OQ-6 security-correctness case. Both expand to
    // `Tagged<Bytes, K>` but with different K — Ed25519PubKey vs
    // X25519PubKey. The type-system rejects mixing them.
    let ed = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("EdPubKey"));
    let x = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("X25519PubKey"));
    let err = unify(&ed, &x).expect_err(
        "Tagged<Bytes, EdPubKey> must NOT unify with Tagged<Bytes, X25519PubKey> — \
         the phantom tag is type-level evidence of which algorithm the bytes belong to",
    );
    match err.kind {
        TypeErrorKind::Mismatch { .. } => {}
        other => panic!("expected Mismatch on phantom-tag divergence, got {:?}", other),
    }
}

#[test]
fn ed25519_public_key_same_as_ed25519_public_key() {
    let ed1 = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("EdPubKey"));
    let ed2 = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("EdPubKey"));
    let subst = unify(&ed1, &ed2).expect("identical Tagged<...> types must unify");
    assert!(subst.is_empty());
}

#[test]
fn tagged_a_k_instantiates_with_concrete_args() {
    // `Tagged<a, k>` unified with `Tagged<Bytes, EdPubKey>` must bind
    // a := Bytes and k := EdPubKey. This is the parametric-nominal
    // instantiation case the design doc §11 (OQ-NT.5) discusses.
    let a = TypeVar(0);
    let k = TypeVar(1);
    let abstract_tagged = tagged(Type::Var(a), Type::Var(k));
    let concrete_tagged = tagged(
        Type::Con("Bytes".to_string(), vec![]),
        nominal("EdPubKey"),
    );
    let subst = unify(&abstract_tagged, &concrete_tagged)
        .expect("Tagged<a, k> must unify with Tagged<Bytes, EdPubKey>");
    assert_eq!(
        subst.lookup(a),
        Some(&Type::Con("Bytes".to_string(), vec![]))
    );
    assert_eq!(subst.lookup(k), Some(&nominal("EdPubKey")));
}

// ---------------------------------------------------------------------------
// 6. PartialEq agrees with unify on identity
// ---------------------------------------------------------------------------

#[test]
fn partial_eq_distinguishes_nominal_types_by_name() {
    // The derived PartialEq on `Type` is what synthesis uses for direct
    // type comparison (e.g. type-index keys). It must agree with unify
    // on whether two nominal types are "the same".
    assert_ne!(nominal("Celsius"), nominal("Fahrenheit"));
    assert_ne!(nominal("Celsius"), Type::float());
    assert_eq!(nominal("Celsius"), nominal("Celsius"));

    // And for the parametric case:
    let ed = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("EdPubKey"));
    let x = tagged(Type::Con("Bytes".to_string(), vec![]), nominal("X25519PubKey"));
    assert_ne!(ed, x);
}

// ---------------------------------------------------------------------------
// 7. Negative control: nominal vs structural error reporting
// ---------------------------------------------------------------------------

#[test]
fn mismatch_error_carries_the_actual_nominal_names() {
    // The error path matters for the human-readable gap report. The
    // mismatch should name the two distinct nominal types — not collapse
    // them to "two Floats".
    let celsius = nominal("Celsius");
    let fahrenheit = nominal("Fahrenheit");
    let err = unify(&celsius, &fahrenheit).unwrap_err();
    match err.kind {
        TypeErrorKind::Mismatch { expected, actual } => {
            // The names must be carried through verbatim.
            if let (Type::Con(n1, _), Type::Con(n2, _)) = (&expected, &actual) {
                assert_eq!(n1, "Celsius");
                assert_eq!(n2, "Fahrenheit");
            } else {
                panic!(
                    "expected Mismatch between two Type::Con, got expected={:?} actual={:?}",
                    expected, actual
                );
            }
        }
        other => panic!("expected Mismatch error, got {:?}", other),
    }
}
