//! Type unification with occurs check.
//!
//! This module implements the unification algorithm for Hindley-Milner
//! type inference. Unification finds a substitution that makes two types
//! equal, or reports an error if no such substitution exists.
//!
//! ## Algorithm
//!
//! Unification proceeds recursively:
//!
//! 1. Apply current substitution to both types
//! 2. Try to reduce type family applications
//! 3. If both are variables with same ID, succeed
//! 4. If one is a variable, bind it (with occurs check)
//! 5. If both are constructors/functions, unify components
//! 6. Otherwise, report mismatch
//!
//! ## Occurs Check
//!
//! The occurs check prevents infinite types. Before binding a variable
//! `a` to a type `t`, we verify that `a` does not appear in `t`.
//!
//! ## Type Family Reduction
//!
//! When encountering a type that looks like a type family application
//! (e.g., `Elem [Int]`), we try to reduce it using the instance definitions
//! before unification proceeds.
//!
//! ## M9 Dependent Types
//!
//! This module extends unification to handle type-level naturals (`TyNat`)
//! and type-level lists (`TyList`) for shape-indexed tensors.
//!
//! ## Type Aliases
//!
//! String is a type alias for [Char] in Haskell, so we handle this
//! equivalence during unification.

use bhc_intern::Symbol;
use bhc_span::Span;
use bhc_types::{Kind, Scheme, Ty, TyCon, TyList, TyNat, TyVar};

use crate::context::TyCtxt;
use crate::diagnostics;
use crate::nat_solver::{NatConstraint, NatSolver};

/// Try to expand a user-defined type alias.
///
/// Given a type like `Fallible Int` where `type Fallible a = Either Failure a`,
/// this collects the applied arguments, matches them against the alias parameters,
/// and returns the expanded type `Either Failure Int`.
///
/// Works for:
/// - `Ty::Con("Fallible")` with 0 args applied so far (if alias has 0 params)
/// - `Ty::App(Ty::Con("Fallible"), arg)` for 1-param aliases
/// - Nested `Ty::App` for multi-param aliases
fn try_expand_type_alias(ctx: &TyCtxt, ty: &Ty) -> Option<Ty> {
    // Extract the head type constructor name and collected arguments.
    let (head_name, args) = collect_type_app(ty);
    let head_sym = match &head_name {
        Ty::Con(c) => c.name,
        _ => return None,
    };

    // Look up in user-defined type aliases
    // Try both the full name and the unqualified name (strip module qualifier)
    let (params, rhs) = ctx.type_aliases.get(&head_sym).or_else(|| {
        let name_str = head_sym.as_str();
        if let Some(pos) = name_str.rfind('.') {
            let unqualified = &name_str[pos + 1..];
            ctx.type_aliases.get(&Symbol::intern(unqualified))
        } else {
            None
        }
    })?;

    // We can expand if we have at least as many args as params.
    // Extra args are applied to the result (partial application is fine).
    if args.len() < params.len() {
        // Under-saturated alias application — can't expand yet
        return None;
    }

    // Substitute params with args in the RHS
    let mut expanded = rhs.clone();
    for (param, arg) in params.iter().zip(args.iter()) {
        expanded = subst_tyvar(&expanded, param.id, arg);
    }

    // If there are extra args beyond the alias params, apply them
    for arg in args.iter().skip(params.len()) {
        expanded = Ty::App(Box::new(expanded), Box::new(arg.clone()));
    }

    Some(expanded)
}

/// Collect a type application spine: `App(App(Con(F), a), b)` → `(Con(F), [a, b])`.
fn collect_type_app(ty: &Ty) -> (Ty, Vec<Ty>) {
    let mut args = Vec::new();
    let mut current = ty;
    loop {
        match current {
            Ty::App(f, a) => {
                args.push((**a).clone());
                current = f;
            }
            _ => {
                args.reverse();
                return (current.clone(), args);
            }
        }
    }
}

/// Substitute a type variable (by id) with a replacement type throughout a type.
fn subst_tyvar(ty: &Ty, var_id: u32, replacement: &Ty) -> Ty {
    match ty {
        Ty::Var(v) if v.id == var_id => replacement.clone(),
        Ty::Var(_) | Ty::Con(_) | Ty::Prim(_) | Ty::Error => ty.clone(),
        Ty::App(f, a) => Ty::App(
            Box::new(subst_tyvar(f, var_id, replacement)),
            Box::new(subst_tyvar(a, var_id, replacement)),
        ),
        Ty::Fun(from, to) => Ty::Fun(
            Box::new(subst_tyvar(from, var_id, replacement)),
            Box::new(subst_tyvar(to, var_id, replacement)),
        ),
        Ty::Tuple(elems) => Ty::Tuple(
            elems
                .iter()
                .map(|e| subst_tyvar(e, var_id, replacement))
                .collect(),
        ),
        Ty::List(elem) => Ty::List(Box::new(subst_tyvar(elem, var_id, replacement))),
        Ty::Forall(vars, body) => {
            // Don't substitute if the var is shadowed by the forall
            if vars.iter().any(|v| v.id == var_id) {
                ty.clone()
            } else {
                Ty::Forall(
                    vars.clone(),
                    Box::new(subst_tyvar(body, var_id, replacement)),
                )
            }
        }
        Ty::Nat(_) | Ty::TyList(_) => ty.clone(),
    }
}

/// Check if a type is the String type constructor (or FilePath alias).
fn is_string_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if matches!(c.name.as_str(), "String" | "FilePath"))
}

/// Check if a type is the Text type constructor (or common Text aliases).
fn is_text_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if matches!(normalize_qualified_tyname(c.name.as_str()),
        "Text" | "MimeType" | "Extension" | "NameSpaceIRI" | "Attr" | "Tag"))
}

/// Check if a type is the Dimension type constructor (XMonad type alias).
fn is_dimension_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if c.name.as_str() == "Dimension")
}

/// Check if a type is the WorkspaceId type constructor (XMonad type alias).
fn is_workspaceid_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if c.name.as_str() == "WorkspaceId")
}

/// Check if a type is the D type constructor (XMonad type alias for (Int, Int)).
fn is_d_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if c.name.as_str() == "D")
}

/// Check if a type is the Position type constructor (XMonad type alias for Int).
fn is_position_con(ty: &Ty) -> bool {
    matches!(ty, Ty::Con(c) if c.name.as_str() == "Position")
}

