| Safe Haskell | None |
|---|
DDC.Type.Check
Description
Check the kind of a type.
- checkType :: (Ord n, Show n, Pretty n) => DataDefs n -> KindEnv n -> Type n -> Either (Error n) (Kind n)
- kindOfType :: (Ord n, Show n, Pretty n) => DataDefs n -> Type n -> Either (Error n) (Kind n)
- takeSortOfKiCon :: KiCon -> Maybe (Sort n)
- kindOfTwCon :: TwCon -> Kind n
- kindOfTcCon :: TcCon -> Kind n
- data Error n
- = ErrorUndefined {
- errorBound :: Bound n
- | ErrorUndefinedCtor {
- errorBound :: Bound n
- | ErrorVarAnnotMismatch {
- errorBound :: Bound n
- errorTypeEnv :: Type n
- | ErrorNakedSort { }
- | ErrorUnappliedKindFun
- | ErrorAppArgMismatch {
- errorChecking :: Type n
- errorParamKind :: Kind n
- errorArgKind :: Kind n
- | ErrorAppNotFun {
- errorChecking :: Type n
- errorFunType :: Type n
- errorFunTypeKind :: Kind n
- errorArgType :: Type n
- errorArgTypeKind :: Kind n
- | ErrorSumKindMismatch {
- errorKindExpected :: Kind n
- errorTypeSum :: TypeSum n
- errorKinds :: [Kind n]
- | ErrorSumKindInvalid {
- errorCheckingSum :: TypeSum n
- errorKind :: Kind n
- | ErrorForallKindInvalid { }
- | ErrorWitnessImplInvalid {
- errorChecking :: Type n
- errorLeftType :: Type n
- errorLeftKind :: Kind n
- errorRightType :: Type n
- errorRightKind :: Kind n
- = ErrorUndefined {
Kinds of Types
checkType :: (Ord n, Show n, Pretty n) => DataDefs n -> KindEnv n -> Type n -> Either (Error n) (Kind n)Source
Check a type in the given environment, returning an error or its kind.
kindOfType :: (Ord n, Show n, Pretty n) => DataDefs n -> Type n -> Either (Error n) (Kind n)Source
Check a type in an empty environment, returning an error or its kind.
Kinds of Constructors
takeSortOfKiCon :: KiCon -> Maybe (Sort n)Source
Take the superkind of an atomic kind constructor.
Yields Nothing for the kind function (~>) as it doesn't have a sort
without being fully applied.
kindOfTwCon :: TwCon -> Kind nSource
Take the kind of a witness type constructor.
kindOfTcCon :: TcCon -> Kind nSource
Take the kind of a computation type constructor.
Errors
Things that can go wrong when checking the kind of at type.
Constructors
| ErrorUndefined | An undefined type variable. |
Fields
| |
| ErrorUndefinedCtor | An undefined type constructor. |
Fields
| |
| ErrorVarAnnotMismatch | The kind annotation on the variables does not match the one in the environment. |
Fields
| |
| ErrorNakedSort | Found a naked sort constructor. |
| ErrorUnappliedKindFun | Found an unapplied kind function constructor. |
| ErrorAppArgMismatch | A type application where the parameter and argument kinds don't match. |
Fields
| |
| ErrorAppNotFun | A type application where the thing being applied is not a function. |
Fields
| |
| ErrorSumKindMismatch | A type sum where the components have differing kinds. |
Fields
| |
| ErrorSumKindInvalid | A type sum that does not have effect or closure kind. |
Fields
| |
| ErrorForallKindInvalid | A forall where the body does not have data or witness kind. |
| ErrorWitnessImplInvalid | A witness implication where the premise or conclusion has an invalid kind. |
Fields
| |