A data type to represent constraints in general, and a type class for constraints that are solvable.
- type Constraints m = [Constraint m]
- data Constraint m = forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool)
- class (Show c, Substitutable c, Monad m) => Solvable c m where
- liftConstraint :: Solvable c m => c -> Constraint m
- liftConstraints :: Solvable c m => [c] -> Constraints m
- mapConstraint :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2
- newtype Operation m = Op_ String
- operation :: Monad m => String -> m () -> Constraint m
- data ConstraintSum f g info
- constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c
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.
|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
|(Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m|
Lifting a constraint to the Constraint data type. Every instance of the Solvable type class can be lifted.
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.