module DDC.Type.Check.Error
(Error(..))
where
import DDC.Type.Exp
data Error n
= ErrorUndefined
{ errorBound :: Bound n }
| ErrorUndefinedCtor
{ errorBound :: Bound n }
| ErrorVarAnnotMismatch
{ errorBound :: Bound n
, errorTypeEnv :: Type n }
| ErrorNakedSort
{ errorSort :: Sort n }
| ErrorUnappliedKindFun
| ErrorAppArgMismatch
{ errorChecking :: Type n
, errorParamKind :: Kind n
, errorArgKind :: Kind n }
| ErrorAppNotFun
{ errorChecking :: Type n
, errorFunType :: Type n
, errorFunTypeKind :: Kind n
, errorArgType :: Type n
, errorArgTypeKind :: Kind n }
| ErrorSumKindMismatch
{ errorKindExpected :: Kind n
, errorTypeSum :: TypeSum n
, errorKinds :: [Kind n] }
| ErrorSumKindInvalid
{ errorCheckingSum :: TypeSum n
, errorKind :: Kind n }
| ErrorForallKindInvalid
{ errorChecking :: Type n
, errorBody :: Type n
, errorKind :: Kind n }
| ErrorWitnessImplInvalid
{ errorChecking :: Type n
, errorLeftType :: Type n
, errorLeftKind :: Kind n
, errorRightType :: Type n
, errorRightKind :: Kind n }
deriving Show