singletons-2.6: A framework for generating singleton types

Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.Prelude.Either

Contents

- The `Either` singleton
- Singletons from `Data.Either`
- Defunctionalization symbols

Description

Defines functions and datatypes relating to the singleton for `Either`, including a singletons version of all the definitions in `Data.Either`.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in `Data.Either`. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

- type family Sing :: k -> Type
- data SEither :: forall a b. Either a b -> Type where
  - SLeft :: forall a (n :: a). (Sing (n :: a)) -> SEither ('Left n)
  - SRight :: forall b (n :: b). (Sing (n :: b)) -> SEither ('Right n)
- either_ :: (a -> c) -> (b -> c) -> Either a b -> c
- type family Either_ (a :: (~>) a c) (a :: (~>) b c) (a :: Either a b) :: c where ...
- sEither_ :: forall a c b (t :: (~>) a c) (t :: (~>) b c) (t :: Either a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c)
- type family Lefts (a :: [Either a b]) :: [a] where ...
- sLefts :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply LeftsSym0 t :: [a])
- type family Rights (a :: [Either a b]) :: [b] where ...
- sRights :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply RightsSym0 t :: [b])
- type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ...
- sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b]))
- type family IsLeft (a :: Either a b) :: Bool where ...
- sIsLeft :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsLeftSym0 t :: Bool)
- type family IsRight (a :: Either a b) :: Bool where ...
- sIsRight :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsRightSym0 t :: Bool)
- data LeftSym0 :: forall (a6989586621679086099 :: Type) (b6989586621679086100 :: Type). (~>) a6989586621679086099 (Either (a6989586621679086099 :: Type) (b6989586621679086100 :: Type))
- type LeftSym1 (t6989586621679310971 :: a6989586621679086099) = 'Left t6989586621679310971
- data RightSym0 :: forall (b6989586621679086100 :: Type) (a6989586621679086099 :: Type). (~>) b6989586621679086100 (Either (a6989586621679086099 :: Type) (b6989586621679086100 :: Type))
- type RightSym1 (t6989586621679310973 :: b6989586621679086100) = 'Right t6989586621679310973
- data Either_Sym0 :: forall a6989586621680466161 c6989586621680466162 b6989586621680466163. (~>) ((~>) a6989586621680466161 c6989586621680466162) ((~>) ((~>) b6989586621680466163 c6989586621680466162) ((~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162))
- data Either_Sym1 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) :: forall b6989586621680466163. (~>) ((~>) b6989586621680466163 c6989586621680466162) ((~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162)
- data Either_Sym2 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) (a6989586621680466198 :: (~>) b6989586621680466163 c6989586621680466162) :: (~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162
- type Either_Sym3 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) (a6989586621680466198 :: (~>) b6989586621680466163 c6989586621680466162) (a6989586621680466199 :: Either a6989586621680466161 b6989586621680466163) = Either_ a6989586621680466197 a6989586621680466198 a6989586621680466199
- data LeftsSym0 :: forall a6989586621680467643 b6989586621680467644. (~>) [Either a6989586621680467643 b6989586621680467644] [a6989586621680467643]
- type LeftsSym1 (a6989586621680467915 :: [Either a6989586621680467643 b6989586621680467644]) = Lefts a6989586621680467915
- data RightsSym0 :: forall a6989586621680467641 b6989586621680467642. (~>) [Either a6989586621680467641 b6989586621680467642] [b6989586621680467642]
- type RightsSym1 (a6989586621680467910 :: [Either a6989586621680467641 b6989586621680467642]) = Rights a6989586621680467910
- data IsLeftSym0 :: forall a6989586621680467637 b6989586621680467638. (~>) (Either a6989586621680467637 b6989586621680467638) Bool
- type IsLeftSym1 (a6989586621680467886 :: Either a6989586621680467637 b6989586621680467638) = IsLeft a6989586621680467886
- data IsRightSym0 :: forall a6989586621680467635 b6989586621680467636. (~>) (Either a6989586621680467635 b6989586621680467636) Bool
- type IsRightSym1 (a6989586621680467884 :: Either a6989586621680467635 b6989586621680467636) = IsRight a6989586621680467884

# The `Either` singleton

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type

