module DDC.Core.Check.Error
(Error(..))
where
import DDC.Core.Exp
import qualified DDC.Type.Check as T
data Error a n
= ErrorType
{ errorTypeError :: T.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 }
| ErrorUndefinedCtor
{ errorChecking :: Exp a 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
{ errorChecking :: Exp a n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLamBodyNotData
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLetMismatch
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n }
| ErrorLetBindingNotData
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorKind :: Kind n }
| ErrorLetBodyNotData
{ errorChecking :: Exp a n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLetLazyNotPure
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorEffect :: Effect n }
| ErrorLetLazyNotEmpty
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorClosure :: Closure n }
| ErrorLetLazyNoWitness
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n }
| 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
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorKind :: Kind n }
| ErrorLetRegionRebound
{ errorChecking :: Exp a n
, errorBind :: Bind n }
| ErrorLetRegionFree
{ errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n }
| 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 }
deriving (Show)