gruel_air/inference/

generate.rs

//! Constraint generation for Hindley-Milner type inference.
//!
//! This module provides the constraint generation phase (Phase 1 of HM inference):
//! - [`ConstraintContext`] - Scoped variable tracking during generation
//! - [`ExprInfo`] - Result of constraint generation for an expression
//! - [`ConstraintGenerator`] - Walks RIR and generates type constraints
//! - Function/method signature types for type checking

use super::constraint::Constraint;
use super::types::{InferType, TypeVarAllocator, TypeVarId};
use crate::Type;
use crate::intern_pool::TypeInternPool;
use crate::scope::ScopedContext;
use crate::types::{
    EnumId, PtrMutability, StructId, parse_array_type_syntax, parse_pointer_type_syntax,
};
use gruel_rir::{InstData, InstRef, Rir};
use gruel_span::Span;
use lasso::{Spur, ThreadedRodeo};
use std::collections::HashMap;

/// Information about a local variable during constraint generation.
#[derive(Debug, Clone)]
pub struct LocalVarInfo {
    /// The inferred type of this variable.
    pub ty: InferType,
    /// Whether the variable is mutable.
    pub is_mut: bool,
    /// Span of the variable declaration.
    pub span: Span,
}

/// Information about a function parameter during constraint generation.
#[derive(Debug, Clone)]
pub struct ParamVarInfo {
    /// The type of this parameter, as InferType for uniform handling.
    pub ty: InferType,
}

/// Information about a function during constraint generation.
///
/// Uses `InferType` rather than `Type` so that array types are represented
/// structurally (as `InferType::Array { element, length }`) rather than by
/// opaque IDs. This allows uniform handling during inference.
#[derive(Debug, Clone)]
pub struct FunctionSig {
    /// Parameter types (in order), as InferTypes for uniform handling.
    pub param_types: Vec<InferType>,
    /// Return type, as InferType for uniform handling.
    pub return_type: InferType,
    /// Whether this is a generic function (has comptime type parameters).
    /// Generic functions skip type checking during constraint generation -
    /// they'll be checked during specialization.
    pub is_generic: bool,
    /// Parameter modes (Normal, Inout, Borrow, Comptime).
    pub param_modes: Vec<gruel_rir::RirParamMode>,
    /// Which parameters are comptime (declared with `comptime` keyword).
    /// This is separate from param_modes because `comptime T: type` sets
    /// is_comptime=true but mode=Normal.
    pub param_comptime: Vec<bool>,
    /// Parameter names, needed for type substitution in generic returns.
    pub param_names: Vec<lasso::Spur>,
    /// The return type as a symbol (used for substitution lookup).
    pub return_type_sym: lasso::Spur,
}

/// Information about a method during constraint generation.
///
/// Used for method calls (receiver.method()) and associated function calls (Type::function()).
#[derive(Debug, Clone)]
pub struct MethodSig {
    /// The struct type this method belongs to (as concrete Type::Struct)
    pub struct_type: Type,
    /// Whether this is a method (has self) or associated function (no self)
    pub has_self: bool,
    /// Parameter types (excluding self), as InferTypes for uniform handling.
    pub param_types: Vec<InferType>,
    /// Return type, as InferType for uniform handling.
    pub return_type: InferType,
}

/// Context for constraint generation within a single function.
pub struct ConstraintContext<'a> {
    /// Local variables in scope.
    pub locals: HashMap<Spur, LocalVarInfo>,
    /// Function parameters.
    pub params: &'a HashMap<Spur, ParamVarInfo>,
    /// Return type of the current function.
    pub return_type: Type,
    /// How many loops we're nested inside (for break/continue validation).
    pub loop_depth: u32,
    /// Scope stack for efficient scope management.
    scope_stack: Vec<Vec<(Spur, Option<LocalVarInfo>)>>,
}

impl<'a> ConstraintContext<'a> {
    /// Create a new context for a function.
    pub fn new(params: &'a HashMap<Spur, ParamVarInfo>, return_type: Type) -> Self {
        Self {
            locals: HashMap::new(),
            params,
            return_type,
            loop_depth: 0,
            scope_stack: Vec::new(),
        }
    }
}

impl ScopedContext for ConstraintContext<'_> {
    type VarInfo = LocalVarInfo;

    fn locals_mut(&mut self) -> &mut HashMap<Spur, Self::VarInfo> {
        &mut self.locals
    }

    fn scope_stack_mut(&mut self) -> &mut Vec<Vec<(Spur, Option<Self::VarInfo>)>> {
        &mut self.scope_stack
    }
}

/// Result of constraint generation for an expression.
#[derive(Debug, Clone)]
pub struct ExprInfo {
    /// The inferred type of this expression.
    pub ty: InferType,
    /// The span of this expression (for error reporting).
    pub span: Span,
}

impl ExprInfo {
    /// Create a new expression info.
    pub fn new(ty: InferType, span: Span) -> Self {
        Self { ty, span }
    }
}

/// Constraint generator that walks RIR and generates type constraints.
///
/// This is Phase 1 of HM inference: constraint generation. The constraints
/// are later solved by the `Unifier` to determine concrete types.
pub struct ConstraintGenerator<'a> {
    /// The RIR being analyzed.
    rir: &'a Rir,
    /// String interner for resolving symbols.
    interner: &'a ThreadedRodeo,
    /// Type variable allocator.
    type_vars: TypeVarAllocator,
    /// Collected constraints.
    constraints: Vec<Constraint>,
    /// Mapping from RIR instruction to its inferred type.
    expr_types: HashMap<InstRef, InferType>,
    /// Function signatures (for call type checking).
    functions: &'a HashMap<Spur, FunctionSig>,
    /// Struct types (name -> Type::new_struct(id)).
    structs: &'a HashMap<Spur, Type>,
    /// Enum types (name -> Type::new_enum(id)).
    enums: &'a HashMap<Spur, Type>,
    /// Method signatures: (struct_id, method_name) -> MethodSig
    methods: &'a HashMap<(StructId, Spur), MethodSig>,
    /// Enum method signatures: (enum_id, method_name) -> MethodSig
    enum_methods: &'a HashMap<(EnumId, Spur), MethodSig>,
    /// Type variables allocated for integer literals.
    /// These start as unbound and need to be defaulted to i32 if unconstrained.
    int_literal_vars: Vec<TypeVarId>,
    /// Type variables allocated for float literals.
    /// These start as unbound and need to be defaulted to f64 if unconstrained.
    float_literal_vars: Vec<TypeVarId>,
    /// Type substitutions for Self and type parameters (used in method bodies).
    /// Maps type names (like "Self") to their concrete types.
    type_subst: Option<&'a HashMap<Spur, Type>>,
    /// Type intern pool for creating pointer and array types during constraint generation.
    type_pool: &'a TypeInternPool,
}

impl<'a> ConstraintGenerator<'a> {
    /// Create a new constraint generator.
    #[allow(clippy::too_many_arguments)]
    pub fn new(
        rir: &'a Rir,
        interner: &'a ThreadedRodeo,
        functions: &'a HashMap<Spur, FunctionSig>,
        structs: &'a HashMap<Spur, Type>,
        enums: &'a HashMap<Spur, Type>,
        methods: &'a HashMap<(StructId, Spur), MethodSig>,
        enum_methods: &'a HashMap<(EnumId, Spur), MethodSig>,
        type_pool: &'a TypeInternPool,
    ) -> Self {
        Self {
            rir,
            interner,
            type_vars: TypeVarAllocator::new(),
            constraints: Vec::new(),
            expr_types: HashMap::new(),
            functions,
            structs,
            enums,
            methods,
            enum_methods,
            int_literal_vars: Vec::new(),
            float_literal_vars: Vec::new(),
            type_subst: None,
            type_pool,
        }
    }

    /// Set type substitutions for `Self` and type parameters (builder pattern).
    ///
    /// The `type_subst` map provides type substitutions for names like "Self"
    /// that should be resolved to concrete types during constraint generation.
    /// This is used for method bodies where `Self { ... }` struct literals
    /// need to know the concrete struct type.
    pub fn with_type_subst(mut self, type_subst: Option<&'a HashMap<Spur, Type>>) -> Self {
        self.type_subst = type_subst;
        self
    }

    /// Get the type variables allocated for integer literals.
    pub fn int_literal_vars(&self) -> &[TypeVarId] {
        &self.int_literal_vars
    }

    /// Allocate a fresh type variable.
    pub fn fresh_var(&mut self) -> TypeVarId {
        self.type_vars.fresh()
    }

    /// Add a constraint.
    pub fn add_constraint(&mut self, constraint: Constraint) {
        self.constraints.push(constraint);
    }

    /// Record the type of an expression.
    pub fn record_type(&mut self, inst_ref: InstRef, ty: InferType) {
        self.expr_types.insert(inst_ref, ty);
    }

    /// Get the recorded type of an expression.
    pub fn get_type(&self, inst_ref: InstRef) -> Option<&InferType> {
        self.expr_types.get(&inst_ref)
    }

