Copyright | (C) 2018 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Defines a drop-in replacement for TypeError
(from GHC.TypeLits)
that can be used at the value level as well. Since this is a drop-in
replacement, it is not recommended to import all of GHC.TypeLits
and Data.Singletons.TypeError at the same time, as many of the definitons
in the latter deliberately clash with the former.
Synopsis
- type family TypeError (a :: PErrorMessage) :: b where ...
- sTypeError :: HasCallStack => Sing err -> Sing (TypeError err)
- typeError :: HasCallStack => ErrorMessage -> a
- data ErrorMessage' s
- = Text s
- | ShowType t
- | (ErrorMessage' s) :<>: (ErrorMessage' s)
- | (ErrorMessage' s) :$$: (ErrorMessage' s)
- type ErrorMessage = ErrorMessage' Text
- type PErrorMessage = ErrorMessage' Symbol
- data family Sing :: k -> Type
- type SErrorMessage = (Sing :: PErrorMessage -> Type)
- type family ConvertPErrorMessage (a :: PErrorMessage) :: ErrorMessage where ...
- showErrorMessage :: ErrorMessage -> String
- data TextSym0 :: forall (s6989586621681262316 :: Type). (~>) s6989586621681262316 (ErrorMessage' (s6989586621681262316 :: Type))
- type TextSym1 (t6989586621681263102 :: s6989586621681262316) = Text t6989586621681263102
- data ShowTypeSym0 :: forall (s6989586621681262316 :: Type) t6989586621681262317. (~>) t6989586621681262317 (ErrorMessage' (s6989586621681262316 :: Type))
- type ShowTypeSym1 (t6989586621681263104 :: t6989586621681262317) = ShowType t6989586621681263104
- data (:<>:@#@$) :: forall (s6989586621681262316 :: Type). (~>) (ErrorMessage' s6989586621681262316) ((~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type)))
- data (:<>:@#@$$) (t6989586621681263106 :: ErrorMessage' (s6989586621681262316 :: Type)) :: (~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type))
- type (:<>:@#@$$$) (t6989586621681263106 :: ErrorMessage' s6989586621681262316) (t6989586621681263107 :: ErrorMessage' s6989586621681262316) = (:<>:) t6989586621681263106 t6989586621681263107
- data (:$$:@#@$) :: forall (s6989586621681262316 :: Type). (~>) (ErrorMessage' s6989586621681262316) ((~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type)))
- data (:$$:@#@$$) (t6989586621681263110 :: ErrorMessage' (s6989586621681262316 :: Type)) :: (~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type))
- type (:$$:@#@$$$) (t6989586621681263110 :: ErrorMessage' s6989586621681262316) (t6989586621681263111 :: ErrorMessage' s6989586621681262316) = (:$$:) t6989586621681263110 t6989586621681263111
- data TypeErrorSym0 :: forall b6989586621681262306. (~>) PErrorMessage b6989586621681262306
- type TypeErrorSym1 (a6989586621681262307 :: PErrorMessage) = TypeError a6989586621681262307
Documentation
type family TypeError (a :: PErrorMessage) :: b where ... Source #
TypeError a = TypeError (ConvertPErrorMessage a) |
sTypeError :: HasCallStack => Sing err -> Sing (TypeError err) Source #
typeError :: HasCallStack => ErrorMessage -> a Source #
data ErrorMessage' s Source #
A description of a custom type error.
This is a variation on ErrorMessage
that is parameterized over what
text type is used in the Text
constructor. Instantiating it with
Text
gives you ErrorMessage
, and instantiating it with Symbol
gives you PErrorMessage
.
Text s | Show the text as is. |
ShowType t | Pretty print the type.
|
(ErrorMessage' s) :<>: (ErrorMessage' s) infixl 6 | Put two pieces of error message next to each other. |
(ErrorMessage' s) :$$: (ErrorMessage' s) infixl 5 | Stack two pieces of error message on top of each other. |
Instances
type ErrorMessage = ErrorMessage' Text Source #
A value-level ErrorMessage'
which uses Text
as its text type.
type PErrorMessage = ErrorMessage' Symbol Source #
A type-level ErrorMessage'
which uses Symbol
as its text kind.
data family Sing :: k -> Type infixl 6 :%<>:infixl 5 :%$$: Source #
The singleton kind-indexed data family.
Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
SDecide k => TestEquality (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
Show (SSymbol s) Source # | |
Show (SNat n) Source # | |
Eq (Sing a) Source # | |
Ord (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
Show (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # | |
Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing m => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
data Sing (a :: Bool) Source # | |
data Sing (a :: Ordering) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Void) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) Source # | |
data Sing (a :: Any) Source # | |
data Sing (a :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
data Sing (b :: [a]) Source # | |
data Sing (b :: Maybe a) Source # | |
data Sing (a :: TYPE rep) Source # | A choice of singleton for the kind Conceivably, one could generalize this instance to `Sing :: k -> Type` for
any kind We cannot produce explicit singleton values for everything in |
Defined in Data.Singletons.TypeRepTYPE | |
data Sing (b :: Min a) Source # | |
data Sing (b :: Max a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (a :: WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) Source # | |
data Sing (b :: Identity a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (b :: Dual a) Source # | |
data Sing (b :: Sum a) Source # | |
data Sing (b :: Product a) Source # | |
data Sing (b :: Down a) Source # | |
data Sing (b :: NonEmpty a) Source # | |
data Sing (c :: Either a b) Source # | |
data Sing (c :: (a, b)) Source # | |
data Sing (c :: Arg a b) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (d :: (a, b, c)) Source # | |
data Sing (c :: Const a b) Source # | |
data Sing (e :: (a, b, c, d)) Source # | |
data Sing (f :: (a, b, c, d, e)) Source # | |
data Sing (g :: (a, b, c, d, e, f)) Source # | |
data Sing (h :: (a, b, c, d, e, f, g)) Source # | |
Defined in Data.Singletons.Prelude.Instances |
type SErrorMessage = (Sing :: PErrorMessage -> Type) Source #
type family ConvertPErrorMessage (a :: PErrorMessage) :: ErrorMessage where ... Source #
Convert a PErrorMessage
to a ErrorMessage
from GHC.TypeLits.
ConvertPErrorMessage (Text t) = Text t | |
ConvertPErrorMessage (ShowType ty) = ShowType ty | |
ConvertPErrorMessage (e1 :<>: e2) = ConvertPErrorMessage e1 :<>: ConvertPErrorMessage e2 | |
ConvertPErrorMessage (e1 :$$: e2) = ConvertPErrorMessage e1 :$$: ConvertPErrorMessage e2 |
showErrorMessage :: ErrorMessage -> String Source #
Convert an ErrorMessage
into a human-readable String
.
Defunctionalization symbols
data TextSym0 :: forall (s6989586621681262316 :: Type). (~>) s6989586621681262316 (ErrorMessage' (s6989586621681262316 :: Type)) Source #
Instances
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source # | |
SuppressUnusedWarnings (TextSym0 :: TyFun s6989586621681262316 (ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply (TextSym0 :: TyFun s (ErrorMessage' s) -> Type) (t6989586621681263102 :: s) Source # | |
Defined in Data.Singletons.TypeError |
data ShowTypeSym0 :: forall (s6989586621681262316 :: Type) t6989586621681262317. (~>) t6989586621681262317 (ErrorMessage' (s6989586621681262316 :: Type)) Source #
Instances
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing ShowTypeSym0 Source # | |
SuppressUnusedWarnings (ShowTypeSym0 :: TyFun t6989586621681262317 (ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263104 :: t) Source # | |
Defined in Data.Singletons.TypeError type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263104 :: t) = (ShowType t6989586621681263104 :: ErrorMessage' s6989586621681262316) |
type ShowTypeSym1 (t6989586621681263104 :: t6989586621681262317) = ShowType t6989586621681263104 Source #
data (:<>:@#@$) :: forall (s6989586621681262316 :: Type). (~>) (ErrorMessage' s6989586621681262316) ((~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type))) infixl 6 Source #
Instances
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing (:<>:@#@$) Source # | |
SuppressUnusedWarnings ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263106 :: ErrorMessage' s6989586621681262316) Source # | |
Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263106 :: ErrorMessage' s6989586621681262316) = (:<>:@#@$$) t6989586621681263106 |
data (:<>:@#@$$) (t6989586621681263106 :: ErrorMessage' (s6989586621681262316 :: Type)) :: (~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type)) infixl 6 Source #
Instances
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing ((:<>:@#@$$) x) Source # | |
SuppressUnusedWarnings ((:<>:@#@$$) t6989586621681263106 :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply ((:<>:@#@$$) t6989586621681263106 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681263107 :: ErrorMessage' s) Source # | |
Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$$) t6989586621681263106 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681263107 :: ErrorMessage' s) = t6989586621681263106 :<>: t6989586621681263107 |
type (:<>:@#@$$$) (t6989586621681263106 :: ErrorMessage' s6989586621681262316) (t6989586621681263107 :: ErrorMessage' s6989586621681262316) = (:<>:) t6989586621681263106 t6989586621681263107 Source #
data (:$$:@#@$) :: forall (s6989586621681262316 :: Type). (~>) (ErrorMessage' s6989586621681262316) ((~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type))) infixl 5 Source #
Instances
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing (:$$:@#@$) Source # | |
SuppressUnusedWarnings ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263110 :: ErrorMessage' s6989586621681262316) Source # | |
Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316 ~> ErrorMessage' s6989586621681262316) -> Type) (t6989586621681263110 :: ErrorMessage' s6989586621681262316) = (:$$:@#@$$) t6989586621681263110 |
data (:$$:@#@$$) (t6989586621681263110 :: ErrorMessage' (s6989586621681262316 :: Type)) :: (~>) (ErrorMessage' s6989586621681262316) (ErrorMessage' (s6989586621681262316 :: Type)) infixl 5 Source #
Instances
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing ((:$$:@#@$$) x) Source # | |
SuppressUnusedWarnings ((:$$:@#@$$) t6989586621681263110 :: TyFun (ErrorMessage' s6989586621681262316) (ErrorMessage' s6989586621681262316) -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply ((:$$:@#@$$) t6989586621681263110 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681263111 :: ErrorMessage' s) Source # | |
Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$$) t6989586621681263110 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681263111 :: ErrorMessage' s) = t6989586621681263110 :$$: t6989586621681263111 |
type (:$$:@#@$$$) (t6989586621681263110 :: ErrorMessage' s6989586621681262316) (t6989586621681263111 :: ErrorMessage' s6989586621681262316) = (:$$:) t6989586621681263110 t6989586621681263111 Source #
data TypeErrorSym0 :: forall b6989586621681262306. (~>) PErrorMessage b6989586621681262306 Source #
Instances
SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681262306 -> Type) Source # | |
Defined in Data.Singletons.TypeError sing :: Sing TypeErrorSym0 Source # | |
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681262306 -> Type) Source # | |
Defined in Data.Singletons.TypeError suppressUnusedWarnings :: () Source # | |
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681262307 :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681262307 :: PErrorMessage) = (TypeError a6989586621681262307 :: k2) |
type TypeErrorSym1 (a6989586621681262307 :: PErrorMessage) = TypeError a6989586621681262307 Source #