/// Normalize a qualified type name to its canonical unqualified form.
/// E.g., "T.Text" -> "Text", "BL.ByteString" -> "ByteString", "M.Map" -> "Map"
fn normalize_qualified_tyname(name: &str) -> &str {
    // If the name contains a dot and the part before the dot looks like a
    // module qualifier (starts with uppercase or is a common abbreviation),
    // return just the part after the last dot.
    if let Some(dot_pos) = name.rfind('.') {
        let qualifier = &name[..dot_pos];
        let base = &name[dot_pos + 1..];
        // Only strip if qualifier looks like a module alias (e.g., T, BL, M, Set, Map, etc.)
        if !qualifier.is_empty() && !base.is_empty() {
            return base;
        }
    }
    name
}

/// Check if two type names refer to the same type, accounting for qualified aliases.
/// E.g., "T.Text" and "Text" are the same, "B.ByteString" and "ByteString" are the same.
fn same_type_name(name1: &str, name2: &str) -> bool {
    if name1 == name2 {
        return true;
    }
    normalize_qualified_tyname(name1) == normalize_qualified_tyname(name2)
}

/// Get the element type of a list, if this is a list type.
fn get_list_elem(ty: &Ty) -> Option<&Ty> {
    match ty {
        Ty::List(elem) => Some(elem.as_ref()),
        _ => None,
    }
}

/// Get the Char type constructor.
fn char_ty() -> Ty {
    use bhc_intern::Symbol;
    use bhc_types::Kind;
    Ty::Con(TyCon::new(Symbol::intern("Char"), Kind::Star))
}

/// Get the Int type constructor.
fn int_ty() -> Ty {
    use bhc_intern::Symbol;
    use bhc_types::Kind;
    Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star))
}

/// Check if two type constructor names are compatible type aliases.
/// Returns true if they both resolve to the same underlying type.
fn are_compatible_type_aliases(name1: &str, name2: &str) -> bool {
    // First, check if they're the same type after normalizing qualified names.
    // E.g., "T.Text" and "Text" should be the same type.
    if same_type_name(name1, name2) {
        return true;
    }

    // Normalize before checking alias groups
    let n1 = normalize_qualified_tyname(name1);
    let n2 = normalize_qualified_tyname(name2);

    // Type aliases for Int
    const INT_ALIASES: &[&str] = &[
        "Int",
        "Dimension",
        "Position",
        "KeyMask",
        "Window",
        "ScreenId",
        "Handle",
    ];

    // Type aliases for String
    const STRING_ALIASES: &[&str] = &["String", "FilePath", "WorkspaceId"];

    // Type aliases for Text
    const TEXT_ALIASES: &[&str] = &[
        "Text",
        "MimeType",
        "Extension",
        "NameSpaceIRI",
        "Attr",
        "Tag",
    ];

    // Check if both are Int aliases
    let is_int1 = INT_ALIASES.contains(&n1);
    let is_int2 = INT_ALIASES.contains(&n2);
    if is_int1 && is_int2 {
        return true;
    }

    // Check if both are String aliases
    let is_str1 = STRING_ALIASES.contains(&n1);
    let is_str2 = STRING_ALIASES.contains(&n2);
    if is_str1 && is_str2 {
        return true;
    }

    // Check if both are Text aliases
    let is_text1 = TEXT_ALIASES.contains(&n1);
    let is_text2 = TEXT_ALIASES.contains(&n2);
    if is_text1 && is_text2 {
        return true;
    }

    // Integer and Int should be compatible in check mode
    let is_integer_like = |s: &str| {
        matches!(
            s,
            "Int"
                | "Integer"
                | "Word"
                | "Int64"
                | "Word8"
                | "Word16"
                | "Word32"
                | "Word64"
                | "Int8"
                | "Int16"
                | "Int32"
                | "CInt"
                | "CSize"
        )
    };
    if is_integer_like(n1) && is_integer_like(n2) {
        return true;
    }

    // Float/Double should be compatible
    let is_float_like =
        |s: &str| matches!(s, "Float" | "Double" | "CDouble" | "CFloat" | "Rational");
    if is_float_like(n1) && is_float_like(n2) {
        return true;
    }

    false
}

/// Try to reduce a type if it looks like a type family application.
///
/// A type family application has the form `F a b c ...` where `F` is
/// the name of an associated type defined in some class. If we can find
/// a matching instance, we reduce to the RHS of the type family definition.
///
/// For example, given:
/// ```haskell
/// class Collection c where
///   type Elem c
///
/// instance Collection [a] where
///   type Elem [a] = a
/// ```
///
/// Then `Elem [Int]` reduces to `Int`.
fn try_reduce_type_family(ctx: &TyCtxt, ty: &Ty) -> Ty {
    // Extract the type constructor name and arguments from the type.
    // A type family application looks like: App(App(Con(name), arg1), arg2)...
    let (family_name, args) = match extract_type_family_app(ty) {
        Some((name, args)) => (name, args),
        None => return ty.clone(),
    };

    // Try to reduce using the type environment
    match ctx.env.reduce_type_family(family_name, &args) {
        Some(reduced) => {
            // Successfully reduced! Apply the current substitution to the result
            // and recursively try to reduce further.
            let reduced = ctx.apply_subst(&reduced);
            try_reduce_type_family(ctx, &reduced)
        }
        None => ty.clone(),
    }
}

/// Check if a type is an unreducible type family application.
///
/// Returns `Some((name, args, class_name))` if the type looks like a type family
/// application that we couldn't reduce. The class_name is the class that defines
/// this associated type, if found.
fn check_unreduced_type_family(ctx: &TyCtxt, ty: &Ty) -> Option<(Symbol, Vec<Ty>, Option<Symbol>)> {
    let (name, args) = extract_type_family_app(ty)?;

    // Check if this is actually a type family (not just a regular type application)
    let class_info = ctx.env.lookup_assoc_type(name);

    if class_info.is_some() {
        // This is a type family - check if it could be reduced
        if ctx.env.reduce_type_family(name, &args).is_none() {
            // Couldn't reduce - this is an unreduced type family
            let class_name = class_info.map(|(ci, _)| ci.name);
            return Some((name, args, class_name));
        }
    }

    None
}

