Safe Haskell | Safe-Infered |
---|
Type checker for the Disciple core language.
- checkExp :: (Ord n, Pretty n) => DataDefs n -> Env n -> Env n -> Exp a n -> Either (Error a n) (Exp a n, Type n, Effect n, Closure n)
- typeOfExp :: (Ord n, Pretty n) => DataDefs n -> Exp a n -> Either (Error a n) (Type n)
- checkWitness :: (Ord n, Pretty n) => Env n -> Env n -> Witness n -> Either (Error a n) (Type n)
- typeOfWitness :: (Ord n, Pretty n) => Witness n -> Either (Error a n) (Type n)
- typeOfWiCon :: WiCon n -> Type n
- data Error a n
- = ErrorType {
- errorTypeError :: Error n
- | ErrorMalformedExp {
- errorChecking :: Exp a n
- | ErrorMalformedType {
- errorChecking :: Exp a n
- errorType :: Type n
- | ErrorNakedType {
- errorChecking :: Exp a n
- | ErrorNakedWitness {
- errorChecking :: Exp a n
- | ErrorVarAnnotMismatch {
- errorBound :: Bound n
- errorTypeEnv :: Type n
- | ErrorAppMismatch {
- errorChecking :: Exp a n
- errorParamType :: Type n
- errorArgType :: Type n
- | ErrorAppNotFun {
- errorChecking :: Exp a n
- errorNotFunType :: Type n
- errorArgType :: Type n
- | ErrorLamShadow {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLamNotPure {
- errorChecking :: Exp a n
- errorEffect :: Effect n
- | ErrorLamBindNotData { }
- | ErrorLamBodyNotData { }
- | ErrorLetMismatch { }
- | ErrorLetBindingNotData { }
- | ErrorLetBodyNotData { }
- | ErrorLetLazyNotPure {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorEffect :: Effect n
- | ErrorLetLazyNotEmpty {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorClosure :: Closure n
- | ErrorLetLazyNoWitness { }
- | ErrorLetLazyWitnessTypeMismatch {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorWitnessTypeHave :: Type n
- errorBindType :: Type n
- errorWitnessTypeExpect :: Type n
- | ErrorLetrecBindingNotLambda {
- errorChecking :: Exp a n
- errorExp :: Exp a n
- | ErrorLetRegionNotRegion { }
- | ErrorLetRegionRebound {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLetRegionFree { }
- | ErrorLetRegionWitnessInvalid {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLetRegionWitnessConflict {
- errorChecking :: Exp a n
- errorBindWitness1 :: Bind n
- errorBindWitness2 :: Bind n
- | ErrorLetRegionWitnessOther {
- errorChecking :: Exp a n
- errorBoundRegion :: Bound n
- errorBindWitness :: Bind n
- | ErrorWithRegionNotRegion {
- errorChecking :: Exp a n
- errorBound :: Bound n
- errorKind :: Kind n
- | ErrorWAppMismatch {
- errorWitness :: Witness n
- errorParamType :: Type n
- errorArgType :: Type n
- | ErrorWAppNotCtor {
- errorWitness :: Witness n
- errorNotFunType :: Type n
- errorArgType :: Type n
- | ErrorCannotJoin {
- errorWitness :: Witness n
- errorWitnessLeft :: Witness n
- errorTypeLeft :: Type n
- errorWitnessRight :: Witness n
- errorTypeRight :: Type n
- | ErrorWitnessNotPurity {
- errorChecking :: Exp a n
- errorWitness :: Witness n
- errorType :: Type n
- | ErrorWitnessNotEmpty {
- errorChecking :: Exp a n
- errorWitness :: Witness n
- errorType :: Type n
- | ErrorCaseDiscrimNotAlgebraic {
- errorChecking :: Exp a n
- errorTypeDiscrim :: Type n
- | ErrorCaseDiscrimTypeUndeclared {
- errorChecking :: Exp a n
- errorTypeDiscrim :: Type n
- | ErrorCaseNoAlternatives {
- errorChecking :: Exp a n
- | ErrorCaseNonExhaustive {
- errorChecking :: Exp a n
- errorCtorNamesMissing :: [n]
- | ErrorCaseNonExhaustiveLarge {
- errorChecking :: Exp a n
- | ErrorCaseOverlapping {
- errorChecking :: Exp a n
- | ErrorCaseTooManyBinders {
- errorChecking :: Exp a n
- errorCtorBound :: Bound n
- errorCtorFields :: Int
- errorPatternFields :: Int
- | ErrorCaseCannotInstantiate {
- errorChecking :: Exp a n
- errorTypeCtor :: Type n
- errorTypeDiscrim :: Type n
- | ErrorCaseDiscrimTypeMismatch {
- errorChecking :: Exp a n
- errorTypeDiscrim :: Type n
- errorTypePattern :: Type n
- | ErrorCaseFieldTypeMismatch {
- errorChecking :: Exp a n
- errorTypeAnnot :: Type n
- errorTypeField :: Type n
- | ErrorCaseAltResultMismatch {
- errorChecking :: Exp a n
- errorAltType1 :: Type n
- errorAltType2 :: Type n
- | ErrorMaxeffNotEff {
- errorChecking :: Exp a n
- errorEffect :: Effect n
- errorKind :: Kind n
- | ErrorMaxcloNotClo {
- errorChecking :: Exp a n
- errorClosure :: Closure n
- errorKind :: Kind n
- | ErrorMaxcloMalformed {
- errorChecking :: Exp a n
- errorClosure :: Closure n
- = ErrorType {
Checking Expressions
:: (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.
Checking Witnesses
:: (Ord n, Pretty n) | |
=> 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) => 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
All the things that can go wrong when type checking an expression or witness.
ErrorType | Found a kind error when checking a type. |
| |
ErrorMalformedExp | Found a malformed expression, and we don't have a more specific diagnosis. |
| |
ErrorMalformedType | Found a malformed type, and we don't have a more specific diagnosis. |
| |
ErrorNakedType | Found a naked |
| |
ErrorNakedWitness | Found a naked |
| |
ErrorVarAnnotMismatch | A bound occurrence of a variable who's type annotation does not match the corresponding annotation in the environment. |
| |
ErrorAppMismatch | A function application where the parameter and argument don't match. |
| |
ErrorAppNotFun | Tried to apply something that is not a function. |
| |
ErrorLamShadow | A type abstraction that tries to shadow a type variable that is already in the environment. |
| |
ErrorLamNotPure | A type or witness abstraction where the body has a visible side effect. |
| |
ErrorLamBindNotData | A value function where the parameter does not have data kind. |
ErrorLamBodyNotData | An abstraction where the body does not have data kind. |
ErrorLetMismatch | A let-expression where the type of the binder does not match the right of the binding. |
ErrorLetBindingNotData | A let-expression where the right of the binding does not have data kind. |
ErrorLetBodyNotData | A let-expression where the body does not have data kind. |
ErrorLetLazyNotPure | A lazy let binding that has a visible side effect. |
| |
ErrorLetLazyNotEmpty | A lazy let binding with a non-empty closure. |
| |
ErrorLetLazyNoWitness | A lazy let binding without a witness that binding is in a lazy region. |
ErrorLetLazyWitnessTypeMismatch | A lazy let binding where the witness has the wrong type. |
| |
ErrorLetrecBindingNotLambda | A recursive let-expression where the right of the binding is not a lambda abstraction. |
| |
ErrorLetRegionNotRegion | A letregion-expression where the bound variable does not have region kind. |
ErrorLetRegionRebound | A letregion-expression that tried to shadow a pre-existing named region variable. |
| |
ErrorLetRegionFree | A letregion-expression where the bound region variable is free in the type of the body. |
ErrorLetRegionWitnessInvalid | A letregion-expression that tried to create a witness with an invalid type. |
| |
ErrorLetRegionWitnessConflict | A letregion-expression that tried to create conflicting witnesses. |
| |
ErrorLetRegionWitnessOther | 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. |
| |
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. |
| |
ErrorWitnessNotEmpty | A witness provided for a forget cast that does not witness emptiness. |
| |
ErrorCaseDiscrimNotAlgebraic | A case-expression where the discriminant type is not algebraic. |
| |
ErrorCaseDiscrimTypeUndeclared | A case-expression where the discriminant type is not in our set of data type declarations. |
| |
ErrorCaseNoAlternatives | A case-expression with no alternatives. |
| |
ErrorCaseNonExhaustive | A case-expression where the alternatives don't cover all the possible data constructors. |
| |
ErrorCaseNonExhaustiveLarge | A case-expression where the alternatives don't cover all the possible constructors, and the type has too many data constructors to list. |
| |
ErrorCaseOverlapping | A case-expression with overlapping alternatives. |
| |
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 discriminant type. |
| |
ErrorCaseDiscrimTypeMismatch | A case-expression where the type of the discriminant 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. |
| |
ErrorMaxeffNotEff | A maxeff-cast where the type provided does not have effect kind. |
| |
ErrorMaxcloNotClo | A maxclo-cast where the type provided does not have closure kind. |
| |
ErrorMaxcloMalformed | A maxclo-case where the closure provided is malformed.
It can only contain |
|