module DDC.Core.Check.Error
(Error(..))
where
import DDC.Core.Exp
import DDC.Type.Universe
import qualified DDC.Type.Check as T
data Error a n
= ErrorType
{ errorTypeError :: T.Error n }
| ErrorData
{ errorData :: T.ErrorData n }
| ErrorExportUndefined
{ errorName :: n }
| ErrorExportDuplicate
{ errorName :: n }
| ErrorExportMismatch
{ errorName :: n
, errorExportType :: Type n
, errorDefType :: Type n }
| ErrorImportDuplicate
{ errorName :: n }
| ErrorImportValueNotData
{ errorName :: n }
| ErrorMismatch
{ errorAnnot :: a
, errorInferred :: Type n
, errorExpected :: Type n
, errorChecking :: Exp a n }
| ErrorUndefinedVar
{ errorAnnot :: a
, errorBound :: Bound n
, errorUniverse :: Universe }
| ErrorUndefinedCtor
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorAppMismatch
{ errrorAnnot :: a
, errorChecking :: Exp a n
, errorParamType :: Type n
, errorArgType :: Type n }
| ErrorAppNotFun
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorNotFunType :: Type n }
| ErrorAppCannotInferPolymorphic
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorLamShadow
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n }
| ErrorLamNotPure
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorUniverse :: Universe
, errorEffect :: Effect n }
| ErrorLamNotEmpty
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorUniverse :: Universe
, errorClosure :: Closure n }
| ErrorLamBindBadKind
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLamBodyNotData
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLamParamUnannotated
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n }
| ErrorLAMParamUnannotated
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorLAMParamBadSort
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n
, errorSort :: Sort n }
| ErrorLetMismatch
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n
, errorType :: Type n }
| ErrorLetBindingNotData
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n
, errorKind :: Kind n }
| ErrorLetBodyNotData
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorType :: Type n
, errorKind :: Kind n }
| ErrorLetrecBindingNotLambda
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorExp :: Exp a n }
| ErrorLetrecMissingAnnot
{ errorAnnot :: a
, errorBind :: Bind n
, errorExp :: Exp a n }
| ErrorLetrecRebound
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n }
| ErrorLetRegionsNotRegion
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBinds :: [Bind n]
, errorKinds :: [Kind n] }
| ErrorLetRegionsRebound
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBinds :: [Bind n] }
| ErrorLetRegionFree
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBinds :: [Bind n]
, errorType :: Type n }
| ErrorLetRegionWitnessInvalid
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBind :: Bind n }
| ErrorLetRegionWitnessConflict
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBindWitness1 :: Bind n
, errorBindWitness2 :: Bind n }
| ErrorLetRegionsWitnessOther
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBoundRegions :: [Bound n]
, errorBindWitness :: Bind n }
| ErrorWithRegionNotRegion
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBound :: Bound n
, errorKind :: Kind n }
| ErrorWithRegionFree
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorBound :: Bound n
, errorType :: Type n }
| ErrorWAppMismatch
{ errorAnnot :: a
, errorWitness :: Witness a n
, errorParamType :: Type n
, errorArgType :: Type n }
| ErrorWAppNotCtor
{ errorAnnot :: a
, errorWitness :: Witness a n
, errorNotFunType :: Type n
, errorArgType :: Type n }
| ErrorCannotJoin
{ errorAnnot :: a
, errorWitness :: Witness a n
, errorWitnessLeft :: Witness a n
, errorTypeLeft :: Type n
, errorWitnessRight :: Witness a n
, errorTypeRight :: Type n }
| ErrorWitnessNotPurity
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorWitness :: Witness a n
, errorType :: Type n }
| ErrorWitnessNotEmpty
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorWitness :: Witness a n
, errorType :: Type n }
| ErrorCaseScrutineeNotAlgebraic
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorTypeScrutinee :: Type n }
| ErrorCaseScrutineeTypeUndeclared
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorTypeScrutinee :: Type n }
| ErrorCaseNoAlternatives
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorCaseNonExhaustive
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorCtorNamesMissing :: [n] }
| ErrorCaseNonExhaustiveLarge
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorCaseOverlapping
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorCaseTooManyBinders
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorCtorDaCon :: DaCon n
, errorCtorFields :: Int
, errorPatternFields :: Int }
| ErrorCaseCannotInstantiate
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorTypeScrutinee :: Type n
, errorTypeCtor :: Type n }
| ErrorCaseScrutineeTypeMismatch
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorTypeScrutinee :: Type n
, errorTypePattern :: Type n }
| ErrorCaseFieldTypeMismatch
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorTypeAnnot :: Type n
, errorTypeField :: Type n }
| ErrorCaseAltResultMismatch
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorAltType1 :: Type n
, errorAltType2 :: Type n }
| ErrorWeakEffNotEff
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorEffect :: Effect n
, errorKind :: Kind n }
| ErrorRunNotSuspension
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorType :: Type n }
| ErrorRunNotSupported
{ errorAnnot :: a
, errorChecking :: Exp a n
, errorEffect :: Effect n }
| ErrorRunCannotInfer
{ errorAnnot :: a
, errorExp :: Exp a n }
| ErrorNakedType
{ errorAnnot :: a
, errorChecking :: Exp a n }
| ErrorNakedWitness
{ errorAnnot :: a
, errorChecking :: Exp a n }
deriving (Show)