    /// Get all collected constraints.
    pub fn constraints(&self) -> &[Constraint] {
        &self.constraints
    }

    /// Take ownership of the collected constraints.
    pub fn take_constraints(self) -> Vec<Constraint> {
        self.constraints
    }

    /// Get the expression type mapping.
    pub fn expr_types(&self) -> &HashMap<InstRef, InferType> {
        &self.expr_types
    }

    /// Consume the constraint generator and return (constraints, int_literal_vars, float_literal_vars, expr_types, type_var_count).
    ///
    /// This is useful when you need ownership of the expression types map.
    /// The `type_var_count` can be used to pre-size the unifier's substitution for better performance.
    pub fn into_parts(
        self,
    ) -> (
        Vec<Constraint>,
        Vec<TypeVarId>,
        Vec<TypeVarId>,
        HashMap<InstRef, InferType>,
        u32,
    ) {
        (
            self.constraints,
            self.int_literal_vars,
            self.float_literal_vars,
            self.expr_types,
            self.type_vars.count(),
        )
    }

    /// Generate constraints for an expression.
    ///
    /// Returns the inferred type of the expression. Records the type in
    /// `expr_types` and adds constraints to `constraints`.
    pub fn generate(&mut self, inst_ref: InstRef, ctx: &mut ConstraintContext) -> ExprInfo {
        let inst = self.rir.get(inst_ref);
        let span = inst.span;

        let ty = match &inst.data {
            InstData::IntConst(_) => {
                // Integer literals get a fresh type variable that we immediately
                // bind to IntLiteral. This allows unification to track when the
                // literal is constrained to a specific integer type.
                //
                // Example: `let x: i64 = 42` generates:
                //   - type_var(?0) for the literal 42
                //   - substitution: ?0 -> IntLiteral
                //   - constraint: Equal(Var(?0), Concrete(i64))
                //
                // During unification, Equal(IntLiteral, Concrete(i64)) succeeds
                // and rebinds ?0 -> Concrete(i64) via rebind_int_literal_to_concrete.
                let var = self.fresh_var();
                self.int_literal_vars.push(var);
                InferType::Var(var)
            }

            InstData::FloatConst(_) => {
                // Float literals work like int literals but default to f64.
                let var = self.fresh_var();
                self.float_literal_vars.push(var);
                InferType::Var(var)
            }

            InstData::BoolConst(_) => InferType::Concrete(Type::BOOL),

            // String constants use the builtin String struct type.
            InstData::StringConst(_) => {
                // Look up the String type from the structs map
                if let Some(string_spur) = self.interner.get("String") {
                    if let Some(&string_ty) = self.structs.get(&string_spur) {
                        InferType::Concrete(string_ty)
                    } else {
                        // Fallback if String struct not found (shouldn't happen after builtin injection)
                        InferType::Concrete(Type::ERROR)
                    }
                } else {
                    InferType::Concrete(Type::ERROR)
                }
            }

            InstData::UnitConst => InferType::Concrete(Type::UNIT),

            // Binary arithmetic: both operands must have the same numeric type
            InstData::Add { lhs, rhs }
            | InstData::Sub { lhs, rhs }
            | InstData::Mul { lhs, rhs }
            | InstData::Div { lhs, rhs }
            | InstData::Mod { lhs, rhs } => self.generate_binary_arith(*lhs, *rhs, ctx),

            // Bitwise operations: operands must be integers (no floats)
            InstData::BitAnd { lhs, rhs }
            | InstData::BitOr { lhs, rhs }
            | InstData::BitXor { lhs, rhs }
            | InstData::Shl { lhs, rhs }
            | InstData::Shr { lhs, rhs } => self.generate_binary_bitwise(*lhs, *rhs, ctx),

            // Comparison operators: operands must match, result is bool
            InstData::Eq { lhs, rhs }
            | InstData::Ne { lhs, rhs }
            | InstData::Lt { lhs, rhs }
            | InstData::Gt { lhs, rhs }
            | InstData::Le { lhs, rhs }
            | InstData::Ge { lhs, rhs } => {
                let lhs_info = self.generate(*lhs, ctx);
                let rhs_info = self.generate(*rhs, ctx);
                // Operands must have the same type
                self.add_constraint(Constraint::equal(lhs_info.ty, rhs_info.ty, span));
                InferType::Concrete(Type::BOOL)
            }

            // Logical operators: operands must be bool, result is bool
            InstData::And { lhs, rhs } | InstData::Or { lhs, rhs } => {
                let lhs_info = self.generate(*lhs, ctx);
                let rhs_info = self.generate(*rhs, ctx);
                self.add_constraint(Constraint::equal(
                    lhs_info.ty,
                    InferType::Concrete(Type::BOOL),
                    lhs_info.span,
                ));
                self.add_constraint(Constraint::equal(
                    rhs_info.ty,
                    InferType::Concrete(Type::BOOL),
                    rhs_info.span,
                ));
                InferType::Concrete(Type::BOOL)
            }

            // Unary negation: operand must be signed integer
            InstData::Neg { operand } => {
                let operand_info = self.generate(*operand, ctx);
                // Result type is the same as operand type
                let result_ty = operand_info.ty.clone();
                // Must be a signed integer
                self.add_constraint(Constraint::is_signed(result_ty.clone(), span));
                result_ty
            }

            // Logical NOT: operand must be bool
            InstData::Not { operand } => {
                let operand_info = self.generate(*operand, ctx);
                self.add_constraint(Constraint::equal(
                    operand_info.ty,
                    InferType::Concrete(Type::BOOL),
                    operand_info.span,
                ));
                InferType::Concrete(Type::BOOL)
            }

            // Bitwise NOT: operand must be integer
            InstData::BitNot { operand } => {
                let operand_info = self.generate(*operand, ctx);
                let result_ty = operand_info.ty.clone();
                // Must be an integer type (signed or unsigned)
                self.add_constraint(Constraint::is_integer(result_ty.clone(), span));
                result_ty
            }

            // Variable reference
            InstData::VarRef { name } => {
                if let Some(local) = ctx.locals.get(name) {
                    local.ty.clone()
                } else if let Some(param) = ctx.params.get(name) {
                    param.ty.clone()
                } else {
                    // Unknown variable - will be caught during semantic analysis
                    InferType::Concrete(Type::ERROR)
                }
            }

            // Parameter reference
            InstData::ParamRef { name, .. } => {
                if let Some(param) = ctx.params.get(name) {
                    param.ty.clone()
                } else {
                    InferType::Concrete(Type::ERROR)
                }
            }

            // Local variable allocation
            InstData::Alloc {
                directives_start: _,
                directives_len: _,
                name,
                is_mut,
                ty: type_annotation,
                init,
            } => {
                let init_info = self.generate(*init, ctx);

                let var_ty = if let Some(ty_sym) = type_annotation {
                    // Explicit type annotation - use it and constrain init to match
                    let ty_name = self.interner.resolve(ty_sym);
                    if let Some(annotated_ty) = self.resolve_type_name(ty_name) {
                        self.add_constraint(Constraint::equal(
                            init_info.ty,
                            annotated_ty.clone(),
                            span,
                        ));
                        annotated_ty
                    } else {
                        // Unknown type name (e.g., struct/enum) - use init type for now.
                        // Semantic analysis will catch undefined types and verify struct/enum
                        // field types match the definition.
                        init_info.ty
                    }
                } else {
                    // No annotation - use the init expression's type
                    init_info.ty
                };

                // Record the variable in scope (if it has a name)
                if let Some(var_name) = name {
                    ctx.insert_local(
                        *var_name,
                        LocalVarInfo {
                            ty: var_ty.clone(),
                            is_mut: *is_mut,
                            span,
                        },
                    );
                }

                // Alloc produces unit type
                InferType::Concrete(Type::UNIT)
            }

            // Struct destructuring — register field bindings for type inference
            InstData::StructDestructure {
                type_name,
                fields_start,
                fields_len,
                init,
            } => {
                self.generate(*init, ctx);

                // Look up the struct type to get field types
                if let Some(&struct_ty) = self.structs.get(type_name)
                    && let Some(struct_id) = struct_ty.as_struct()
                {
                    let struct_def = self.type_pool.struct_def(struct_id);
                    let rir_fields = self.rir.get_destructure_fields(*fields_start, *fields_len);
                    for field in &rir_fields {
                        if field.is_wildcard {
                            continue;
                        }
                        let field_name = self.interner.resolve(&field.field_name);
                        if let Some((_, struct_field)) = struct_def.find_field(field_name) {
                            let binding_name = field.binding_name.unwrap_or(field.field_name);
                            ctx.insert_local(
                                binding_name,
                                LocalVarInfo {
                                    ty: InferType::Concrete(struct_field.ty),
                                    is_mut: field.is_mut,
                                    span,
                                },
                            );
                        }
                    }
                }

                InferType::Concrete(Type::UNIT)
            }

            // Assignment
            InstData::Assign { name, value } => {
                let value_info = self.generate(*value, ctx);
                if let Some(local) = ctx.locals.get(name) {
                    // Constrain value to match variable type
                    self.add_constraint(Constraint::equal(value_info.ty, local.ty.clone(), span));
                }
                // Assignment produces unit
                InferType::Concrete(Type::UNIT)
            }

            // Return statement
            InstData::Ret(value) => {
                if let Some(val_ref) = value {
                    let value_info = self.generate(*val_ref, ctx);
                    // Constrain return value to match function return type
                    self.add_constraint(Constraint::equal(
                        value_info.ty,
                        InferType::Concrete(ctx.return_type),
                        span,
                    ));
                } else {
                    // Return without value - function must return unit
                    self.add_constraint(Constraint::equal(
                        InferType::Concrete(Type::UNIT),
                        InferType::Concrete(ctx.return_type),
                        span,
                    ));
                }
                // Return diverges
                InferType::Concrete(Type::NEVER)
            }

            // Function call
            InstData::Call {
                name,
                args_start,
                args_len,
            } => {
                let args = self.rir.get_call_args(*args_start, *args_len);
                if let Some(func) = self.functions.get(name) {
                    // For generic functions, skip constraint generation for arguments.
                    // The types will be checked during specialization when we know
                    // the concrete type substitutions.
                    if func.is_generic {
                        // Process all arguments and build type substitution map
                        let mut type_subst: std::collections::HashMap<lasso::Spur, Type> =
                            std::collections::HashMap::new();

                        for (i, arg) in args.iter().enumerate() {
                            let arg_info = self.generate(arg.value, ctx);

                            // If this is a comptime parameter, extract the type for substitution
                            if i < func.param_comptime.len() && func.param_comptime[i] {
                                // The argument should be a TypeConst - extract the concrete type
                                if let InferType::Concrete(Type::COMPTIME_TYPE) = &arg_info.ty {
                                    // This is a type value - get the actual type from the RIR
                                    let arg_inst = self.rir.get(arg.value);
                                    if let gruel_rir::InstData::TypeConst { type_name } =
                                        &arg_inst.data
                                    {
                                        // Resolve type_name to a concrete Type
                                        let type_name_str = self.interner.resolve(type_name);
                                        let concrete_ty = match type_name_str {
                                            "i8" => Type::I8,
                                            "i16" => Type::I16,
                                            "i32" => Type::I32,
                                            "i64" => Type::I64,
                                            "u8" => Type::U8,
                                            "u16" => Type::U16,
                                            "u32" => Type::U32,
                                            "u64" => Type::U64,
                                            "bool" => Type::BOOL,
                                            "()" => Type::UNIT,
                                            _ => Type::ERROR, // Unknown type
                                        };
                                        if i < func.param_names.len() {
                                            type_subst.insert(func.param_names[i], concrete_ty);
                                        }
                                    }
                                }
                            }
                        }

                        // Compute the actual return type by substituting type parameters

                        if func.return_type == InferType::Concrete(Type::COMPTIME_TYPE) {
                            // Return type is a type parameter - look it up in substitutions
                            if let Some(&concrete_ty) = type_subst.get(&func.return_type_sym) {
                                InferType::Concrete(concrete_ty)
                            } else {
                                func.return_type.clone()
                            }
                        } else {
                            func.return_type.clone()
                        }
                    } else if args.len() != func.param_types.len() {
                        // Check argument count matches parameter count.
                        // Semantic analysis will emit a proper error; we just need to avoid
                        // panicking and process what we can.
                        // Still process all arguments to catch type errors within them
                        for arg in args.iter() {
                            self.generate(arg.value, ctx);
                        }
                        // Return the declared return type (error will be caught in sema)
                        func.return_type.clone()
                    } else {
                        // Generate constraints for each argument
                        for (arg, param_ty) in args.iter().zip(func.param_types.iter()) {
                            let arg_info = self.generate(arg.value, ctx);
                            self.add_constraint(Constraint::equal(
                                arg_info.ty,
                                param_ty.clone(),
                                arg_info.span,
                            ));
                        }
                        func.return_type.clone()
                    }
                } else {
                    // Unknown function - still process arguments for constraint generation
                    for arg in args.iter() {
                        self.generate(arg.value, ctx);
                    }
                    InferType::Concrete(Type::ERROR)
                }
            }

            // Intrinsic call
            InstData::Intrinsic {
                name,
                args_start,
                args_len,
            } => {
                let intrinsic_name = self.interner.resolve(name);
                let args = self.rir.get_inst_refs(*args_start, *args_len);

                if intrinsic_name == "intCast" || intrinsic_name == "cast" {
                    // @intCast/@cast: target type is inferred from context
                    // The argument must be a numeric type (checked in sema)
                    if !args.is_empty() {
                        let arg_info = self.generate(args[0], ctx);
                        let _ = arg_info;
                    }
                    // Return type is inferred from context - create a fresh type variable
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else if intrinsic_name == "read_line" {
                    // @read_line: returns String (same as string constants)
                    if let Some(string_spur) = self.interner.get("String") {
                        if let Some(&string_ty) = self.structs.get(&string_spur) {
                            InferType::Concrete(string_ty)
                        } else {
                            // Fallback if String struct not found
                            InferType::Concrete(Type::ERROR)
                        }
                    } else {
                        InferType::Concrete(Type::ERROR)
                    }
                } else if intrinsic_name == "parse_i32" {
                    // @parse_i32: takes a String, returns i32
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::I32)
                } else if intrinsic_name == "parse_i64" {
                    // @parse_i64: takes a String, returns i64
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::I64)
                } else if intrinsic_name == "parse_u32" {
                    // @parse_u32: takes a String, returns u32
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::U32)
                } else if intrinsic_name == "parse_u64" {
                    // @parse_u64: takes a String, returns u64
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::U64)
                } else if intrinsic_name == "random_u32" {
                    // @random_u32: no arguments, returns u32
                    InferType::Concrete(Type::U32)
                } else if intrinsic_name == "random_u64" {
                    // @random_u64: no arguments, returns u64
                    InferType::Concrete(Type::U64)
                } else if intrinsic_name == "syscall" {
                    // @syscall: syscall_num and up to 6 args (all u64), returns i64
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::I64)
                } else if intrinsic_name == "ptr_to_int" {
                    // @ptr_to_int: takes a pointer, returns u64
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::U64)
                } else if intrinsic_name == "ptr_write" {
                    // @ptr_write: takes a pointer and value, returns unit
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::UNIT)
                } else if intrinsic_name == "is_null" {
                    // @is_null: takes a pointer, returns bool
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::BOOL)
                } else if intrinsic_name == "ptr_read" {
                    // @ptr_read: takes ptr const T or ptr mut T, returns T
                    // The return type depends on the pointee type of the argument.
                    // We create a fresh type variable that will be resolved during
                    // semantic analysis when the actual pointer type is known.
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else if intrinsic_name == "ptr_offset" {
                    // @ptr_offset: takes (ptr T, i64), returns ptr T
                    // The return type is the same as the input pointer type.
                    // We create a fresh type variable for proper inference.
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else if intrinsic_name == "raw" || intrinsic_name == "raw_mut" {
                    // @raw / @raw_mut: takes a value, returns a pointer to it
                    // The return type is ptr const T or ptr mut T where T is the argument type.
                    // We create a fresh type variable for proper inference.
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else if intrinsic_name == "int_to_ptr" || intrinsic_name == "null_ptr" {
                    // @int_to_ptr / @null_ptr: returns a pointer type inferred from context
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else if intrinsic_name == "ptr_copy" {
                    // @ptr_copy: (dst: ptr mut T, src: ptr const T, count: u64) -> ()
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    InferType::Concrete(Type::UNIT)
                } else if intrinsic_name == "target_arch" {
                    // @target_arch: returns Arch enum
                    if let Some(arch_spur) = self.interner.get("Arch") {
                        if let Some(&arch_ty) = self.enums.get(&arch_spur) {
                            InferType::Concrete(arch_ty)
                        } else {
                            InferType::Concrete(Type::ERROR)
                        }
                    } else {
                        InferType::Concrete(Type::ERROR)
                    }
                } else if intrinsic_name == "target_os" {
                    // @target_os: returns Os enum
                    if let Some(os_spur) = self.interner.get("Os") {
                        if let Some(&os_ty) = self.enums.get(&os_spur) {
                            InferType::Concrete(os_ty)
                        } else {
                            InferType::Concrete(Type::ERROR)
                        }
                    } else {
                        InferType::Concrete(Type::ERROR)
                    }
                } else if intrinsic_name == "range" {
                    // @range: takes 1-3 integer args, returns the same integer type
                    // (used as iterable in for-in loops)
                    if !args.is_empty() {
                        let first = self.generate(args[0], ctx);
                        for arg_ref in args.iter().skip(1) {
                            let arg_info = self.generate(*arg_ref, ctx);
                            self.add_constraint(Constraint::equal(
                                first.ty.clone(),
                                arg_info.ty,
                                span,
                            ));
                        }
                        first.ty
                    } else {
                        InferType::Concrete(Type::ERROR)
                    }
                } else if intrinsic_name == "field" {
                    // @field(value, field_name): returns the type of the named field.
                    // The field name is a comptime_str resolved at compile time, so
                    // the return type depends on which field is accessed. Use a fresh
                    // type variable — sema determines the concrete type.
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    let result_var = self.fresh_var();
                    InferType::Var(result_var)
                } else {
                    // Generate constraints for arguments (they need to be processed)
                    for arg_ref in args.iter() {
                        self.generate(*arg_ref, ctx);
                    }
                    // @dbg and other intrinsics return Unit
                    InferType::Concrete(Type::UNIT)
                }
            }

            // Type intrinsic (@size_of, @align_of, @typeName, @typeInfo)
            InstData::TypeIntrinsic { name, type_arg: _ } => {
                let intrinsic_name = self.interner.resolve(name);
                match intrinsic_name {
                    "typeName" => InferType::Concrete(Type::COMPTIME_STR),
                    "typeInfo" => {
                        // @typeInfo returns a comptime struct — use a fresh var
                        // since the actual type is determined by the comptime evaluator.
                        InferType::Var(self.fresh_var())
                    }
                    _ => {
                        // @size_of, @align_of return i32
                        InferType::Concrete(Type::I32)
                    }
                }
            }

            // Block
            InstData::Block { extra_start, len } => {
                ctx.push_scope();
                let mut last_ty = InferType::Concrete(Type::UNIT);
                let block_insts = self.rir.get_extra(*extra_start, *len);
                for &inst_raw in block_insts {
                    let block_inst_ref = InstRef::from_raw(inst_raw);
                    let info = self.generate(block_inst_ref, ctx);
                    last_ty = info.ty;
                }
                ctx.pop_scope();
                last_ty
            }

            // Branch (if/else)
            InstData::Branch {
                cond,
                then_block,
                else_block,
            } => {
                let cond_info = self.generate(*cond, ctx);
                self.add_constraint(Constraint::equal(
                    cond_info.ty,
                    InferType::Concrete(Type::BOOL),
                    cond_info.span,
                ));

                let then_info = self.generate(*then_block, ctx);

                if let Some(else_ref) = else_block {
                    let else_info = self.generate(*else_ref, ctx);

                    // Handle Never type coercion:
                    // - If one branch is Never, the if-else takes the other branch's type
                    // - If both are Never, the result is Never
                    // - Otherwise, both must unify to the same type
                    let then_is_never = matches!(&then_info.ty, InferType::Concrete(Type::NEVER));
                    let else_is_never = matches!(&else_info.ty, InferType::Concrete(Type::NEVER));

                    match (then_is_never, else_is_never) {
                        (true, true) => {
                            // Both diverge - result is Never
                            InferType::Concrete(Type::NEVER)
                        }
                        (true, false) => {
                            // Then diverges - result is else type
                            else_info.ty
                        }
                        (false, true) => {
                            // Else diverges - result is then type
                            then_info.ty
                        }
                        (false, false) => {
                            // Neither diverges - both must have the same type
                            let result_var = self.fresh_var();
                            let result_ty = InferType::Var(result_var);
                            self.add_constraint(Constraint::equal(
                                then_info.ty,
                                result_ty.clone(),
                                then_info.span,
                            ));
                            self.add_constraint(Constraint::equal(
                                else_info.ty,
                                result_ty.clone(),
                                else_info.span,
                            ));
                            result_ty
                        }
                    }
                } else {
                    // No else branch - the if expression has unit type
                    // (or the then branch type if it's unit-compatible)
                    InferType::Concrete(Type::UNIT)
                }
            }

            // While loop
            InstData::Loop { cond, body } => {
                let cond_info = self.generate(*cond, ctx);
                self.add_constraint(Constraint::equal(
                    cond_info.ty,
                    InferType::Concrete(Type::BOOL),
                    cond_info.span,
                ));

                ctx.loop_depth += 1;
                self.generate(*body, ctx);
                ctx.loop_depth -= 1;

                // Loops produce unit
                InferType::Concrete(Type::UNIT)
            }

            // For-in loop (desugared to while in sema, but inference still sees it)
            InstData::For {
                binding,
                is_mut,
                iterable,
                body,
            } => {
                // Generate constraints for the iterable to determine the element type
                let iterable_info = self.generate(*iterable, ctx);

                // Determine the binding type from the iterable:
                // - For @range: the iterable returns the integer type directly
                // - For arrays: extract the element type from InferType::Array
                let binding_ty = match &iterable_info.ty {
                    InferType::Array { element, .. } => *element.clone(),
                    other => other.clone(),
                };

                // Register the binding so the body can reference it
                ctx.insert_local(
                    *binding,
                    LocalVarInfo {
                        ty: binding_ty,
                        is_mut: *is_mut,
                        span,
                    },
                );

                ctx.loop_depth += 1;
                self.generate(*body, ctx);
                ctx.loop_depth -= 1;

                // For loops produce unit
                InferType::Concrete(Type::UNIT)
            }

            // Infinite loop
            InstData::InfiniteLoop { body } => {
                ctx.loop_depth += 1;
                self.generate(*body, ctx);
                ctx.loop_depth -= 1;

                // Infinite loop without break never returns
                InferType::Concrete(Type::NEVER)
            }

            // Break/Continue
            InstData::Break | InstData::Continue => InferType::Concrete(Type::NEVER),

            // Match expression
            InstData::Match {
                scrutinee,
                arms_start,
                arms_len,
            } => {
                let scrutinee_info = self.generate(*scrutinee, ctx);
                let arms = self.rir.get_match_arms(*arms_start, *arms_len);

                // Collect arm types, handling Never coercion
                let mut arm_types: Vec<ExprInfo> = Vec::new();
                for (pattern, body) in arms.iter() {
                    // Patterns constrain the scrutinee type
                    let pattern_ty = self.pattern_type(pattern);
                    self.add_constraint(Constraint::equal(
                        scrutinee_info.ty.clone(),
                        pattern_ty,
                        pattern.span(),
                    ));

                    // For DataVariant/StructVariant patterns, add bound variables to scope before
                    // generating body constraints, so VarRef lookups resolve correctly.
                    let bindings_to_remove = match pattern {
                        gruel_rir::RirPattern::DataVariant {
                            type_name,
                            variant,
                            bindings,
                            ..
                        } => {
                            let mut added_bindings = Vec::new();
                            if let Some(&enum_ty) = self.enums.get(type_name)
                                && let Some(enum_id) = enum_ty.as_enum()
                            {
                                let enum_def = self.type_pool.enum_def(enum_id);
                                let variant_name = self.interner.resolve(variant);
                                if let Some(variant_idx) = enum_def.find_variant(variant_name) {
                                    let field_types = &enum_def.variants[variant_idx].fields;
                                    for (i, binding) in bindings.iter().enumerate() {
                                        if !binding.is_wildcard
                                            && let Some(name) = binding.name
                                        {
                                            let field_ty = if i < field_types.len() {
                                                InferType::Concrete(field_types[i])
                                            } else {
                                                InferType::Concrete(Type::ERROR)
                                            };
                                            let old = ctx.locals.insert(
                                                name,
                                                LocalVarInfo {
                                                    ty: field_ty,
                                                    is_mut: binding.is_mut,
                                                    span: pattern.span(),
                                                },
                                            );
                                            added_bindings.push((name, old));
                                        }
                                    }
                                }
                            } else {
                                // Enum not found — likely a comptime type variable.
                                // Register bindings with fresh type variables so body
                                // constraint generation can still resolve variable references.
                                for binding in bindings.iter() {
                                    if !binding.is_wildcard
                                        && let Some(name) = binding.name
                                    {
                                        let var = self.fresh_var();
                                        let old = ctx.locals.insert(
                                            name,
                                            LocalVarInfo {
                                                ty: InferType::Var(var),
                                                is_mut: binding.is_mut,
                                                span: pattern.span(),
                                            },
                                        );
                                        added_bindings.push((name, old));
                                    }
                                }
                            }
                            added_bindings
                        }
                        gruel_rir::RirPattern::StructVariant {
                            type_name,
                            variant,
                            field_bindings,
                            ..
                        } => {
                            let mut added_bindings = Vec::new();
                            if let Some(&enum_ty) = self.enums.get(type_name)
                                && let Some(enum_id) = enum_ty.as_enum()
                            {
                                let enum_def = self.type_pool.enum_def(enum_id);
                                let variant_name = self.interner.resolve(variant);
                                if let Some(variant_idx) = enum_def.find_variant(variant_name) {
                                    let variant_def = &enum_def.variants[variant_idx];
                                    for fb in field_bindings {
                                        if !fb.binding.is_wildcard
                                            && let Some(name) = fb.binding.name
                                        {
                                            let field_name = self.interner.resolve(&fb.field_name);
                                            let field_ty = if let Some(idx) =
                                                variant_def.find_field(field_name)
                                            {
                                                InferType::Concrete(variant_def.fields[idx])
                                            } else {
                                                InferType::Concrete(Type::ERROR)
                                            };
                                            let old = ctx.locals.insert(
                                                name,
                                                LocalVarInfo {
                                                    ty: field_ty,
                                                    is_mut: fb.binding.is_mut,
                                                    span: pattern.span(),
                                                },
                                            );
                                            added_bindings.push((name, old));
                                        }
                                    }
                                }
                            } else {
                                // Enum not found — likely a comptime type variable.
                                // Register bindings with fresh type variables.
                                for fb in field_bindings {
                                    if !fb.binding.is_wildcard
                                        && let Some(name) = fb.binding.name
                                    {
                                        let var = self.fresh_var();
                                        let old = ctx.locals.insert(
                                            name,
                                            LocalVarInfo {
                                                ty: InferType::Var(var),
                                                is_mut: fb.binding.is_mut,
                                                span: pattern.span(),
                                            },
                                        );
                                        added_bindings.push((name, old));
                                    }
                                }
                            }
                            added_bindings
                        }
                        _ => Vec::new(),
                    };

                    // Generate body and collect its type
                    let body_info = self.generate(*body, ctx);
                    arm_types.push(body_info);

                    // Remove DataVariant bindings from scope after body generation
                    for (name, old_val) in bindings_to_remove {
                        match old_val {
                            Some(prev) => {
                                ctx.locals.insert(name, prev);
                            }
                            None => {
                                ctx.locals.remove(&name);
                            }
                        }
                    }
                }

                // Handle Never type coercion:
                // Filter out Never arms and use the remaining non-Never types
                let non_never_arms: Vec<_> = arm_types
                    .iter()
                    .filter(|info| !matches!(&info.ty, InferType::Concrete(Type::NEVER)))
                    .collect();

                if non_never_arms.is_empty() {
                    // All arms diverge - result is Never
                    InferType::Concrete(Type::NEVER)
                } else {
                    // Create constraints for non-Never arms to have the same type
                    let result_var = self.fresh_var();
                    let result_ty = InferType::Var(result_var);
                    for arm_info in non_never_arms {
                        self.add_constraint(Constraint::equal(
                            arm_info.ty.clone(),
                            result_ty.clone(),
                            arm_info.span,
                        ));
                    }
                    result_ty
                }
            }

            // Struct initialization
            InstData::StructInit {
                type_name,
                fields_start,
                fields_len,
                ..
            } => {
                // Check type_subst first (for Self and type parameters in method bodies)
                let struct_ty = self
                    .type_subst
                    .and_then(|subst| subst.get(type_name).copied())
                    .or_else(|| self.structs.get(type_name).copied());

                if let Some(struct_ty) = struct_ty {
                    let fields = self.rir.get_field_inits(*fields_start, *fields_len);
                    // Generate constraints for each field
                    for (_, value_ref) in fields.iter() {
                        self.generate(*value_ref, ctx);
                    }
                    InferType::Concrete(struct_ty)
                } else {
                    InferType::Concrete(Type::ERROR)
                }
            }

            // Field access
            InstData::FieldGet { base, field: _ } => {
                // Generate constraints for the base expression (needed for nested field access)
                let _base_info = self.generate(*base, ctx);
                // We need to look up the field type from the struct definition.
                // For now, use a fresh type variable - full resolution happens during
                // semantic analysis which has access to struct definitions.
                let result_var = self.fresh_var();
                InferType::Var(result_var)
            }

            // Field assignment
            InstData::FieldSet {
                base,
                field: _,
                value,
            } => {
                self.generate(*base, ctx);
                self.generate(*value, ctx);
                InferType::Concrete(Type::UNIT)
            }

            // Enum variant (unit or path)
            InstData::EnumVariant { type_name, .. } => {
                if let Some(&enum_ty) = self.enums.get(type_name) {
                    InferType::Concrete(enum_ty)
                } else {
                    // May be a comptime type variable — use fresh var
                    let var = self.fresh_var();
                    InferType::Var(var)
                }
            }

            // Enum struct variant construction
            InstData::EnumStructVariant {
                type_name,
                fields_start,
                fields_len,
                ..
            } => {
                // Generate constraints for field value expressions
                let fields = self.rir.get_field_inits(*fields_start, *fields_len);
                for (_, value_ref) in fields.iter() {
                    self.generate(*value_ref, ctx);
                }
                if let Some(&enum_ty) = self.enums.get(type_name) {
                    InferType::Concrete(enum_ty)
                } else {
                    // May be a comptime type variable — use fresh var
                    let var = self.fresh_var();
                    InferType::Var(var)
                }
            }

            // Array initialization
            InstData::ArrayInit {
                elems_start,
                elems_len,
            } => {
                let elements = self.rir.get_inst_refs(*elems_start, *elems_len);
                if elements.is_empty() {
                    // Empty array - need type annotation to know element type
                    // Use a fresh type variable for the element type
                    let elem_var = self.fresh_var();
                    InferType::Array {
                        element: Box::new(InferType::Var(elem_var)),
                        length: 0,
                    }
                } else {
                    // Get element type from first element, constrain rest to match
                    let first_info = self.generate(elements[0], ctx);
                    for elem_ref in elements.iter().skip(1) {
                        let elem_info = self.generate(*elem_ref, ctx);
                        self.add_constraint(Constraint::equal(
                            elem_info.ty,
                            first_info.ty.clone(),
                            elem_info.span,
                        ));
                    }
                    // Build the array type with the inferred element type
                    InferType::Array {
                        element: Box::new(first_info.ty),
                        length: elements.len() as u64,
                    }
                }
            }

            // Array index
            InstData::IndexGet { base, index } => {
                let base_info = self.generate(*base, ctx);
                let index_info = self.generate(*index, ctx);
                // Index must be an unsigned integer type
                self.add_constraint(Constraint::is_unsigned(index_info.ty, index_info.span));

                // Extract element type from array type.
                // If base is InferType::Array, we can get the element type directly.
                // Otherwise, we need a fresh variable that will be resolved later.
                match &base_info.ty {
                    InferType::Array { element, .. } => (**element).clone(),
                    _ => {
                        // Base might be a type variable that will resolve to an array.
                        // Use a fresh variable for the element type.
                        let result_var = self.fresh_var();
                        InferType::Var(result_var)
                    }
                }
            }

            // Array index assignment
            InstData::IndexSet { base, index, value } => {
                let base_info = self.generate(*base, ctx);
                let index_info = self.generate(*index, ctx);
                // Index must be an unsigned integer type
                self.add_constraint(Constraint::is_unsigned(index_info.ty, index_info.span));

                let value_info = self.generate(*value, ctx);

                // Constrain value type to match array element type
                if let InferType::Array { element, .. } = &base_info.ty {
                    self.add_constraint(Constraint::equal(
                        value_info.ty,
                        (**element).clone(),
                        value_info.span,
                    ));
                }

                InferType::Concrete(Type::UNIT)
            }

            // Type declarations don't produce values
            InstData::FnDecl { .. }
            | InstData::StructDecl { .. }
            | InstData::EnumDecl { .. }
            | InstData::DropFnDecl { .. }
            | InstData::ConstDecl { .. } => InferType::Concrete(Type::UNIT),

            // Method call: receiver.method(args)
            InstData::MethodCall {
                receiver,
                method,
                args_start,
                args_len,
            } => {
                // Generate type for receiver
                let receiver_info = self.generate(*receiver, ctx);
                let args = self.rir.get_call_args(*args_start, *args_len);

                // Get struct name from receiver type if it's a struct
                // If we can't determine the struct type, we still generate constraints
                // for the arguments and return a type variable (actual error is in sema)

                if let InferType::Concrete(ty) = &receiver_info.ty {
                    if let Some(struct_id) = ty.as_struct() {
                        // Use StructId directly for method lookup
                        let method_key = (struct_id, *method);
                        if let Some(method_sig) = self.methods.get(&method_key) {
                            // Generate constraints for arguments
                            for (arg, param_type) in args.iter().zip(method_sig.param_types.iter())
                            {
                                let arg_info = self.generate(arg.value, ctx);
                                self.add_constraint(Constraint::equal(
                                    arg_info.ty,
                                    param_type.clone(),
                                    arg_info.span,
                                ));
                            }
                            method_sig.return_type.clone()
                        } else {
                            // Method not found in pre-built context - may be an anonymous
                            // struct method registered during comptime evaluation.
                            // Use a fresh type variable so inference doesn't poison
                            // surrounding expressions with ERROR.
                            for arg in args.iter() {
                                self.generate(arg.value, ctx);
                            }
                            InferType::Var(self.fresh_var())
                        }
                    } else if let Some(enum_id) = ty.as_enum() {
                        // Enum receiver - check enum_methods
                        let method_key = (enum_id, *method);
                        if let Some(method_sig) = self.enum_methods.get(&method_key) {
                            for (arg, param_type) in args.iter().zip(method_sig.param_types.iter())
                            {
                                let arg_info = self.generate(arg.value, ctx);
                                self.add_constraint(Constraint::equal(
                                    arg_info.ty,
                                    param_type.clone(),
                                    arg_info.span,
                                ));
                            }
                            method_sig.return_type.clone()
                        } else {
                            // Enum method not found - use fresh var, sema reports error
                            for arg in args.iter() {
                                self.generate(arg.value, ctx);
                            }
                            InferType::Var(self.fresh_var())
                        }
                    } else {
                        // Non-struct/non-enum receiver - sema will report the error
                        for arg in args.iter() {
                            self.generate(arg.value, ctx);
                        }
                        InferType::Concrete(Type::ERROR)
                    }
                } else {
                    // Non-concrete receiver type - use fresh var, sema resolves it
                    for arg in args.iter() {
                        self.generate(arg.value, ctx);
                    }
                    InferType::Var(self.fresh_var())
                }
            }

            // Associated function call: Type::function(args)
            InstData::AssocFnCall {
                type_name,
                function,
                args_start,
                args_len,
            } => {
                let args = self.rir.get_call_args(*args_start, *args_len);
                // Get struct ID from type name for method lookup
                let struct_id = self.structs.get(type_name).and_then(|ty| ty.as_struct());

                if let Some(struct_id) = struct_id {
                    let method_key = (struct_id, *function);
                    if let Some(method_sig) = self.methods.get(&method_key) {
                        // Generate constraints for arguments
                        for (arg, param_type) in args.iter().zip(method_sig.param_types.iter()) {
                            let arg_info = self.generate(arg.value, ctx);
                            self.add_constraint(Constraint::equal(
                                arg_info.ty,
                                param_type.clone(),
                                arg_info.span,
                            ));
                        }
                        method_sig.return_type.clone()
                    } else {
                        // Method not found - may be an anonymous struct method
                        // registered during comptime. Use fresh var to avoid ERROR poison.
                        for arg in args.iter() {
                            self.generate(arg.value, ctx);
                        }
                        InferType::Var(self.fresh_var())
                    }
                } else {
                    // Type not found in pre-built context - may be a comptime type var.
                    // Use fresh var so inference doesn't poison surrounding expressions.
                    for arg in args.iter() {
                        self.generate(arg.value, ctx);
                    }
                    InferType::Var(self.fresh_var())
                }
            }

            // Comptime block: the type depends on whether evaluation succeeds at compile time.
            // For type inference, we use a fresh type variable that can unify with
            // whatever type is expected from the context (e.g., a let binding's type annotation).
            // Similar to integer literals, comptime blocks can adapt to their context.
            InstData::Comptime { expr: _ } => {
                // Comptime blocks are fully evaluated by the comptime interpreter in sema,
                // which handles its own type checking (comptime_str, TypeInfo structs, etc.).
                // We don't generate constraints for the inner expression because comptime
                // has types (comptime_str, anonymous structs from @typeInfo) that don't
                // exist in the regular type system and would cause false unification errors.
                // Use a fresh variable so comptime can unify with whatever the context expects.
                let var = self.fresh_var();
                self.int_literal_vars.push(var);
                InferType::Var(var)
            }

            // Comptime unroll for: the iterable is evaluated at comptime, the body is unrolled.
            // Like regular for loops, the result type is unit.
            // We must generate constraints for the body so that type inference resolves
            // types for runtime expressions inside the loop body (e.g., `total + 1`).
            // The binding variable holds a comptime value and is handled by sema, but
            // we register it as an integer type variable so VarRef lookups don't fail.
            InstData::ComptimeUnrollFor {
                binding,
                iterable,
                body,
            } => {
                // Generate constraints for the iterable (it's a comptime block)
                self.generate(*iterable, ctx);

                // Register the binding as a fresh type variable.
                // The actual comptime value type is determined by sema, but HM
                // inference needs the binding in scope so VarRef doesn't fail.
                let binding_ty = {
                    let var = self.fresh_var();
                    InferType::Var(var)
                };
                ctx.insert_local(
                    *binding,
                    LocalVarInfo {
                        ty: binding_ty,
                        is_mut: false,
                        span,
                    },
                );

                // Generate constraints for the body
                self.generate(*body, ctx);

                InferType::Concrete(Type::UNIT)
            }

            // Checked block: for type inference purposes, the type is the type of the inner expression
            // The actual checking of unchecked operations happens in sema
            InstData::Checked { expr } => {
                // Generate constraints for the inner expression
                let inner_info = self.generate(*expr, ctx);
                inner_info.ty
            }

            // Type constant: a type used as a value (e.g., `i32` in `identity(i32, 42)`)
            // This has the special ComptimeType type which indicates it's a type value.
            InstData::TypeConst { .. } => InferType::Concrete(Type::COMPTIME_TYPE),

            // Anonymous struct type: a struct type used as a comptime value
            // This also has the ComptimeType type.
            InstData::AnonStructType { .. } => InferType::Concrete(Type::COMPTIME_TYPE),

            // Anonymous enum type: an enum type used as a comptime value
            // This also has the ComptimeType type.
            InstData::AnonEnumType { .. } => InferType::Concrete(Type::COMPTIME_TYPE),
        };

        // Record the type for this expression
        self.record_type(inst_ref, ty.clone());
        ExprInfo::new(ty, span)
    }

    /// Generate constraints for a binary arithmetic operation (+, -, *, /, %).
    ///
    /// Operands must be numeric (integer or float).
    fn generate_binary_arith(
        &mut self,
        lhs: InstRef,
        rhs: InstRef,
        ctx: &mut ConstraintContext,
    ) -> InferType {
        let lhs_info = self.generate(lhs, ctx);
        let rhs_info = self.generate(rhs, ctx);

        let result_var = self.fresh_var();
        let result_ty = InferType::Var(result_var);

        self.add_constraint(Constraint::equal(
            lhs_info.ty,
            result_ty.clone(),
            lhs_info.span,
        ));
        self.add_constraint(Constraint::equal(
            rhs_info.ty,
            result_ty.clone(),
            rhs_info.span,
        ));

        // Result must be numeric (integer or float)
        self.add_constraint(Constraint::is_numeric(result_ty.clone(), lhs_info.span));

        result_ty
    }

    /// Generate constraints for a binary bitwise operation (&, |, ^, <<, >>).
    ///
    /// Operands must be integers (floats are not allowed).
    fn generate_binary_bitwise(
        &mut self,
        lhs: InstRef,
        rhs: InstRef,
        ctx: &mut ConstraintContext,
    ) -> InferType {
        let lhs_info = self.generate(lhs, ctx);
        let rhs_info = self.generate(rhs, ctx);

        let result_var = self.fresh_var();
        let result_ty = InferType::Var(result_var);

        self.add_constraint(Constraint::equal(
            lhs_info.ty,
            result_ty.clone(),
            lhs_info.span,
        ));
        self.add_constraint(Constraint::equal(
            rhs_info.ty,
            result_ty.clone(),
            rhs_info.span,
        ));

        // Result must be an integer type (no floats)
        self.add_constraint(Constraint::is_integer(result_ty.clone(), lhs_info.span));

        result_ty
    }

    /// Get the inferred type for a pattern.
    fn pattern_type(&mut self, pattern: &gruel_rir::RirPattern) -> InferType {
        match pattern {
            gruel_rir::RirPattern::Wildcard(_) => {
                // Wildcard matches anything - use a fresh type variable
                let var = self.fresh_var();
                InferType::Var(var)
            }
            gruel_rir::RirPattern::Int(_, _) => InferType::IntLiteral,
            gruel_rir::RirPattern::Bool(_, _) => InferType::Concrete(Type::BOOL),
            gruel_rir::RirPattern::Path { type_name, .. }
            | gruel_rir::RirPattern::DataVariant { type_name, .. }
            | gruel_rir::RirPattern::StructVariant { type_name, .. } => {
                if let Some(&enum_ty) = self.enums.get(type_name) {
                    InferType::Concrete(enum_ty)
                } else {
                    // Enum type not found — may be a comptime type variable
                    // (e.g., `let Opt = Option(i32); match x { Opt::Some(v) => ... }`).
                    // Use a fresh type variable so arm bodies can still infer types.
                    let var = self.fresh_var();
                    InferType::Var(var)
                }
            }
        }
    }

    /// Resolve a type name to an InferType.
    ///
    /// Handles primitive types, array syntax `[T; N]`, pointer syntax `ptr mut T` / `ptr const T`,
    /// and struct/enum types.
    fn resolve_type_name(&self, name: &str) -> Option<InferType> {
        // Check for array syntax first: [T; N]
        if let Some((element_type_str, length)) = parse_array_type_syntax(name) {
            // Recursively resolve the element type
            let element_ty = self.resolve_type_name(&element_type_str)?;
            return Some(InferType::Array {
                element: Box::new(element_ty),
                length,
            });
        }

        // Check for pointer syntax: ptr mut T / ptr const T
        if let Some((pointee_type_str, mutability)) = parse_pointer_type_syntax(name) {
            // Recursively resolve the pointee type
            let pointee_infer_ty = self.resolve_type_name(&pointee_type_str)?;

            // Convert InferType to Type so we can intern the pointer
            let pointee_ty = match pointee_infer_ty {
                InferType::Concrete(ty) => ty,
                // Can't handle non-concrete types in pointer positions during constraint generation
                _ => return None,
            };

            // Intern the pointer type
            let ptr_ty = match mutability {
                PtrMutability::Mut => {
                    let ptr_id = self.type_pool.intern_ptr_mut_from_type(pointee_ty);
                    Type::new_ptr_mut(ptr_id)
                }
                PtrMutability::Const => {
                    let ptr_id = self.type_pool.intern_ptr_const_from_type(pointee_ty);
                    Type::new_ptr_const(ptr_id)
                }
            };
            return Some(InferType::Concrete(ptr_ty));
        }

        // Check primitives
        let ty = match name {
            "i8" => Type::I8,
            "i16" => Type::I16,
            "i32" => Type::I32,
            "i64" => Type::I64,
            "u8" => Type::U8,
            "u16" => Type::U16,
            "u32" => Type::U32,
            "u64" => Type::U64,
            "isize" => Type::ISIZE,
            "usize" => Type::USIZE,
            "f16" => Type::F16,
            "f32" => Type::F32,
            "f64" => Type::F64,
            "bool" => Type::BOOL,
            "()" => Type::UNIT,
            _ => {
                // Check for struct types (including builtin String)
                if let Some(name_spur) = self.interner.get(name) {
                    if let Some(&struct_ty) = self.structs.get(&name_spur) {
                        return Some(InferType::Concrete(struct_ty));
                    }
                    if let Some(&enum_ty) = self.enums.get(&name_spur) {
                        return Some(InferType::Concrete(enum_ty));
                    }
                }
                return None;
            }
        };
        Some(InferType::Concrete(ty))
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use lasso::ThreadedRodeo;

    /// Helper to create a minimal RIR, interner, and type pool for testing.
    fn make_test_rir_interner_and_type_pool() -> (Rir, ThreadedRodeo, TypeInternPool) {
        let rir = Rir::new();
        let interner = ThreadedRodeo::new();
        let type_pool = TypeInternPool::new();
        (rir, interner, type_pool)
    }

    #[test]
    fn test_constraint_generator_int_literal() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Add an integer constant to RIR
        let inst_ref = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(0, 2),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(inst_ref, &mut ctx);

        // Integer literals now get a type variable (tracked as int literal var)
        assert!(matches!(info.ty, InferType::Var(_)));
        // The type variable should be tracked in int_literal_vars
        assert_eq!(cgen.int_literal_vars().len(), 1);
        // No constraints should be generated for a simple literal
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_bool_literal() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        let inst_ref = rir.add_inst(gruel_rir::Inst {
            data: InstData::BoolConst(true),
            span: Span::new(0, 4),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::BOOL);

        let info = cgen.generate(inst_ref, &mut ctx);

        assert_eq!(info.ty, InferType::Concrete(Type::BOOL));
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_binary_add() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: 1 + 2
        let lhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(1),
            span: Span::new(0, 1),
        });
        let rhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(2),
            span: Span::new(4, 5),
        });
        let add = rir.add_inst(gruel_rir::Inst {
            data: InstData::Add { lhs, rhs },
            span: Span::new(0, 5),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(add, &mut ctx);

        // Result should be a type variable
        assert!(info.ty.is_var());
        // Should generate 3 constraints: lhs = result, rhs = result, IsNumeric(result)
        assert_eq!(cgen.constraints().len(), 3);
        // Verify the third constraint is IsNumeric
        match &cgen.constraints()[2] {
            Constraint::IsNumeric(_, _) => {}
            _ => panic!("Expected IsNumeric constraint for arithmetic result"),
        }
    }

    #[test]
    fn test_constraint_generator_comparison() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: 1 < 2
        let lhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(1),
            span: Span::new(0, 1),
        });
        let rhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(2),
            span: Span::new(4, 5),
        });
        let lt = rir.add_inst(gruel_rir::Inst {
            data: InstData::Lt { lhs, rhs },
            span: Span::new(0, 5),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::BOOL);

        let info = cgen.generate(lt, &mut ctx);

        // Comparisons always return Bool
        assert_eq!(info.ty, InferType::Concrete(Type::BOOL));
        // Should generate 1 constraint: lhs type = rhs type
        assert_eq!(cgen.constraints().len(), 1);
    }

    #[test]
    fn test_constraint_generator_logical_and() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: true && false
        let lhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::BoolConst(true),
            span: Span::new(0, 4),
        });
        let rhs = rir.add_inst(gruel_rir::Inst {
            data: InstData::BoolConst(false),
            span: Span::new(8, 13),
        });
        let and = rir.add_inst(gruel_rir::Inst {
            data: InstData::And { lhs, rhs },
            span: Span::new(0, 13),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::BOOL);

        let info = cgen.generate(and, &mut ctx);

        // Logical operators return Bool
        assert_eq!(info.ty, InferType::Concrete(Type::BOOL));
        // Should generate 2 constraints: lhs = bool, rhs = bool
        assert_eq!(cgen.constraints().len(), 2);
    }

    #[test]
    fn test_constraint_generator_negation() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: -42
        let operand = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(1, 3),
        });
        let neg = rir.add_inst(gruel_rir::Inst {
            data: InstData::Neg { operand },
            span: Span::new(0, 3),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(neg, &mut ctx);

        // Negation preserves the operand type (now a type variable for the int literal)
        assert!(matches!(info.ty, InferType::Var(_)));
        // Should generate 1 constraint: IsSigned for the result
        assert_eq!(cgen.constraints().len(), 1);
        // Verify it's an IsSigned constraint
        match &cgen.constraints()[0] {
            Constraint::IsSigned(_, _) => {}
            _ => panic!("Expected IsSigned constraint"),
        }
    }

    #[test]
    fn test_constraint_generator_return() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: return 42
        let value = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(7, 9),
        });
        let ret = rir.add_inst(gruel_rir::Inst {
            data: InstData::Ret(Some(value)),
            span: Span::new(0, 9),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(ret, &mut ctx);

        // Return is divergent (Never type)
        assert_eq!(info.ty, InferType::Concrete(Type::NEVER));
        // Should generate 1 constraint: return value = return type
        assert_eq!(cgen.constraints().len(), 1);
    }

    #[test]
    fn test_constraint_generator_if_else() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: if true { 1 } else { 2 }
        let cond = rir.add_inst(gruel_rir::Inst {
            data: InstData::BoolConst(true),
            span: Span::new(3, 7),
        });
        let then_val = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(1),
            span: Span::new(10, 11),
        });
        let else_val = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(2),
            span: Span::new(20, 21),
        });
        let branch = rir.add_inst(gruel_rir::Inst {
            data: InstData::Branch {
                cond,
                then_block: then_val,
                else_block: Some(else_val),
            },
            span: Span::new(0, 25),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(branch, &mut ctx);

        // Result should be a type variable (unified from both branches)
        assert!(info.ty.is_var());
        // Should generate 3 constraints: cond = bool, then = result, else = result
        assert_eq!(cgen.constraints().len(), 3);
    }

    #[test]
    fn test_constraint_generator_while_loop() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: while true { 0 }
        let cond = rir.add_inst(gruel_rir::Inst {
            data: InstData::BoolConst(true),
            span: Span::new(6, 10),
        });
        let body = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0),
            span: Span::new(13, 14),
        });
        let loop_inst = rir.add_inst(gruel_rir::Inst {
            data: InstData::Loop { cond, body },
            span: Span::new(0, 15),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::UNIT);

        let info = cgen.generate(loop_inst, &mut ctx);

        // While loops produce Unit
        assert_eq!(info.ty, InferType::Concrete(Type::UNIT));
        // Should generate 1 constraint: cond = bool
        assert_eq!(cgen.constraints().len(), 1);
    }

    #[test]
    fn test_constraint_context_scope() {
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        // Use an interner to create a symbol
        let interner = ThreadedRodeo::new();
        let sym = interner.get_or_intern("x");
        ctx.insert_local(
            sym,
            LocalVarInfo {
                ty: InferType::Concrete(Type::I32),
                is_mut: false,
                span: Span::new(0, 1),
            },
        );

        assert!(ctx.locals.contains_key(&sym));

        // Push a scope and shadow the variable
        ctx.push_scope();
        ctx.insert_local(
            sym,
            LocalVarInfo {
                ty: InferType::Concrete(Type::I64),
                is_mut: true,
                span: Span::new(10, 15),
            },
        );

        // Should see the shadowed version
        let local = ctx.locals.get(&sym).unwrap();
        assert_eq!(local.ty, InferType::Concrete(Type::I64));
        assert!(local.is_mut);

        // Pop scope - should restore original
        ctx.pop_scope();
        let local = ctx.locals.get(&sym).unwrap();
        assert_eq!(local.ty, InferType::Concrete(Type::I32));
        assert!(!local.is_mut);
    }

    #[test]
    fn test_expr_info_creation() {
        let info = ExprInfo::new(InferType::IntLiteral, Span::new(5, 10));
        assert!(info.ty.is_int_literal());
        assert_eq!(info.span, Span::new(5, 10));
    }

    /// Helper to create a non-generic FunctionSig for tests
    fn make_test_func_sig(param_types: Vec<InferType>, return_type: InferType) -> FunctionSig {
        let num_params = param_types.len();
        FunctionSig {
            param_types,
            return_type,
            is_generic: false,
            param_modes: vec![gruel_rir::RirParamMode::Normal; num_params],
            param_comptime: vec![false; num_params],
            param_names: vec![],
            return_type_sym: lasso::Spur::default(),
        }
    }

    #[test]
    fn test_function_sig() {
        let sig = make_test_func_sig(
            vec![
                InferType::Concrete(Type::I32),
                InferType::Concrete(Type::BOOL),
            ],
            InferType::Concrete(Type::I64),
        );
        assert_eq!(sig.param_types.len(), 2);
        assert_eq!(sig.return_type, InferType::Concrete(Type::I64));
    }

    #[test]
    fn test_constraint_generator_infinite_loop() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: loop { 0 }
        let body = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0),
            span: Span::new(6, 7),
        });
        let loop_inst = rir.add_inst(gruel_rir::Inst {
            data: InstData::InfiniteLoop { body },
            span: Span::new(0, 10),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::UNIT);

        let info = cgen.generate(loop_inst, &mut ctx);

        // Infinite loop produces Never (diverges)
        assert_eq!(info.ty, InferType::Concrete(Type::NEVER));
        // No constraints for infinite loop itself
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_break_continue() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        let break_inst = rir.add_inst(gruel_rir::Inst {
            data: InstData::Break,
            span: Span::new(0, 5),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::UNIT);

        let info = cgen.generate(break_inst, &mut ctx);

        // Break diverges
        assert_eq!(info.ty, InferType::Concrete(Type::NEVER));
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_index_get() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: arr[0]
        let base = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0), // Placeholder for array
            span: Span::new(0, 3),
        });
        let index = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0),
            span: Span::new(4, 5),
        });
        let index_get = rir.add_inst(gruel_rir::Inst {
            data: InstData::IndexGet { base, index },
            span: Span::new(0, 6),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(index_get, &mut ctx);

        // Result is a type variable (element type unknown)
        assert!(info.ty.is_var());
        // Should generate 1 constraint: index must be unsigned
        assert_eq!(cgen.constraints().len(), 1);
        match &cgen.constraints()[0] {
            Constraint::IsUnsigned(_, _) => {}
            _ => panic!("Expected IsUnsigned constraint for index"),
        }
    }

    #[test]
    fn test_constraint_generator_index_set() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: arr[0] = 42
        let base = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0), // Placeholder for array
            span: Span::new(0, 3),
        });
        let index = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(0),
            span: Span::new(4, 5),
        });
        let value = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(9, 11),
        });
        let index_set = rir.add_inst(gruel_rir::Inst {
            data: InstData::IndexSet { base, index, value },
            span: Span::new(0, 11),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::UNIT);

        let info = cgen.generate(index_set, &mut ctx);

        // Index assignment produces Unit
        assert_eq!(info.ty, InferType::Concrete(Type::UNIT));
        // Should generate 1 constraint: index must be unsigned
        assert_eq!(cgen.constraints().len(), 1);
        match &cgen.constraints()[0] {
            Constraint::IsUnsigned(_, _) => {}
            _ => panic!("Expected IsUnsigned constraint for index"),
        }
    }

    #[test]
    fn test_constraint_generator_empty_block() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: { } (empty block)
        let block = rir.add_inst(gruel_rir::Inst {
            data: InstData::Block {
                extra_start: 0,
                len: 0,
            },
            span: Span::new(0, 2),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::UNIT);

        let info = cgen.generate(block, &mut ctx);

        // Empty block produces Unit
        assert_eq!(info.ty, InferType::Concrete(Type::UNIT));
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_bitwise_not() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: !42 (bitwise NOT)
        let operand = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(1, 3),
        });
        let bitnot = rir.add_inst(gruel_rir::Inst {
            data: InstData::BitNot { operand },
            span: Span::new(0, 3),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(bitnot, &mut ctx);

        // Bitwise NOT preserves the operand type (now a type variable for int literal)
        assert!(matches!(info.ty, InferType::Var(_)));
        // Should generate 1 constraint: IsInteger for the result
        assert_eq!(cgen.constraints().len(), 1);
        match &cgen.constraints()[0] {
            Constraint::IsInteger(_, _) => {}
            _ => panic!("Expected IsInteger constraint"),
        }
    }

    #[test]
    fn test_constraint_generator_function_call_arg_count_mismatch() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let mut functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Register a function that takes 2 parameters
        let func_name = interner.get_or_intern("foo");
        functions.insert(
            func_name,
            make_test_func_sig(
                vec![
                    InferType::Concrete(Type::I32),
                    InferType::Concrete(Type::I32),
                ],
                InferType::Concrete(Type::BOOL),
            ),
        );

        // Create a call with only 1 argument (mismatch)
        let arg = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(4, 6),
        });
        let (args_start, args_len) = rir.add_call_args(&[gruel_rir::RirCallArg {
            value: arg,
            mode: gruel_rir::RirArgMode::Normal,
        }]);
        let call = rir.add_inst(gruel_rir::Inst {
            data: InstData::Call {
                name: func_name,
                args_start,
                args_len,
            },
            span: Span::new(0, 7),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::BOOL);

        let info = cgen.generate(call, &mut ctx);

        // Should still return the declared return type
        assert_eq!(info.ty, InferType::Concrete(Type::BOOL));
        // No constraints generated when arg count mismatches (error will be in sema)
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_unknown_function() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new(); // Empty - no functions registered
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create a call to an unknown function
        let unknown_func = interner.get_or_intern("unknown");
        let arg = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(42),
            span: Span::new(8, 10),
        });
        let (args_start, args_len) = rir.add_call_args(&[gruel_rir::RirCallArg {
            value: arg,
            mode: gruel_rir::RirArgMode::Normal,
        }]);
        let call = rir.add_inst(gruel_rir::Inst {
            data: InstData::Call {
                name: unknown_func,
                args_start,
                args_len,
            },
            span: Span::new(0, 11),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(call, &mut ctx);

        // Unknown function returns Error type
        assert_eq!(info.ty, InferType::Concrete(Type::ERROR));
        // Arguments should still be processed (but no constraints generated for them)
        assert_eq!(cgen.constraints().len(), 0);
    }

    #[test]
    fn test_constraint_generator_match_multiple_arms() {
        let (mut rir, interner, type_pool) = make_test_rir_interner_and_type_pool();
        let functions = HashMap::new();
        let structs = HashMap::new();
        let enums = HashMap::new();
        let methods: HashMap<(StructId, Spur), MethodSig> = HashMap::new();
        let enum_methods: HashMap<(EnumId, Spur), MethodSig> = HashMap::new();

        // Create: match x { 1 => 10, 2 => 20, _ => 30 }
        let scrutinee = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(5),
            span: Span::new(6, 7),
        });

        // Arm 1: 1 => 10
        let body1 = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(10),
            span: Span::new(15, 17),
        });
        let pattern1 = gruel_rir::RirPattern::Int(1, Span::new(10, 11));

        // Arm 2: 2 => 20
        let body2 = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(20),
            span: Span::new(25, 27),
        });
        let pattern2 = gruel_rir::RirPattern::Int(2, Span::new(20, 21));

        // Arm 3: _ => 30
        let body3 = rir.add_inst(gruel_rir::Inst {
            data: InstData::IntConst(30),
            span: Span::new(35, 37),
        });
        let pattern3 = gruel_rir::RirPattern::Wildcard(Span::new(30, 31));

        let arms = vec![(pattern1, body1), (pattern2, body2), (pattern3, body3)];
        let (arms_start, arms_len) = rir.add_match_arms(&arms);
        let match_inst = rir.add_inst(gruel_rir::Inst {
            data: InstData::Match {
                scrutinee,
                arms_start,
                arms_len,
            },
            span: Span::new(0, 40),
        });

        let mut cgen = ConstraintGenerator::new(
            &rir,
            &interner,
            &functions,
            &structs,
            &enums,
            &methods,
            &enum_methods,
            &type_pool,
        );
        let params = HashMap::new();
        let mut ctx = ConstraintContext::new(&params, Type::I32);

        let info = cgen.generate(match_inst, &mut ctx);

        // Result should be a type variable (unified from all arm bodies)
        assert!(info.ty.is_var());

        // Should generate 6 constraints:
        // - 3 for pattern types matching scrutinee type (each arm)
        // - 3 for body types matching result type (each arm)
        assert_eq!(cgen.constraints().len(), 6);

        // Verify all constraints are Equal constraints
        for constraint in cgen.constraints() {
            match constraint {
                Constraint::Equal(_, _, _) => {}
                _ => panic!("Expected Equal constraint in match"),
            }
        }
    }
}