DDC.Type.Check

Check the kind of a type.

Documentation

data Config n

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.

configGlobalCaps :: TypeEnv n

Types of globally available capabilities.

The inferred types of computations do not contain these capabilities as they are always available and thus do not need to be tracked in types.

configNameIsHole :: Maybe (n -> Bool)

This name represents some hole in the expression that needs to be filled in by the type checker.

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.

configGeneralLetRec :: Bool

Allow general let-rec

configImplicitRun :: Bool

Automatically run effectful applications.

configImplicitBox :: Bool

Automatically box bodies of abstractions.

configOfProfile :: Profile n -> Config n

Convert a language 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)

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

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)

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)

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)

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

Kinds of Constructors

takeSortOfKiCon :: KiCon -> Maybe (Sort n)

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 n

Take the kind of a witness type constructor.

kindOfTcCon :: TcCon -> Kind n

Take the kind of a computation type constructor.

Errors

data Error n

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

ErrorInfinite

Cannot construct infinite type.

Fields

errorTypeVar :: Type n

errorTypeBind :: 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)

data ErrorData n

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)