/// Extract the type constructor name and arguments from a potential type family application.
///
/// Returns `Some((name, args))` if the type is of the form `Con(name) arg1 arg2 ...`.
/// Returns `None` if the type is not a type application with a constructor at the head.
fn extract_type_family_app(ty: &Ty) -> Option<(Symbol, Vec<Ty>)> {
    let mut current = ty;
    let mut args = Vec::new();

    // Walk through nested applications to collect arguments
    loop {
        match current {
            Ty::App(func, arg) => {
                // Collect argument (in reverse order, will reverse at the end)
                args.push(arg.as_ref().clone());
                current = func.as_ref();
            }
            Ty::Con(tycon) => {
                // Found the type constructor at the head
                args.reverse();
                return Some((tycon.name, args));
            }
            _ => {
                // Not a type application with a constructor head
                return None;
            }
        }
    }
}

/// Unify two types, updating the substitution in the context.
///
/// If unification fails, an error diagnostic is emitted and the types
/// may be left partially unified.
pub fn unify(ctx: &mut TyCtxt, t1: &Ty, t2: &Ty, span: Span) {
    // Apply current substitution to both types
    let t1 = ctx.apply_subst(t1);
    let t2 = ctx.apply_subst(t2);

    // Try to reduce type family applications before unifying
    let t1 = try_reduce_type_family(ctx, &t1);
    let t2 = try_reduce_type_family(ctx, &t2);

    unify_inner(ctx, &t1, &t2, span);
}

