Struct Unifier 

pub struct Unifier {
    pub substitution: Substitution,
}

Unification engine for type inference.

The unifier processes constraints and builds a substitution mapping type variables to their resolved types.

Fields

substitution: Substitution

The current substitution being built.

Implementations

impl Unifier

pub fn new() -> Self

Create a new unifier with an empty substitution.

pub fn with_capacity(type_var_count: u32) -> Self

Create a new unifier with a pre-sized substitution.

Use this when you know how many type variables will be created (e.g., from TypeVarAllocator::count()).

pub fn unify(&mut self, lhs: &InferType, rhs: &InferType) -> UnifyResult

Unify two types.

This is the core of Algorithm W. It updates the substitution to make the two types equal, or returns an error if they cannot be unified.

Unification rules:

1. Concrete(T) = Concrete(T) → succeeds if types are equal
2. Var(α) = τ → binds α to τ (after occurs check)
3. τ = Var(α) → binds α to τ (symmetric)
4. IntLiteral = Concrete(integer) → succeeds (literal takes integer type)
5. IntLiteral = IntLiteral → succeeds (both stay as IntLiteral)
6. IntLiteral = Concrete(non-integer) → fails
7. Array(T1, N) = Array(T2, N) → succeeds if T1 unifies with T2
8. Array(T1, N1) = Array(T2, N2) where N1 ≠ N2 → fails

pub fn check_signed(&self, ty: &InferType) -> UnifyResult

Check that a type is signed.

Returns an error if the type is a concrete unsigned integer. For type variables and IntLiterals, this check is deferred (the constraint would need to be stored and checked later).

pub fn check_integer(&self, ty: &InferType) -> UnifyResult

Check that a type is an integer (signed or unsigned).

Returns an error if the type is a concrete non-integer type. For type variables and IntLiterals, the check passes.

pub fn check_numeric(&self, ty: &InferType) -> UnifyResult

Check that a type is numeric (integer or float).

Returns an error if the type is a concrete non-numeric type (e.g., bool). For type variables, IntLiteral, and FloatLiteral, the check passes.

pub fn check_unsigned(&self, ty: &InferType) -> UnifyResult

Check that a type is an unsigned integer.

Returns an error if the type is a concrete signed integer or non-integer type. For type variables, the check is deferred. For IntLiteral, we allow it and it will be bound to u64 (the default unsigned type).

pub fn solve_constraints( &mut self, constraints: &[Constraint], ) -> Vec<UnificationError>

Solve a list of constraints, collecting any errors.

This is the main entry point for Algorithm W. It processes each constraint in order, updates the substitution, and collects errors for reporting.

On error, the unifier continues processing remaining constraints to catch as many errors as possible in one pass. Type variables involved in errors are bound to Type::ERROR for recovery.

Returns a list of errors (empty if all constraints were satisfied).

pub fn default_int_literal_vars(&mut self, int_literal_vars: &[TypeVarId])

Default all IntLiteral types bound to type variables to i32.

Called at the end of unification for a function to resolve any unconstrained integer literals. This processes all type variables in the substitution that are bound to IntLiteral. Default unconstrained integer literal type variables to i32.

Takes the list of type variables that were allocated for integer literals during constraint generation. Any that remain unbound (not constrained to a specific integer type) are defaulted to i32.

pub fn default_float_literal_vars(&mut self, float_literal_vars: &[TypeVarId])

Default unconstrained float literal type variables to f64.

pub fn resolve_infer_type(&self, ty: &InferType) -> InferType

Resolve a type to its final form after applying all substitutions.

Follows the substitution chain and defaults IntLiteral to i32. For arrays, recursively resolves the element type. Returns the fully-resolved InferType.

pub fn resolve(&self, ty: &InferType) -> Option<Type>

Resolve a type to its final concrete type.

Follows the substitution chain and defaults IntLiteral to i32. Returns None if the type resolves to an unbound type variable or an array (arrays need to be handled separately to create ArrayTypeIds).

pub fn resolve_or_error(&self, ty: &InferType) -> Type

Resolve a type to its final concrete type, with error recovery.

Like resolve, but returns Type::ERROR instead of None for unbound type variables. This allows compilation to continue with error recovery.

Note: For arrays, this returns Type::ERROR. Use resolve_infer_type and handle InferType::Array explicitly to create proper ArrayTypeIds.

Trait Implementations

impl Debug for Unifier

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Unifier

fn default() -> Self

Returns the “default value” for a type.