//! Type checker for the Lux language

#![allow(dead_code, unused_variables)]

use std::collections::HashMap;

use crate::ast::{
    self, BinaryOp, Declaration, EffectDecl, ExternFnDecl, Expr, FunctionDecl, HandlerDecl, Ident,
    ImplDecl, ImportDecl, LetDecl, Literal, LiteralKind, MatchArm, Parameter, Pattern, Program,
    Span, Statement, TraitDecl, TypeDecl, TypeExpr, UnaryOp, VariantFields,
};
use crate::diagnostics::{find_similar_names, format_did_you_mean, Diagnostic, ErrorCode, Severity};
use crate::exhaustiveness::{check_exhaustiveness, missing_patterns_hint};
use crate::modules::ModuleLoader;
use crate::schema::{SchemaRegistry, Compatibility, BreakingChange, AutoMigration};
use crate::types::{
    self, unify, unify_with_env, EffectDef, EffectOpDef, EffectSet, HandlerDef, Property, PropertySet,
    TraitBoundDef, TraitDef, TraitImpl, TraitMethodDef, Type, TypeEnv, TypeScheme, VariantDef,
    VariantFieldsDef, VersionInfo,
};

/// Type checking error
#[derive(Debug, Clone)]
pub struct TypeError {
    pub message: String,
    pub span: Span,
}

impl std::fmt::Display for TypeError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(
            f,
            "Type error at {}-{}: {}",
            self.span.start, self.span.end, self.message
        )
    }
}

impl TypeError {
    /// Convert to a rich diagnostic for Elm-style error display
    pub fn to_diagnostic(&self) -> Diagnostic {
        // Categorize the error and extract hints, error code, and type info
        let (code, title, hints, expected, actual) = categorize_type_error(&self.message);

        Diagnostic {
            severity: Severity::Error,
            code,
            title,
            message: self.message.clone(),
            span: self.span,
            hints,
            expected_type: expected,
            actual_type: actual,
            secondary_spans: Vec::new(),
        }
    }
}

/// Extract expected and actual types from an error message
fn extract_types_from_message(message: &str) -> (Option<String>, Option<String>) {
    // Try to extract "expected X, got Y" patterns
    let patterns = [
        ("expected ", ", got "),
        ("expected ", " but got "),
        ("expected ", " found "),
    ];

    for (exp_prefix, got_prefix) in patterns {
        if let Some(exp_start) = message.to_lowercase().find(exp_prefix) {
            let after_expected = &message[exp_start + exp_prefix.len()..];
            if let Some(got_pos) = after_expected.to_lowercase().find(got_prefix) {
                let expected = after_expected[..got_pos].trim().to_string();
                let after_got = &after_expected[got_pos + got_prefix.len()..];
                // Take until end of word or punctuation
                let actual = after_got
                    .split(|c: char| c == ',' || c == '.' || c == ';' || c == ')' || c.is_whitespace())
                    .next()
                    .unwrap_or("")
                    .trim()
                    .to_string();
                if !expected.is_empty() && !actual.is_empty() {
                    return (Some(expected), Some(actual));
                }
            }
        }
    }

    // Try "cannot unify X with Y" pattern
    if let Some(unify_pos) = message.to_lowercase().find("cannot unify ") {
        let after_unify = &message[unify_pos + 13..];
        if let Some(with_pos) = after_unify.to_lowercase().find(" with ") {
            let type1 = after_unify[..with_pos].trim().to_string();
            let type2 = after_unify[with_pos + 6..]
                .split(|c: char| c == ',' || c == '.' || c == ';' || c == ')' || c.is_whitespace())
                .next()
                .unwrap_or("")
                .trim()
                .to_string();
            if !type1.is_empty() && !type2.is_empty() {
                return (Some(type1), Some(type2));
            }
        }
    }

    (None, None)
}

