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

Safe HaskellNone

DDC.Core.Check

Contents

Description

Type checker for the Disciple Core language.

The functions in this module do not check for language fragment compliance. This needs to be done separately via DDC.Core.Fragment.

Synopsis

Configuration

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.

Type checker trace

data CheckTrace Source

Human readable trace of the type checker.

Constructors

CheckTrace 

Fields

checkTraceDoc :: Doc
 

Instances

Checking Modules

checkModuleSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> Module a n

Module to check.

-> Mode n

Type checker mode.

-> (Either (Error a n) (Module (AnTEC a n) n), CheckTrace) 

Type check a module.

If it's good, you get a new version with types attached to all the bound variables

If it's bad, you get a description of the error.

Checking Expressions

data Mode n Source

What mode we're performing type checking/inference in.

Constructors

Recon

Reconstruct the type of the expression, requiring type annotations on parameters as well as type applications to already be present.

Synth

The ascending smoke of incense. Synthesise the type of the expression, producing unification variables for bidirectional type inference.

Check (Type n)

The descending tongue of flame. Check the type of an expression against this expected type, and unify expected types into unification variables for bidirecional type inference.

Instances

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

checkExpSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> KindEnv n

Starting kind environment.

-> TypeEnv n

Starting type environment.

-> Exp a n

Expression to check.

-> Mode n

Check mode.

-> (Either (Error a n) (Exp (AnTEC a n) n, Type n, Effect n, Closure n), CheckTrace) 

Type check an expression.

If it's good, you get a new version with types attached every AST node, as well as every binding occurrence of a variable.

If it's bad, you get a description of the error.

The kinds and types of primitives are added to the environments automatically, you don't need to supply these as part of the starting kind and type environment.

typeOfExpSource

Arguments

:: (Ord n, Pretty n, Show n) 
=> Config n

Static configuration.

-> KindEnv n

Starting Kind environment

-> TypeEnv n

Starting Type environment.

-> Exp a n

Expression to check.

-> Either (Error a n) (Type n) 

Like checkExp, but only return the value type of an expression.

Checking Witnesses

checkWitnessSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> KindEnv n

Starting Kind Environment.

-> TypeEnv n

Strating Type Environment.

-> Witness a n

Witness to check.

-> Either (Error a n) (Witness (AnT a n) n, Type n) 

Check a witness.

If it's good, you get a new version with types attached to all the bound variables, as well as the type of the overall witness.

If it's bad, you get a description of the error.

The returned expression has types attached to all variable occurrences, so you can call typeOfWitness on any open subterm.

The kinds and types of primitives are added to the environments automatically, you don't need to supply these as part of the starting environments.

typeOfWitness :: (Ord n, Show n, Pretty n) => Config n -> Witness a n -> Either (Error a n) (Type n)Source

Like checkWitness, but check in an empty environment.

As this function is not given an environment, the types of free variables must be attached directly to the bound occurrences. This attachment is performed by checkWitness above.

typeOfWiCon :: WiCon n -> Type nSource

Take the type of a witness constructor.

Annotations

data AnTEC a n Source

The type checker adds this annotation to every node in the AST, giving its type, effect and closure.

Constructors

AnTEC 

Instances

Typeable2 AnTEC 
(Show a, Show n) => Show (AnTEC a n) 
Pretty (AnTEC a n) 
(NFData a, NFData n) => NFData (AnTEC a n) 

Error messages

data Error a n Source

All the things that can go wrong when type checking an expression or witness.

Constructors

ErrorType

Found a kind error when checking a type.

Fields

errorTypeError :: Error n
 
ErrorData

Found an error in the data type definitions.

Fields

errorData :: ErrorData n
 
ErrorExportUndefined

Exported value is undefined.

Fields

errorName :: n
 
ErrorExportDuplicate

Exported name is exported multiple times.

Fields

errorName :: n
 
ErrorExportMismatch

Type signature of exported binding does not match the type at the definition site.

ErrorImportDuplicate

Imported name is imported multiple times.

Fields

errorName :: n
 
ErrorImportValueNotData

An imported value that doesn't have kind Data.

Fields

errorName :: n
 
ErrorMismatch

Generic mismatch between expected and inferred types.

ErrorUndefinedVar

An undefined type variable.

ErrorUndefinedCtor

A data constructor that wasn't in the set of data definitions.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorAppMismatch

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

ErrorAppNotFun

Tried to apply something that is not a function.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorNotFunType :: Type n
 
ErrorAppCannotInferPolymorphic

Cannot infer type of polymorphic expression.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorLamShadow

A type abstraction that tries to shadow a type variable that is already in the environment.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLamNotPure

An abstraction where the body has a visible side effect that is not supported by the current language fragment.

