syntax-tree-0.1.0.1: Typed ASTs

Safe HaskellNone
LanguageHaskell2010

AST.Class.Unify

Description

A class for unification

Synopsis

Documentation

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

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, unifyError

Methods

binding :: BindingDict (UVarOf m) m t Source #

The implementation for unification variables binding and lookup

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

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.

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

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 (KNodesConstraint t (Unify m)) Source #

unifyRecursive :: KNodesConstraint t (Unify m) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Unify m)) Source #

Instances
Recursive (Unify m) Source # 
Instance details

Defined in AST.Class.Unify

Methods

recurse :: (KNodes k, Unify m k) => Proxy (Unify m k) -> Dict (KNodesConstraint k (Unify m)) Source #

type family UVarOf (m :: Type -> Type) :: Knot -> Type Source #

Unification variable type for a unification monad

data BindingDict v m t Source #

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

It is parameterized on:

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

Has 2 implementations in syntax-tree:

Constructors

BindingDict 

Fields