Safe Haskell	Safe-Infered

DDC.Core.Check.Error

Description

Errors produced when checking core expressions.

Synopsis

Documentation

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)