Top.Constraint

A data type to represent constraints in general, and a type class for constraints that are solvable.

Documentation

type Constraints m = [Constraint m]

data Constraint m

Constructors

forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool)

Instances

Show (Constraint m)

Substitutable (Constraint m)

Monad m => Solvable (Constraint m) m

class (Show c, Substitutable c, Monad m) => Solvable c m where

A constraint is solvable if it knows how it can be solved in a certain state (a monadic operation), if it can check afterwards whether the final state satisfies it, and when it can be shown.

Methods

solveConstraint :: c -> m ()

checkCondition :: c -> m Bool

Instances

Monad m => Solvable (Constraint m) m

(TypeConstraintInfo info, HasSubst m info, HasTI m info) => Solvable (EqualityConstraint info) m

(HasBasic m info, HasTI m info, HasSubst m info, HasQual m info, PolyTypeConstraintInfo info) => Solvable (PolymorphismConstraint info) m

(HasQual m info, PolyTypeConstraintInfo info) => Solvable (ExtraConstraint info) m

(Solvable a m, Solvable b m) => Solvable (Either a b) m

If both constraints of type a and b can be solved in a Monad m, then 'Either a b' constraints can also be solved in this monad.

(Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m

liftConstraint :: Solvable c m => c -> Constraint m

Lifting a constraint to the Constraint data type. Every instance of the Solvable type class can be lifted.

liftConstraints :: Solvable c m => [c] -> Constraints m

mapConstraint :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2

newtype Operation m

Constructors

Op_ String

Instances

Show (Operation m)

Substitutable (Operation m)

operation :: Monad m => String -> m () -> Constraint m

data ConstraintSum f g info

The data type ConstraintSum is similar to the (standard) Either data type. However, its Show instance is slightly different as the name of the constructor is not shown.

Constructors

SumLeft (f info)

SumRight (g info)

Instances

(Functor f, Functor g) => Functor (ConstraintSum f g)

(Show (f info), Show (g info)) => Show (ConstraintSum f g info)

(Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info)

(Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m

constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c

Similar to the either function.