Struct UnificationTable 

pub struct UnificationTable { /* private fields */ }

Union-Find table implementing Robinson unification with occurs check.

Type variables are allocated by [fresh] and resolved by [find]. [zonk] fully resolves a type after inference, converting remaining unbound variables to InferType::Unknown (which maps to LogosType::Unknown).

Implementations

impl UnificationTable

pub fn new() -> UnificationTable

pub fn fresh(&mut self) -> InferType

Allocate a fresh unbound type variable, returning the wrapped InferType.

pub fn fresh_var(&mut self) -> TyVar

Allocate a fresh unbound type variable, returning the raw TyVar.

pub fn instantiate(&mut self, scheme: &TypeScheme) -> InferType

Instantiate a TypeScheme by replacing each quantified variable with a fresh one.

Each call site of a generic function gets independent fresh variables so that two calls to identity(42) and identity(true) do not interfere.

pub fn find(&self, tv: TyVar) -> InferType

Follow the binding chain for a type variable (iterative, no path compression).

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

Resolve type variables, keeping unbound variables as Var(tv).

Unlike [zonk], this does not convert unbound variables to Unknown. Use this during inference to preserve generic type params as Var(tv) so they can be unified at call sites.

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

Fully resolve all type variables in a type.

Unbound variables become InferType::Unknown, which maps to LogosType::Unknown when converted by [to_logos_type].

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

Zonk then convert to LogosType. Unsolved variables become Unknown.

pub fn unify(&mut self, a: &InferType, b: &InferType) -> Result<(), TypeError>

Unify two types, binding type variables as needed.

Returns Ok(()) if unification succeeds (bindings may be updated). Returns Err(TypeError) on a genuine type contradiction.