Safe Haskell | None |
---|
Check the kind of a type.
- checkType :: (Ord n, Pretty n) => DataDefs n -> Env n -> Type n -> Either (Error n) (Kind n)
- kindOfType :: (Ord 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, Pretty n) => DataDefs n -> Env 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, 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
Type errors.
ErrorUndefined | An undefined type variable. |
| |
ErrorUndefinedCtor | An undefined type constructor. |
| |
ErrorVarAnnotMismatch | The kind annotation on the variables does not match the one in the environment. |
| |
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. |
| |
ErrorAppNotFun | A type application where the thing being applied is not a function. |
| |
ErrorSumKindMismatch | A type sum where the components have differing kinds. |
| |
ErrorSumKindInvalid | A type sum that does not have effect or closure kind. |
| |
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. |
|