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() -> Self

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.