Safe Haskell	None

DDC.Core.Check

Contents

Configuration
Type checker trace
Checking Modules
Checking Expressions
Checking Witnesses
Annotations
Error messages

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

Pretty CheckTrace
Monoid CheckTrace

Checking Modules

checkModule Source

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)

checkExp Source

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.

typeOfExp Source

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

checkWitness Source

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
Fields annotType :: Type n annotEffect :: Effect n annotClosure :: Closure n annotTail :: a

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.
Fields errorName :: n errorExportType :: Type n errorDefType :: Type n
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.
Fields errorAnnot :: a errorInferred :: Type n errorExpected :: Type n errorChecking :: Exp a n
ErrorUndefinedVar	An undefined type variable.
Fields errorAnnot :: a errorBound :: Bound n errorUniverse :: Universe
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.
Fields errrorAnnot :: a errorChecking :: Exp a n errorParamType :: Type n errorArgType :: Type n
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.
Fields errorAnnot :: a errorChecking :: Exp a n errorUniverse :: Universe errorEffect :: Effect n
ErrorLamNotEmpty	An abstraction where the body has a visible closure that is not supported by the current language fragment.
Fields errorAnnot :: a errorChecking :: Exp a n errorUniverse :: Universe errorClosure :: Closure n
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.
Fields errorAnnot :: a errorChecking :: Exp a n errorBindWitness1 :: Bind n errorBindWitness2 :: Bind n
ErrorLetRegionsWitnessOther	A letregion-expression where a bound witnesses was not for the the region variable being introduced.
Fields errorAnnot :: a errorChecking :: Exp a n errorBoundRegions :: [Bound n] errorBindWitness :: Bind n
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.
Fields errorAnnot :: a errorWitness :: Witness a n errorParamType :: Type n errorArgType :: Type n
ErrorWAppNotCtor	Tried to perform a witness application with a non-witness.
Fields errorAnnot :: a errorWitness :: Witness a n errorNotFunType :: Type n errorArgType :: Type n
ErrorCannotJoin	An invalid witness join.
Fields errorAnnot :: a errorWitness :: Witness a n errorWitnessLeft :: Witness a n errorTypeLeft :: Type n errorWitnessRight :: Witness a n errorTypeRight :: Type n
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.
Fields errorAnnot :: a errorChecking :: Exp a n errorTypeScrutinee :: Type n
ErrorCaseScrutineeTypeUndeclared	A case-expression where the scrutinee type is not in our set of data type declarations.
Fields errorAnnot :: a errorChecking :: Exp a n errorTypeScrutinee :: Type n
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.
Fields errorAnnot :: a errorChecking :: Exp a n errorCtorDaCon :: DaCon n errorCtorFields :: Int errorPatternFields :: Int
ErrorCaseCannotInstantiate	A case-expression where the pattern types could not be instantiated with the arguments of the scrutinee type.
Fields errorAnnot :: a errorChecking :: Exp a n errorTypeScrutinee :: Type n errorTypeCtor :: Type n
ErrorCaseScrutineeTypeMismatch	A case-expression where the type of the scrutinee does not match the type of the pattern.
Fields errorAnnot :: a errorChecking :: Exp a n errorTypeScrutinee :: Type n errorTypePattern :: Type n
ErrorCaseFieldTypeMismatch	A case-expression where the annotation on a pattern variable binder does not match the field type of the constructor.
Fields errorAnnot :: a errorChecking :: Exp a n errorTypeAnnot :: Type n errorTypeField :: Type n
ErrorCaseAltResultMismatch	A case-expression where the result types of the alternatives are not identical.
Fields errorAnnot :: a errorChecking :: Exp a n errorAltType1 :: Type n errorAltType2 :: Type n
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)