type Sing 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` 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 type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SEither :: forall a b. Either a b -> Type where Source #

Constructors

SLeft :: forall a (n :: a). (Sing (n :: a)) -> SEither ('Left n) |
SRight :: forall b (n :: b). (Sing (n :: b)) -> SEither ('Right n) |

#### Instances

Instances details

(SDecide a, SDecide b) => TestCoercion (SEither :: Either a b -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (Coercion a0 b0)
(SDecide a, SDecide b) => TestEquality (SEither :: Either a b -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (a0 :~: b0)
(ShowSing a, ShowSing b) => Show (SEither z) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SEither z -> ShowS show :: SEither z -> String showList :: [SEither z] -> ShowS

# Singletons from `Data.Either`

either_ :: (a -> c) -> (b -> c) -> Either a b -> c Source #

type family Either_ (a :: (~>) a c) (a :: (~>) b c) (a :: Either a b) :: c where ... Source #

Equations

Either_ f _ ('Left x) = Apply f x |
Either_ _ g ('Right y) = Apply g y |

sEither_ :: forall a c b (t :: (~>) a c) (t :: (~>) b c) (t :: Either a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c) Source #

The preceding two definitions are derived from the function `either` in `Data.Either`. The extra underscore is to avoid name clashes with the type `Either`.

type family Lefts (a :: [Either a b]) :: [a] where ... Source #

Equations

Lefts '[] = '[] |
Lefts ('(:) ('Left x) xs) = Apply (Apply (:@#@$) x) (Apply LeftsSym0 xs) |
Lefts ('(:) ('Right _) xs) = Apply LeftsSym0 xs |

sLefts :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply LeftsSym0 t :: [a]) Source #

type family Rights (a :: [Either a b]) :: [b] where ... Source #

Equations

Rights '[] = '[] |
Rights ('(:) ('Left _) xs) = Apply RightsSym0 xs |
Rights ('(:) ('Right x) xs) = Apply (Apply (:@#@$) x) (Apply RightsSym0 xs) |

sRights :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply RightsSym0 t :: [b]) Source #

type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ... Source #

Equations

PartitionEithers a_6989586621680467888 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621680467893LeftSym1 a_6989586621680467888)) (Let6989586621680467893RightSym1 a_6989586621680467888))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_6989586621680467888 |

sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) Source #

type family IsLeft (a :: Either a b) :: Bool where ... Source #

Equations

IsLeft ('Left _) = TrueSym0 |
IsLeft ('Right _) = FalseSym0 |

sIsLeft :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsLeftSym0 t :: Bool) Source #

type family IsRight (a :: Either a b) :: Bool where ... Source #

Equations

IsRight ('Left _) = FalseSym0 |
IsRight ('Right _) = TrueSym0 |

sIsRight :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsRightSym0 t :: Bool) Source #

# Defunctionalization symbols

data LeftSym0 :: forall (a6989586621679086099 :: Type) (b6989586621679086100 :: Type). (~>) a6989586621679086099 (Either (a6989586621679086099 :: Type) (b6989586621679086100 :: Type)) Source #

#### Instances

Instances details

SingI (LeftSym0 :: TyFun a (Either a b) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing LeftSym0 Source #
SuppressUnusedWarnings (LeftSym0 :: TyFun a6989586621679086099 (Either a6989586621679086099 b6989586621679086100) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (LeftSym0 :: TyFun a (Either a b6989586621679086100) -> Type) (t6989586621679310971 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Apply (LeftSym0 :: TyFun a (Either a b6989586621679086100) -> Type) (t6989586621679310971 :: a) = 'Left t6989586621679310971 :: Either a b6989586621679086100

type LeftSym1 (t6989586621679310971 :: a6989586621679086099) = 'Left t6989586621679310971 Source #

data RightSym0 :: forall (b6989586621679086100 :: Type) (a6989586621679086099 :: Type). (~>) b6989586621679086100 (Either (a6989586621679086099 :: Type) (b6989586621679086100 :: Type)) Source #

#### Instances

Instances details

SingI (RightSym0 :: TyFun b (Either a b) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing RightSym0 Source #
SuppressUnusedWarnings (RightSym0 :: TyFun b6989586621679086100 (Either a6989586621679086099 b6989586621679086100) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (RightSym0 :: TyFun b (Either a6989586621679086099 b) -> Type) (t6989586621679310973 :: b) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Apply (RightSym0 :: TyFun b (Either a6989586621679086099 b) -> Type) (t6989586621679310973 :: b) = 'Right t6989586621679310973 :: Either a6989586621679086099 b

type RightSym1 (t6989586621679310973 :: b6989586621679086100) = 'Right t6989586621679310973 Source #

data Either_Sym0 :: forall a6989586621680466161 c6989586621680466162 b6989586621680466163. (~>) ((~>) a6989586621680466161 c6989586621680466162) ((~>) ((~>) b6989586621680466163 c6989586621680466162) ((~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162)) Source #

#### Instances

Instances details

SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing Either_Sym0 Source #
SuppressUnusedWarnings (Either_Sym0 :: TyFun (a6989586621680466161 ~> c6989586621680466162) ((b6989586621680466163 ~> c6989586621680466162) ~> (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (Either_Sym0 :: TyFun (a6989586621680466161 ~> c6989586621680466162) ((b6989586621680466163 ~> c6989586621680466162) ~> (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162)) -> Type) (a6989586621680466197 :: a6989586621680466161 ~> c6989586621680466162) Source # |

Instance details

Defined in Data.Singletons.Prelude.Either

type Apply (Either_Sym0 :: TyFun (a6989586621680466161 ~> c6989586621680466162) ((b6989586621680466163 ~> c6989586621680466162) ~> (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162)) -> Type) (a6989586621680466197 :: a6989586621680466161 ~> c6989586621680466162) = Either_Sym1 a6989586621680466197 b6989586621680466163 :: TyFun (b6989586621680466163 ~> c6989586621680466162) (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162) -> Type

data Either_Sym1 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) :: forall b6989586621680466163. (~>) ((~>) b6989586621680466163 c6989586621680466162) ((~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162) Source #

#### Instances

Instances details

SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym1 d b) Source #
SuppressUnusedWarnings (Either_Sym1 a6989586621680466197 b6989586621680466163 :: TyFun (b6989586621680466163 ~> c6989586621680466162) (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (Either_Sym1 a6989586621680466197 b6989586621680466163 :: TyFun (b6989586621680466163 ~> c6989586621680466162) (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162) -> Type) (a6989586621680466198 :: b6989586621680466163 ~> c6989586621680466162) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym1 a6989586621680466197 b6989586621680466163 :: TyFun (b6989586621680466163 ~> c6989586621680466162) (Either a6989586621680466161 b6989586621680466163 ~> c6989586621680466162) -> Type) (a6989586621680466198 :: b6989586621680466163 ~> c6989586621680466162) = Either_Sym2 a6989586621680466197 a6989586621680466198

data Either_Sym2 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) (a6989586621680466198 :: (~>) b6989586621680466163 c6989586621680466162) :: (~>) (Either a6989586621680466161 b6989586621680466163) c6989586621680466162 Source #

#### Instances

Instances details

(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym2 d1 d2) Source #
SuppressUnusedWarnings (Either_Sym2 a6989586621680466198 a6989586621680466197 :: TyFun (Either a6989586621680466161 b6989586621680466163) c6989586621680466162 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (Either_Sym2 a6989586621680466198 a6989586621680466197 :: TyFun (Either a b) c -> Type) (a6989586621680466199 :: Either a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym2 a6989586621680466198 a6989586621680466197 :: TyFun (Either a b) c -> Type) (a6989586621680466199 :: Either a b) = Either_ a6989586621680466198 a6989586621680466197 a6989586621680466199

type Either_Sym3 (a6989586621680466197 :: (~>) a6989586621680466161 c6989586621680466162) (a6989586621680466198 :: (~>) b6989586621680466163 c6989586621680466162) (a6989586621680466199 :: Either a6989586621680466161 b6989586621680466163) = Either_ a6989586621680466197 a6989586621680466198 a6989586621680466199 Source #

data LeftsSym0 :: forall a6989586621680467643 b6989586621680467644. (~>) [Either a6989586621680467643 b6989586621680467644] [a6989586621680467643] Source #

#### Instances

Instances details

SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing LeftsSym0 Source #
SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a6989586621680467643 b6989586621680467644] [a6989586621680467643] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621680467915 :: [Either a b]) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621680467915 :: [Either a b]) = Lefts a6989586621680467915

type LeftsSym1 (a6989586621680467915 :: [Either a6989586621680467643 b6989586621680467644]) = Lefts a6989586621680467915 Source #

data RightsSym0 :: forall a6989586621680467641 b6989586621680467642. (~>) [Either a6989586621680467641 b6989586621680467642] [b6989586621680467642] Source #

#### Instances

Instances details

SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing RightsSym0 Source #
SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a6989586621680467641 b6989586621680467642] [b6989586621680467642] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621680467910 :: [Either a b]) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621680467910 :: [Either a b]) = Rights a6989586621680467910

type RightsSym1 (a6989586621680467910 :: [Either a6989586621680467641 b6989586621680467642]) = Rights a6989586621680467910 Source #

data IsLeftSym0 :: forall a6989586621680467637 b6989586621680467638. (~>) (Either a6989586621680467637 b6989586621680467638) Bool Source #

#### Instances

Instances details

SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsLeftSym0 Source #
SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a6989586621680467637 b6989586621680467638) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467886 :: Either a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467886 :: Either a b) = IsLeft a6989586621680467886

type IsLeftSym1 (a6989586621680467886 :: Either a6989586621680467637 b6989586621680467638) = IsLeft a6989586621680467886 Source #

data IsRightSym0 :: forall a6989586621680467635 b6989586621680467636. (~>) (Either a6989586621680467635 b6989586621680467636) Bool Source #

#### Instances

Instances details

SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsRightSym0 Source #
SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a6989586621680467635 b6989586621680467636) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source #
type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467884 :: Either a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Either type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467884 :: Either a b) = IsRight a6989586621680467884

type IsRightSym1 (a6989586621680467884 :: Either a6989586621680467635 b6989586621680467636) = IsRight a6989586621680467884 Source #