Safe Haskell	None

DDC.Type.Check

Contents

Checking types.
Wrappers for specific universes.
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

configPrimKinds :: KindEnv n: Kinds of primitive types.
configPrimTypes :: TypeEnv n: Types of primitive operators.
configDataDefs :: DataDefs n: Data type definitions.
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.
configEffectCapabilities :: Bool: Treat effects as capabilities.
configNameIsHole :: Maybe (n -> Bool): This name represents some hole in the expression that needs to be filled in by the type checker.

configOfProfile :: Profile n -> Config nSource

Convert a langage profile to a type checker configuration.

Checking types.

checkType :: (Ord n, Show n, Pretty n) => Config n -> KindEnv n -> Universe -> Type n -> Either (Error n) (Type n, Type n)Source

Check a type in the given universe with the given environment Returns the updated type and its classifier (a kind or sort), depeding on the universe of the type being checked.

checkTypeM Source

Arguments

:: (Ord n, Show n, Pretty n)
=> Config n	Type checker configuration.
-> KindEnv n	Top-level kind environment.
-> Context n	Local context.
-> Universe	What universe the type to check is in.
-> Type n	The type to check (can be a Spec or Kind)
-> Mode n	Type checker mode.
-> CheckM n (Type n, Kind n, Context n)

Check a type returning its kind, or a kind returning its sort.

The unverse of the thing to check is directly specified, and if the thing is not actually in this universe they you'll get an error.

We track what universe the provided kind is in for defence against transform bugs. Types like ([a : [b : Data]. b]. a -> a), should not be accepted by the source parser, but may be created by bogus program transformations. Quantifiers cannot be used at the kind level, so it's better to fail early.

Wrappers for specific universes.

checkSpec :: (Ord n, Show n, Pretty n) => Config n -> KindEnv n -> Type n -> Either (Error n) (Type n, Kind n)Source

Check a spec in the given environment, returning an error or its kind.

kindOfSpec :: (Ord n, Show n, Pretty n) => Config n -> Type n -> Either (Error n) (Kind n)Source

Check a spec in an empty environment, returning an error or its kind.

sortOfKind :: (Ord n, Show n, Pretty n) => Config n -> Kind n -> Either (Error n) (Sort n)Source

Check a kind in an empty environment, returning an error or its sort.

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

ErrorUniverseMalfunction	Tried to check a type using the wrong universe, for example: asking for the kind of a kind.
Fields errorType :: Type n errorUniverse :: Universe
ErrorMismatch	Generic kind mismatch.
Fields errorUniverse :: Universe errorInferred :: Type n errorExpected :: Type n errorChecking :: Type n
ErrorUndefined	An undefined type variable.
Fields errorBound :: Bound n
ErrorUnappliedKindFun	Found an unapplied kind function constructor.
ErrorNakedSort	Found a naked sort constructor.
Fields errorSort :: Sort n
ErrorUndefinedTypeCtor	An undefined type constructor.
Fields errorBound :: Bound 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
ErrorAppArgMismatch	A type application where the parameter and argument kinds don't match.
Fields errorChecking :: Type n errorFunType :: Type n errorFunKind :: Kind n errorArgType :: Type n errorArgKind :: 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
ErrorForallKindInvalid	A forall where the body does not have data or witness kind.
Fields errorChecking :: Type n errorBody :: Type n errorKind :: 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

Instances

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

data ErrorData n Source

Things that can go wrong when checking data type definitions.

Constructors

ErrorDataDupTypeName	A duplicate data type constructor name.
Fields errorDataDupTypeName :: n
ErrorDataDupCtorName	A duplicate data constructor name.
Fields errorDataCtorName :: n
ErrorDataWrongResult	A data constructor with the wrong result type.
Fields errorDataCtorName :: n errorDataCtorResultActual :: Type n errorDataCtorResultExpected :: Type n

Instances

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