module DDC.Type.Check.Error
( Error (..)
, ErrorData (..))
where
import DDC.Type.Universe
import DDC.Type.Exp
data Error n
= ErrorUniverseMalfunction
{ errorType :: Type n
, errorUniverse :: Universe }
| ErrorMismatch
{ errorUniverse :: Universe
, errorInferred :: Type n
, errorExpected :: Type n
, errorChecking :: Type n }
| ErrorInfinite
{ errorTypeVar :: Type n
, errorTypeBind :: Type n }
| ErrorUndefined
{ errorBound :: Bound n }
| ErrorUnappliedKindFun
| ErrorNakedSort
{ errorSort :: Sort n }
| ErrorUndefinedTypeCtor
{ errorBound :: Bound n }
| ErrorAppNotFun
{ errorChecking :: Type n
, errorFunType :: Type n
, errorFunTypeKind :: Kind n
, errorArgType :: Type n }
| ErrorAppArgMismatch
{ errorChecking :: Type n
, errorFunType :: Type n
, errorFunKind :: Kind n
, errorArgType :: Type n
, errorArgKind :: Kind n }
| ErrorWitnessImplInvalid
{ errorChecking :: Type n
, errorLeftType :: Type n
, errorLeftKind :: Kind n
, errorRightType :: Type n
, errorRightKind :: Kind n }
| ErrorForallKindInvalid
{ errorChecking :: Type n
, errorBody :: Type n
, errorKind :: Kind n }
| ErrorSumKindMismatch
{ errorKindExpected :: Kind n
, errorTypeSum :: TypeSum n
, errorKinds :: [Kind n] }
| ErrorSumKindInvalid
{ errorCheckingSum :: TypeSum n
, errorKind :: Kind n }
deriving Show
data ErrorData n
= ErrorDataDupTypeName
{ errorDataDupTypeName :: n }
| ErrorDataDupCtorName
{ errorDataCtorName :: n }
| ErrorDataWrongResult
{ errorDataCtorName :: n
, errorDataCtorResultActual :: Type n
, errorDataCtorResultExpected :: Type n }
deriving Show