ErrorLamNotEmpty

An abstraction where the body has a visible closure that is not supported by the current language fragment.

ErrorLamBindBadKind

A value function where the parameter does not have data or witness kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLamBodyNotData

An abstraction where the body does not have data kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLamParamUnannotated

A function abstraction without a type annotation on the parameter.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLAMParamUnannotated

A type abstraction without a kind annotation on the parameter.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorLAMParamBadSort

A type abstraction parameter with a bad sort.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorSort :: Sort n
 
ErrorLetMismatch

A let-expression where the type of the binder does not match the right of the binding.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorType :: Type n
 
ErrorLetBindingNotData

A let-expression where the right of the binding does not have data kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorKind :: Kind n
 
ErrorLetBodyNotData

A let-expression where the body does not have data kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLetrecBindingNotLambda

A recursive let-expression where the right of the binding is not a lambda abstraction.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorExp :: Exp a n
 
ErrorLetrecMissingAnnot

A recursive let-binding with a missing type annotation.

Fields

errorAnnot :: a
 
errorBind :: Bind n
 
errorExp :: Exp a n
 
ErrorLetrecRebound

A recursive let-expression that has more than one binding with the same name.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLetRegionsNotRegion

A letregion-expression where the some of the bound variables do not have region kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
errorKinds :: [Kind n]
 
ErrorLetRegionsRebound

A letregion-expression that tried to shadow some pre-existing named region variables.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
ErrorLetRegionFree

A letregion-expression where some of the the bound region variables are free in the type of the body.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
errorType :: Type n
 
ErrorLetRegionWitnessInvalid

A letregion-expression that tried to create a witness with an invalid type.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLetRegionWitnessConflict

A letregion-expression that tried to create conflicting witnesses.

ErrorLetRegionsWitnessOther

A letregion-expression where a bound witnesses was not for the the region variable being introduced.

ErrorWithRegionNotRegion

A withregion-expression where the handle does not have region kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBound :: Bound n
 
errorKind :: Kind n
 
ErrorWithRegionFree

A letregion-expression where some of the the bound region variables are free in the type of the body.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorBound :: Bound n
 
errorType :: Type n
 
ErrorWAppMismatch

A witness application where the argument type does not match the parameter type.

ErrorWAppNotCtor

Tried to perform a witness application with a non-witness.

ErrorCannotJoin

An invalid witness join.

ErrorWitnessNotPurity

A witness provided for a purify cast that does not witness purity.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorWitness :: Witness a n
 
errorType :: Type n
 
ErrorWitnessNotEmpty

A witness provided for a forget cast that does not witness emptiness.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorWitness :: Witness a n
 
errorType :: Type n
 
ErrorCaseScrutineeNotAlgebraic

A case-expression where the scrutinee type is not algebraic.

ErrorCaseScrutineeTypeUndeclared

A case-expression where the scrutinee type is not in our set of data type declarations.

ErrorCaseNoAlternatives

A case-expression with no alternatives.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorCaseNonExhaustive

A case-expression where the alternatives don't cover all the possible data constructors.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorCtorNamesMissing :: [n]
 
ErrorCaseNonExhaustiveLarge

A case-expression where the alternatives don't cover all the possible constructors, and the type has too many data constructors to list.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorCaseOverlapping

A case-expression with overlapping alternatives.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorCaseTooManyBinders

A case-expression where one of the patterns has too many binders.

ErrorCaseCannotInstantiate

A case-expression where the pattern types could not be instantiated with the arguments of the scrutinee type.

ErrorCaseScrutineeTypeMismatch

A case-expression where the type of the scrutinee does not match the type of the pattern.

ErrorCaseFieldTypeMismatch

A case-expression where the annotation on a pattern variable binder does not match the field type of the constructor.

ErrorCaseAltResultMismatch

A case-expression where the result types of the alternatives are not identical.

ErrorWeakEffNotEff

A weakeff-cast where the type provided does not have effect kind.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorEffect :: Effect n
 
errorKind :: Kind n
 
ErrorRunNotSuspension

A run cast applied to a non-suspension.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorType :: Type n
 
ErrorRunNotSupported

A run cast where the context does not support the suspended effect.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
errorEffect :: Effect n
 
ErrorRunCannotInfer

A run cast where we cannot infer the type of the suspended computation and thus cannot check if its effects are suppored by the context.

Fields

errorAnnot :: a
 
errorExp :: Exp a n
 
ErrorNakedType

Found a naked XType that wasn't the argument of an application.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 
ErrorNakedWitness

Found a naked XWitness that wasn't the argument of an application.

Fields

errorAnnot :: a
 
errorChecking :: Exp a n
 

Instances

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