Safe Haskell	Safe-Inferred
Language	Haskell2010

Hyper.Unify

Description

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

Instances

Instances details

Generic (UVar t) Source #
Instance details Defined in Hyper.Unify.Binding Associated Types type Rep (UVar t) :: Type -> Type # Methods from :: UVar t -> Rep (UVar t) x # to :: Rep (UVar t) x -> UVar t #
Show (UVar t) Source #
Instance details Defined in Hyper.Unify.Binding Methods showsPrec :: Int -> UVar t -> ShowS # show :: UVar t -> String # showList :: [UVar t] -> ShowS #
Eq (UVar t) Source #
Instance details Defined in Hyper.Unify.Binding Methods (==) :: UVar t -> UVar t -> Bool # (/=) :: UVar t -> UVar t -> Bool #
Ord (UVar t) Source #
Instance details Defined in Hyper.Unify.Binding Methods compare :: UVar t -> UVar t -> Ordering # (<) :: UVar t -> UVar t -> Bool # (<=) :: UVar t -> UVar t -> Bool # (>) :: UVar t -> UVar t -> Bool # (>=) :: UVar t -> UVar t -> Bool # max :: UVar t -> UVar t -> UVar t # min :: UVar t -> UVar t -> UVar t #
type Rep (UVar t) Source #
Instance details Defined in Hyper.Unify.Binding type Rep (UVar t) = D1 ('MetaData "UVar" "Hyper.Unify.Binding" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'True) (C1 ('MetaCons "UVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

module Hyper.Unify.Constraints

data UnifyError t h Source #

An error that occurred during unification

Constructors

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

Instances details

HFoldable t => HFoldable (UnifyError t) Source #
Instance details Defined in Hyper.Unify.Error Methods hfoldMap :: Monoid a => (forall (n :: HyperType). HWitness (UnifyError t) n -> (p # n) -> a) -> (UnifyError t # p) -> a Source #
HFunctor t => HFunctor (UnifyError t) Source #
Instance details Defined in Hyper.Unify.Error Methods hmap :: (forall (n :: HyperType). HWitness (UnifyError t) n -> (p # n) -> q # n) -> (UnifyError t # p) -> UnifyError t # q Source #
HNodes t => HNodes (UnifyError t) Source #
Instance details Defined in Hyper.Unify.Error Associated Types type HNodesConstraint (UnifyError t) c Source # type HWitnessType (UnifyError t) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n :: HyperType) r. HNodesConstraint (UnifyError t) c => HWitness (UnifyError t) n -> Proxy c -> (c n => r) -> r Source #
HTraversable t => HTraversable (UnifyError t) Source #
Instance details Defined in Hyper.Unify.Error Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (UnifyError t # ContainedH f p) -> f (UnifyError t # p) Source #
Generic (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Associated Types type Rep (UnifyError t h) :: Type -> Type # Methods from :: UnifyError t h -> Rep (UnifyError t h) x # to :: Rep (UnifyError t h) x -> UnifyError t h #
Constraints (UnifyError t h) Show => Show (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods showsPrec :: Int -> UnifyError t h -> ShowS # show :: UnifyError t h -> String # showList :: [UnifyError t h] -> ShowS #
Constraints (UnifyError t h) Binary => Binary (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods put :: UnifyError t h -> Put # get :: Get (UnifyError t h) # putList :: [UnifyError t h] -> Put #
Constraints (UnifyError t h) NFData => NFData (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods rnf :: UnifyError t h -> () #
Constraints (UnifyError t h) Eq => Eq (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods (==) :: UnifyError t h -> UnifyError t h -> Bool # (/=) :: UnifyError t h -> UnifyError t h -> Bool #
Constraints (UnifyError t h) Ord => Ord (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods compare :: UnifyError t h -> UnifyError t h -> Ordering # (<) :: UnifyError t h -> UnifyError t h -> Bool # (<=) :: UnifyError t h -> UnifyError t h -> Bool # (>) :: UnifyError t h -> UnifyError t h -> Bool # (>=) :: UnifyError t h -> UnifyError t h -> Bool # max :: UnifyError t h -> UnifyError t h -> UnifyError t h # min :: UnifyError t h -> UnifyError t h -> UnifyError t h #
Constraints (UnifyError t h) Pretty => Pretty (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error Methods pPrintPrec :: PrettyLevel -> Rational -> UnifyError t h -> Doc # pPrint :: UnifyError t h -> Doc # pPrintList :: PrettyLevel -> [UnifyError t h] -> Doc #
type HWitnessType (UnifyError t) Source #
Instance details Defined in Hyper.Unify.Error type HWitnessType (UnifyError t)
type HNodesConstraint (UnifyError t) constraint Source #
Instance details Defined in Hyper.Unify.Error type HNodesConstraint (UnifyError t) constraint = (HNodesConstraint t constraint, constraint t)
type Rep (UnifyError t h) Source #
Instance details Defined in Hyper.Unify.Error type Rep (UnifyError t h) = D1 ('MetaData "UnifyError" "Hyper.Unify.Error" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'False) ((C1 ('MetaCons "SkolemUnified" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (h :# t)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (h :# t))) :+: C1 ('MetaCons "SkolemEscape" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (h :# t)))) :+: (C1 ('MetaCons "ConstraintsViolation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t h)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeConstraintsOf t))) :+: (C1 ('MetaCons "Occurs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t h)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t h))) :+: C1 ('MetaCons "Mismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t h)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t h))))))

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 #

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) Source #

unifyUnbound :: Unify m t => (WithConstraint (UVarOf m) # t) -> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m (UVarOf m # t) Source #