Safe Haskell	None

DDC.Type.Check

Contents

Kinds of Types
Kinds of Constructors
Errors

Description

Check the kind of a type.

Synopsis

Documentation

data Config n Source

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.

Constructors

Config

Fields

configPrimDataDefs :: DataDefs n: Data type definitions.
configPrimSupers :: SuperEnv n: Super kinds of primitive kinds.
configPrimKinds :: KindEnv n: Kinds of primitive types.
configPrimTypes :: TypeEnv n: Types of primitive operators.
configTrackedEffects :: Bool: Track effect type information.
configTrackedClosures :: Bool: Track closure type information.
configFunctionalEffects :: Bool: Attach effect information to function types.
configFunctionalClosures :: Bool: Attach closure information to function types.

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

data Error n Source

Things that can go wrong when checking the kind of at type.

Constructors

ErrorUndefined	An undefined type variable.
Fields errorBound :: Bound n
ErrorUndefinedCtor	An undefined type constructor.
Fields errorBound :: Bound n
ErrorVarAnnotMismatch	The kind annotation on the variables does not match the one in the environment.
Fields errorBound :: Bound n errorTypeEnv :: Type n
ErrorNakedSort	Found a naked sort constructor.
Fields errorSort :: Sort n
ErrorUnappliedKindFun	Found an unapplied kind function constructor.
ErrorAppArgMismatch	A type application where the parameter and argument kinds don't match.
Fields errorChecking :: Type n errorParamKind :: Kind n errorArgKind :: Kind n
ErrorAppNotFun	A type application where the thing being applied is not a function.
Fields errorChecking :: Type n errorFunType :: Type n errorFunTypeKind :: Kind n errorArgType :: Type n errorArgTypeKind :: Kind n
ErrorSumKindMismatch	A type sum where the components have differing kinds.
Fields errorKindExpected :: Kind n errorTypeSum :: TypeSum n errorKinds :: [Kind n]
ErrorSumKindInvalid	A type sum that does not have effect or closure kind.
Fields errorCheckingSum :: TypeSum n errorKind :: Kind n
ErrorForallKindInvalid	A forall where the body does not have data or witness kind.
Fields errorChecking :: Type n errorBody :: Type n errorKind :: Kind n
ErrorWitnessImplInvalid	A witness implication where the premise or conclusion has an invalid kind.
Fields errorChecking :: Type n errorLeftType :: Type n errorLeftKind :: Kind n errorRightType :: Type n errorRightKind :: Kind n

Instances

Show n => Show (Error n)
(Eq n, Show n, Pretty n) => Pretty (Error n)