Safe Haskell	Safe-Infered

DDC.Core.Check

Contents

Checking Expressions
Checking Witnesses
Error messages

Description

Type checker for the Disciple core language.

Synopsis

Checking Expressions

checkExp Source

Arguments

:: (Ord n, Pretty n)
=> DataDefs n	Data type definitions.
-> Env n	Kind environment.
-> Env n	Type environment.
-> Exp a n	Expression to check.
-> Either (Error a n) (Exp a n, Type n, Effect n, Closure n)

Type check an expression.

If it's good, you get a new version with types attached to all the bound variables, as well its the type, effect and closure.

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 typeOfExp on any open subterm.

typeOfExp :: (Ord n, Pretty n) => DataDefs n -> Exp a n -> Either (Error a n) (Type n)Source

Like checkExp, but check in an empty environment, and only return the value type of an expression.

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 checkExp above.

Checking Witnesses

checkWitness Source

Arguments

:: (Ord n, Pretty n)
=> DataDefs n	Data type definitions.
-> Env n	Kind Environment.
-> Env n	Type Environment.
-> Witness n	Witness to check.
-> Either (Error a 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.

typeOfWitness :: (Ord n, Pretty n) => DataDefs n -> Witness 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.

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
ErrorMalformedExp	Found a malformed expression, and we don't have a more specific diagnosis.
Fields errorChecking :: Exp a n
ErrorMalformedType	Found a malformed type, and we don't have a more specific diagnosis.
Fields errorChecking :: Exp a n errorType :: Type n
ErrorNakedType	Found a naked `XType` that wasn't the argument of an application.
Fields errorChecking :: Exp a n
ErrorNakedWitness	Found a naked `XWitness` that wasn't the argument of an application.
Fields errorChecking :: Exp a n
ErrorVarAnnotMismatch	A bound occurrence of a variable who's type annotation does not match the corresponding annotation in the environment.
Fields errorBound :: Bound n errorTypeEnv :: Type n
ErrorUndefinedCtor	A data constructor that wasn't in the set of data definitions.
Fields errorChecking :: Exp a n
ErrorAppMismatch	A function application where the parameter and argument don't match.
Fields errorChecking :: Exp a n errorParamType :: Type n errorArgType :: Type n
ErrorAppNotFun	Tried to apply something that is not a function.
Fields errorChecking :: Exp a n errorNotFunType :: Type n errorArgType :: Type n
ErrorLamShadow	A type abstraction that tries to shadow a type variable that is already in the environment.
Fields errorChecking :: Exp a n errorBind :: Bind n
ErrorLamNotPure	A type or witness abstraction where the body has a visible side effect.
Fields errorChecking :: Exp a n errorEffect :: Effect n
ErrorLamBindNotData	A value function where the parameter does not have data kind.
Fields errorChecking :: Exp a n errorType :: Type n errorKind :: Kind n
ErrorLamBodyNotData	An abstraction where the body does not have data kind.
Fields errorChecking :: Exp a n errorBind :: Bind n errorType :: Type n errorKind :: Kind n
ErrorLetMismatch	A let-expression where the type of the binder does not match the right of the binding.
Fields 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 errorChecking :: Exp a n errorBind :: Bind n errorKind :: Kind n
ErrorLetBodyNotData	A let-expression where the body does not have data kind.
Fields errorChecking :: Exp a n errorType :: Type n errorKind :: Kind n
ErrorLetLazyNotPure	A lazy let binding that has a visible side effect.
Fields errorChecking :: Exp a n errorBind :: Bind n errorEffect :: Effect n
ErrorLetLazyNotEmpty	A lazy let binding with a non-empty closure.
Fields errorChecking :: Exp a n errorBind :: Bind n errorClosure :: Closure n
ErrorLetLazyNoWitness	A lazy let binding without a witness that binding is in a lazy region.
Fields errorChecking :: Exp a n errorBind :: Bind n errorType :: Type n
ErrorLetLazyWitnessTypeMismatch	A lazy let binding where the witness has the wrong type.
Fields errorChecking :: Exp a n errorBind :: Bind n errorWitnessTypeHave :: Type n errorBindType :: Type n errorWitnessTypeExpect :: Type n
ErrorLetrecBindingNotLambda	A recursive let-expression where the right of the binding is not a lambda abstraction.
Fields errorChecking :: Exp a n errorExp :: Exp a n
ErrorLetRegionNotRegion	A letregion-expression where the bound variable does not have region kind.
Fields errorChecking :: Exp a n errorBind :: Bind n errorKind :: Kind n
ErrorLetRegionRebound	A letregion-expression that tried to shadow a pre-existing named region variable.
Fields errorChecking :: Exp a n errorBind :: Bind n
ErrorLetRegionFree	A letregion-expression where the bound region variable is free in the type of the body.
Fields errorChecking :: Exp a n errorBind :: Bind n errorType :: Type n
ErrorLetRegionWitnessInvalid	A letregion-expression that tried to create a witness with an invalid type.
Fields errorChecking :: Exp a n errorBind :: Bind n
ErrorLetRegionWitnessConflict	A letregion-expression that tried to create conflicting witnesses.
Fields errorChecking :: Exp a n errorBindWitness1 :: Bind n errorBindWitness2 :: Bind n
ErrorLetRegionWitnessOther	A letregion-expression where a bound witnesses was not for the the region variable being introduced.
Fields errorChecking :: Exp a n errorBoundRegion :: Bound n errorBindWitness :: Bind n
ErrorWithRegionNotRegion	A withregion-expression where the handle does not have region kind.
Fields errorChecking :: Exp a n errorBound :: Bound n errorKind :: Kind n
ErrorWAppMismatch	A witness application where the argument type does not match the parameter type.
Fields errorWitness :: Witness n errorParamType :: Type n errorArgType :: Type n
ErrorWAppNotCtor	Tried to perform a witness application with a non-witness.
Fields errorWitness :: Witness n errorNotFunType :: Type n errorArgType :: Type n
ErrorCannotJoin	An invalid witness join.
Fields errorWitness :: Witness n errorWitnessLeft :: Witness n errorTypeLeft :: Type n errorWitnessRight :: Witness n errorTypeRight :: Type n
ErrorWitnessNotPurity	A witness provided for a purify cast that does not witness purity.
Fields errorChecking :: Exp a n errorWitness :: Witness n errorType :: Type n
ErrorWitnessNotEmpty	A witness provided for a forget cast that does not witness emptiness.
Fields errorChecking :: Exp a n errorWitness :: Witness n errorType :: Type n
ErrorCaseDiscrimNotAlgebraic	A case-expression where the discriminant type is not algebraic.
Fields errorChecking :: Exp a n errorTypeDiscrim :: Type n
ErrorCaseDiscrimTypeUndeclared	A case-expression where the discriminant type is not in our set of data type declarations.
Fields errorChecking :: Exp a n errorTypeDiscrim :: Type n
ErrorCaseNoAlternatives	A case-expression with no alternatives.
Fields errorChecking :: Exp a n
ErrorCaseNonExhaustive	A case-expression where the alternatives don't cover all the possible data constructors.
Fields 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 errorChecking :: Exp a n
ErrorCaseOverlapping	A case-expression with overlapping alternatives.
Fields errorChecking :: Exp a n
ErrorCaseTooManyBinders	A case-expression where one of the patterns has too many binders.
Fields errorChecking :: Exp a n errorCtorBound :: Bound n errorCtorFields :: Int errorPatternFields :: Int
ErrorCaseCannotInstantiate	A case-expression where the pattern types could not be instantiated with the arguments of the discriminant type.
Fields errorChecking :: Exp a n errorTypeCtor :: Type n errorTypeDiscrim :: Type n
ErrorCaseDiscrimTypeMismatch	A case-expression where the type of the discriminant does not match the type of the pattern.
Fields errorChecking :: Exp a n errorTypeDiscrim :: 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 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 errorChecking :: Exp a n errorAltType1 :: Type n errorAltType2 :: Type n
ErrorMaxeffNotEff	A maxeff-cast where the type provided does not have effect kind.
Fields errorChecking :: Exp a n errorEffect :: Effect n errorKind :: Kind n
ErrorMaxcloNotClo	A maxclo-cast where the type provided does not have closure kind.
Fields errorChecking :: Exp a n errorClosure :: Closure n errorKind :: Kind n
ErrorMaxcloMalformed	A maxclo-case where the closure provided is malformed. It can only contain `Use` terms.
Fields errorChecking :: Exp a n errorClosure :: Closure n

Instances

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