ddc-core-0.4.1.3: Disciplined Disciple Compiler core language and type checker.

Safe HaskellNone

DDC.Type.Check

Contents

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.

checkTypeMSource

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.

ErrorMismatch

Generic kind mismatch.

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.

ErrorAppArgMismatch

A type application where the parameter and argument kinds don't match.

ErrorWitnessImplInvalid

A witness implication where the premise or conclusion has an invalid kind.

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.

ErrorSumKindInvalid

A type sum that does not have effect or closure kind.

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.

ErrorDataDupCtorName

A duplicate data constructor name.

Fields

errorDataCtorName :: n
 
ErrorDataWrongResult

A data constructor with the wrong result type.

Instances

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