Safe Haskell | None |
---|
Check the kind of a type.
- data Config n = Config {}
- configOfProfile :: Profile n -> Config n
- checkType :: (Ord n, Show n, Pretty n) => Config n -> KindEnv n -> Type n -> Either (Error n) (Kind n)
- kindOfType :: (Ord n, Show n, Pretty n) => Config 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 {
Documentation
Static configuration for the type checker. These fields don't change as we decend into the tree.
The starting configuration should be converted from the profile that
defines the language fragment you are checking.
See DDC.Core.Fragment and use configOfProfile
below.
Config | |
|
configOfProfile :: Profile n -> Config nSource
Convert a langage profile to a type checker configuration.
Kinds of Types
checkType :: (Ord n, Show n, Pretty n) => Config 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) => Config 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.
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. |
|