Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Unification
Synopsis
- unify :: forall m t. Unify m t => (UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
- module Hyper.Class.Unify
- data UVar (t :: AHyperType)
- module Hyper.Unify.Constraints
- data UnifyError t h
- = SkolemUnified (h :# t) (h :# t)
- | SkolemEscape (h :# t)
- | ConstraintsViolation (t h) (TypeConstraintsOf t)
- | Occurs (t h) (t h)
- | Mismatch (t h) (t h)
- updateConstraints :: Unify m t => TypeConstraintsOf t -> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
- updateTermConstraints :: forall m t. Unify m t => (UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> TypeConstraintsOf t -> m ()
- updateTermConstraintsH :: Unify m t => (WithConstraint (UVarOf m) # t) -> m ()
- unifyUTerms :: forall m t. Unify m t => (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
- unifyUnbound :: Unify m t => (WithConstraint (UVarOf m) # t) -> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
Documentation
unify :: forall m t. Unify m t => (UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t) Source #
Unify unification variables
module Hyper.Class.Unify
data UVar (t :: AHyperType) Source #
A unification variable identifier pure state based unification
module Hyper.Unify.Constraints
data UnifyError t h Source #
An error that occurred during unification
SkolemUnified (h :# t) (h :# t) | A universally quantified variable was unified with a different type |
SkolemEscape (h :# t) | A universally quantified variable escapes its scope |
ConstraintsViolation (t h) (TypeConstraintsOf t) | A term violates constraints that should apply to it |
Occurs (t h) (t h) | Infinite type encountered. A type occurs within itself |
Mismatch (t h) (t h) | Unification between two mismatching type structures |
Instances
Exported only for SPECIALIZE pragmas
updateConstraints :: Unify m t => TypeConstraintsOf t -> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m () Source #
updateTermConstraints :: forall m t. Unify m t => (UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> TypeConstraintsOf t -> m () Source #
updateTermConstraintsH :: Unify m t => (WithConstraint (UVarOf m) # t) -> m () Source #