/// Categorize a type error message to provide better titles, hints, and error codes
fn categorize_type_error(message: &str) -> (Option<ErrorCode>, String, Vec<String>, Option<String>, Option<String>) {
    let message_lower = message.to_lowercase();
    let (expected, actual) = extract_types_from_message(message);

    if message_lower.contains("type mismatch") {
        (
            Some(ErrorCode::E0201),
            "Type Mismatch".to_string(),
            vec!["Check that the types on both sides of the expression are compatible.".to_string()],
            expected,
            actual,
        )
    } else if message_lower.contains("undefined variable") {
        (
            Some(ErrorCode::E0301),
            "Undefined Variable".to_string(),
            vec![
                "Check the spelling of the variable name.".to_string(),
                "Make sure the variable is defined before use.".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("undefined function") || message_lower.contains("function") && message_lower.contains("not found") {
        (
            Some(ErrorCode::E0302),
            "Undefined Function".to_string(),
            vec![
                "Check the spelling of the function name.".to_string(),
                "Make sure the function is imported or defined.".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("not found") || message_lower.contains("unknown") && message_lower.contains("name") {
        (
            Some(ErrorCode::E0301),
            "Unknown Name".to_string(),
            vec![
                "Check the spelling of the name.".to_string(),
                "Make sure the variable is defined before use.".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("cannot unify") {
        (
            Some(ErrorCode::E0202),
            "Cannot Unify Types".to_string(),
            vec!["The types are not compatible. Check your function arguments and return types.".to_string()],
            expected,
            actual,
        )
    } else if message_lower.contains("expected") && message_lower.contains("argument") {
        (
            Some(ErrorCode::E0209),
            "Wrong Number of Arguments".to_string(),
            vec!["Check the function signature and provide the correct number of arguments.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("pure") && message_lower.contains("effect") {
        (
            Some(ErrorCode::E0701),
            "Purity Violation".to_string(),
            vec![
                "Functions marked 'is pure' cannot perform effects.".to_string(),
                "Remove the 'is pure' annotation or handle the effects.".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("effect") && message_lower.contains("unhandled") {
        (
            Some(ErrorCode::E0401),
            "Unhandled Effect".to_string(),
            vec!["Use a 'handle' expression to provide an implementation for this effect.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("recursive") {
        (
            Some(ErrorCode::E0205),
            "Invalid Recursion".to_string(),
            vec!["Check that recursive calls have proper base cases.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("unknown effect") {
        (
            Some(ErrorCode::E0402),
            "Unknown Effect".to_string(),
            vec![
                "Make sure the effect is spelled correctly.".to_string(),
                "Built-in effects: Console, File, Process, Http, Random, Time, Sql.".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("record has no field") || message_lower.contains("missing field") {
        (
            Some(ErrorCode::E0207),
            "Missing Record Field".to_string(),
            vec!["Check the field name spelling or review the record definition.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("undefined field") {
        (
            Some(ErrorCode::E0308),
            "Undefined Field".to_string(),
            vec!["Check the field name spelling or review the record definition.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("cannot access field") {
        (
            Some(ErrorCode::E0308),
            "Invalid Field Access".to_string(),
            vec!["Field access is only valid on record types.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("effect") && (message_lower.contains("not available") || message_lower.contains("missing")) {
        (
            Some(ErrorCode::E0403),
            "Missing Effect Handler".to_string(),
            vec![
                "Add the effect to your function's effect list.".to_string(),
                "Example: fn myFn(): Int with {Console, Sql} = ...".to_string(),
            ],
            None,
            None,
        )
    } else if message_lower.contains("non-exhaustive") || message_lower.contains("exhaustive") {
        (
            Some(ErrorCode::E0501),
            "Non-Exhaustive Patterns".to_string(),
            vec!["Add patterns for the missing cases or use a wildcard pattern '_'.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("duplicate") {
        (
            Some(ErrorCode::E0305),
            "Duplicate Definition".to_string(),
            vec!["Each name can only be defined once in the same scope.".to_string()],
            None,
            None,
        )
    } else if message_lower.contains("return type") {
        (
            Some(ErrorCode::E0211),
            "Return Type Mismatch".to_string(),
            vec!["The function body's type doesn't match the declared return type.".to_string()],
            expected,
            actual,
        )
    } else {
        (
            Some(ErrorCode::E0200),
            "Type Error".to_string(),
            vec![],
            expected,
            actual,
        )
    }
}

/// Check if an operator is commutative
fn is_commutative_op(op: BinaryOp) -> bool {
    matches!(
        op,
        BinaryOp::Add | BinaryOp::Mul | BinaryOp::Eq | BinaryOp::Ne | BinaryOp::And | BinaryOp::Or
    )
}

/// Check if a function body represents a commutative operation on its two parameters
fn is_commutative_body(body: &Expr, param1: &str, param2: &str) -> bool {
    match body {
        Expr::BinaryOp { op, left, right, .. } => {
            if !is_commutative_op(*op) {
                return false;
            }
            // Check if it's (param1 op param2) or (param2 op param1)
            let left_is_p1 = matches!(left.as_ref(), Expr::Var(id) if id.name == param1);
            let left_is_p2 = matches!(left.as_ref(), Expr::Var(id) if id.name == param2);
            let right_is_p1 = matches!(right.as_ref(), Expr::Var(id) if id.name == param1);
            let right_is_p2 = matches!(right.as_ref(), Expr::Var(id) if id.name == param2);
            (left_is_p1 && right_is_p2) || (left_is_p2 && right_is_p1)
        }
        // Handle block expressions - check last expression
        Expr::Block { statements, result, .. } => {
            if !statements.is_empty() {
                return false;
            }
            is_commutative_body(result, param1, param2)
        }
        _ => false,
    }
}

/// Check if an expression references any of the given parameter names
fn references_params(expr: &Expr, params: &[&str]) -> bool {
    match expr {
        Expr::Var(id) => params.contains(&id.name.as_str()),
        Expr::BinaryOp { left, right, .. } => {
            references_params(left, params) || references_params(right, params)
        }
        Expr::UnaryOp { operand, .. } => references_params(operand, params),
        Expr::If {
            condition,
            then_branch,
            else_branch,
            ..
        } => {
            references_params(condition, params)
                || references_params(then_branch, params)
                || references_params(else_branch, params)
        }
        Expr::Call { func, args, .. } => {
            references_params(func, params) || args.iter().any(|a| references_params(a, params))
        }
        Expr::Block { statements, result, .. } => {
            statements.iter().any(|s| match s {
                Statement::Let { value, .. } => references_params(value, params),
                Statement::Expr(e) => references_params(e, params),
            }) || references_params(result, params)
        }
        Expr::Field { object, .. } | Expr::TupleIndex { object, .. } => references_params(object, params),
        Expr::Lambda { body, .. } => references_params(body, params),
        Expr::Tuple { elements, .. } => elements.iter().any(|e| references_params(e, params)),
        Expr::List { elements, .. } => elements.iter().any(|e| references_params(e, params)),
        Expr::Record { spread, fields, .. } => {
            spread.as_ref().is_some_and(|s| references_params(s, params))
                || fields.iter().any(|(_, e)| references_params(e, params))
        }
        Expr::Match { scrutinee, arms, .. } => {
            references_params(scrutinee, params)
                || arms.iter().any(|a| references_params(&a.body, params))
        }
        _ => false,
    }
}

/// Check if a function body is idempotent (f(f(x)) == f(x))
/// Uses conservative pattern recognition
fn is_idempotent_body(body: &Expr, params: &[Parameter]) -> bool {
    let param_names: Vec<&str> = params.iter().map(|p| p.name.name.as_str()).collect();

    // Pattern 1: Constant - body doesn't reference any parameters
    if !references_params(body, &param_names) {
        return true;
    }

    // Pattern 2: Identity function (single param, body is just that param)
    if params.len() == 1 {
        if let Expr::Var(id) = body {
            if id.name == params[0].name.name {
                return true;
            }
        }
    }

    // Pattern 3: Field projection on single param (e.g., person.name)
    if params.len() == 1 {
        if let Expr::Field { object, .. } = body {
            if let Expr::Var(id) = object.as_ref() {
                if id.name == params[0].name.name {
                    return true;
                }
            }
        }
    }

    // Pattern 4: Clamping pattern - if x < min then min else if x > max then max else x
    // or simpler: if x < 0 then 0 else x
    if params.len() == 1 && is_clamping_pattern(body, &params[0].name.name) {
        return true;
    }

    // Pattern 5: Absolute value - if x < 0 then -x else x
    if params.len() == 1 && is_abs_pattern(body, &params[0].name.name) {
        return true;
    }

    // Handle block wrapper
    if let Expr::Block { statements, result, .. } = body {
        if statements.is_empty() {
            return is_idempotent_body(result, params);
        }
    }

    false
}

/// Check if body matches: if x < bound then bound else x (or similar clamping patterns)
fn is_clamping_pattern(body: &Expr, param: &str) -> bool {
    if let Expr::If {
        condition,
        then_branch,
        else_branch,
        ..
    } = body
    {
        // Check if then_branch is a constant and else_branch is the param (or recursive)
        let else_is_param = matches!(else_branch.as_ref(), Expr::Var(id) if id.name == param);
        let else_is_clamp = is_clamping_pattern(else_branch, param);

        if else_is_param || else_is_clamp {
            // Check if condition is a comparison involving the param
            if let Expr::BinaryOp { left, right, op, .. } = condition.as_ref() {
                let left_is_param = matches!(left.as_ref(), Expr::Var(id) if id.name == param);
                let right_is_param = matches!(right.as_ref(), Expr::Var(id) if id.name == param);
                if (left_is_param || right_is_param)
                    && matches!(
                        op,
                        BinaryOp::Lt | BinaryOp::Le | BinaryOp::Gt | BinaryOp::Ge
                    )
                {
                    return true;
                }
            }
        }
    }
    false
}

/// Check if body matches: if x < 0 then -x else x
fn is_abs_pattern(body: &Expr, param: &str) -> bool {
    if let Expr::If {
        condition,
        then_branch,
        else_branch,
        ..
    } = body
    {
        let else_is_param = matches!(else_branch.as_ref(), Expr::Var(id) if id.name == param);
        if !else_is_param {
            return false;
        }

        // Check if then_branch is -param
        if let Expr::UnaryOp {
            op: ast::UnaryOp::Neg,
            operand,
            ..
        } = then_branch.as_ref()
        {
            if matches!(operand.as_ref(), Expr::Var(id) if id.name == param) {
                // Check condition is param < 0
                if let Expr::BinaryOp {
                    op: BinaryOp::Lt,
                    left,
                    right,
                    ..
                } = condition.as_ref()
                {
                    let left_is_param = matches!(left.as_ref(), Expr::Var(id) if id.name == param);
                    let right_is_zero =
                        matches!(right.as_ref(), Expr::Literal(lit) if matches!(lit.kind, LiteralKind::Int(0)));
                    if left_is_param && right_is_zero {
                        return true;
                    }
                }
            }
        }
    }
    false
}

/// Check if a function body contains recursive calls to the function
fn has_recursive_calls(func_name: &str, body: &Expr) -> bool {
    match body {
        Expr::Call { func, args, .. } => {
            // Check if this call is to the function itself
            if let Expr::Var(id) = func.as_ref() {
                if id.name == func_name {
                    return true;
                }
            }
            // Check in function expression and arguments
            has_recursive_calls(func_name, func)
                || args.iter().any(|a| has_recursive_calls(func_name, a))
        }
        Expr::BinaryOp { left, right, .. } => {
            has_recursive_calls(func_name, left) || has_recursive_calls(func_name, right)
        }
        Expr::UnaryOp { operand, .. } => has_recursive_calls(func_name, operand),
        Expr::If {
            condition,
            then_branch,
            else_branch,
            ..
        } => {
            has_recursive_calls(func_name, condition)
                || has_recursive_calls(func_name, then_branch)
                || has_recursive_calls(func_name, else_branch)
        }
        Expr::Block { statements, result, .. } => {
            statements.iter().any(|s| match s {
                Statement::Let { value, .. } => has_recursive_calls(func_name, value),
                Statement::Expr(e) => has_recursive_calls(func_name, e),
            }) || has_recursive_calls(func_name, result)
        }
        Expr::Match { scrutinee, arms, .. } => {
            has_recursive_calls(func_name, scrutinee)
                || arms.iter().any(|a| has_recursive_calls(func_name, &a.body))
        }
        Expr::Lambda { body, .. } => has_recursive_calls(func_name, body),
        Expr::Tuple { elements, .. } | Expr::List { elements, .. } => {
            elements.iter().any(|e| has_recursive_calls(func_name, e))
        }
        Expr::Record { spread, fields, .. } => {
            spread.as_ref().is_some_and(|s| has_recursive_calls(func_name, s))
                || fields.iter().any(|(_, e)| has_recursive_calls(func_name, e))
        }
        Expr::Field { object, .. } | Expr::TupleIndex { object, .. } => has_recursive_calls(func_name, object),
        Expr::Let { value, body, .. } => {
            has_recursive_calls(func_name, value) || has_recursive_calls(func_name, body)
        }
        Expr::Run { expr, handlers, .. } => {
            has_recursive_calls(func_name, expr)
                || handlers.iter().any(|(_, e)| has_recursive_calls(func_name, e))
        }
        _ => false,
    }
}

/// Find all recursive call arguments: returns Vec of argument lists
fn find_recursive_call_args<'a>(func_name: &str, body: &'a Expr) -> Vec<&'a [Expr]> {
    let mut result = Vec::new();
    collect_recursive_call_args(func_name, body, &mut result);
    result
}

fn collect_recursive_call_args<'a>(func_name: &str, body: &'a Expr, result: &mut Vec<&'a [Expr]>) {
    match body {
        Expr::Call { func, args, .. } => {
            if let Expr::Var(id) = func.as_ref() {
                if id.name == func_name {
                    result.push(args.as_slice());
                }
            }
            collect_recursive_call_args(func_name, func, result);
            for arg in args {
                collect_recursive_call_args(func_name, arg, result);
            }
        }
        Expr::BinaryOp { left, right, .. } => {
            collect_recursive_call_args(func_name, left, result);
            collect_recursive_call_args(func_name, right, result);
        }
        Expr::UnaryOp { operand, .. } => {
            collect_recursive_call_args(func_name, operand, result);
        }
        Expr::If {
            condition,
            then_branch,
            else_branch,
            ..
        } => {
            collect_recursive_call_args(func_name, condition, result);
            collect_recursive_call_args(func_name, then_branch, result);
            collect_recursive_call_args(func_name, else_branch, result);
        }
        Expr::Block { statements, result: res, .. } => {
            for s in statements {
                match s {
                    Statement::Let { value, .. } => {
                        collect_recursive_call_args(func_name, value, result)
                    }
                    Statement::Expr(e) => collect_recursive_call_args(func_name, e, result),
                }
            }
            collect_recursive_call_args(func_name, res, result);
        }
        Expr::Match { scrutinee, arms, .. } => {
            collect_recursive_call_args(func_name, scrutinee, result);
            for arm in arms {
                collect_recursive_call_args(func_name, &arm.body, result);
            }
        }
        Expr::Lambda { body, .. } => collect_recursive_call_args(func_name, body, result),
        Expr::Let { value, body, .. } => {
            collect_recursive_call_args(func_name, value, result);
            collect_recursive_call_args(func_name, body, result);
        }
        _ => {}
    }
}

/// Check if an argument is structurally decreasing from a parameter
/// Recognizes patterns like: n - 1, n - k (for positive k)
fn is_structurally_decreasing(arg: &Expr, param_name: &str) -> bool {
    match arg {
        // Pattern: n - 1, n - k for positive k
        Expr::BinaryOp {
            op: BinaryOp::Sub,
            left,
            right,
            ..
        } => {
            if let Expr::Var(id) = left.as_ref() {
                if id.name == param_name {
                    // Check if right side is a positive integer literal
                    if let Expr::Literal(lit) = right.as_ref() {
                        if let LiteralKind::Int(n) = lit.kind {
                            return n > 0;
                        }
                    }
                }
            }
            false
        }
        _ => false,
    }
}

/// Generate an auto-migration expression based on detected auto-migratable changes
/// Creates an expression like: { existingField1: old.existingField1, ..., newOptionalField: None }
fn generate_auto_migration_expr(
    prev_def: &ast::TypeDef,
    new_def: &ast::TypeDef,
    auto_migrations: &[AutoMigration],
    span: Span,
) -> Option<Expr> {
    // Only handle record types for auto-migration
    let (prev_fields, new_fields) = match (prev_def, new_def) {
        (ast::TypeDef::Record(prev), ast::TypeDef::Record(new)) => (prev, new),
        _ => return None,
    };

    // Build a record expression with all fields
    let mut field_exprs: Vec<(ast::Ident, Expr)> = Vec::new();

    // Map of new fields that need auto-migration defaults
    let auto_migrate_fields: std::collections::HashSet<String> = auto_migrations
        .iter()
        .filter_map(|m| match m {
            AutoMigration::AddFieldWithDefault { field_name, .. } => Some(field_name.clone()),
            AutoMigration::WidenType { .. } => None,
        })
        .collect();

    // For each field in the new definition
    for new_field in new_fields {
        let field_name = &new_field.name.name;

        if auto_migrate_fields.contains(field_name) {
            // New optional field - add with None default
            field_exprs.push((
                new_field.name.clone(),
                Expr::Var(Ident::new("None", span)),
            ));
        } else {
            // Existing field - copy from old: old.fieldName
            field_exprs.push((
                new_field.name.clone(),
                Expr::Field {
                    object: Box::new(Expr::Var(Ident::new("old", span))),
                    field: new_field.name.clone(),
                    span,
                },
            ));
        }
    }

    // Build the record expression
    Some(Expr::Record {
        spread: None,
        fields: field_exprs,
        span,
    })
}

/// Check if a function terminates (structural recursion check)
fn check_termination(func: &FunctionDecl) -> Result<(), String> {
    // Non-recursive functions always terminate
    if !has_recursive_calls(&func.name.name, &func.body) {
        return Ok(());
    }

    // For recursive functions, check structural recursion
    let param_names: Vec<&str> = func.params.iter().map(|p| p.name.name.as_str()).collect();
    let recursive_calls = find_recursive_call_args(&func.name.name, &func.body);

    for call_args in recursive_calls {
        // At least one argument must be structurally decreasing
        let has_decreasing = call_args.iter().enumerate().any(|(i, arg)| {
            if i < param_names.len() {
                is_structurally_decreasing(arg, param_names[i])
            } else {
                false
            }
        });

        if !has_decreasing {
            return Err("Recursive call has no provably decreasing argument".to_string());
        }
    }

    Ok(())
}

/// Property constraint on a function parameter
#[derive(Debug, Clone)]
pub struct ParamPropertyConstraint {
    pub param_name: String,
    pub param_index: usize,
    pub required_properties: PropertySet,
}

/// Type checker
pub struct TypeChecker {
    env: TypeEnv,
    current_effects: EffectSet,
    /// Effects inferred from the current function body (for effect inference)
    inferred_effects: EffectSet,
    /// Whether we're inferring effects (no explicit declaration)
    inferring_effects: bool,
    errors: Vec<TypeError>,
    /// Type parameters in scope (maps "T" -> Type::Var(n) for generics)
    type_params: HashMap<String, Type>,
    /// Property constraints from where clauses: func_name -> Vec<(param_name, properties)>
    property_constraints: HashMap<String, Vec<ParamPropertyConstraint>>,
    /// Versioned type definitions: type_name -> version -> TypeDef
    versioned_types: HashMap<String, HashMap<u32, types::TypeDef>>,
    /// Latest version for each versioned type: type_name -> highest_version
    latest_versions: HashMap<String, u32>,
    /// Migrations: type_name -> source_version -> migration_body
    migrations: HashMap<String, HashMap<u32, Expr>>,
    /// Schema registry for compatibility checking
    schema_registry: SchemaRegistry,
}

impl TypeChecker {
    pub fn new() -> Self {
        Self {
            env: TypeEnv::with_builtins(),
            current_effects: EffectSet::empty(),
            inferred_effects: EffectSet::empty(),
            inferring_effects: false,
            errors: Vec::new(),
            type_params: HashMap::new(),
            property_constraints: HashMap::new(),
            versioned_types: HashMap::new(),
            latest_versions: HashMap::new(),
            migrations: HashMap::new(),
            schema_registry: SchemaRegistry::new(),
        }
    }

    /// Look up a type scheme by name (for REPL :info command)
    pub fn lookup(&self, name: &str) -> Option<&TypeScheme> {
        self.env.bindings.get(name)
    }

    /// Get the inferred type of a binding as a display string (for LSP inlay hints)
    pub fn get_inferred_type(&self, name: &str) -> Option<String> {
        let scheme = self.env.bindings.get(name)?;
        let type_str = scheme.typ.to_string();
        // Skip unhelpful types
        if type_str == "<error>" || type_str.contains('?') {
            return None;
        }
        Some(type_str)
    }

    /// Get auto-generated migrations from type checking
    /// Returns: type_name -> from_version -> migration_body
    pub fn get_auto_migrations(&self) -> &HashMap<String, HashMap<u32, Expr>> {
        &self.migrations
    }

    /// Type check a program
    pub fn check_program(&mut self, program: &Program) -> Result<(), Vec<TypeError>> {
        // First pass: collect all declarations
        for decl in &program.declarations {
            self.collect_declaration(decl);
        }

        // Check for circular type definitions
        self.check_type_cycles(program);

        // Second pass: type check all declarations
        for decl in &program.declarations {
            self.check_declaration(decl);
        }

        if self.errors.is_empty() {
            Ok(())
        } else {
            Err(self.errors.clone())
        }
    }

    /// Check for circular type alias definitions
    fn check_type_cycles(&mut self, program: &Program) {
        use std::collections::HashSet;

        // Build a map of type alias dependencies
        let mut alias_deps: HashMap<String, Vec<String>> = HashMap::new();

        for decl in &program.declarations {
            if let Declaration::Type(type_decl) = decl {
                if let ast::TypeDef::Alias(type_expr) = &type_decl.definition {
                    let deps = self.collect_type_references(type_expr);
                    alias_deps.insert(type_decl.name.name.clone(), deps);
                }
            }
        }

        // Check for cycles using DFS
        fn has_cycle(
            name: &str,
            alias_deps: &HashMap<String, Vec<String>>,
            visiting: &mut HashSet<String>,
            visited: &mut HashSet<String>,
            cycle_path: &mut Vec<String>,
        ) -> bool {
            if visiting.contains(name) {
                cycle_path.push(name.to_string());
                return true;
            }
            if visited.contains(name) {
                return false;
            }

            visiting.insert(name.to_string());
            cycle_path.push(name.to_string());

            if let Some(deps) = alias_deps.get(name) {
                for dep in deps {
                    if alias_deps.contains_key(dep) {
                        if has_cycle(dep, alias_deps, visiting, visited, cycle_path) {
                            return true;
                        }
                    }
                }
            }

            visiting.remove(name);
            cycle_path.pop();
            visited.insert(name.to_string());
            false
        }

        let mut visited = HashSet::new();

        for type_name in alias_deps.keys() {
            let mut visiting = HashSet::new();
            let mut cycle_path = Vec::new();

            if has_cycle(type_name, &alias_deps, &mut visiting, &mut visited, &mut cycle_path) {
                // Find the span for this type declaration
                let span = program.declarations.iter().find_map(|d| {
                    if let Declaration::Type(t) = d {
                        if t.name.name == *type_name {
                            return Some(t.span);
                        }
                    }
                    None
                }).unwrap_or(Span::default());

                self.errors.push(TypeError {
                    message: format!(
                        "Circular type definition detected: {}",
                        cycle_path.join(" -> ")
                    ),
                    span,
                });
            }
        }
    }

    /// Collect all type names referenced in a type expression
    fn collect_type_references(&self, type_expr: &TypeExpr) -> Vec<String> {
        let mut refs = Vec::new();
        self.collect_type_refs_helper(type_expr, &mut refs);
        refs
    }

    fn collect_type_refs_helper(&self, type_expr: &TypeExpr, refs: &mut Vec<String>) {
        match type_expr {
            TypeExpr::Named(ident) => {
                // Only include user-defined types, not builtins
                match ident.name.as_str() {
                    "Int" | "Float" | "Bool" | "String" | "Char" | "Unit" | "_" => {}
                    name => refs.push(name.to_string()),
                }
            }
            TypeExpr::App(constructor, args) => {
                self.collect_type_refs_helper(constructor, refs);
                for arg in args {
                    self.collect_type_refs_helper(arg, refs);
                }
            }
            TypeExpr::Function { params, return_type, .. } => {
                for p in params {
                    self.collect_type_refs_helper(p, refs);
                }
                self.collect_type_refs_helper(return_type, refs);
            }
            TypeExpr::Tuple(elements) => {
                for e in elements {
                    self.collect_type_refs_helper(e, refs);
                }
            }
            TypeExpr::Record(fields) => {
                for f in fields {
                    self.collect_type_refs_helper(&f.typ, refs);
                }
            }
            TypeExpr::Unit => {}
            TypeExpr::Versioned { base, .. } => {
                self.collect_type_refs_helper(base, refs);
            }
        }
    }

    /// Type check a program with module support
    pub fn check_program_with_modules(
        &mut self,
        program: &Program,
        loader: &ModuleLoader,
    ) -> Result<(), Vec<TypeError>> {
        // First, process imports
        self.load_type_imports(&program.imports, loader);

        // Then check the program normally
        self.check_program(program)
    }

    /// Load type bindings from imported modules
    fn load_type_imports(&mut self, imports: &[ImportDecl], loader: &ModuleLoader) {
        use crate::modules::ImportKind;

        let resolved = match loader.resolve_imports(imports) {
            Ok(r) => r,
            Err(e) => {
                self.errors.push(TypeError {
                    message: format!("Import error: {}", e.message),
                    span: Span { start: 0, end: 0 },
                });
                return;
            }
        };

        for (name, import) in resolved {
            match import.kind {
                ImportKind::Module => {
                    // Import as a module object - create a record type
                    let module = match loader.get_module(&import.module_path) {
                        Some(m) => m,
                        None => continue,
                    };

                    // Create a temporary checker to get types from the module
                    let mut module_checker = TypeChecker::new();
                    for decl in &module.program.declarations {
                        module_checker.collect_declaration(decl);
                    }

                    // Build a record type with all exported names
                    let mut fields = Vec::new();
                    for export_name in &module.exports {
                        if let Some(scheme) = module_checker.env.lookup(export_name) {
                            fields.push((export_name.clone(), scheme.instantiate()));
                        }
                    }

                    if !fields.is_empty() {
                        self.env.bind(&name, TypeScheme::mono(Type::Record(fields)));
                    }

                    // Also copy type definitions so imported types are usable
                    for (type_name, type_def) in &module_checker.env.types {
                        if !self.env.types.contains_key(type_name) {
                            self.env.types.insert(type_name.clone(), type_def.clone());
                        }
                    }
                }
                ImportKind::Direct => {
                    // Import a specific name directly
                    let module = match loader.get_module(&import.module_path) {
                        Some(m) => m,
                        None => continue,
                    };

                    // Get the type for this specific export
                    let mut module_checker = TypeChecker::new();
                    for decl in &module.program.declarations {
                        module_checker.collect_declaration(decl);
                    }

                    if let Some(scheme) = module_checker.env.lookup(&import.name) {
                        self.env.bind(&name, scheme.clone());
                    }

                    // Also copy effects if the imported name is an effect
                    if let Some(effect) = module_checker.env.lookup_effect(&import.name) {
                        self.env.effects.insert(name.clone(), effect.clone());
                    }

                    // Also copy types if the imported name is a type
                    if let Some(type_def) = module_checker.env.types.get(&import.name) {
                        self.env.types.insert(name.clone(), type_def.clone());
                    }
                }
            }
        }
    }

    /// Collect type signatures from declarations (first pass)
    fn collect_declaration(&mut self, decl: &Declaration) {
        match decl {
            Declaration::Function(func) => {
                let scheme = self.function_type(func);
                self.env.bind(&func.name.name, scheme);
            }
            Declaration::Effect(effect) => {
                let effect_def = self.effect_def(effect);
                self.env
                    .effects
                    .insert(effect.name.name.clone(), effect_def);
            }
            Declaration::Type(type_decl) => {
                // Save old type params for this scope
                let old_params = std::mem::take(&mut self.type_params);

                // Bind type parameters to fresh type variables
                let mut bound_vars = Vec::new();
                for param in &type_decl.type_params {
                    let var = Type::var();
                    if let Type::Var(n) = &var {
                        bound_vars.push(*n);
                    }
                    self.type_params.insert(param.name.clone(), var);
                }

                // Build the parameterized return type
                let base_type = if type_decl.type_params.is_empty() {
                    Type::Named(type_decl.name.name.clone())
                } else {
                    Type::App {
                        constructor: Box::new(Type::Named(type_decl.name.name.clone())),
                        args: type_decl
                            .type_params
                            .iter()
                            .map(|p| self.type_params.get(&p.name).unwrap().clone())
                            .collect(),
                    }
                };

                // Register the type definition
                let type_def = self.type_def(type_decl);
                self.env.types.insert(type_decl.name.name.clone(), type_def.clone());

                // Track versioned types for schema evolution
                if let Some(version) = &type_decl.version {
                    let type_name = type_decl.name.name.clone();
                    let version_num = version.number;

                    // Store the type definition for this version
                    self.versioned_types
                        .entry(type_name.clone())
                        .or_default()
                        .insert(version_num, type_def.clone());

                    // Update latest version if this is higher
                    let current_latest = self.latest_versions.get(&type_name).copied().unwrap_or(0);
                    if version_num > current_latest {
                        self.latest_versions.insert(type_name.clone(), version_num);
                    }

                    // Register migrations (Phase 4)
                    for migration in &type_decl.migrations {
                        self.migrations
                            .entry(type_name.clone())
                            .or_default()
                            .insert(migration.from_version.number, migration.body.clone());
                    }

                    // Register in schema registry and check compatibility
                    self.schema_registry.register(&type_name, type_decl);

                    // Check compatibility with previous version if this isn't v1
                    if version_num > 1 {
                        let prev_version = version_num - 1;

                        // Check if both versions are registered
                        if self.schema_registry.get_version(&type_name, prev_version).is_some() {
                            match self.schema_registry.check_compatibility(&type_name, prev_version, version_num) {
                                Ok(Compatibility::Breaking(changes)) => {
                                    // Check if a migration exists for the breaking changes
                                    let has_migration = self.schema_registry.has_migration(&type_name, prev_version, version_num);

                                    if !has_migration {
                                        // No migration for breaking changes - this is a warning
                                        let change_descriptions: Vec<String> = changes.iter().map(|c| {
                                            match c {
                                                BreakingChange::FieldRemoved { field_name } =>
                                                    format!("field '{}' removed", field_name),
                                                BreakingChange::FieldRenamed { old_name, new_name } =>
                                                    format!("field '{}' renamed to '{}'", old_name, new_name),
                                                BreakingChange::FieldTypeChanged { field_name, old_type, new_type } =>
                                                    format!("field '{}' type changed from {} to {}", field_name, old_type, new_type),
                                                BreakingChange::RequiredFieldAdded { field_name } =>
                                                    format!("required field '{}' added", field_name),
                                            }
                                        }).collect();

                                        self.errors.push(TypeError {
                                            message: format!(
                                                "Breaking changes in {} @v{} without migration from @v{}: {}. \
                                                 Add 'from @v{} = {{ ... }}' to provide a migration.",
                                                type_name, version_num, prev_version,
                                                change_descriptions.join(", "),
                                                prev_version
                                            ),
                                            span: type_decl.name.span,
                                        });
                                    }
                                }
                                Ok(Compatibility::AutoMigrate(auto_migrations)) => {
                                    // Generate automatic migration if one wasn't provided
                                    if !self.migrations.get(&type_name).map(|m| m.contains_key(&prev_version)).unwrap_or(false) {
                                        // Get the previous version's fields to build the migration
                                        if let Some(prev_def) = self.schema_registry.get_version(&type_name, prev_version) {
                                            if let Some(generated) = generate_auto_migration_expr(
                                                &prev_def.definition,
                                                &type_decl.definition,
                                                &auto_migrations,
                                                type_decl.name.span,
                                            ) {
                                                // Register the auto-generated migration
                                                self.migrations
                                                    .entry(type_name.clone())
                                                    .or_default()
                                                    .insert(prev_version, generated);
                                            }
                                        }
                                    }
                                }
                                Ok(Compatibility::Compatible) => {
                                    // No issues - fully compatible
                                }
                                Err(_) => {
                                    // Previous version not registered yet - that's fine
                                }
                            }
                        }
                    }
                }

                // Register ADT constructors as values with polymorphic types
                if let ast::TypeDef::Enum(variants) = &type_decl.definition {
                    for variant in variants {
                        let constructor_type = match &variant.fields {
                            VariantFields::Unit => {
                                // Unit variant is just the type itself
                                base_type.clone()
                            }
                            VariantFields::Tuple(field_types) => {
                                // Tuple variant is a function from fields to the type
                                let param_types: Vec<Type> = field_types
                                    .iter()
                                    .map(|t| self.resolve_type(t))
                                    .collect();
                                Type::function(param_types, base_type.clone())
                            }
                            VariantFields::Record(fields) => {
                                // Record variant is a function from record to the type
                                let field_types: Vec<(String, Type)> = fields
                                    .iter()
                                    .map(|f| (f.name.name.clone(), self.resolve_type(&f.typ)))
                                    .collect();
                                Type::function(vec![Type::Record(field_types)], base_type.clone())
                            }
                        };
                        // Wrap in polymorphic TypeScheme for generic types
                        let scheme = TypeScheme {
                            vars: bound_vars.clone(),
                            typ: constructor_type,
                        };
                        self.env.bind(&variant.name.name, scheme);
                    }
                }

                // Restore old type params
                self.type_params = old_params;
            }
            Declaration::Handler(handler) => {
                let handler_def = self.handler_def(handler);
                self.env
                    .handlers
                    .insert(handler.name.name.clone(), handler_def);
                // Also bind the handler as a value so it can be referenced in run...with expressions
                // Handler type is the effect it handles (as an opaque type for now)
                let handler_type = Type::Named(format!("Handler<{}>", handler.effect.name));
                self.env.bind(&handler.name.name, TypeScheme::mono(handler_type));
            }
            Declaration::Let(let_decl) => {
                // Will be typed in second pass
                let typ = if let Some(ref type_expr) = let_decl.typ {
                    self.resolve_type(type_expr)
                } else {
                    Type::var()
                };
                self.env.bind(&let_decl.name.name, TypeScheme::mono(typ));
            }
            Declaration::Trait(trait_decl) => {
                let trait_def = self.trait_def(trait_decl);
                self.env.traits.insert(trait_decl.name.name.clone(), trait_def);
            }
            Declaration::Impl(impl_decl) => {
                // Will be checked in second pass
                let trait_impl = self.collect_impl(impl_decl);
                self.env.trait_impls.push(trait_impl);
            }
            Declaration::ExternFn(ext) => {
                // Register extern fn type signature (like a regular function but no body)
                let param_types: Vec<Type> = ext
                    .params
                    .iter()
                    .map(|p| self.resolve_type(&p.typ))
                    .collect();
                let return_type = self.resolve_type(&ext.return_type);
                let fn_type = Type::function(param_types, return_type);
                self.env.bind(&ext.name.name, TypeScheme::mono(fn_type));
            }
        }
    }

    /// Type check a declaration (second pass)
    fn check_declaration(&mut self, decl: &Declaration) {
        match decl {
            Declaration::Function(func) => {
                self.check_function(func);
            }
            Declaration::Let(let_decl) => {
                self.check_let_decl(let_decl);
            }
            Declaration::Handler(handler) => {
                self.check_handler(handler);
            }
            Declaration::Impl(impl_decl) => {
                self.check_impl(impl_decl);
            }
            // Effects, types, and traits don't need checking beyond collection
            _ => {}
        }
    }

    fn check_function(&mut self, func: &FunctionDecl) {
        // Validate that all declared effects exist
        let builtin_effects = ["Console", "Fail", "State", "Reader", "Random", "Time", "File", "Process", "Http", "HttpServer", "Test", "Sql", "Postgres"];
        for effect in &func.effects {
            let is_builtin = builtin_effects.contains(&effect.name.as_str());
            let is_defined = self.env.lookup_effect(&effect.name).is_some();
            if !is_builtin && !is_defined {
                // Find similar effect names for suggestion
                let mut available: Vec<&str> = builtin_effects.to_vec();
                available.extend(self.env.effects.keys().map(|s| s.as_str()));
                let suggestions = find_similar_names(&effect.name, available, 2);

                let mut message = format!("Unknown effect: {}", effect.name);
                if let Some(hint) = format_did_you_mean(&suggestions) {
                    message.push_str(&format!(". {}", hint));
                }
                self.errors.push(TypeError {
                    message,
                    span: effect.span,
                });
            }
        }

        // Set up the environment with parameters
        let mut local_env = self.env.clone();
        for param in &func.params {
            let param_type = self.resolve_type(&param.typ);
            local_env.bind(&param.name.name, TypeScheme::mono(param_type));
        }

        // Determine if we need to infer effects
        let explicit_effects = !func.effects.is_empty();
        let declared_effects = EffectSet::from_iter(func.effects.iter().map(|e| e.name.clone()));

        // Save old state
        let old_effects = std::mem::replace(&mut self.current_effects, declared_effects.clone());
        let old_inferring = std::mem::replace(&mut self.inferring_effects, !explicit_effects);
        let old_inferred = std::mem::replace(&mut self.inferred_effects, EffectSet::empty());

        // Type check the body
        let old_env = std::mem::replace(&mut self.env, local_env);
        let body_type = self.infer_expr(&func.body);
        self.env = old_env;

        // Get the inferred effects before restoring state
        let inferred = std::mem::replace(&mut self.inferred_effects, old_inferred);

        // Restore state
        self.current_effects = old_effects;
        self.inferring_effects = old_inferring;

        // Check that body type matches return type (expand type aliases for record types)
        let return_type = self.resolve_type(&func.return_type);
        if let Err(e) = unify_with_env(&body_type, &return_type, &self.env) {
            self.errors.push(TypeError {
                message: format!(
                    "Function '{}' body has type {}, but declared return type is {}: {}",
                    func.name.name, body_type, return_type, e
                ),
                span: func.span,
            });
        }

        // Check behavioral properties
        let properties = PropertySet::from_ast(&func.properties);

        // Pure functions cannot have effects
        let effective_effects = if explicit_effects {
            &declared_effects
        } else {
            &inferred
        };

        if properties.is_pure() && !effective_effects.is_empty() {
            let effects_str = if explicit_effects {
                func.effects
                    .iter()
                    .map(|e| e.name.as_str())
                    .collect::<Vec<_>>()
                    .join(", ")
            } else {
                format!("{} (inferred)", inferred)
            };
            self.errors.push(TypeError {
                message: format!(
                    "Function '{}' is declared as pure but has effects: {{{}}}",
                    func.name.name, effects_str
                ),
                span: func.span,
            });
        }

        // Deterministic functions cannot use non-deterministic effects (Random, Time)
        if properties.contains(Property::Deterministic) {
            let non_det_effects: Vec<_> = effective_effects
                .effects
                .iter()
                .filter(|e| matches!(e.as_str(), "Random" | "Time"))
                .cloned()
                .collect();
            if !non_det_effects.is_empty() {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as deterministic but uses non-deterministic effects: {{{}}}",
                        func.name.name,
                        non_det_effects.join(", ")
                    ),
                    span: func.span,
                });
            }
        }

        // Commutative functions must have 2 params and use a commutative operation
        if properties.contains(Property::Commutative) {
            if func.params.len() != 2 {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as commutative but has {} parameters (expected 2)",
                        func.name.name,
                        func.params.len()
                    ),
                    span: func.span,
                });
            } else if !is_commutative_body(&func.body, &func.params[0].name.name, &func.params[1].name.name) {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as commutative but its body is not a commutative operation on its parameters",
                        func.name.name
                    ),
                    span: func.span,
                });
            }
        }

        // Idempotent functions must satisfy f(f(x)) == f(x)
        // We verify this through pattern recognition
        if properties.contains(Property::Idempotent) {
            if !is_idempotent_body(&func.body, &func.params) {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as idempotent but could not be verified. \
                         Recognized patterns: identity, constants, clamping, projections, abs. \
                         Use 'assume is idempotent' if you're certain it is idempotent.",
                        func.name.name
                    ),
                    span: func.span,
                });
            }
        }

        // Total functions must terminate and cannot fail
        if properties.is_total() {
            // Check 1: Cannot use Fail effect
            if effective_effects.contains("Fail") {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as total but uses the Fail effect",
                        func.name.name
                    ),
                    span: func.span,
                });
            }

            // Check 2: Must terminate (structural recursion)
            if let Err(reason) = check_termination(func) {
                self.errors.push(TypeError {
                    message: format!(
                        "Function '{}' is declared as total but may not terminate: {}",
                        func.name.name, reason
                    ),
                    span: func.span,
                });
            }
        }

        // If effects were declared, verify that inferred effects are a subset
        if explicit_effects && !inferred.is_subset(&declared_effects) {
            let missing: Vec<_> = inferred
                .effects
                .iter()
                .filter(|e| !declared_effects.contains(e))
                .cloned()
                .collect();
            self.errors.push(TypeError {
                message: format!(
                    "Function '{}' uses effects {{{}}} but only declares {{{}}}",
                    func.name.name,
                    missing.join(", "),
                    declared_effects
                ),
                span: func.span,
            });
        }

        // Check where clause property constraints
        for where_clause in &func.where_clauses {
            match where_clause {
                ast::WhereClause::PropertyConstraint {
                    type_param,
                    property,
                    span,
                } => {
                    // Find which parameter has this type and record the constraint
                    let param_with_type = func.params.iter().find(|p| {
                        // Check if param's type is the type parameter
                        if let TypeExpr::Named(name) = &p.typ {
                            name.name == type_param.name
                        } else {
                            false
                        }
                    });

                    if let Some((param_index, param)) = func.params.iter().enumerate().find(|(_, p)| {
                        if let TypeExpr::Named(name) = &p.typ {
                            name.name == type_param.name
                        } else {
                            false
                        }
                    }) {
                        // Record the constraint for checking at call sites
                        let constraints = self
                            .property_constraints
                            .entry(func.name.name.clone())
                            .or_insert_with(Vec::new);

                        // Check if we already have a constraint for this param
                        if let Some(existing) = constraints.iter_mut().find(|c| c.param_name == param.name.name) {
                            existing.required_properties.insert(Property::from(*property));
                        } else {
                            let mut props = PropertySet::empty();
                            props.insert(Property::from(*property));
                            constraints.push(ParamPropertyConstraint {
                                param_name: param.name.name.clone(),
                                param_index,
                                required_properties: props,
                            });
                        }
                    } else if !func.type_params.iter().any(|p| p.name == type_param.name)
                        && !func.params.iter().any(|p| p.name.name == type_param.name)
                    {
                        self.errors.push(TypeError {
                            message: format!(
                                "Unknown type parameter '{}' in where clause",
                                type_param.name
                            ),
                            span: *span,
                        });
                    }
                }
                ast::WhereClause::ResultRefinement { predicate, span } => {
                    // Result refinements are checked at runtime or via SMT solver
                    // For now, we just type-check the predicate expression
                    // (would need 'result' in scope, which we don't have yet)
                }
                ast::WhereClause::TraitConstraint(constraint) => {
                    // Validate that the type parameter exists
                    if !func.type_params.iter().any(|p| p.name == constraint.type_param.name)
                        && !func.params.iter().any(|p| p.name.name == constraint.type_param.name)
                    {
                        self.errors.push(TypeError {
                            message: format!(
                                "Unknown type parameter '{}' in where clause",
                                constraint.type_param.name
                            ),
                            span: constraint.span,
                        });
                    }
                    // Validate that each trait in the bounds exists
                    for bound in &constraint.bounds {
                        if !self.env.traits.contains_key(&bound.trait_name.name) {
                            // Find similar trait names for suggestion
                            let available_traits: Vec<&str> = self.env.traits.keys()
                                .map(|s| s.as_str())
                                .collect();
                            let suggestions = find_similar_names(&bound.trait_name.name, available_traits, 2);

                            let mut message = format!("Unknown trait: {}", bound.trait_name.name);
                            if let Some(hint) = format_did_you_mean(&suggestions) {
                                message.push_str(&format!(". {}", hint));
                            }

                            self.errors.push(TypeError {
                                message,
                                span: bound.span,
                            });
                        }
                    }
                }
            }
        }
    }

    fn check_let_decl(&mut self, let_decl: &LetDecl) {
        let inferred = self.infer_expr(&let_decl.value);

        // Use the declared type if present, otherwise use inferred
        let final_type = if let Some(ref type_expr) = let_decl.typ {
            let declared = self.resolve_type(type_expr);
            if let Err(e) = unify_with_env(&inferred, &declared, &self.env) {
                self.errors.push(TypeError {
                    message: format!(
                        "Variable '{}' has type {}, but declared type is {}: {}",
                        let_decl.name.name, inferred, declared, e
                    ),
                    span: let_decl.span,
                });
            }
            // Use declared type (preserves version annotations)
            declared
        } else {
            inferred
        };

        // Update the binding with the final type
        let scheme = self.env.generalize(&final_type);
        self.env.bind(&let_decl.name.name, scheme);
    }

    fn check_handler(&mut self, handler: &HandlerDecl) {
        // Look up the effect being handled
        let effect = match self.env.lookup_effect(&handler.effect.name) {
            Some(e) => e.clone(),
            None => {
                // Find similar effect names for suggestion
                let available_effects: Vec<&str> = self.env.effects.keys()
                    .map(|s| s.as_str())
                    .collect();
                let suggestions = find_similar_names(&handler.effect.name, available_effects, 2);

                let mut message = format!("Unknown effect: {}", handler.effect.name);
                if let Some(hint) = format_did_you_mean(&suggestions) {
                    message.push_str(&format!(". {}", hint));
                }

                self.errors.push(TypeError {
                    message,
                    span: handler.effect.span,
                });
                return;
            }
        };

        // Check each implementation
        for impl_ in &handler.implementations {
            let op = match effect
                .operations
                .iter()
                .find(|o| o.name == impl_.op_name.name)
            {
                Some(o) => o.clone(),
                None => {
                    self.errors.push(TypeError {
                        message: format!(
                            "Effect '{}' has no operation '{}'",
                            handler.effect.name, impl_.op_name.name
                        ),
                        span: impl_.op_name.span,
                    });
                    continue;
                }
            };

            // Set up environment with operation parameters
            let mut local_env = self.env.clone();
            for (i, param_name) in impl_.params.iter().enumerate() {
                if i < op.params.len() {
                    local_env.bind(&param_name.name, TypeScheme::mono(op.params[i].1.clone()));
                }
            }

            // Add resume if present
            if let Some(ref resume) = impl_.resume {
                // resume has type: fn(return_type) -> result_type
                let resume_type = Type::function(vec![op.return_type.clone()], Type::var());
                local_env.bind(&resume.name, TypeScheme::mono(resume_type));
            }

            // Type check the implementation body
            let old_env = std::mem::replace(&mut self.env, local_env);
            let _body_type = self.infer_expr(&impl_.body);
            self.env = old_env;
        }
    }

    /// Infer the type of an expression
    fn infer_expr(&mut self, expr: &Expr) -> Type {
        match expr {
            Expr::Literal(lit) => self.infer_literal(lit),

            Expr::Var(ident) => match self.env.lookup(&ident.name) {
                Some(scheme) => scheme.instantiate(),
                None => {
                    // Find similar variable names for "Did you mean?" suggestion
                    let available_names: Vec<&str> = self.env.bindings.keys()
                        .map(|s| s.as_str())
                        .collect();
                    let suggestions = find_similar_names(&ident.name, available_names, 2);

                    let mut message = format!("Undefined variable: {}", ident.name);
                    if let Some(hint) = format_did_you_mean(&suggestions) {
                        message.push_str(&format!(". {}", hint));
                    }

                    self.errors.push(TypeError {
                        message,
                        span: ident.span,
                    });
                    Type::Error
                }
            },

            Expr::BinaryOp {
                op,
                left,
                right,
                span,
            } => self.infer_binary_op(*op, left, right, *span),

            Expr::UnaryOp { op, operand, span } => self.infer_unary_op(*op, operand, *span),

            Expr::Call { func, args, span } => self.infer_call(func, args, *span),

            Expr::EffectOp {
                effect,
                operation,
                args,
                span,
            } => self.infer_effect_op(effect, operation, args, *span),

            Expr::Field {
                object,
                field,
                span,
            } => self.infer_field(object, field, *span),

            Expr::TupleIndex {
                object,
                index,
                span,
            } => {
                let object_type = self.infer_expr(object);
                match &object_type {
                    Type::Tuple(types) => {
                        if *index < types.len() {
                            types[*index].clone()
                        } else {
                            self.errors.push(TypeError {
                                message: format!(
                                    "Tuple index {} out of bounds for tuple with {} elements",
                                    index,
                                    types.len()
                                ),
                                span: *span,
                            });
                            Type::Error
                        }
                    }
                    Type::Var(_) => Type::var(),
                    _ => {
                        self.errors.push(TypeError {
                            message: format!(
                                "Cannot use tuple index on non-tuple type {}",
                                object_type
                            ),
                            span: *span,
                        });
                        Type::Error
                    }
                }
            }

            Expr::Lambda {
                params,
                return_type,
                effects,
                body,
                span,
            } => self.infer_lambda(params, return_type.as_deref(), effects, body, *span),

            Expr::Let {
                name,
                typ,
                value,
                body,
                span,
            } => self.infer_let(name, typ.as_ref(), value, body, *span),

            Expr::If {
                condition,
                then_branch,
                else_branch,
                span,
            } => self.infer_if(condition, then_branch, else_branch, *span),

            Expr::Match {
                scrutinee,
                arms,
                span,
            } => self.infer_match(scrutinee, arms, *span),

            Expr::Block {
                statements,
                result,
                span,
            } => self.infer_block(statements, result, *span),

            Expr::Record {
                spread,
                fields,
                span,
            } => self.infer_record(spread.as_deref(), fields, *span),

            Expr::Tuple { elements, span } => self.infer_tuple(elements, *span),

            Expr::List { elements, span } => self.infer_list(elements, *span),

            Expr::Run {
                expr,
                handlers,
                span,
            } => self.infer_run(expr, handlers, *span),

            Expr::Resume { value, span } => {
                // Resume is special - it continues the computation
                // For now, just infer the value type
                let _ = self.infer_expr(value);
                Type::var() // Resume's type depends on context
            }
        }
    }

    fn infer_literal(&self, lit: &Literal) -> Type {
        match &lit.kind {
            LiteralKind::Int(_) => Type::Int,
            LiteralKind::Float(_) => Type::Float,
            LiteralKind::String(_) => Type::String,
            LiteralKind::Char(_) => Type::Char,
            LiteralKind::Bool(_) => Type::Bool,
            LiteralKind::Unit => Type::Unit,
        }
    }

    fn infer_binary_op(&mut self, op: BinaryOp, left: &Expr, right: &Expr, span: Span) -> Type {
        let left_type = self.infer_expr(left);
        let right_type = self.infer_expr(right);

        match op {
            BinaryOp::Add => {
                // Add supports both numeric types and string concatenation
                if let Err(e) = unify_with_env(&left_type, &right_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operands of '{}' must have same type: {}", op, e),
                        span,
                    });
                }
                match &left_type {
                    Type::Int | Type::Float | Type::String | Type::Var(_) => left_type,
                    _ => {
                        self.errors.push(TypeError {
                            message: format!(
                                "Operator '{}' requires numeric or string operands, got {}",
                                op, left_type
                            ),
                            span,
                        });
                        Type::Error
                    }
                }
            }

            BinaryOp::Concat => {
                // Concat (++) supports strings and lists
                if let Err(e) = unify_with_env(&left_type, &right_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operands of '++' must have same type: {}", e),
                        span,
                    });
                }
                match &left_type {
                    Type::String | Type::List(_) | Type::Var(_) => left_type,
                    _ => {
                        self.errors.push(TypeError {
                            message: format!(
                                "Operator '++' requires String or List operands, got {}",
                                left_type
                            ),
                            span,
                        });
                        Type::Error
                    }
                }
            }

            BinaryOp::Sub | BinaryOp::Mul | BinaryOp::Div | BinaryOp::Mod => {
                // Arithmetic: both operands must be same numeric type
                if let Err(e) = unify_with_env(&left_type, &right_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operands of '{}' must have same type: {}", op, e),
                        span,
                    });
                }
                // Check that they're numeric
                match &left_type {
                    Type::Int | Type::Float | Type::Var(_) => left_type,
                    _ => {
                        self.errors.push(TypeError {
                            message: format!(
                                "Operator '{}' requires numeric operands, got {}",
                                op, left_type
                            ),
                            span,
                        });
                        Type::Error
                    }
                }
            }

            BinaryOp::Eq | BinaryOp::Ne => {
                // Equality: operands must have same type
                if let Err(e) = unify_with_env(&left_type, &right_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operands of '{}' must have same type: {}", op, e),
                        span,
                    });
                }
                Type::Bool
            }

            BinaryOp::Lt | BinaryOp::Le | BinaryOp::Gt | BinaryOp::Ge => {
                // Comparison: operands must be same orderable type
                if let Err(e) = unify_with_env(&left_type, &right_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operands of '{}' must have same type: {}", op, e),
                        span,
                    });
                }
                Type::Bool
            }

            BinaryOp::And | BinaryOp::Or => {
                // Logical: both must be Bool
                if let Err(e) = unify_with_env(&left_type, &Type::Bool, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Left operand of '{}' must be Bool: {}", op, e),
                        span: left.span(),
                    });
                }
                if let Err(e) = unify_with_env(&right_type, &Type::Bool, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Right operand of '{}' must be Bool: {}", op, e),
                        span: right.span(),
                    });
                }
                Type::Bool
            }

            BinaryOp::Pipe => {
                // Pipe: a |> f means f(a)
                // right must be a function that accepts left's type
                let result_type = Type::var();
                let expected_fn = Type::function(vec![left_type.clone()], result_type.clone());
                if let Err(e) = unify_with_env(&right_type, &expected_fn, &self.env) {
                    self.errors.push(TypeError {
                        message: format!(
                            "Pipe target must be a function accepting {}: {}",
                            left_type, e
                        ),
                        span,
                    });
                }
                result_type
            }
        }
    }

    fn infer_unary_op(&mut self, op: UnaryOp, operand: &Expr, span: Span) -> Type {
        let operand_type = self.infer_expr(operand);

        match op {
            UnaryOp::Neg => match &operand_type {
                Type::Int | Type::Float | Type::Var(_) => operand_type,
                _ => {
                    self.errors.push(TypeError {
                        message: format!(
                            "Operator '-' requires numeric operand, got {}",
                            operand_type
                        ),
                        span,
                    });
                    Type::Error
                }
            },
            UnaryOp::Not => {
                if let Err(e) = unify_with_env(&operand_type, &Type::Bool, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Operator '!' requires Bool operand: {}", e),
                        span,
                    });
                }
                Type::Bool
            }
        }
    }

    fn infer_call(&mut self, func: &Expr, args: &[Expr], span: Span) -> Type {
        let func_type = self.infer_expr(func);
        let arg_types: Vec<Type> = args.iter().map(|a| self.infer_expr(a)).collect();

        // Propagate effects from callback arguments to enclosing scope
        for arg_type in &arg_types {
            if let Type::Function { effects, .. } = arg_type {
                for effect in &effects.effects {
                    if self.inferring_effects {
                        self.inferred_effects.insert(effect.clone());
                    }
                }
            }
        }

        // Check property constraints from where clauses
        if let Expr::Var(func_id) = func {
            if let Some(constraints) = self.property_constraints.get(&func_id.name).cloned() {
                for constraint in &constraints {
                    // Check if the argument at the constrained position satisfies the constraint
                    if constraint.param_index < args.len() {
                        let arg = &args[constraint.param_index];
                        let arg_props = self.get_expr_properties(arg);

                        if !arg_props.satisfies(&constraint.required_properties) {
                            self.errors.push(TypeError {
                                message: format!(
                                    "Argument '{}' to '{}' does not satisfy property constraint: \
                                     expected {:?}, but argument has {:?}",
                                    constraint.param_name,
                                    func_id.name,
                                    constraint.required_properties,
                                    arg_props
                                ),
                                span: arg.span(),
                            });
                        }
                    }
                }
            }
        }

        let result_type = Type::var();
        // Include current effects in the expected function type
        // This allows calling functions that require effects when those effects are available
        let expected_fn = Type::function_with_effects(
            arg_types.clone(),
            result_type.clone(),
            self.current_effects.clone(),
        );

        match unify_with_env(&func_type, &expected_fn, &self.env) {
            Ok(subst) => result_type.apply(&subst),
            Err(e) => {
                // Provide more detailed error message based on the type of mismatch
                let message = if e.contains("arity mismatch") || e.contains("different number") {
                    // Try to extract actual function arity
                    if let Type::Function { params, .. } = &func_type {
                        format!(
                            "Function expects {} argument(s), but {} were provided",
                            params.len(),
                            arg_types.len()
                        )
                    } else {
                        format!("Type mismatch in function call: {}", e)
                    }
                } else if e.contains("Effect mismatch") {
                    format!("Type mismatch in function call: {}", e)
                } else {
                    // Get function name if available for better error
                    let fn_name = if let Expr::Var(id) = func {
                        Some(id.name.clone())
                    } else {
                        None
                    };

                    if let Some(name) = fn_name {
                        format!("Type error in call to '{}': {}", name, e)
                    } else {
                        format!("Type mismatch in function call: {}", e)
                    }
                };

                self.errors.push(TypeError { message, span });
                Type::Error
            }
        }
    }

    /// Get the behavioral properties of an expression (conservative)
    fn get_expr_properties(&self, expr: &Expr) -> PropertySet {
        match expr {
            Expr::Var(id) => {
                // Look up the function and get its properties
                if let Some(scheme) = self.env.lookup(&id.name) {
                    let typ = scheme.instantiate();
                    if let Type::Function { properties, .. } = typ {
                        return properties;
                    }
                }
                PropertySet::empty()
            }
            // Lambdas: could analyze but for now be conservative
            Expr::Lambda { .. } => PropertySet::empty(),
            // Other expressions: no properties
            _ => PropertySet::empty(),
        }
    }

    fn infer_effect_op(
        &mut self,
        effect: &Ident,
        operation: &Ident,
        args: &[Expr],
        span: Span,
    ) -> Type {
        // Check if this is actually a module access, not an effect operation
        // This includes stdlib modules (List, String, etc.) and user-imported modules
        if let Some(scheme) = self.env.lookup(&effect.name) {
            let module_type = scheme.instantiate();
            // Get the field type - if it's a Record, treat it as a module
            if let Type::Record(fields) = &module_type {
                if let Some((_, field_type)) = fields.iter().find(|(n, _)| n == &operation.name) {
                    // It's a function call on a module field
                    let arg_types: Vec<Type> = args.iter().map(|a| self.infer_expr(a)).collect();

                    // Propagate effects from callback arguments to enclosing scope
                    for arg_type in &arg_types {
                        if let Type::Function { effects, .. } = arg_type {
                            for effect in &effects.effects {
                                if self.inferring_effects {
                                    self.inferred_effects.insert(effect.clone());
                                }
                            }
                        }
                    }

                    let result_type = Type::var();
                    let expected_fn = Type::function(arg_types, result_type.clone());

                    if let Err(e) = unify_with_env(field_type, &expected_fn, &self.env) {
                        self.errors.push(TypeError {
                            message: format!(
                                "Type mismatch in {}.{} call: {}",
                                effect.name, operation.name, e
                            ),
                            span,
                        });
                    }
                    return result_type;
                } else {
                    self.errors.push(TypeError {
                        message: format!(
                            "Module '{}' has no member '{}'",
                            effect.name, operation.name
                        ),
                        span,
                    });
                    return Type::Error;
                }
            }
            // Fall through to normal error handling if module field not found
        }

        // Built-in effects are always available
        let builtin_effects = ["Console", "Fail", "State", "Reader", "Random", "Time", "File", "Process", "Http", "HttpServer", "Test", "Sql", "Postgres"];
        let is_builtin = builtin_effects.contains(&effect.name.as_str());

        // Track this effect for inference
        if self.inferring_effects {
            self.inferred_effects.insert(effect.name.clone());
        }

        // Check that we're in a context that allows this effect
        // Skip this check if we're inferring effects (no explicit declaration)
        if !self.inferring_effects && !is_builtin && !self.current_effects.contains(&effect.name) {
            self.errors.push(TypeError {
                message: format!(
                    "Effect '{}' not available in current context. Available: {{{}}}",
                    effect.name, self.current_effects
                ),
                span,
            });
        }

        // Look up the operation - clone to avoid borrow issues
        let op = self
            .env
            .lookup_effect_op(&effect.name, &operation.name)
            .cloned();

        match op {
            Some(op) => {
                // Check argument types
                let arg_types: Vec<Type> = args.iter().map(|a| self.infer_expr(a)).collect();

                // Propagate effects from callback arguments to enclosing scope
                for arg_type in &arg_types {
                    if let Type::Function { effects, .. } = arg_type {
                        for effect in &effects.effects {
                            if self.inferring_effects {
                                self.inferred_effects.insert(effect.clone());
                            }
                        }
                    }
                }

                if arg_types.len() != op.params.len() {
                    self.errors.push(TypeError {
                        message: format!(
                            "Effect operation '{}.{}' expects {} arguments, got {}",
                            effect.name,
                            operation.name,
                            op.params.len(),
                            arg_types.len()
                        ),
                        span,
                    });
                }

                for (i, (arg_type, (_, param_type))) in
                    arg_types.iter().zip(op.params.iter()).enumerate()
                {
                    if let Err(e) = unify_with_env(arg_type, param_type, &self.env) {
                        self.errors.push(TypeError {
                            message: format!(
                                "Argument {} of '{}.{}' has type {}, expected {}: {}",
                                i + 1,
                                effect.name,
                                operation.name,
                                arg_type,
                                param_type,
                                e
                            ),
                            span,
                        });
                    }
                }

                op.return_type.clone()
            }
            None => {
                self.errors.push(TypeError {
                    message: format!(
                        "Unknown effect operation: {}.{}",
                        effect.name, operation.name
                    ),
                    span,
                });
                Type::Error
            }
        }
    }

    fn infer_field(&mut self, object: &Expr, field: &Ident, span: Span) -> Type {
        let object_type = self.infer_expr(object);
        let object_type = self.env.expand_type_alias(&object_type);

        match &object_type {
            Type::Record(fields) => match fields.iter().find(|(n, _)| n == &field.name) {
                Some((_, t)) => t.clone(),
                None => {
                    // Find similar field names
                    let available_fields: Vec<&str> = fields.iter().map(|(n, _)| n.as_str()).collect();
                    let suggestions = find_similar_names(&field.name, available_fields.clone(), 2);

                    let mut message = format!("Record has no field '{}'", field.name);
                    if let Some(hint) = format_did_you_mean(&suggestions) {
                        message.push_str(&format!(". {}", hint));
                    } else if !available_fields.is_empty() {
                        message.push_str(&format!(". Available fields: {}", available_fields.join(", ")));
                    }

                    self.errors.push(TypeError { message, span });
                    Type::Error
                }
            },
            Type::Var(_) => {
                // Can't infer field access on unknown type
                Type::var()
            }
            _ => {
                self.errors.push(TypeError {
                    message: format!(
                        "Cannot access field '{}' on non-record type {}",
                        field.name, object_type
                    ),
                    span,
                });
                Type::Error
            }
        }
    }

    fn infer_lambda(
        &mut self,
        params: &[Parameter],
        return_type: Option<&TypeExpr>,
        effects: &[Ident],
        body: &Expr,
        _span: Span,
    ) -> Type {
        // Set up environment with parameters
        let mut local_env = self.env.clone();
        let param_types: Vec<Type> = params
            .iter()
            .map(|p| {
                let t = self.resolve_type(&p.typ);
                local_env.bind(&p.name.name, TypeScheme::mono(t.clone()));
                t
            })
            .collect();

        // Determine if we need to infer effects for this lambda
        let explicit_effects = !effects.is_empty();
        let declared_effects = EffectSet::from_iter(effects.iter().map(|e| e.name.clone()));

        // Save old state
        let old_effects = std::mem::replace(&mut self.current_effects, declared_effects.clone());
        let old_inferring = std::mem::replace(&mut self.inferring_effects, !explicit_effects);
        let old_inferred = std::mem::replace(&mut self.inferred_effects, EffectSet::empty());

        // Type check body
        let old_env = std::mem::replace(&mut self.env, local_env);
        let body_type = self.infer_expr(body);
        self.env = old_env;

        // Get the inferred effects before restoring state
        let inferred = std::mem::replace(&mut self.inferred_effects, old_inferred);

        // Restore state
        self.current_effects = old_effects;
        self.inferring_effects = old_inferring;

        // Check return type if specified
        let ret_type = if let Some(rt) = return_type {
            let declared = self.resolve_type(rt);
            if let Err(e) = unify_with_env(&body_type, &declared, &self.env) {
                self.errors.push(TypeError {
                    message: format!(
                        "Lambda body type {} doesn't match declared {}: {}",
                        body_type, declared, e
                    ),
                    span: body.span(),
                });
            }
            declared
        } else {
            body_type
        };

        // Use inferred effects if not explicitly declared
        let final_effects = if explicit_effects {
            declared_effects
        } else {
            inferred
        };

        Type::function_with_effects(param_types, ret_type, final_effects)
    }

    fn infer_let(
        &mut self,
        name: &Ident,
        typ: Option<&TypeExpr>,
        value: &Expr,
        body: &Expr,
        _span: Span,
    ) -> Type {
        let value_type = self.infer_expr(value);

        // Check declared type if present (expand type aliases for record types)
        if let Some(type_expr) = typ {
            let declared = self.resolve_type(type_expr);
            if let Err(e) = unify_with_env(&value_type, &declared, &self.env) {
                self.errors.push(TypeError {
                    message: format!(
                        "Variable '{}' has type {}, but declared type is {}: {}",
                        name.name, value_type, declared, e
                    ),
                    span: name.span,
                });
            }
        }

        // Extend environment and check body
        let scheme = self.env.generalize(&value_type);
        let old_env = self.env.clone();
        self.env.bind(&name.name, scheme);
        let body_type = self.infer_expr(body);
        self.env = old_env;

        body_type
    }

    fn infer_if(
        &mut self,
        condition: &Expr,
        then_branch: &Expr,
        else_branch: &Expr,
        span: Span,
    ) -> Type {
        let cond_type = self.infer_expr(condition);
        if let Err(e) = unify_with_env(&cond_type, &Type::Bool, &self.env) {
            self.errors.push(TypeError {
                message: format!("If condition must be Bool, got {}: {}", cond_type, e),
                span: condition.span(),
            });
        }

        let then_type = self.infer_expr(then_branch);
        let else_type = self.infer_expr(else_branch);

        match unify_with_env(&then_type, &else_type, &self.env) {
            Ok(subst) => then_type.apply(&subst),
            Err(e) => {
                self.errors.push(TypeError {
                    message: format!(
                        "If branches have incompatible types: then={}, else={}: {}",
                        then_type, else_type, e
                    ),
                    span,
                });
                Type::Error
            }
        }
    }

    fn infer_match(&mut self, scrutinee: &Expr, arms: &[MatchArm], span: Span) -> Type {
        let scrutinee_type = self.infer_expr(scrutinee);

        if arms.is_empty() {
            self.errors.push(TypeError {
                message: "Match expression must have at least one arm".to_string(),
                span,
            });
            return Type::Error;
        }

        let mut result_type: Option<Type> = None;

        for arm in arms {
            // Check pattern and get bindings
            let bindings = self.check_pattern(&arm.pattern, &scrutinee_type);

            // Extend environment with pattern bindings
            let old_env = self.env.clone();
            for (name, typ) in bindings {
                self.env.bind(name, TypeScheme::mono(typ));
            }

            // Check guard if present
            if let Some(ref guard) = arm.guard {
                let guard_type = self.infer_expr(guard);
                if let Err(e) = unify_with_env(&guard_type, &Type::Bool, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Match guard must be Bool: {}", e),
                        span: guard.span(),
                    });
                }
            }

            // Check body
            let body_type = self.infer_expr(&arm.body);
            self.env = old_env;

            // Unify with previous arms
            match &result_type {
                None => result_type = Some(body_type),
                Some(prev) => {
                    if let Err(e) = unify_with_env(prev, &body_type, &self.env) {
                        self.errors.push(TypeError {
                            message: format!(
                                "Match arm has incompatible type: expected {}, got {}: {}",
                                prev, body_type, e
                            ),
                            span: arm.span,
                        });
                    }
                }
            }
        }

        // Check exhaustiveness
        let exhaustiveness = check_exhaustiveness(&scrutinee_type, arms, &self.env);

        if !exhaustiveness.is_exhaustive {
            let hint = missing_patterns_hint(&exhaustiveness.missing_patterns);
            self.errors.push(TypeError {
                message: format!(
                    "Non-exhaustive pattern match. {}",
                    hint
                ),
                span,
            });
        }

        // Warn about redundant arms
        for idx in exhaustiveness.redundant_arms {
            self.errors.push(TypeError {
                message: format!(
                    "Redundant pattern: this arm will never be matched because previous patterns cover all cases"
                ),
                span: arms[idx].span,
            });
        }

        result_type.unwrap_or(Type::Error)
    }

    fn check_pattern(&mut self, pattern: &Pattern, expected: &Type) -> Vec<(String, Type)> {
        match pattern {
            Pattern::Wildcard(_) => Vec::new(),

            Pattern::Var(ident) => {
                vec![(ident.name.clone(), expected.clone())]
            }

            Pattern::Literal(lit) => {
                let lit_type = self.infer_literal(lit);
                if let Err(e) = unify_with_env(&lit_type, expected, &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Pattern literal type mismatch: {}", e),
                        span: lit.span,
                    });
                }
                Vec::new()
            }

            Pattern::Constructor { name, fields, span, .. } => {
                // Look up constructor
                // For now, handle Option specially
                match name.name.as_str() {
                    "None" => {
                        if let Err(e) = unify_with_env(expected, &Type::Option(Box::new(Type::var())), &self.env) {
                            self.errors.push(TypeError {
                                message: format!(
                                    "None pattern doesn't match type {}: {}",
                                    expected, e
                                ),
                                span: *span,
                            });
                        }
                        Vec::new()
                    }
                    "Some" => {
                        let inner_type = Type::var();
                        if let Err(e) = unify_with_env(expected, &Type::Option(Box::new(inner_type.clone())), &self.env)
                        {
                            self.errors.push(TypeError {
                                message: format!(
                                    "Some pattern doesn't match type {}: {}",
                                    expected, e
                                ),
                                span: *span,
                            });
                        }
                        if fields.len() == 1 {
                            self.check_pattern(&fields[0], &inner_type)
                        } else {
                            Vec::new()
                        }
                    }
                    _ => {
                        // Generic constructor handling
                        let mut bindings = Vec::new();
                        for field in fields {
                            bindings.extend(self.check_pattern(field, &Type::var()));
                        }
                        bindings
                    }
                }
            }

            Pattern::Tuple { elements, span } => {
                let element_types: Vec<Type> = elements.iter().map(|_| Type::var()).collect();
                if let Err(e) = unify_with_env(expected, &Type::Tuple(element_types.clone()), &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Tuple pattern doesn't match type {}: {}", expected, e),
                        span: *span,
                    });
                }

                let mut bindings = Vec::new();
                for (elem, typ) in elements.iter().zip(element_types.iter()) {
                    bindings.extend(self.check_pattern(elem, typ));
                }
                bindings
            }

            Pattern::Record { fields, span } => {
                let field_types: Vec<(String, Type)> = fields
                    .iter()
                    .map(|(n, _)| (n.name.clone(), Type::var()))
                    .collect();

                if let Err(e) = unify_with_env(expected, &Type::Record(field_types.clone()), &self.env) {
                    self.errors.push(TypeError {
                        message: format!("Record pattern doesn't match type {}: {}", expected, e),
                        span: *span,
                    });
                }

                let mut bindings = Vec::new();
                for ((_, pattern), (_, typ)) in fields.iter().zip(field_types.iter()) {
                    bindings.extend(self.check_pattern(pattern, typ));
                }
                bindings
            }
        }
    }

    fn infer_block(&mut self, statements: &[Statement], result: &Expr, _span: Span) -> Type {
        // Process statements
        for stmt in statements {
            match stmt {
                Statement::Expr(e) => {
                    self.infer_expr(e);
                }
                Statement::Let {
                    name, typ, value, ..
                } => {
                    let value_type = self.infer_expr(value);

                    if let Some(type_expr) = typ {
                        let declared = self.resolve_type(type_expr);
                        if let Err(e) = unify_with_env(&value_type, &declared, &self.env) {
                            self.errors.push(TypeError {
                                message: format!(
                                    "Variable '{}' has type {}, but declared type is {}: {}",
                                    name.name, value_type, declared, e
                                ),
                                span: name.span,
                            });
                        }
                    }

                    let scheme = self.env.generalize(&value_type);
                    self.env.bind(&name.name, scheme);
                }
            }
        }

        // Return the type of the result expression
        self.infer_expr(result)
    }

    fn infer_record(
        &mut self,
        spread: Option<&Expr>,
        fields: &[(Ident, Expr)],
        span: Span,
    ) -> Type {
        // Start with spread fields if present
        let mut field_types: Vec<(String, Type)> = if let Some(spread_expr) = spread {
            let spread_type = self.infer_expr(spread_expr);
            let spread_type = self.env.expand_type_alias(&spread_type);
            match spread_type {
                Type::Record(spread_fields) => spread_fields,
                _ => {
                    self.errors.push(TypeError {
                        message: format!(
                            "Spread expression must be a record type, got {}",
                            spread_type
                        ),
                        span,
                    });
                    Vec::new()
                }
            }
        } else {
            Vec::new()
        };

        // Apply explicit field overrides
        let explicit_types: Vec<(String, Type)> = fields
            .iter()
            .map(|(name, expr)| (name.name.clone(), self.infer_expr(expr)))
            .collect();

        for (name, typ) in explicit_types {
            if let Some(existing) = field_types.iter_mut().find(|(n, _)| n == &name) {
                existing.1 = typ;
            } else {
                field_types.push((name, typ));
            }
        }

        Type::Record(field_types)
    }

    fn infer_tuple(&mut self, elements: &[Expr], _span: Span) -> Type {
        let element_types: Vec<Type> = elements.iter().map(|e| self.infer_expr(e)).collect();
        Type::Tuple(element_types)
    }

    fn infer_list(&mut self, elements: &[Expr], span: Span) -> Type {
        if elements.is_empty() {
            return Type::List(Box::new(Type::var()));
        }

        let first_type = self.infer_expr(&elements[0]);
        for elem in &elements[1..] {
            let elem_type = self.infer_expr(elem);
            if let Err(e) = unify_with_env(&first_type, &elem_type, &self.env) {
                self.errors.push(TypeError {
                    message: format!("List elements must have same type: {}", e),
                    span,
                });
            }
        }

        Type::List(Box::new(first_type))
    }

    fn infer_run(&mut self, expr: &Expr, handlers: &[(Ident, Expr)], _span: Span) -> Type {
        // The handlers provide implementations for effects
        // After running, those effects are no longer present

        // Add the handled effects to available effects
        let handled_effects: EffectSet =
            EffectSet::from_iter(handlers.iter().map(|(e, _)| e.name.clone()));

        // Built-in effects are always available in run blocks (they have runtime implementations)
        let builtin_effects: EffectSet =
            EffectSet::from_iter(["Console", "Fail", "State", "Reader", "Random", "Time", "File", "Process", "Http", "HttpServer", "Sql"].iter().map(|s| s.to_string()));

        // Extend current effects with handled ones and built-in effects
        let combined = self.current_effects.union(&handled_effects).union(&builtin_effects);
        let old_effects = std::mem::replace(&mut self.current_effects, combined);

        // Type check the expression
        let result_type = self.infer_expr(expr);

        // Type check handlers
        for (effect_name, handler_expr) in handlers {
            // Just check the handler expression for now
            let _ = self.infer_expr(handler_expr);

            // Verify the effect exists
            if self.env.lookup_effect(&effect_name.name).is_none() {
                // Find similar effect names for suggestion
                let available_effects: Vec<&str> = self.env.effects.keys()
                    .map(|s| s.as_str())
                    .collect();
                let suggestions = find_similar_names(&effect_name.name, available_effects, 2);

                let mut message = format!("Unknown effect: {}", effect_name.name);
                if let Some(hint) = format_did_you_mean(&suggestions) {
                    message.push_str(&format!(". {}", hint));
                }

                self.errors.push(TypeError {
                    message,
                    span: effect_name.span,
                });
            }
        }

        self.current_effects = old_effects;
        result_type
    }

    // Helper methods

    fn function_type(&mut self, func: &FunctionDecl) -> TypeScheme {
        // Save old type params and start fresh for this function's scope
        let old_params = std::mem::take(&mut self.type_params);

        // Bind type parameters to fresh type variables
        let mut bound_vars = Vec::new();
        for param in &func.type_params {
            let var = Type::var();
            if let Type::Var(n) = &var {
                bound_vars.push(*n);
            }
            self.type_params.insert(param.name.clone(), var);
        }

        // Resolve parameter and return types (will use type_params for generics)
        let param_types: Vec<Type> = func
            .params
            .iter()
            .map(|p| self.resolve_type(&p.typ))
            .collect();

        let return_type = self.resolve_type(&func.return_type);
        let effects = EffectSet::from_iter(func.effects.iter().map(|e| e.name.clone()));
        let properties = PropertySet::from_ast(&func.properties);

        // Restore old type params
        self.type_params = old_params;

        // Return polymorphic type scheme with bound variables
        TypeScheme {
            vars: bound_vars,
            typ: Type::function_with_properties(param_types, return_type, effects, properties),
        }
    }

    fn effect_def(&self, effect: &EffectDecl) -> EffectDef {
        EffectDef {
            name: effect.name.name.clone(),
            type_params: effect.type_params.iter().map(|p| p.name.clone()).collect(),
            operations: effect
                .operations
                .iter()
                .map(|op| EffectOpDef {
                    name: op.name.name.clone(),
                    params: op
                        .params
                        .iter()
                        .map(|p| (p.name.name.clone(), self.resolve_type(&p.typ)))
                        .collect(),
                    return_type: self.resolve_type(&op.return_type),
                })
                .collect(),
        }
    }

    fn type_def(&self, type_decl: &TypeDecl) -> types::TypeDef {
        match &type_decl.definition {
            ast::TypeDef::Alias(t) => types::TypeDef::Alias(self.resolve_type(t)),
            ast::TypeDef::Record(fields) => types::TypeDef::Record(
                fields
                    .iter()
                    .map(|f| (f.name.name.clone(), self.resolve_type(&f.typ)))
                    .collect(),
            ),
            ast::TypeDef::Enum(variants) => types::TypeDef::Enum(
                variants
                    .iter()
                    .map(|v| VariantDef {
                        name: v.name.name.clone(),
                        fields: match &v.fields {
                            VariantFields::Unit => VariantFieldsDef::Unit,
                            VariantFields::Tuple(types) => VariantFieldsDef::Tuple(
                                types.iter().map(|t| self.resolve_type(t)).collect(),
                            ),
                            VariantFields::Record(fields) => VariantFieldsDef::Record(
                                fields
                                    .iter()
                                    .map(|f| (f.name.name.clone(), self.resolve_type(&f.typ)))
                                    .collect(),
                            ),
                        },
                    })
                    .collect(),
            ),
        }
    }

    fn handler_def(&self, handler: &HandlerDecl) -> HandlerDef {
        HandlerDef {
            name: handler.name.name.clone(),
            effect: handler.effect.name.clone(),
            params: handler
                .params
                .iter()
                .map(|p| (p.name.name.clone(), self.resolve_type(&p.typ)))
                .collect(),
        }
    }

    fn trait_def(&self, trait_decl: &TraitDecl) -> TraitDef {
        let methods = trait_decl
            .methods
            .iter()
            .map(|m| TraitMethodDef {
                name: m.name.name.clone(),
                type_params: m.type_params.iter().map(|p| p.name.clone()).collect(),
                params: m
                    .params
                    .iter()
                    .map(|p| (p.name.name.clone(), self.resolve_type(&p.typ)))
                    .collect(),
                return_type: self.resolve_type(&m.return_type),
                has_default: m.default_impl.is_some(),
            })
            .collect();

        let super_traits = trait_decl
            .super_traits
            .iter()
            .map(|b| TraitBoundDef {
                trait_name: b.trait_name.name.clone(),
                type_args: b.type_args.iter().map(|t| self.resolve_type(t)).collect(),
            })
            .collect();

        TraitDef {
            name: trait_decl.name.name.clone(),
            type_params: trait_decl.type_params.iter().map(|p| p.name.clone()).collect(),
            super_traits,
            methods,
        }
    }

    fn collect_impl(&self, impl_decl: &ImplDecl) -> TraitImpl {
        use std::collections::HashMap;

        let methods: HashMap<String, Type> = impl_decl
            .methods
            .iter()
            .map(|m| {
                let return_type = m
                    .return_type
                    .as_ref()
                    .map(|t| self.resolve_type(t))
                    .unwrap_or_else(Type::var);
                let param_types: Vec<Type> = m
                    .params
                    .iter()
                    .map(|p| self.resolve_type(&p.typ))
                    .collect();
                let func_type = Type::function(param_types, return_type);
                (m.name.name.clone(), func_type)
            })
            .collect();

        let constraints = impl_decl
            .constraints
            .iter()
            .map(|c| {
                let bounds = c
                    .bounds
                    .iter()
                    .map(|b| TraitBoundDef {
                        trait_name: b.trait_name.name.clone(),
                        type_args: b.type_args.iter().map(|t| self.resolve_type(t)).collect(),
                    })
                    .collect();
                (c.type_param.name.clone(), bounds)
            })
            .collect();

        TraitImpl {
            trait_name: impl_decl.trait_name.name.clone(),
            trait_args: impl_decl
                .trait_args
                .iter()
                .map(|t| self.resolve_type(t))
                .collect(),
            target_type: self.resolve_type(&impl_decl.target_type),
            type_params: impl_decl.type_params.iter().map(|p| p.name.clone()).collect(),
            constraints,
            methods,
        }
    }

    fn check_impl(&mut self, impl_decl: &ImplDecl) {
        // Verify the trait exists
        let trait_name = &impl_decl.trait_name.name;
        let trait_def = match self.env.traits.get(trait_name) {
            Some(def) => def.clone(),
            None => {
                self.errors.push(TypeError {
                    message: format!("Unknown trait: {}", trait_name),
                    span: impl_decl.span,
                });
                return;
            }
        };

        // Verify all required methods are implemented
        for method_def in &trait_def.methods {
            if !method_def.has_default {
                let implemented = impl_decl.methods.iter().any(|m| m.name.name == method_def.name);
                if !implemented {
                    self.errors.push(TypeError {
                        message: format!(
                            "Missing implementation for required method '{}' of trait '{}'",
                            method_def.name, trait_name
                        ),
                        span: impl_decl.span,
                    });
                }
            }
        }

        // Type check each implemented method
        for impl_method in &impl_decl.methods {
            // Find the method signature in the trait
            let method_def = trait_def.methods.iter().find(|m| m.name == impl_method.name.name);
            if method_def.is_none() {
                self.errors.push(TypeError {
                    message: format!(
                        "Method '{}' is not defined in trait '{}'",
                        impl_method.name.name, trait_name
                    ),
                    span: impl_method.span,
                });
                continue;
            }

            // Set up local environment with parameters
            let mut local_env = self.env.clone();
            for param in &impl_method.params {
                let param_type = self.resolve_type(&param.typ);
                local_env.bind(&param.name.name, TypeScheme::mono(param_type));
            }

            // Type check the body
            let old_env = std::mem::replace(&mut self.env, local_env);
            let body_type = self.infer_expr(&impl_method.body);
            self.env = old_env;

            // Check return type matches if specified
            if let Some(ref return_type_expr) = impl_method.return_type {
                let return_type = self.resolve_type(return_type_expr);
                if let Err(e) = unify_with_env(&body_type, &return_type, &self.env) {
                    self.errors.push(TypeError {
                        message: format!(
                            "Method '{}' body has type {}, but declared return type is {}: {}",
                            impl_method.name.name, body_type, return_type, e
                        ),
                        span: impl_method.span,
                    });
                }
            }
        }
    }

    fn resolve_type(&self, type_expr: &TypeExpr) -> Type {
        match type_expr {
            TypeExpr::Named(ident) => match ident.name.as_str() {
                "Int" => Type::Int,
                "Float" => Type::Float,
                "Bool" => Type::Bool,
                "String" => Type::String,
                "Char" => Type::Char,
                "Unit" => Type::Unit,
                "_" => Type::var(),
                name => {
                    // Check if it's a type parameter in scope (for generics)
                    if let Some(var) = self.type_params.get(name) {
                        return var.clone();
                    }
                    Type::Named(name.to_string())
                }
            },
            TypeExpr::App(constructor, args) => {
                let resolved_args: Vec<Type> = args.iter().map(|a| self.resolve_type(a)).collect();

                // Handle built-in generic types
                if let TypeExpr::Named(name) = constructor.as_ref() {
                    match name.name.as_str() {
                        "List" if resolved_args.len() == 1 => {
                            return Type::List(Box::new(resolved_args[0].clone()));
                        }
                        "Option" if resolved_args.len() == 1 => {
                            return Type::Option(Box::new(resolved_args[0].clone()));
                        }
                        "Map" if resolved_args.len() == 2 => {
                            return Type::Map(Box::new(resolved_args[0].clone()), Box::new(resolved_args[1].clone()));
                        }
                        _ => {}
                    }
                }

                Type::App {
                    constructor: Box::new(self.resolve_type(constructor)),
                    args: resolved_args,
                }
            }
            TypeExpr::Function {
                params,
                return_type,
                effects,
            } => Type::function_with_effects(
                params.iter().map(|p| self.resolve_type(p)).collect(),
                self.resolve_type(return_type),
                EffectSet::from_iter(effects.iter().map(|e| e.name.clone())),
            ),
            TypeExpr::Tuple(elements) => {
                Type::Tuple(elements.iter().map(|e| self.resolve_type(e)).collect())
            }
            TypeExpr::Record(fields) => Type::Record(
                fields
                    .iter()
                    .map(|f| (f.name.name.clone(), self.resolve_type(&f.typ)))
                    .collect(),
            ),
            TypeExpr::Unit => Type::Unit,
            TypeExpr::Versioned { base, constraint } => {
                // Resolve the base type and preserve version information
                let base_type = self.resolve_type(base);
                let version_info = match constraint {
                    ast::VersionConstraint::Exact(v) => VersionInfo::Exact(v.number),
                    ast::VersionConstraint::AtLeast(v) => VersionInfo::AtLeast(v.number),
                    ast::VersionConstraint::Latest(_) => VersionInfo::Latest,
                };
                Type::Versioned {
                    base: Box::new(base_type),
                    version: version_info,
                }
            }
        }
    }
}

impl Default for TypeChecker {
    fn default() -> Self {
        Self::new()
    }
}