| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
AST.Unify
Description
Unification
Synopsis
- unify :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UVarOf m) t -> m (Tree (UVarOf m) t)
- 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
- binding :: BindingDict (UVarOf m) m t
- unifyError :: Tree (UnifyError t) (UVarOf m) -> m a
- 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 ()
- unifyRecursive :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Unify m))
- data BindingDict v m t = BindingDict {}
- type family UVarOf (m :: Type -> Type) :: Knot -> Type
- module AST.Unify.Constraints
- data UnifyError t k
- = SkolemUnified (k # t) (k # t)
- | SkolemEscape (k # t)
- | ConstraintsViolation (t k) (TypeConstraintsOf t)
- | Occurs (t k) (t k)
- | Mismatch (t k) (t k)
- updateConstraints :: Unify m t => TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m ()
- updateTermConstraints :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTermBody (UVarOf m)) t -> TypeConstraintsOf t -> m ()
- updateTermConstraintsH :: Unify m t => Tree (WithConstraint (UVarOf m)) t -> m ()
- unifyUTerms :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t)
- unifyUnbound :: Unify m t => Tree (UVarOf m) t -> TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t)
Documentation
unify :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UVarOf m) t -> m (Tree (UVarOf m) t) Source #
Unify unification variables
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
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 #
data BindingDict v m t Source #
BindingDict implements unification variables for a type in a unification monad.
It is parameterized on:
Has 2 implementations in syntax-tree:
bindingDictfor pure state based unificationstBindingforSTbased unification
type family UVarOf (m :: Type -> Type) :: Knot -> Type Source #
Unification variable type for a unification monad
module AST.Unify.Constraints
data UnifyError t k Source #
An error that occurred during unification
Constructors
| SkolemUnified (k # t) (k # t) | A universally quantified variable was unified with a different type |
| SkolemEscape (k # t) | A universally quantified variable escapes its scope |
| ConstraintsViolation (t k) (TypeConstraintsOf t) | A term violates constraints that should apply to it |
| Occurs (t k) (t k) | Infinite type encountered. A type occurs within itself |
| Mismatch (t k) (t k) | Unification between two mismatching type structures |
Instances
Exported only for SPECIALIZE pragmas
updateConstraints :: Unify m t => TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m () Source #
updateTermConstraints :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTermBody (UVarOf m)) t -> TypeConstraintsOf t -> m () Source #
updateTermConstraintsH :: Unify m t => Tree (WithConstraint (UVarOf m)) t -> m () Source #