/// Inner unification after substitution has been applied.
fn unify_inner(ctx: &mut TyCtxt, t1: &Ty, t2: &Ty, span: Span) {
    // Try to reduce type family applications before structural matching.
    // This handles cases where a type family application appears as a
    // sub-component (e.g., in `Fun(Int, Size Int)` where `Size Int` should
    // reduce to `Int`).
    let t1_reduced = try_reduce_type_family(ctx, t1);
    let t2_reduced = try_reduce_type_family(ctx, t2);
    let t1 = if t1_reduced != *t1 { &t1_reduced } else { t1 };
    let t2 = if t2_reduced != *t2 { &t2_reduced } else { t2 };

    // Try expanding user-defined type aliases before structural matching.
    // E.g., `type Fallible a = Either Failure a` allows `Fallible Int` to
    // unify with `Either () Int`.
    let t1_alias = try_expand_type_alias(ctx, t1);
    let t2_alias = try_expand_type_alias(ctx, t2);
    if t1_alias.is_some() || t2_alias.is_some() {
        let t1_exp = t1_alias.as_ref().unwrap_or(t1);
        let t2_exp = t2_alias.as_ref().unwrap_or(t2);
        unify_inner(ctx, t1_exp, t2_exp, span);
        return;
    }

    match (t1, t2) {
        // Error types unify with anything (error recovery)
        (Ty::Error, _) | (_, Ty::Error) => {}

        // Same variable unifies trivially
        (Ty::Var(v1), Ty::Var(v2)) if v1.id == v2.id => {}

        // Variable on either side: bind it
        (Ty::Var(v), t) | (t, Ty::Var(v)) => {
            bind_var(ctx, v, t, span);
        }

        // Type constructors: must have same name OR be compatible type aliases
        (Ty::Con(c1), Ty::Con(c2)) => {
            if c1.name == c2.name {
                // Same type, OK
            } else if same_type_name(c1.name.as_str(), c2.name.as_str()) {
                // Same type after normalizing qualified names (e.g., T.Text = Text)
            } else if are_compatible_type_aliases(c1.name.as_str(), c2.name.as_str()) {
                // Type aliases that should be equivalent
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // Primitive types: must be the same
        (Ty::Prim(p1), Ty::Prim(p2)) => {
            if p1 != p2 {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // Type applications: unify both components
        (Ty::App(f1, a1), Ty::App(f2, a2)) => {
            unify_inner(ctx, f1, f2, span);
            // Apply updated substitution before unifying arguments
            let a1 = ctx.apply_subst(a1);
            let a2 = ctx.apply_subst(a2);
            unify_inner(ctx, &a1, &a2, span);
        }

        // Function types: unify domain and codomain
        (Ty::Fun(from1, to1), Ty::Fun(from2, to2)) => {
            unify_inner(ctx, from1, from2, span);
            // Apply updated substitution before unifying codomains
            let to1 = ctx.apply_subst(to1);
            let to2 = ctx.apply_subst(to2);
            unify_inner(ctx, &to1, &to2, span);
        }

        // Tuple types: must have same length, unify components
        (Ty::Tuple(tys1), Ty::Tuple(tys2)) => {
            if tys1.len() != tys2.len() {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
                return;
            }
            for (elem1, elem2) in tys1.iter().zip(tys2.iter()) {
                let applied1 = ctx.apply_subst(elem1);
                let applied2 = ctx.apply_subst(elem2);
                unify_inner(ctx, &applied1, &applied2, span);
            }
        }

        // List types: unify element types
        (Ty::List(elem1), Ty::List(elem2)) => {
            unify_inner(ctx, elem1, elem2, span);
        }

        // Cross-type: App(f, a) vs List(elem) — treat List(elem) as App([], elem)
        // This allows HKT-style types like `f a` to unify with `[a]`
        (Ty::App(f, a), Ty::List(elem)) => {
            let list_con = Ty::Con(TyCon::new(Symbol::intern("[]"), Kind::star_to_star()));
            unify_inner(ctx, f, &list_con, span);
            let a_applied = ctx.apply_subst(a);
            let elem_applied = ctx.apply_subst(elem);
            unify_inner(ctx, &a_applied, &elem_applied, span);
        }
        (Ty::List(elem), Ty::App(f, a)) => {
            let list_con = Ty::Con(TyCon::new(Symbol::intern("[]"), Kind::star_to_star()));
            unify_inner(ctx, &list_con, f, span);
            let elem_applied = ctx.apply_subst(elem);
            let a_applied = ctx.apply_subst(a);
            unify_inner(ctx, &elem_applied, &a_applied, span);
        }

        // Forall types: instantiate with fresh variables before unifying.
        // This ensures each use of a polymorphic type gets independent type vars.
        (Ty::Forall(vars, body), t2) => {
            let scheme = Scheme::poly(vars.clone(), body.as_ref().clone());
            let instantiated = crate::instantiate::instantiate(ctx, &scheme);
            unify_inner(ctx, &instantiated, t2, span);
        }

        (t1, Ty::Forall(vars, body)) => {
            let scheme = Scheme::poly(vars.clone(), body.as_ref().clone());
            let instantiated = crate::instantiate::instantiate(ctx, &scheme);
            unify_inner(ctx, t1, &instantiated, span);
        }

        // === M9 Dependent Types: Type-level naturals ===
        (Ty::Nat(n1), Ty::Nat(n2)) => {
            unify_nat(ctx, n1, n2, span);
        }

        // === M9 Dependent Types: Type-level lists ===
        (Ty::TyList(l1), Ty::TyList(l2)) => {
            unify_ty_list(ctx, l1, l2, span);
        }

        // === Type alias: String = [Char] ===
        // In Haskell, String is defined as `type String = [Char]`, so these
        // types should unify. Handle both directions.
        // When unifying String with [a], unify a with Char.
        (t1, t2) if is_string_con(t1) => {
            if let Some(elem) = get_list_elem(t2) {
                // String ~ [elem] => unify elem with Char
                let char = char_ty();
                unify_inner(ctx, elem, &char, span);
            } else if is_string_con(t2) {
                // String ~ String, ok
            } else if is_workspaceid_con(t2) {
                // String ~ WorkspaceId, ok (WorkspaceId = String)
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }
        (t1, t2) if is_string_con(t2) => {
            if let Some(elem) = get_list_elem(t1) {
                // [elem] ~ String => unify elem with Char
                let char = char_ty();
                unify_inner(ctx, elem, &char, span);
            } else if is_workspaceid_con(t1) {
                // WorkspaceId ~ String, ok (WorkspaceId = String)
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // === Type alias: Dimension = Int (XMonad) ===
        (t1, t2) if is_dimension_con(t1) => {
            let int = int_ty();
            if is_dimension_con(t2) {
                // Dimension ~ Dimension, ok
            } else if is_position_con(t2) {
                // Dimension ~ Position, both are Int aliases
            } else {
                unify_inner(ctx, &int, t2, span);
            }
        }
        (t1, t2) if is_dimension_con(t2) => {
            let int = int_ty();
            if is_position_con(t1) {
                // Position ~ Dimension, both are Int aliases
            } else {
                unify_inner(ctx, t1, &int, span);
            }
        }

        // === Type alias: Position = Int (XMonad) ===
        (t1, t2) if is_position_con(t1) => {
            let int = int_ty();
            if is_position_con(t2) {
                // Position ~ Position, ok
            } else {
                unify_inner(ctx, &int, t2, span);
            }
        }
        (t1, t2) if is_position_con(t2) => {
            let int = int_ty();
            unify_inner(ctx, t1, &int, span);
        }

        // === Type alias: WorkspaceId = String (XMonad) ===
        (t1, t2) if is_workspaceid_con(t1) => {
            if is_workspaceid_con(t2) {
                // WorkspaceId ~ WorkspaceId, ok
            } else if let Some(elem) = get_list_elem(t2) {
                // WorkspaceId ~ [elem] => unify elem with Char (WorkspaceId = String = [Char])
                let char = char_ty();
                unify_inner(ctx, elem, &char, span);
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }
        (t1, t2) if is_workspaceid_con(t2) => {
            if let Some(elem) = get_list_elem(t1) {
                // [elem] ~ WorkspaceId => unify elem with Char
                let char = char_ty();
                unify_inner(ctx, elem, &char, span);
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // === Type alias: D = (Int, Int) (XMonad) ===
        (t1, t2) if is_d_con(t1) => {
            let int = int_ty();
            if is_d_con(t2) {
                // D ~ D, ok
            } else if let Ty::Tuple(elems) = t2 {
                if elems.len() == 2 {
                    unify_inner(ctx, &int, &elems[0], span);
                    unify_inner(ctx, &int, &elems[1], span);
                } else {
                    diagnostics::emit_type_mismatch(ctx, t1, t2, span);
                }
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }
        (t1, t2) if is_d_con(t2) => {
            let int = int_ty();
            if let Ty::Tuple(elems) = t1 {
                if elems.len() == 2 {
                    unify_inner(ctx, &elems[0], &int, span);
                    unify_inner(ctx, &elems[1], &int, span);
                } else {
                    diagnostics::emit_type_mismatch(ctx, t1, t2, span);
                }
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // === Type alias: Text ≈ String ≈ [Char] (for check mode) ===
        // In check mode, be permissive with Text/String/[Char] conversions
        // since Pandoc and many Haskell packages freely convert between them.
        (t1, t2) if is_text_con(t1) => {
            if is_text_con(t2) || is_string_con(t2) {
                // Text ~ Text or Text ~ String, ok
            } else if let Some(_elem) = get_list_elem(t2) {
                // Text ~ [a], ok (treat as compatible)
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }
        (t1, t2) if is_text_con(t2) => {
            if is_string_con(t1) {
                // String ~ Text, ok
            } else if let Some(_elem) = get_list_elem(t1) {
                // [a] ~ Text, ok
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }

        // Different type structures: mismatch
        _ => {
            // Check if either type is an unreduced type family application.
            // If so, provide a more specific error message.
            if let Some((name, args, class_name)) = check_unreduced_type_family(ctx, t1) {
                diagnostics::emit_type_family_reduction_failed(ctx, name, &args, class_name, span);
            } else if let Some((name, args, class_name)) = check_unreduced_type_family(ctx, t2) {
                diagnostics::emit_type_family_reduction_failed(ctx, name, &args, class_name, span);
            } else {
                diagnostics::emit_type_mismatch(ctx, t1, t2, span);
            }
        }
    }
}

// === M9 Dependent Types: Type-level natural unification ===

/// Unify two type-level naturals.
///
/// This uses the `NatSolver` for complex arithmetic constraints that
/// can't be solved by simple structural unification.
fn unify_nat(ctx: &mut TyCtxt, n1: &TyNat, n2: &TyNat, span: Span) {
    match (n1, n2) {
        // Same literals unify trivially
        (TyNat::Lit(v1), TyNat::Lit(v2)) => {
            if v1 != v2 {
                diagnostics::emit_dimension_mismatch(ctx, *v1, *v2, span);
            }
        }

        // Same variable unifies trivially
        (TyNat::Var(v1), TyNat::Var(v2)) if v1.id == v2.id => {}

        // Variable on either side: bind it
        (TyNat::Var(v), n) | (n, TyNat::Var(v)) => {
            bind_nat_var(ctx, v, n, span);
        }

        // Addition: try to solve or record constraint
        (TyNat::Add(a1, b1), TyNat::Add(a2, b2)) => {
            // Structurally unify the components
            unify_nat(ctx, a1, a2, span);
            let b1_applied = ctx.subst.apply_nat(b1);
            let b2_applied = ctx.subst.apply_nat(b2);
            unify_nat(ctx, &b1_applied, &b2_applied, span);
        }

        // Multiplication: try to solve or record constraint
        (TyNat::Mul(a1, b1), TyNat::Mul(a2, b2)) => {
            // Structurally unify the components
            unify_nat(ctx, a1, a2, span);
            let b1_applied = ctx.subst.apply_nat(b1);
            let b2_applied = ctx.subst.apply_nat(b2);
            unify_nat(ctx, &b1_applied, &b2_applied, span);
        }

        // For complex cases, use the constraint solver
        _ => {
            // First try to evaluate to ground values
            if let (Some(v1), Some(v2)) = (n1.eval(), n2.eval()) {
                if v1 != v2 {
                    diagnostics::emit_dimension_mismatch(ctx, v1, v2, span);
                }
                return;
            }

            // Use NatSolver for complex arithmetic constraints
            // This handles cases like: a + 3 = 10 => a = 7
            let mut solver = NatSolver::new();
            solver.add_constraint(NatConstraint::Equal(n1.clone(), n2.clone()));

            match solver.solve() {
                Ok(subst) => {
                    // Apply the solved substitution to our type context
                    for (var_id, nat) in subst.iter() {
                        // Create a TyVar for this binding
                        let ty_var = TyVar::new(var_id, bhc_types::Kind::Nat);
                        ctx.subst.insert(&ty_var, Ty::Nat(nat.clone()));
                    }
                }
                Err(err) => {
                    // Solver couldn't find a solution
                    diagnostics::emit_nat_solver_error(ctx, &err, span);
                }
            }
        }
    }
}

/// Bind a type-level natural variable to a value.
fn bind_nat_var(ctx: &mut TyCtxt, var: &TyVar, n: &TyNat, span: Span) {
    // Skip if binding to self
    if let TyNat::Var(v) = n {
        if v.id == var.id {
            return;
        }
    }

    // Occurs check for naturals
    if occurs_check_nat(var, n) {
        diagnostics::emit_nat_occurs_check_error(ctx, var, n, span);
        return;
    }

    // Add binding to substitution (wrap in Ty::Nat)
    ctx.subst.insert(var, Ty::Nat(n.clone()));
}

/// Check if a type variable occurs in a type-level natural.
fn occurs_check_nat(var: &TyVar, n: &TyNat) -> bool {
    match n {
        TyNat::Lit(_) => false,
        TyNat::Var(v) => v.id == var.id,
        TyNat::Add(a, b) | TyNat::Mul(a, b) => occurs_check_nat(var, a) || occurs_check_nat(var, b),
    }
}

// === M9 Dependent Types: Type-level list unification ===

/// Unify two type-level lists.
fn unify_ty_list(ctx: &mut TyCtxt, l1: &TyList, l2: &TyList, span: Span) {
    match (l1, l2) {
        // Both empty: unify trivially
        (TyList::Nil, TyList::Nil) => {}

        // Same variable unifies trivially
        (TyList::Var(v1), TyList::Var(v2)) if v1.id == v2.id => {}

        // Variable on either side: bind it
        (TyList::Var(v), l) | (l, TyList::Var(v)) => {
            bind_ty_list_var(ctx, v, l, span);
        }

        // Both cons: unify heads and tails
        (TyList::Cons(h1, t1), TyList::Cons(h2, t2)) => {
            // Unify heads
            let h1_applied = ctx.apply_subst(h1);
            let h2_applied = ctx.apply_subst(h2);
            unify_inner(ctx, &h1_applied, &h2_applied, span);

            // Unify tails
            let t1_applied = ctx.subst.apply_ty_list(t1);
            let t2_applied = ctx.subst.apply_ty_list(t2);
            unify_ty_list(ctx, &t1_applied, &t2_applied, span);
        }

        // Length mismatch: one is empty, other is not
        (TyList::Nil, TyList::Cons(_, _)) | (TyList::Cons(_, _), TyList::Nil) => {
            diagnostics::emit_shape_length_mismatch(ctx, l1, l2, span);
        }

        // Append: handle structurally or defer
        (TyList::Append(xs1, ys1), TyList::Append(xs2, ys2)) => {
            // Try structural unification
            let xs1_applied = ctx.subst.apply_ty_list(xs1);
            let xs2_applied = ctx.subst.apply_ty_list(xs2);
            unify_ty_list(ctx, &xs1_applied, &xs2_applied, span);

            let ys1_applied = ctx.subst.apply_ty_list(ys1);
            let ys2_applied = ctx.subst.apply_ty_list(ys2);
            unify_ty_list(ctx, &ys1_applied, &ys2_applied, span);
        }

        // Other cases: cannot unify
        _ => {
            diagnostics::emit_shape_mismatch(ctx, l1, l2, span);
        }
    }
}

/// Bind a type-level list variable to a value.
fn bind_ty_list_var(ctx: &mut TyCtxt, var: &TyVar, l: &TyList, span: Span) {
    // Skip if binding to self
    if let TyList::Var(v) = l {
        if v.id == var.id {
            return;
        }
    }

    // Occurs check for lists
    if occurs_check_ty_list(var, l) {
        diagnostics::emit_ty_list_occurs_check_error(ctx, var, l, span);
        return;
    }

    // Add binding to substitution (wrap in Ty::TyList)
    ctx.subst.insert(var, Ty::TyList(l.clone()));
}

/// Check if a type variable occurs in a type-level list.
fn occurs_check_ty_list(var: &TyVar, l: &TyList) -> bool {
    match l {
        TyList::Nil => false,
        TyList::Var(v) => v.id == var.id,
        TyList::Cons(head, tail) => occurs_check(var, head) || occurs_check_ty_list(var, tail),
        TyList::Append(xs, ys) => occurs_check_ty_list(var, xs) || occurs_check_ty_list(var, ys),
    }
}

/// Bind a type variable to a type after occurs check.
fn bind_var(ctx: &mut TyCtxt, var: &TyVar, ty: &Ty, span: Span) {
    // Skip if binding to self
    if let Ty::Var(v) = ty {
        if v.id == var.id {
            return;
        }
    }

    // Occurs check: ensure var doesn't appear in ty
    if occurs_check(var, ty) {
        diagnostics::emit_occurs_check_error(ctx, var, ty, span);
        return;
    }

    // Add binding to substitution
    ctx.subst.insert(var, ty.clone());
}

/// Check if a type variable occurs in a type (prevents infinite types).
fn occurs_check(var: &TyVar, ty: &Ty) -> bool {
    match ty {
        Ty::Var(v) => v.id == var.id,
        Ty::Con(_) | Ty::Prim(_) | Ty::Error => false,
        Ty::App(f, a) => occurs_check(var, f) || occurs_check(var, a),
        Ty::Fun(from, to) => occurs_check(var, from) || occurs_check(var, to),
        Ty::Tuple(tys) => tys.iter().any(|t| occurs_check(var, t)),
        Ty::List(elem) => occurs_check(var, elem),
        Ty::Forall(bound, body) => {
            // var occurring in bound vars doesn't count (it's shadowed)
            if bound.iter().any(|v| v.id == var.id) {
                false
            } else {
                occurs_check(var, body)
            }
        }
        // M9: Check in type-level naturals and lists
        Ty::Nat(n) => occurs_check_nat(var, n),
        Ty::TyList(l) => occurs_check_ty_list(var, l),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use bhc_intern::Symbol;
    use bhc_span::FileId;
    use bhc_types::{Kind, TyCon};

    fn test_context() -> TyCtxt {
        TyCtxt::new(FileId::new(0))
    }

    #[test]
    fn test_unify_same_var() {
        let mut ctx = test_context();
        let a = ctx.fresh_ty_var();

        unify(&mut ctx, &Ty::Var(a.clone()), &Ty::Var(a), Span::DUMMY);

        assert!(!ctx.has_errors());
    }

    #[test]
    fn test_unify_var_with_con() {
        let mut ctx = test_context();
        let a = ctx.fresh_ty_var();
        let int = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));

        unify(&mut ctx, &Ty::Var(a.clone()), &int, Span::DUMMY);

        assert!(!ctx.has_errors());
        assert_eq!(ctx.apply_subst(&Ty::Var(a)), int);
    }

    #[test]
    fn test_unify_function_types() {
        let mut ctx = test_context();
        let a = ctx.fresh_ty_var();
        let int = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));

        // a -> a ~ Int -> Int
        let t1 = Ty::fun(Ty::Var(a.clone()), Ty::Var(a.clone()));
        let t2 = Ty::fun(int.clone(), int.clone());

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        assert_eq!(ctx.apply_subst(&Ty::Var(a)), int);
    }

    #[test]
    fn test_occurs_check_fails() {
        let mut ctx = test_context();
        let a = ctx.fresh_ty_var();

        // a ~ a -> a (infinite type)
        let t = Ty::fun(Ty::Var(a.clone()), Ty::Var(a.clone()));

        unify(&mut ctx, &Ty::Var(a), &t, Span::DUMMY);

        assert!(ctx.has_errors());
    }

    #[test]
    fn test_unify_mismatch() {
        let mut ctx = test_context();
        let int = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));
        let bool_ty = Ty::Con(TyCon::new(Symbol::intern("Bool"), Kind::Star));

        unify(&mut ctx, &int, &bool_ty, Span::DUMMY);

        assert!(ctx.has_errors());
    }

    #[test]
    fn test_unify_tuples() {
        let mut ctx = test_context();
        let a = ctx.fresh_ty_var();
        let b = ctx.fresh_ty_var();
        let int = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));
        let bool_ty = Ty::Con(TyCon::new(Symbol::intern("Bool"), Kind::Star));

        let t1 = Ty::Tuple(vec![Ty::Var(a.clone()), Ty::Var(b.clone())]);
        let t2 = Ty::Tuple(vec![int.clone(), bool_ty.clone()]);

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        assert_eq!(ctx.apply_subst(&Ty::Var(a)), int);
        assert_eq!(ctx.apply_subst(&Ty::Var(b)), bool_ty);
    }

    #[test]
    fn test_unify_tuple_length_mismatch() {
        let mut ctx = test_context();
        let int = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));

        let t1 = Ty::Tuple(vec![int.clone(), int.clone()]);
        let t2 = Ty::Tuple(vec![int.clone()]);

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(ctx.has_errors());
    }

    // === M9 Dependent Types: Nat unification tests ===

    #[test]
    fn test_unify_nat_literals() {
        let mut ctx = test_context();
        let n1 = Ty::Nat(TyNat::Lit(1024));
        let n2 = Ty::Nat(TyNat::Lit(1024));

        unify(&mut ctx, &n1, &n2, Span::DUMMY);

        assert!(!ctx.has_errors());
    }

    #[test]
    fn test_unify_nat_literal_mismatch() {
        let mut ctx = test_context();
        let n1 = Ty::Nat(TyNat::Lit(1024));
        let n2 = Ty::Nat(TyNat::Lit(768));

        unify(&mut ctx, &n1, &n2, Span::DUMMY);

        assert!(ctx.has_errors());
    }

    #[test]
    fn test_unify_nat_var_to_literal() {
        let mut ctx = test_context();
        let m = TyVar::new(1, Kind::Nat);

        let t1 = Ty::Nat(TyNat::Var(m.clone()));
        let t2 = Ty::Nat(TyNat::Lit(256));

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        let result = ctx.apply_subst(&Ty::Nat(TyNat::Var(m)));
        assert_eq!(result, Ty::Nat(TyNat::Lit(256)));
    }

    #[test]
    fn test_unify_nat_var_to_var() {
        let mut ctx = test_context();
        let m = TyVar::new(1, Kind::Nat);
        let n = TyVar::new(2, Kind::Nat);

        let t1 = Ty::Nat(TyNat::Var(m.clone()));
        let t2 = Ty::Nat(TyNat::Var(n.clone()));

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        // After unification, both should resolve to the same thing
        let r1 = ctx.apply_subst(&Ty::Nat(TyNat::Var(m.clone())));
        let r2 = ctx.apply_subst(&Ty::Nat(TyNat::Var(n.clone())));
        // One should be bound to the other
        assert!(r1 == Ty::Nat(TyNat::Var(n)) || r2 == Ty::Nat(TyNat::Var(m)));
    }

    #[test]
    fn test_unify_nat_add_with_solver() {
        let mut ctx = test_context();
        let a = TyVar::new(1, Kind::Nat);

        // a + 3 = 10, so a should be 7
        let t1 = Ty::Nat(TyNat::add(TyNat::Var(a.clone()), TyNat::Lit(3)));
        let t2 = Ty::Nat(TyNat::Lit(10));

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        let result = ctx.apply_subst(&Ty::Nat(TyNat::Var(a)));
        assert_eq!(result, Ty::Nat(TyNat::Lit(7)));
    }

    #[test]
    fn test_unify_nat_mul_with_solver() {
        let mut ctx = test_context();
        let a = TyVar::new(1, Kind::Nat);

        // a * 4 = 12, so a should be 3
        let t1 = Ty::Nat(TyNat::mul(TyNat::Var(a.clone()), TyNat::Lit(4)));
        let t2 = Ty::Nat(TyNat::Lit(12));

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(!ctx.has_errors());
        let result = ctx.apply_subst(&Ty::Nat(TyNat::Var(a)));
        assert_eq!(result, Ty::Nat(TyNat::Lit(3)));
    }

    #[test]
    fn test_unify_nat_mul_not_divisible() {
        let mut ctx = test_context();
        let a = TyVar::new(1, Kind::Nat);

        // a * 4 = 10 has no integer solution
        let t1 = Ty::Nat(TyNat::mul(TyNat::Var(a.clone()), TyNat::Lit(4)));
        let t2 = Ty::Nat(TyNat::Lit(10));

        unify(&mut ctx, &t1, &t2, Span::DUMMY);

        assert!(ctx.has_errors());
    }

    #[test]
    fn test_unify_ty_list_nil() {
        let mut ctx = test_context();
        let l1 = Ty::TyList(TyList::Nil);
        let l2 = Ty::TyList(TyList::Nil);

        unify(&mut ctx, &l1, &l2, Span::DUMMY);

        assert!(!ctx.has_errors());
    }

    #[test]
    fn test_unify_ty_list_cons() {
        let mut ctx = test_context();
        let shape1 = TyList::from_vec(vec![Ty::Nat(TyNat::Lit(1024)), Ty::Nat(TyNat::Lit(768))]);
        let shape2 = TyList::from_vec(vec![Ty::Nat(TyNat::Lit(1024)), Ty::Nat(TyNat::Lit(768))]);

        unify(
            &mut ctx,
            &Ty::TyList(shape1),
            &Ty::TyList(shape2),
            Span::DUMMY,
        );

        assert!(!ctx.has_errors());
    }

    #[test]
    fn test_unify_ty_list_length_mismatch() {
        let mut ctx = test_context();
        let shape1 = TyList::from_vec(vec![Ty::Nat(TyNat::Lit(1024))]);
        let shape2 = TyList::from_vec(vec![Ty::Nat(TyNat::Lit(1024)), Ty::Nat(TyNat::Lit(768))]);

        unify(
            &mut ctx,
            &Ty::TyList(shape1),
            &Ty::TyList(shape2),
            Span::DUMMY,
        );

        assert!(ctx.has_errors());
    }

    #[test]
    fn test_unify_ty_list_with_var() {
        let mut ctx = test_context();
        let m = TyVar::new(1, Kind::Nat);
        let shape1 = TyList::from_vec(vec![
            Ty::Nat(TyNat::Var(m.clone())),
            Ty::Nat(TyNat::Lit(768)),
        ]);
        let shape2 = TyList::from_vec(vec![Ty::Nat(TyNat::Lit(1024)), Ty::Nat(TyNat::Lit(768))]);

        unify(
            &mut ctx,
            &Ty::TyList(shape1),
            &Ty::TyList(shape2),
            Span::DUMMY,
        );

        assert!(!ctx.has_errors());
        let result = ctx.apply_subst(&Ty::Nat(TyNat::Var(m)));
        assert_eq!(result, Ty::Nat(TyNat::Lit(1024)));
    }

    // === Type Family Reduction Tests ===

    #[test]
    fn test_extract_type_family_app_simple() {
        // Test extracting Elem [Int] = App(Con(Elem), List(Int))
        let elem_sym = Symbol::intern("Elem");
        let int_ty = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));
        let list_int = Ty::List(Box::new(int_ty.clone()));

        let elem_con = Ty::Con(TyCon::new(elem_sym, Kind::star_to_star()));
        let type_family_app = Ty::App(Box::new(elem_con), Box::new(list_int.clone()));

        let result = extract_type_family_app(&type_family_app);
        assert!(result.is_some());

        let (name, args) = result.unwrap();
        assert_eq!(name, elem_sym);
        assert_eq!(args.len(), 1);
        assert_eq!(args[0], list_int);
    }

    #[test]
    fn test_extract_type_family_app_multi_arg() {
        // Test extracting F a b = App(App(Con(F), a), b)
        let f_sym = Symbol::intern("F");
        let a_ty = Ty::Con(TyCon::new(Symbol::intern("A"), Kind::Star));
        let b_ty = Ty::Con(TyCon::new(Symbol::intern("B"), Kind::Star));

        let f_con = Ty::Con(TyCon::new(f_sym, Kind::Star));
        let app1 = Ty::App(Box::new(f_con), Box::new(a_ty.clone()));
        let app2 = Ty::App(Box::new(app1), Box::new(b_ty.clone()));

        let result = extract_type_family_app(&app2);
        assert!(result.is_some());

        let (name, args) = result.unwrap();
        assert_eq!(name, f_sym);
        assert_eq!(args.len(), 2);
        assert_eq!(args[0], a_ty);
        assert_eq!(args[1], b_ty);
    }

    #[test]
    fn test_extract_type_family_app_not_app() {
        // A Ty::Con is extracted as a 0-argument type family application
        let int_ty = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));
        let result = extract_type_family_app(&int_ty);
        assert!(result.is_some());
        let (name, args) = result.unwrap();
        assert_eq!(name, Symbol::intern("Int"));
        assert!(args.is_empty());

        // A Ty::Var is not a type family application
        let var_ty = Ty::Var(TyVar::new_star(0));
        assert!(extract_type_family_app(&var_ty).is_none());
    }

    #[test]
    fn test_type_family_reduction_in_unify() {
        use crate::env::{AssocTypeImpl, AssocTypeInfo, ClassInfo, InstanceInfo};
        use rustc_hash::FxHashMap;

        let mut ctx = test_context();

        // Set up: class Collection c where type Elem c
        let collection = Symbol::intern("Collection");
        let elem = Symbol::intern("Elem");
        let list_sym = Symbol::intern("List");
        let int_sym = Symbol::intern("Int");
        let c_var = TyVar::new_star(100);
        let a_var = TyVar::new_star(101);

        let class_info = ClassInfo {
            name: collection,
            params: vec![c_var.clone()],
            supers: vec![],
            methods: FxHashMap::default(),
            fundeps: vec![],
            assoc_types: vec![AssocTypeInfo {
                name: elem,
                params: vec![c_var.clone()],
                kind: Kind::Star,
                default: None,
            }],
        };

        ctx.env.register_class(class_info);

        // Set up: instance Collection [a] where type Elem [a] = a
        let list_con = Ty::Con(TyCon::new(list_sym, Kind::star_to_star()));
        let a_ty = Ty::Var(a_var.clone());
        let list_a = Ty::App(Box::new(list_con.clone()), Box::new(a_ty.clone()));

        let instance_info = InstanceInfo {
            class: collection,
            types: vec![list_a.clone()],
            context: vec![],
            methods: FxHashMap::default(),
            assoc_type_impls: vec![AssocTypeImpl {
                name: elem,
                args: vec![list_a.clone()],
                rhs: a_ty.clone(),
            }],
        };

        ctx.env.register_instance(instance_info);

        // Create Elem [Int] = App(Con(Elem), App(Con(List), Con(Int)))
        let int_ty = Ty::Con(TyCon::new(int_sym, Kind::Star));
        let list_int = Ty::App(Box::new(list_con.clone()), Box::new(int_ty.clone()));
        let elem_con = Ty::Con(TyCon::new(elem, Kind::star_to_star()));
        let elem_list_int = Ty::App(Box::new(elem_con), Box::new(list_int));

        // Unify Elem [Int] with Int - should succeed because Elem [Int] reduces to Int
        unify(&mut ctx, &elem_list_int, &int_ty, Span::DUMMY);

        // Should have no errors - the type family reduced to Int
        assert!(!ctx.has_errors(), "Type family reduction should succeed");
    }

    #[test]
    fn test_type_family_reduction_failure_emits_error() {
        use crate::env::{AssocTypeInfo, ClassInfo};
        use rustc_hash::FxHashMap;

        let mut ctx = test_context();

        // Set up: class Collection c where type Elem c
        // But no instances!
        let collection = Symbol::intern("Collection");
        let elem = Symbol::intern("Elem");
        let int_sym = Symbol::intern("Int");
        let c_var = TyVar::new_star(100);

        let class_info = ClassInfo {
            name: collection,
            params: vec![c_var.clone()],
            supers: vec![],
            methods: FxHashMap::default(),
            fundeps: vec![],
            assoc_types: vec![AssocTypeInfo {
                name: elem,
                params: vec![c_var.clone()],
                kind: Kind::Star,
                default: None,
            }],
        };

        ctx.env.register_class(class_info);

        // Try to use Elem Int, but there's no instance Collection Int
        let int_ty = Ty::Con(TyCon::new(int_sym, Kind::Star));
        let elem_con = Ty::Con(TyCon::new(elem, Kind::star_to_star()));
        let elem_int = Ty::App(Box::new(elem_con), Box::new(int_ty.clone()));

        // Try to unify Elem Int with Bool - should fail with type family error
        let bool_ty = Ty::Con(TyCon::new(Symbol::intern("Bool"), Kind::Star));
        unify(&mut ctx, &elem_int, &bool_ty, Span::DUMMY);

        // Should have an error about type family reduction failure
        assert!(
            ctx.has_errors(),
            "Should emit error for unreduced type family"
        );
    }

    #[test]
    fn test_check_unreduced_type_family() {
        use crate::env::{AssocTypeInfo, ClassInfo};
        use rustc_hash::FxHashMap;

        let mut ctx = test_context();

        // Set up: class Container c where type Item c
        let container = Symbol::intern("Container");
        let item = Symbol::intern("Item");
        let c_var = TyVar::new_star(100);

        let class_info = ClassInfo {
            name: container,
            params: vec![c_var.clone()],
            supers: vec![],
            methods: FxHashMap::default(),
            fundeps: vec![],
            assoc_types: vec![AssocTypeInfo {
                name: item,
                params: vec![c_var.clone()],
                kind: Kind::Star,
                default: None,
            }],
        };

        ctx.env.register_class(class_info);

        // Create Item Bool with no matching instance
        let bool_ty = Ty::Con(TyCon::new(Symbol::intern("Bool"), Kind::Star));
        let item_con = Ty::Con(TyCon::new(item, Kind::star_to_star()));
        let item_bool = Ty::App(Box::new(item_con), Box::new(bool_ty));

        // check_unreduced_type_family should detect this
        let result = check_unreduced_type_family(&ctx, &item_bool);
        assert!(result.is_some(), "Should detect unreduced type family");

        let (name, args, class_name) = result.unwrap();
        assert_eq!(name, item);
        assert_eq!(args.len(), 1);
        assert_eq!(class_name, Some(container));
    }

    #[test]
    fn test_check_unreduced_type_family_returns_none_for_regular_type() {
        let ctx = test_context();

        // Regular type applications are not type families
        let maybe = Symbol::intern("Maybe");
        let int_ty = Ty::Con(TyCon::new(Symbol::intern("Int"), Kind::Star));
        let maybe_con = Ty::Con(TyCon::new(maybe, Kind::star_to_star()));
        let maybe_int = Ty::App(Box::new(maybe_con), Box::new(int_ty));

        // Should return None because Maybe is not a type family
        let result = check_unreduced_type_family(&ctx, &maybe_int);
        assert!(
            result.is_none(),
            "Regular type application is not a type family"
        );
    }
}
