AST.Unify.Error

A type for unification errors

Documentation

data UnifyError t k

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

KNodes t => KNodes (UnifyError t)

Defined in AST.Unify.Error

Associated Types

type KNodesConstraint (UnifyError t) c :: Constraint

data KWitness (UnifyError t) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (UnifyError t) c => KWitness (UnifyError t) n -> Proxy c -> (c n -> r) -> r

KFunctor t => KFunctor (UnifyError t)

Defined in AST.Unify.Error

Methods

mapK :: (forall (n :: Knot -> Type). KWitness (UnifyError t) n -> Tree p n -> Tree q n) -> Tree (UnifyError t) p -> Tree (UnifyError t) q

KFoldable t => KFoldable (UnifyError t)

Defined in AST.Unify.Error

Methods

foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (UnifyError t) n -> Tree p n -> a) -> Tree (UnifyError t) p -> a

KTraversable t => KTraversable (UnifyError t)

Defined in AST.Unify.Error

Methods

sequenceK :: Applicative f => Tree (UnifyError t) (ContainedK f p) -> f (Tree (UnifyError t) p)

Constraints (UnifyError t k) Eq => Eq (UnifyError t k)

Defined in AST.Unify.Error

Methods

(==) :: UnifyError t k -> UnifyError t k -> Bool

(/=) :: UnifyError t k -> UnifyError t k -> Bool

Constraints (UnifyError t k) Ord => Ord (UnifyError t k)

Defined in AST.Unify.Error

Methods

compare :: UnifyError t k -> UnifyError t k -> Ordering

(<) :: UnifyError t k -> UnifyError t k -> Bool

(<=) :: UnifyError t k -> UnifyError t k -> Bool

(>) :: UnifyError t k -> UnifyError t k -> Bool

(>=) :: UnifyError t k -> UnifyError t k -> Bool

max :: UnifyError t k -> UnifyError t k -> UnifyError t k

min :: UnifyError t k -> UnifyError t k -> UnifyError t k

Constraints (UnifyError t k) Show => Show (UnifyError t k)

Defined in AST.Unify.Error

Methods

showsPrec :: Int -> UnifyError t k -> ShowS

show :: UnifyError t k -> String

showList :: [UnifyError t k] -> ShowS

Generic (UnifyError t k)

Defined in AST.Unify.Error

Associated Types

type Rep (UnifyError t k) :: Type -> Type

Methods

from :: UnifyError t k -> Rep (UnifyError t k) x

to :: Rep (UnifyError t k) x -> UnifyError t k

Constraints (UnifyError t k) Binary => Binary (UnifyError t k)

Defined in AST.Unify.Error

Methods

put :: UnifyError t k -> Put

get :: Get (UnifyError t k)

putList :: [UnifyError t k] -> Put

Constraints (UnifyError t k) NFData => NFData (UnifyError t k)

Defined in AST.Unify.Error

Methods

rnf :: UnifyError t k -> ()

Constraints (UnifyError t k) Pretty => Pretty (UnifyError t k)

Defined in AST.Unify.Error

Methods

pPrintPrec :: PrettyLevel -> Rational -> UnifyError t k -> Doc

pPrint :: UnifyError t k -> Doc

pPrintList :: PrettyLevel -> [UnifyError t k] -> Doc

data KWitness (UnifyError t) n

Defined in AST.Unify.Error

data KWitness (UnifyError t) n where

• W_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness (UnifyError t) t
• E_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness t n -> KWitness (UnifyError t) n

type KNodesConstraint (UnifyError t) c

Defined in AST.Unify.Error

type KNodesConstraint (UnifyError t) c = (c t, KNodesConstraint t c)

type Rep (UnifyError t k)

Defined in AST.Unify.Error

type Rep (UnifyError t k) = D1 (MetaData "UnifyError" "AST.Unify.Error" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) ((C1 (MetaCons "SkolemUnified" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t))) :+: C1 (MetaCons "SkolemEscape" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t)))) :+: (C1 (MetaCons "ConstraintsViolation" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k)) :*: 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 k)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k))) :+: C1 (MetaCons "Mismatch" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k))))))

_SkolemUnified :: forall t k. Prism' (UnifyError t k) ((#) k t, (#) k t)

_SkolemEscape :: forall t k. Prism' (UnifyError t k) ((#) k t)

_ConstraintsViolation :: forall t k. Prism' (UnifyError t k) (t k, TypeConstraintsOf t)

_Occurs :: forall t k. Prism' (UnifyError t k) (t k, t k)

_Mismatch :: forall t k. Prism' (UnifyError t k) (t k, t k)