Hyper.Class.Unify

A class for unification

Documentation

class (Eq (UVarOf m # t), RTraversable t, ZipMatch t, HasTypeConstraints t, HasQuantifiedVar t, Monad m, MonadQuantify (TypeConstraintsOf t) (QVar t) m) => Unify m t where

Unify m t enables unify to perform unification for t in the Monad m.

The unifyRecursive method represents the constraint that Unify m applies to all recursive child nodes. It replaces context for Unify to avoid UndecidableSuperClasses.

Minimal complete definition

binding

Methods

binding :: BindingDict (UVarOf m) m t

The implementation for unification variables binding and lookup

unifyError :: (UnifyError t # UVarOf m) -> m a

Handles a unification error.

If unifyError is called then unification has failed. A compiler implementation may present an error message based on the provided UnifyError when this occurs.

default unifyError :: (MonadError (e # Pure) m, HSubset' e (UnifyError t)) => (UnifyError t # UVarOf m) -> m a

structureMismatch :: (forall c. Unify m c => (UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)) -> (t # UVarOf m) -> (t # UVarOf m) -> m ()

What to do when top-levels of terms being unified do not match.

Usually this will cause a unifyError.

Some AST terms could be equivalent despite not matching structurally, like record field extentions with the fields ordered differently. Those would override the default implementation to handle the unification of mismatching structures.

unifyRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))

default unifyRecursive :: HNodesConstraint t (Unify m) => Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))

Instances

Recursive (Unify m)

Defined in Hyper.Class.Unify

Methods

recurse :: forall (h :: HyperType) proxy. (HNodes h, Unify m h) => proxy (Unify m h) -> Dict (HNodesConstraint h (Unify m))

type family UVarOf (m :: Type -> Type) :: HyperType

Unification variable type for a unification monad

class Unify m t => UnifyGen m t where

A class for unification monads with scope levels

Minimal complete definition

scopeConstraints

Methods

scopeConstraints :: Proxy t -> m (TypeConstraintsOf t)

Get the current scope constraint

unifyGenRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))

default unifyGenRecursive :: HNodesConstraint t (UnifyGen m) => Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))

Instances

Recursive (UnifyGen m)

Defined in Hyper.Class.Unify

Methods

recurse :: forall (h :: HyperType) proxy. (HNodes h, UnifyGen m h) => proxy (UnifyGen m h) -> Dict (HNodesConstraint h (UnifyGen m))

data BindingDict v m t

BindingDict implements unification variables for a type in a unification monad.

It is parameterized on:

• v: The unification variable HyperType
• m: The Monad to bind in
• t: The unified term's HyperType

Has 2 implementations in hypertypes:

• bindingDict for pure state based unification
• stBinding for ST based unification

Constructors

BindingDict

Fields

• lookupVar :: !((v # t) -> m (UTerm v # t))
• newVar :: !((UTerm v # t) -> m (v # t))
• bindVar :: !((v # t) -> (UTerm v # t) -> m ())

applyBindings :: forall m t. Unify m t => (UVarOf m # t) -> m (Pure # t)

Resolve a term from a unification variable.

Note that this must be done after all unifications involving the term and its children are done, as it replaces unification state with cached resolved terms.

semiPruneLookup :: Unify m t => (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)

Look up a variable, and return last variable pointing to result. Prunes all variables on way to point to the last variable (path-compression ala union-find).

occursError :: Unify m t => (UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a

Format and throw an occurs check error