singletons-2.5.1: A framework for generating singleton types

Copyright | (C) 2018 Ryan Scott
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.TypeError

Contents

- Defunctionalization symbols

Description

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 (s6989586621681254413 :: Type). (~>) s6989586621681254413 (ErrorMessage' (s6989586621681254413 :: Type))
- type TextSym1 (t6989586621681255199 :: s6989586621681254413) = Text t6989586621681255199
- data ShowTypeSym0 :: forall (s6989586621681254413 :: Type) t6989586621681254414. (~>) t6989586621681254414 (ErrorMessage' (s6989586621681254413 :: Type))
- type ShowTypeSym1 (t6989586621681255201 :: t6989586621681254414) = ShowType t6989586621681255201
- data (:<>:@#@$) :: forall (s6989586621681254413 :: Type). (~>) (ErrorMessage' s6989586621681254413) ((~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type)))
- data (:<>:@#@$$) (t6989586621681255203 :: ErrorMessage' (s6989586621681254413 :: Type)) :: (~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type))
- type (:<>:@#@$$$) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) (t6989586621681255204 :: ErrorMessage' s6989586621681254413) = (:<>:) t6989586621681255203 t6989586621681255204
- data (:$$:@#@$) :: forall (s6989586621681254413 :: Type). (~>) (ErrorMessage' s6989586621681254413) ((~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type)))
- data (:$$:@#@$$) (t6989586621681255207 :: ErrorMessage' (s6989586621681254413 :: Type)) :: (~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type))
- type (:$$:@#@$$$) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) (t6989586621681255208 :: ErrorMessage' s6989586621681254413) = (:$$:) t6989586621681255207 t6989586621681255208
- data TypeErrorSym0 :: forall b6989586621681254403. (~>) PErrorMessage b6989586621681254403
- type TypeErrorSym1 (a6989586621681254404 :: PErrorMessage) = TypeError a6989586621681254404

# Documentation

type family TypeError (a :: PErrorMessage) :: b where ... Source #

A drop-in replacement for `TypeError`. This also exists at the value-level as `typeError`.

Equations

TypeError a = TypeError (ConvertPErrorMessage a) |

sTypeError :: HasCallStack => Sing err -> Sing (TypeError err) Source #

The singleton for `typeError`.

Note that this is not quite as expressive as `TypeError`, as it is unable to handle `ShowType` constructors at all.

typeError :: HasCallStack => ErrorMessage -> a Source #

The value-level counterpart to `TypeError`.

Note that this is not quite as expressive as `TypeError`, as it is unable to print the contents of `ShowType` constructors (it will simply print `"<type>"` in their place).

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`.

Constructors

Text s | Show the text as is.
ShowType t | Pretty print the type. `ShowType :: k -> ErrorMessage`
(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

SingKind PErrorMessage Source # |
Instance details Defined in Data.Singletons.TypeError Associated Types type Demote PErrorMessage = (r :: Type) Source # Methods fromSing :: Sing a -> Demote PErrorMessage Source # toSing :: Demote PErrorMessage -> SomeSing PErrorMessage Source #
SingI t => SingI (Text t :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (Text t) Source #
SingI ty => SingI (ShowType ty :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (ShowType ty) Source #
(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :<>: e2) Source #
(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :$$: e2) Source #
SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TypeErrorSym0 Source #
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TextSym0 Source #
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:$$:@#@$) Source #
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:<>:@#@$) Source #
SuppressUnusedWarnings (TextSym0 :: TyFun s6989586621681254413 (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ShowTypeSym0 Source #
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:$$:@#@$$) x) Source #
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:<>:@#@$$) x) Source #
SuppressUnusedWarnings (ShowTypeSym0 :: TyFun t6989586621681254414 (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SingI (TyCon1 (Text :: Symbol -> ErrorMessage' Symbol)) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 Text) Source #
SingI (TyCon1 (ShowType :: t -> ErrorMessage' Symbol) :: t ~> ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ShowType) Source #
SingI x => SingI (TyCon1 ((:<>:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ((:<>:) x)) Source #
SingI x => SingI (TyCon1 ((:$$:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ((:$$:) x)) Source #
SingI (TyCon2 ((:<>:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol)) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon2 (:<>:)) Source #
SingI (TyCon2 ((:$$:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol)) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon2 (:$$:)) Source #
type Demote PErrorMessage Source # |
Instance details Defined in Data.Singletons.TypeError type Demote PErrorMessage = ErrorMessage
data Sing (a :: PErrorMessage) Source # |

Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

- SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
- SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
- (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
- (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) = (TypeError a6989586621681254404 :: k2)
type Apply (TextSym0 :: TyFun s (ErrorMessage' s) -> Type) (t6989586621681255199 :: s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (TextSym0 :: TyFun s (ErrorMessage' s) -> Type) (t6989586621681255199 :: s) = Text t6989586621681255199
type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255201 :: t) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255201 :: t) = (ShowType t6989586621681255201 :: ErrorMessage' s6989586621681254413)
type Apply ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255204 :: ErrorMessage' s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255204 :: ErrorMessage' s) = t6989586621681255203 :<>: t6989586621681255204
type Apply ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255208 :: ErrorMessage' s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255208 :: ErrorMessage' s) = t6989586621681255207 :$$: t6989586621681255208
type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) = (:<>:@#@$$) t6989586621681255203
type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) = (:$$:@#@$$) t6989586621681255207

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 # |
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) Source #
SDecide k => TestEquality (Sing :: k -> Type) Source # |
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) Source #
Show (SSymbol s) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS Source # show :: SSymbol s -> String Source # showList :: [SSymbol s] -> ShowS Source #
Show (SNat n) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS Source # show :: SNat n -> String Source # showList :: [SNat n] -> ShowS Source #
Eq (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: Sing a -> Sing a -> Bool Source # (/=) :: Sing a -> Sing a -> Bool Source #
Ord (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods compare :: Sing a -> Sing a -> Ordering Source # (<) :: Sing a -> Sing a -> Bool Source # (<=) :: Sing a -> Sing a -> Bool Source # (>) :: Sing a -> Sing a -> Bool Source # (>=) :: Sing a -> Sing a -> Bool Source # max :: Sing a -> Sing a -> Sing a Source # min :: Sing a -> Sing a -> Sing a Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> Sing a -> ShowS Source # show :: Sing a -> String Source # showList :: [Sing a] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing m => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing Bool => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing Bool => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
data Sing (a :: Bool) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

- SFalse :: forall (a :: Bool). Sing False
- STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

- SLT :: forall (a :: Ordering). Sing LT
- SEQ :: forall (a :: Ordering). Sing EQ
- SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

- SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

- SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ()) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

- STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

- SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

- SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (a :: PErrorMessage) Source # |

Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

- SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
- SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
- (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
- (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

data Sing (b :: [a]) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

- SNil :: forall k (b :: [k]). Sing ([] :: [k])
- SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)

data Sing (b :: Maybe a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

- SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
- SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

newtype Sing (a :: TYPE rep) Source #

A choice of singleton for the kind ``TYPE` rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`.

Conceivably, one could generalize this instance to `Sing :: k -> Type` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks).

We cannot produce explicit singleton values for everything in ``TYPE` rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.

Instance details Defined in Data.Singletons.TypeRepTYPE newtype Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

- SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

- SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

- SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

- SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

- SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

- SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

- SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

- SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

- SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

- SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

- SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

- SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

- SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

- (:%|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :| n)

data Sing (c :: Either a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

- SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
- SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

- STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)

data Sing (c :: Arg a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

- SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)

newtype Sing (f :: k1 ~> k2) Source # |

Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {

- applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (d :: (a, b, c)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

- STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)

data Sing (c :: Const a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

- SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)

data Sing (e :: (a, b, c, d)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

- STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)

data Sing (f :: (a, b, c, d, e)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

- STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)

data Sing (g :: (a, b, c, d, e, f)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

- STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)

data Sing (h :: (a, b, c, d, e, f, g)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

- STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

type SErrorMessage = (Sing :: PErrorMessage -> Type) Source #

type family ConvertPErrorMessage (a :: PErrorMessage) :: ErrorMessage where ... Source #

Convert a `PErrorMessage` to a `ErrorMessage` from GHC.TypeLits.

Equations

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 (s6989586621681254413 :: Type). (~>) s6989586621681254413 (ErrorMessage' (s6989586621681254413 :: Type)) Source #

Instances

SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TextSym0 Source #
SuppressUnusedWarnings (TextSym0 :: TyFun s6989586621681254413 (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply (TextSym0 :: TyFun s (ErrorMessage' s) -> Type) (t6989586621681255199 :: s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (TextSym0 :: TyFun s (ErrorMessage' s) -> Type) (t6989586621681255199 :: s) = Text t6989586621681255199

type TextSym1 (t6989586621681255199 :: s6989586621681254413) = Text t6989586621681255199 Source #

data ShowTypeSym0 :: forall (s6989586621681254413 :: Type) t6989586621681254414. (~>) t6989586621681254414 (ErrorMessage' (s6989586621681254413 :: Type)) Source #

Instances

SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ShowTypeSym0 Source #
SuppressUnusedWarnings (ShowTypeSym0 :: TyFun t6989586621681254414 (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255201 :: t) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (ShowTypeSym0 :: TyFun t (ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255201 :: t) = (ShowType t6989586621681255201 :: ErrorMessage' s6989586621681254413)

type ShowTypeSym1 (t6989586621681255201 :: t6989586621681254414) = ShowType t6989586621681255201 Source #

data (:<>:@#@$) :: forall (s6989586621681254413 :: Type). (~>) (ErrorMessage' s6989586621681254413) ((~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type))) infixl 6 Source #

Instances

SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:<>:@#@$) Source #
SuppressUnusedWarnings ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) = (:<>:@#@$$) t6989586621681255203

data (:<>:@#@$$) (t6989586621681255203 :: ErrorMessage' (s6989586621681254413 :: Type)) :: (~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type)) infixl 6 Source #

Instances

SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:<>:@#@$$) x) Source #
SuppressUnusedWarnings ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255204 :: ErrorMessage' s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:<>:@#@$$) t6989586621681255203 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255204 :: ErrorMessage' s) = t6989586621681255203 :<>: t6989586621681255204

type (:<>:@#@$$$) (t6989586621681255203 :: ErrorMessage' s6989586621681254413) (t6989586621681255204 :: ErrorMessage' s6989586621681254413) = (:<>:) t6989586621681255203 t6989586621681255204 Source #

data (:$$:@#@$) :: forall (s6989586621681254413 :: Type). (~>) (ErrorMessage' s6989586621681254413) ((~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type))) infixl 5 Source #

Instances

SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:$$:@#@$) Source #
SuppressUnusedWarnings ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$) :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413 ~> ErrorMessage' s6989586621681254413) -> Type) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) = (:$$:@#@$$) t6989586621681255207

data (:$$:@#@$$) (t6989586621681255207 :: ErrorMessage' (s6989586621681254413 :: Type)) :: (~>) (ErrorMessage' s6989586621681254413) (ErrorMessage' (s6989586621681254413 :: Type)) infixl 5 Source #

Instances

SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:$$:@#@$$) x) Source #
SuppressUnusedWarnings ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s6989586621681254413) (ErrorMessage' s6989586621681254413) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255208 :: ErrorMessage' s) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply ((:$$:@#@$$) t6989586621681255207 :: TyFun (ErrorMessage' s) (ErrorMessage' s) -> Type) (t6989586621681255208 :: ErrorMessage' s) = t6989586621681255207 :$$: t6989586621681255208

type (:$$:@#@$$$) (t6989586621681255207 :: ErrorMessage' s6989586621681254413) (t6989586621681255208 :: ErrorMessage' s6989586621681254413) = (:$$:) t6989586621681255207 t6989586621681255208 Source #

data TypeErrorSym0 :: forall b6989586621681254403. (~>) PErrorMessage b6989586621681254403 Source #

Instances

SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TypeErrorSym0 Source #
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) = (TypeError a6989586621681254404 :: k2)

type TypeErrorSym1 (a6989586621681254404 :: PErrorMessage) = TypeError a6989586621681254404 Source #