DDC.Core.Check

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.

Configuration

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.

Type checker trace

data CheckTrace

Human readable trace of the type checker.

Constructors

CheckTrace

Fields

checkTraceDoc :: Doc

Instances

Monoid CheckTrace

Pretty CheckTrace

Checking Modules

checkModule

Arguments

:: (Show a, 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

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)

data Demand

Demand placed on suspensions by the surrounding context.

Constructors

DemandRun

Run suspensions as we encounter them.

DemandNone

Ignore suspensions, don't run them.

Instances

Show Demand

checkExp

Arguments

:: (Show a, Ord n, Show n, Pretty n)

=> Config n

Static configuration.

-> KindEnv n

Starting kind environment.

-> TypeEnv n

Starting type environment.

-> Mode n

Check mode.

-> Demand

Demand placed on the expression.

-> Exp a n

Expression to check.

-> (Either (Error a n) (Exp (AnTEC a n) n, Type n, Effect 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

Arguments

:: (Show a, 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

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)

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 n

Take the type of a witness constructor.

Annotations

data AnTEC a n

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

(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

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

ErrorImportCapNotEffect

An imported capability that does not have kind Effect.

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

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

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

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

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)