Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	GHC2021

Data.Tuple.Singletons

Contents

Singleton definitions
Singletons from Data.Tuple
Defunctionalization symbols

Description

Defines functions and datatypes relating to the singleton for tuples, including singled versions of all the definitions in Data.Tuple.

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.Tuple. 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 STuple0 :: () -> Type where
- STuple0 :: STuple0 ('() :: ())
data STuple2 :: forall (a :: Type) (b :: Type). (a, b) -> Type where
- STuple2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). (Sing n) -> (Sing n) -> STuple2 ('(n, n) :: (a :: Type, b :: Type))
data STuple3 :: forall (a :: Type) (b :: Type) (c :: Type). (a, b, c) -> Type where
- STuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (n :: a) (n :: b) (n :: c). (Sing n) -> (Sing n) -> (Sing n) -> STuple3 ('(n, n, n) :: (a :: Type, b :: Type, c :: Type))
data STuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type). (a, b, c, d) -> Type where
- STuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple4 ('(n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type))
data STuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type). (a, b, c, d, e) -> Type where
- STuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple5 ('(n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type))
data STuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type). (a, b, c, d, e, f) -> Type where
- STuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple6 ('(n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))
data STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type). (a, b, c, d, e, f, g) -> Type where
- STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (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) -> STuple7 ('(n, n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))
type family Fst (a :: (a, b)) :: a where ...
sFst :: forall (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t :: a) :: Type
type family Snd (a :: (a, b)) :: b where ...
sSnd :: forall (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t :: b) :: Type
type family Curry (a :: (~>) (a, b) c) (a :: a) (a :: b) :: c where ...
sCurry :: forall (t :: (~>) (a, b) c) (t :: a) (t :: b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t :: c) :: Type
type family Uncurry (a :: (~>) a ((~>) b c)) (a :: (a, b)) :: c where ...
sUncurry :: forall (t :: (~>) a ((~>) b c)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t :: c) :: Type
type family Swap (a :: (a, b)) :: (b, a) where ...
sSwap :: forall (t :: (a, b)). Sing t -> Sing (Apply SwapSym0 t :: (b, a)) :: Type
type family Tuple0Sym0 :: () where ...
data Tuple2Sym0 :: (~>) a ((~>) b (a :: Type, b :: Type))
data Tuple2Sym1 (a6989586621679052039 :: a) :: (~>) b (a :: Type, b :: Type)
type family Tuple2Sym2 (a6989586621679052039 :: a) (a6989586621679052040 :: b) :: (a :: Type, b :: Type) where ...
data Tuple3Sym0 :: (~>) a ((~>) b ((~>) c (a :: Type, b :: Type, c :: Type)))
data Tuple3Sym1 (a6989586621679052070 :: a) :: (~>) b ((~>) c (a :: Type, b :: Type, c :: Type))
data Tuple3Sym2 (a6989586621679052070 :: a) (a6989586621679052071 :: b) :: (~>) c (a :: Type, b :: Type, c :: Type)
type family Tuple3Sym3 (a6989586621679052070 :: a) (a6989586621679052071 :: b) (a6989586621679052072 :: c) :: (a :: Type, b :: Type, c :: Type) where ...
data Tuple4Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type))))
data Tuple4Sym1 (a6989586621679052119 :: a) :: (~>) b ((~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type)))
data Tuple4Sym2 (a6989586621679052119 :: a) (a6989586621679052120 :: b) :: (~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type))
data Tuple4Sym3 (a6989586621679052119 :: a) (a6989586621679052120 :: b) (a6989586621679052121 :: c) :: (~>) d (a :: Type, b :: Type, c :: Type, d :: Type)
type family Tuple4Sym4 (a6989586621679052119 :: a) (a6989586621679052120 :: b) (a6989586621679052121 :: c) (a6989586621679052122 :: d) :: (a :: Type, b :: Type, c :: Type, d :: Type) where ...
data Tuple5Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)))))
data Tuple5Sym1 (a6989586621679052188 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type))))
data Tuple5Sym2 (a6989586621679052188 :: a) (a6989586621679052189 :: b) :: (~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)))
data Tuple5Sym3 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) :: (~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type))
data Tuple5Sym4 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) (a6989586621679052191 :: d) :: (~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)
type family Tuple5Sym5 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) (a6989586621679052191 :: d) (a6989586621679052192 :: e) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type) where ...
data Tuple6Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))))))
data Tuple6Sym1 (a6989586621679052279 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)))))
data Tuple6Sym2 (a6989586621679052279 :: a) (a6989586621679052280 :: b) :: (~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))))
data Tuple6Sym3 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) :: (~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)))
data Tuple6Sym4 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) :: (~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))
data Tuple6Sym5 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) (a6989586621679052283 :: e) :: (~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)
type family Tuple6Sym6 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) (a6989586621679052283 :: e) (a6989586621679052284 :: f) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type) where ...
data Tuple7Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)))))))
data Tuple7Sym1 (a6989586621679052394 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))))))
data Tuple7Sym2 (a6989586621679052394 :: a) (a6989586621679052395 :: b) :: (~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)))))
data Tuple7Sym3 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) :: (~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))))
data Tuple7Sym4 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) :: (~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)))
data Tuple7Sym5 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) :: (~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))
data Tuple7Sym6 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) (a6989586621679052399 :: f) :: (~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)
type family Tuple7Sym7 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) (a6989586621679052399 :: f) (a6989586621679052400 :: g) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type) where ...
data FstSym0 :: (~>) (a, b) a
type family FstSym1 (a6989586621679180883 :: (a, b)) :: a where ...
data SndSym0 :: (~>) (a, b) b
type family SndSym1 (a6989586621679180879 :: (a, b)) :: b where ...
data CurrySym0 :: (~>) ((~>) (a, b) c) ((~>) a ((~>) b c))
data CurrySym1 (a6989586621679180871 :: (~>) (a, b) c) :: (~>) a ((~>) b c)
data CurrySym2 (a6989586621679180871 :: (~>) (a, b) c) (a6989586621679180872 :: a) :: (~>) b c
type family CurrySym3 (a6989586621679180871 :: (~>) (a, b) c) (a6989586621679180872 :: a) (a6989586621679180873 :: b) :: c where ...
data UncurrySym0 :: (~>) ((~>) a ((~>) b c)) ((~>) (a, b) c)
data UncurrySym1 (a6989586621679180863 :: (~>) a ((~>) b c)) :: (~>) (a, b) c
type family UncurrySym2 (a6989586621679180863 :: (~>) a ((~>) b c)) (a6989586621679180864 :: (a, b)) :: c where ...
data SwapSym0 :: (~>) (a, b) (b, a)
type family SwapSym1 (a6989586621679180857 :: (a, b)) :: (b, a) where ...

Singleton definitions

See Sing for more info.

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SAll
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SBool
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SChar
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Ord.Singletons type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.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.Base.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Proxy.Singletons type Sing = SProxy :: Proxy t -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons type Sing = SArg :: Arg a b -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Const.Singletons type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Product.Singletons type Sing = SProduct :: Product f g a -> Type
type Sing Source #
Instance details Defined in Data.Functor.Sum.Singletons type Sing = SSum :: Sum f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Compose.Singletons type Sing = SCompose :: Compose f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data STuple0 :: () -> Type where Source #

Constructors

STuple0 :: STuple0 ('() :: ())

Instances

Instances details

TestCoercion STuple0 Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testCoercion :: forall (a :: k) (b :: k). STuple0 a -> STuple0 b -> Maybe (Coercion a b) #
TestEquality STuple0 Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testEquality :: forall (a :: k) (b :: k). STuple0 a -> STuple0 b -> Maybe (a :~: b) #
Show (STuple0 z) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods showsPrec :: Int -> STuple0 z -> ShowS # show :: STuple0 z -> String # showList :: [STuple0 z] -> ShowS #

data STuple2 :: forall (a :: Type) (b :: Type). (a, b) -> Type where Source #

Constructors

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

Instances

Instances details

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

data STuple3 :: forall (a :: Type) (b :: Type) (c :: Type). (a, b, c) -> Type where Source #

Constructors

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

Instances

Instances details

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

data STuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type). (a, b, c, d) -> Type where Source #

Constructors

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

Instances

Instances details

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

data STuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type). (a, b, c, d, e) -> Type where Source #

Constructors

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

Instances

Instances details

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

data STuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type). (a, b, c, d, e, f) -> Type where Source #

Constructors

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

Instances

Instances details

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

data STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type). (a, b, c, d, e, f, g) -> Type where Source #

Constructors

STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (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) -> STuple7 ('(n, n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))

Instances

Instances details

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

Singletons from `Data.Tuple`

type family Fst (a :: (a, b)) :: a where ... Source #

Equations

Fst '(x, _) = x

sFst :: forall (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t :: a) :: Type Source #

type family Snd (a :: (a, b)) :: b where ... Source #

Equations

Snd '(_, y) = y

sSnd :: forall (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t :: b) :: Type Source #

type family Curry (a :: (~>) (a, b) c) (a :: a) (a :: b) :: c where ... Source #

Equations

Curry f x y = Apply f (Apply (Apply Tuple2Sym0 x) y)

sCurry :: forall (t :: (~>) (a, b) c) (t :: a) (t :: b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t :: c) :: Type Source #

type family Uncurry (a :: (~>) a ((~>) b c)) (a :: (a, b)) :: c where ... Source #

Equations

Uncurry f p = Apply (Apply f (Apply FstSym0 p)) (Apply SndSym0 p)

sUncurry :: forall (t :: (~>) a ((~>) b c)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t :: c) :: Type Source #

type family Swap (a :: (a, b)) :: (b, a) where ... Source #

Equations

Swap '(a, b) = Apply (Apply Tuple2Sym0 b) a

sSwap :: forall (t :: (a, b)). Sing t -> Sing (Apply SwapSym0 t :: (b, a)) :: Type Source #

Defunctionalization symbols

type family Tuple0Sym0 :: () where ... Source #

Equations

Tuple0Sym0 = '()

data Tuple2Sym0 :: (~>) a ((~>) b (a :: Type, b :: Type)) Source #

Instances

Instances details

SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple2Sym0 Source #
SuppressUnusedWarnings (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) (a6989586621679052039 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) (a6989586621679052039 :: a) = Tuple2Sym1 a6989586621679052039 :: TyFun b (a, b) -> Type

data Tuple2Sym1 (a6989586621679052039 :: a) :: (~>) b (a :: Type, b :: Type) Source #

Instances

Instances details

SingI1 (Tuple2Sym1 :: a -> TyFun b (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple2Sym1 x) Source #
SingI d => SingI (Tuple2Sym1 d :: TyFun b (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple2Sym1 d) Source #
SuppressUnusedWarnings (Tuple2Sym1 a6989586621679052039 :: TyFun b (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple2Sym1 a6989586621679052039 :: TyFun k2 (k1, k2) -> Type) (a6989586621679052040 :: k2) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple2Sym1 a6989586621679052039 :: TyFun k2 (k1, k2) -> Type) (a6989586621679052040 :: k2) = '(a6989586621679052039, a6989586621679052040)

type family Tuple2Sym2 (a6989586621679052039 :: a) (a6989586621679052040 :: b) :: (a :: Type, b :: Type) where ... Source #

Equations

Tuple2Sym2 a6989586621679052039 a6989586621679052040 = '(a6989586621679052039, a6989586621679052040)

data Tuple3Sym0 :: (~>) a ((~>) b ((~>) c (a :: Type, b :: Type, c :: Type))) Source #

Instances

Instances details

SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple3Sym0 Source #
SuppressUnusedWarnings (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) (a6989586621679052070 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) (a6989586621679052070 :: a) = Tuple3Sym1 a6989586621679052070 :: TyFun b (c ~> (a, b, c)) -> Type

data Tuple3Sym1 (a6989586621679052070 :: a) :: (~>) b ((~>) c (a :: Type, b :: Type, c :: Type)) Source #

Instances

Instances details

SingI1 (Tuple3Sym1 :: a -> TyFun b (c ~> (a, b, c)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple3Sym1 x) Source #
SingI d => SingI (Tuple3Sym1 d :: TyFun b (c ~> (a, b, c)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple3Sym1 d) Source #
SuppressUnusedWarnings (Tuple3Sym1 a6989586621679052070 :: TyFun b (c ~> (a, b, c)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple3Sym1 a6989586621679052070 :: TyFun b (c ~> (a, b, c)) -> Type) (a6989586621679052071 :: b) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple3Sym1 a6989586621679052070 :: TyFun b (c ~> (a, b, c)) -> Type) (a6989586621679052071 :: b) = Tuple3Sym2 a6989586621679052070 a6989586621679052071 :: TyFun c (a, b, c) -> Type

data Tuple3Sym2 (a6989586621679052070 :: a) (a6989586621679052071 :: b) :: (~>) c (a :: Type, b :: Type, c :: Type) Source #

Instances

Instances details

SingI2 (Tuple3Sym2 :: a -> b -> TyFun c (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple3Sym2 x y) Source #
SingI d => SingI1 (Tuple3Sym2 d :: b -> TyFun c (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple3Sym2 d x) Source #
(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 :: TyFun c (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple3Sym2 d1 d2) Source #
SuppressUnusedWarnings (Tuple3Sym2 a6989586621679052070 a6989586621679052071 :: TyFun c (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple3Sym2 a6989586621679052070 a6989586621679052071 :: TyFun k3 (k1, k2, k3) -> Type) (a6989586621679052072 :: k3) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple3Sym2 a6989586621679052070 a6989586621679052071 :: TyFun k3 (k1, k2, k3) -> Type) (a6989586621679052072 :: k3) = '(a6989586621679052070, a6989586621679052071, a6989586621679052072)

type family Tuple3Sym3 (a6989586621679052070 :: a) (a6989586621679052071 :: b) (a6989586621679052072 :: c) :: (a :: Type, b :: Type, c :: Type) where ... Source #

Equations

Tuple3Sym3 a6989586621679052070 a6989586621679052071 a6989586621679052072 = '(a6989586621679052070, a6989586621679052071, a6989586621679052072)

data Tuple4Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type)))) Source #

Instances

Instances details

SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple4Sym0 Source #
SuppressUnusedWarnings (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) (a6989586621679052119 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) (a6989586621679052119 :: a) = Tuple4Sym1 a6989586621679052119 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type

data Tuple4Sym1 (a6989586621679052119 :: a) :: (~>) b ((~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type))) Source #

Instances

Instances details

SingI1 (Tuple4Sym1 :: a -> TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple4Sym1 x) Source #
SingI d1 => SingI (Tuple4Sym1 d1 :: TyFun b (c ~> (d2 ~> (a, b, c, d2))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple4Sym1 d1) Source #
SuppressUnusedWarnings (Tuple4Sym1 a6989586621679052119 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple4Sym1 a6989586621679052119 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) (a6989586621679052120 :: b) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple4Sym1 a6989586621679052119 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) (a6989586621679052120 :: b) = Tuple4Sym2 a6989586621679052119 a6989586621679052120 :: TyFun c (d ~> (a, b, c, d)) -> Type

data Tuple4Sym2 (a6989586621679052119 :: a) (a6989586621679052120 :: b) :: (~>) c ((~>) d (a :: Type, b :: Type, c :: Type, d :: Type)) Source #

Instances

Instances details

SingI2 (Tuple4Sym2 :: a -> b -> TyFun c (d ~> (a, b, c, d)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple4Sym2 x y) Source #
SingI d1 => SingI1 (Tuple4Sym2 d1 :: b -> TyFun c (d2 ~> (a, b, c, d2)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple4Sym2 d1 x) Source #
(SingI d1, SingI d2) => SingI (Tuple4Sym2 d1 d2 :: TyFun c (d3 ~> (a, b, c, d3)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple4Sym2 d1 d2) Source #
SuppressUnusedWarnings (Tuple4Sym2 a6989586621679052119 a6989586621679052120 :: TyFun c (d ~> (a, b, c, d)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple4Sym2 a6989586621679052119 a6989586621679052120 :: TyFun c (d ~> (a, b, c, d)) -> Type) (a6989586621679052121 :: c) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple4Sym2 a6989586621679052119 a6989586621679052120 :: TyFun c (d ~> (a, b, c, d)) -> Type) (a6989586621679052121 :: c) = Tuple4Sym3 a6989586621679052119 a6989586621679052120 a6989586621679052121 :: TyFun d (a, b, c, d) -> Type

data Tuple4Sym3 (a6989586621679052119 :: a) (a6989586621679052120 :: b) (a6989586621679052121 :: c) :: (~>) d (a :: Type, b :: Type, c :: Type, d :: Type) Source #

Instances

Instances details

SingI d1 => SingI2 (Tuple4Sym3 d1 :: b -> c -> TyFun d2 (a, b, c, d2) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple4Sym3 d1 x y) Source #
(SingI d1, SingI d2) => SingI1 (Tuple4Sym3 d1 d2 :: c -> TyFun d3 (a, b, c, d3) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple4Sym3 d1 d2 x) Source #
(SingI d1, SingI d2, SingI d3) => SingI (Tuple4Sym3 d1 d2 d3 :: TyFun d4 (a, b, c, d4) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple4Sym3 d1 d2 d3) Source #
SuppressUnusedWarnings (Tuple4Sym3 a6989586621679052119 a6989586621679052120 a6989586621679052121 :: TyFun d (a, b, c, d) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple4Sym3 a6989586621679052119 a6989586621679052120 a6989586621679052121 :: TyFun k4 (k1, k2, k3, k4) -> Type) (a6989586621679052122 :: k4) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple4Sym3 a6989586621679052119 a6989586621679052120 a6989586621679052121 :: TyFun k4 (k1, k2, k3, k4) -> Type) (a6989586621679052122 :: k4) = '(a6989586621679052119, a6989586621679052120, a6989586621679052121, a6989586621679052122)

type family Tuple4Sym4 (a6989586621679052119 :: a) (a6989586621679052120 :: b) (a6989586621679052121 :: c) (a6989586621679052122 :: d) :: (a :: Type, b :: Type, c :: Type, d :: Type) where ... Source #

Equations

Tuple4Sym4 a6989586621679052119 a6989586621679052120 a6989586621679052121 a6989586621679052122 = '(a6989586621679052119, a6989586621679052120, a6989586621679052121, a6989586621679052122)

data Tuple5Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type))))) Source #

Instances

Instances details

SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple5Sym0 Source #
SuppressUnusedWarnings (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) (a6989586621679052188 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) (a6989586621679052188 :: a) = Tuple5Sym1 a6989586621679052188 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type

data Tuple5Sym1 (a6989586621679052188 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)))) Source #

Instances

Instances details

SingI1 (Tuple5Sym1 :: a -> TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple5Sym1 x) Source #
SingI d1 => SingI (Tuple5Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (a, b, c, d2, e)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple5Sym1 d1) Source #
SuppressUnusedWarnings (Tuple5Sym1 a6989586621679052188 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple5Sym1 a6989586621679052188 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) (a6989586621679052189 :: b) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple5Sym1 a6989586621679052188 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) (a6989586621679052189 :: b) = Tuple5Sym2 a6989586621679052188 a6989586621679052189 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type

data Tuple5Sym2 (a6989586621679052188 :: a) (a6989586621679052189 :: b) :: (~>) c ((~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type))) Source #

Instances

Instances details

SingI2 (Tuple5Sym2 :: a -> b -> TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple5Sym2 x y) Source #
SingI d1 => SingI1 (Tuple5Sym2 d1 :: b -> TyFun c (d2 ~> (e ~> (a, b, c, d2, e))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple5Sym2 d1 x) Source #
(SingI d1, SingI d2) => SingI (Tuple5Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (a, b, c, d3, e))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple5Sym2 d1 d2) Source #
SuppressUnusedWarnings (Tuple5Sym2 a6989586621679052188 a6989586621679052189 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple5Sym2 a6989586621679052188 a6989586621679052189 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) (a6989586621679052190 :: c) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple5Sym2 a6989586621679052188 a6989586621679052189 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) (a6989586621679052190 :: c) = Tuple5Sym3 a6989586621679052188 a6989586621679052189 a6989586621679052190 :: TyFun d (e ~> (a, b, c, d, e)) -> Type

data Tuple5Sym3 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) :: (~>) d ((~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)) Source #

Instances

Instances details

SingI d1 => SingI2 (Tuple5Sym3 d1 :: b -> c -> TyFun d2 (e ~> (a, b, c, d2, e)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple5Sym3 d1 x y) Source #
(SingI d1, SingI d2) => SingI1 (Tuple5Sym3 d1 d2 :: c -> TyFun d3 (e ~> (a, b, c, d3, e)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple5Sym3 d1 d2 x) Source #
(SingI d1, SingI d2, SingI d3) => SingI (Tuple5Sym3 d1 d2 d3 :: TyFun d4 (e ~> (a, b, c, d4, e)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple5Sym3 d1 d2 d3) Source #
SuppressUnusedWarnings (Tuple5Sym3 a6989586621679052188 a6989586621679052189 a6989586621679052190 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple5Sym3 a6989586621679052188 a6989586621679052189 a6989586621679052190 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) (a6989586621679052191 :: d) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple5Sym3 a6989586621679052188 a6989586621679052189 a6989586621679052190 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) (a6989586621679052191 :: d) = Tuple5Sym4 a6989586621679052188 a6989586621679052189 a6989586621679052190 a6989586621679052191 :: TyFun e (a, b, c, d, e) -> Type

data Tuple5Sym4 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) (a6989586621679052191 :: d) :: (~>) e (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type) Source #

Instances

Instances details

(SingI d1, SingI d2) => SingI2 (Tuple5Sym4 d1 d2 :: c -> d3 -> TyFun e (a, b, c, d3, e) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple5Sym4 d1 d2 x y) Source #
(SingI d1, SingI d2, SingI d3) => SingI1 (Tuple5Sym4 d1 d2 d3 :: d4 -> TyFun e (a, b, c, d4, e) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple5Sym4 d1 d2 d3 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple5Sym4 d1 d2 d3 d5 :: TyFun e (a, b, c, d4, e) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple5Sym4 d1 d2 d3 d5) Source #
SuppressUnusedWarnings (Tuple5Sym4 a6989586621679052188 a6989586621679052189 a6989586621679052190 a6989586621679052191 :: TyFun e (a, b, c, d, e) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple5Sym4 a6989586621679052188 a6989586621679052189 a6989586621679052190 a6989586621679052191 :: TyFun k5 (k1, k2, k3, k4, k5) -> Type) (a6989586621679052192 :: k5) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple5Sym4 a6989586621679052188 a6989586621679052189 a6989586621679052190 a6989586621679052191 :: TyFun k5 (k1, k2, k3, k4, k5) -> Type) (a6989586621679052192 :: k5) = '(a6989586621679052188, a6989586621679052189, a6989586621679052190, a6989586621679052191, a6989586621679052192)

type family Tuple5Sym5 (a6989586621679052188 :: a) (a6989586621679052189 :: b) (a6989586621679052190 :: c) (a6989586621679052191 :: d) (a6989586621679052192 :: e) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type) where ... Source #

Equations

Tuple5Sym5 a6989586621679052188 a6989586621679052189 a6989586621679052190 a6989586621679052191 a6989586621679052192 = '(a6989586621679052188, a6989586621679052189, a6989586621679052190, a6989586621679052191, a6989586621679052192)

data Tuple6Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)))))) Source #

Instances

Instances details

SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple6Sym0 Source #
SuppressUnusedWarnings (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) (a6989586621679052279 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) (a6989586621679052279 :: a) = Tuple6Sym1 a6989586621679052279 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type

data Tuple6Sym1 (a6989586621679052279 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))))) Source #

Instances

Instances details

SingI1 (Tuple6Sym1 :: a -> TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple6Sym1 x) Source #
SingI d1 => SingI (Tuple6Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (a, b, c, d2, e, f))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple6Sym1 d1) Source #
SuppressUnusedWarnings (Tuple6Sym1 a6989586621679052279 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym1 a6989586621679052279 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) (a6989586621679052280 :: b) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym1 a6989586621679052279 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) (a6989586621679052280 :: b) = Tuple6Sym2 a6989586621679052279 a6989586621679052280 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type

data Tuple6Sym2 (a6989586621679052279 :: a) (a6989586621679052280 :: b) :: (~>) c ((~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)))) Source #

Instances

Instances details

SingI2 (Tuple6Sym2 :: a -> b -> TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple6Sym2 x y) Source #
SingI d1 => SingI1 (Tuple6Sym2 d1 :: b -> TyFun c (d2 ~> (e ~> (f ~> (a, b, c, d2, e, f)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple6Sym2 d1 x) Source #
(SingI d1, SingI d2) => SingI (Tuple6Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (a, b, c, d3, e, f)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple6Sym2 d1 d2) Source #
SuppressUnusedWarnings (Tuple6Sym2 a6989586621679052279 a6989586621679052280 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym2 a6989586621679052279 a6989586621679052280 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) (a6989586621679052281 :: c) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym2 a6989586621679052279 a6989586621679052280 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) (a6989586621679052281 :: c) = Tuple6Sym3 a6989586621679052279 a6989586621679052280 a6989586621679052281 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type

data Tuple6Sym3 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) :: (~>) d ((~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))) Source #

Instances

Instances details

SingI d1 => SingI2 (Tuple6Sym3 d1 :: b -> c -> TyFun d2 (e ~> (f ~> (a, b, c, d2, e, f))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple6Sym3 d1 x y) Source #
(SingI d1, SingI d2) => SingI1 (Tuple6Sym3 d1 d2 :: c -> TyFun d3 (e ~> (f ~> (a, b, c, d3, e, f))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple6Sym3 d1 d2 x) Source #
(SingI d1, SingI d2, SingI d3) => SingI (Tuple6Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (a, b, c, d4, e, f))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple6Sym3 d1 d2 d3) Source #
SuppressUnusedWarnings (Tuple6Sym3 a6989586621679052279 a6989586621679052280 a6989586621679052281 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym3 a6989586621679052279 a6989586621679052280 a6989586621679052281 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) (a6989586621679052282 :: d) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym3 a6989586621679052279 a6989586621679052280 a6989586621679052281 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) (a6989586621679052282 :: d) = Tuple6Sym4 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type

data Tuple6Sym4 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) :: (~>) e ((~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)) Source #

Instances

Instances details

(SingI d1, SingI d2) => SingI2 (Tuple6Sym4 d1 d2 :: c -> d3 -> TyFun e (f ~> (a, b, c, d3, e, f)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple6Sym4 d1 d2 x y) Source #
(SingI d1, SingI d2, SingI d3) => SingI1 (Tuple6Sym4 d1 d2 d3 :: d4 -> TyFun e (f ~> (a, b, c, d4, e, f)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple6Sym4 d1 d2 d3 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple6Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (a, b, c, d4, e, f)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple6Sym4 d1 d2 d3 d5) Source #
SuppressUnusedWarnings (Tuple6Sym4 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym4 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) (a6989586621679052283 :: e) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym4 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) (a6989586621679052283 :: e) = Tuple6Sym5 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 a6989586621679052283 :: TyFun f (a, b, c, d, e, f) -> Type

data Tuple6Sym5 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) (a6989586621679052283 :: e) :: (~>) f (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type) Source #

Instances

Instances details

(SingI d1, SingI d2, SingI d3) => SingI2 (Tuple6Sym5 d1 d2 d3 :: d4 -> e -> TyFun f (a, b, c, d4, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple6Sym5 d1 d2 d3 x y) Source #
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI1 (Tuple6Sym5 d1 d2 d3 d5 :: e -> TyFun f (a, b, c, d4, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple6Sym5 d1 d2 d3 d5 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple6Sym5 d1 d2 d3 d5 d6 :: TyFun f (a, b, c, d4, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple6Sym5 d1 d2 d3 d5 d6) Source #
SuppressUnusedWarnings (Tuple6Sym5 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 a6989586621679052283 :: TyFun f (a, b, c, d, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple6Sym5 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 a6989586621679052283 :: TyFun k6 (k1, k2, k3, k4, k5, k6) -> Type) (a6989586621679052284 :: k6) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple6Sym5 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 a6989586621679052283 :: TyFun k6 (k1, k2, k3, k4, k5, k6) -> Type) (a6989586621679052284 :: k6) = '(a6989586621679052279, a6989586621679052280, a6989586621679052281, a6989586621679052282, a6989586621679052283, a6989586621679052284)

type family Tuple6Sym6 (a6989586621679052279 :: a) (a6989586621679052280 :: b) (a6989586621679052281 :: c) (a6989586621679052282 :: d) (a6989586621679052283 :: e) (a6989586621679052284 :: f) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type) where ... Source #

Equations

Tuple6Sym6 a6989586621679052279 a6989586621679052280 a6989586621679052281 a6989586621679052282 a6989586621679052283 a6989586621679052284 = '(a6989586621679052279, a6989586621679052280, a6989586621679052281, a6989586621679052282, a6989586621679052283, a6989586621679052284)

data Tuple7Sym0 :: (~>) a ((~>) b ((~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))))))) Source #

Instances

Instances details

SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing Tuple7Sym0 Source #
SuppressUnusedWarnings (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) (a6989586621679052394 :: a) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) (a6989586621679052394 :: a) = Tuple7Sym1 a6989586621679052394 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type

data Tuple7Sym1 (a6989586621679052394 :: a) :: (~>) b ((~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)))))) Source #

Instances

Instances details

SingI1 (Tuple7Sym1 :: a -> TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym1 x) Source #
SingI d1 => SingI (Tuple7Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym1 d1) Source #
SuppressUnusedWarnings (Tuple7Sym1 a6989586621679052394 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym1 a6989586621679052394 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) (a6989586621679052395 :: b) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym1 a6989586621679052394 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) (a6989586621679052395 :: b) = Tuple7Sym2 a6989586621679052394 a6989586621679052395 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type

data Tuple7Sym2 (a6989586621679052394 :: a) (a6989586621679052395 :: b) :: (~>) c ((~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))))) Source #

Instances

Instances details

SingI2 (Tuple7Sym2 :: a -> b -> TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple7Sym2 x y) Source #
SingI d1 => SingI1 (Tuple7Sym2 d1 :: b -> TyFun c (d2 ~> (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym2 d1 x) Source #
(SingI d1, SingI d2) => SingI (Tuple7Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (g ~> (a, b, c, d3, e, f, g))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym2 d1 d2) Source #
SuppressUnusedWarnings (Tuple7Sym2 a6989586621679052394 a6989586621679052395 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym2 a6989586621679052394 a6989586621679052395 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) (a6989586621679052396 :: c) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym2 a6989586621679052394 a6989586621679052395 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) (a6989586621679052396 :: c) = Tuple7Sym3 a6989586621679052394 a6989586621679052395 a6989586621679052396 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type

data Tuple7Sym3 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) :: (~>) d ((~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)))) Source #

Instances

Instances details

SingI d1 => SingI2 (Tuple7Sym3 d1 :: b -> c -> TyFun d2 (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple7Sym3 d1 x y) Source #
(SingI d1, SingI d2) => SingI1 (Tuple7Sym3 d1 d2 :: c -> TyFun d3 (e ~> (f ~> (g ~> (a, b, c, d3, e, f, g)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym3 d1 d2 x) Source #
(SingI d1, SingI d2, SingI d3) => SingI (Tuple7Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (g ~> (a, b, c, d4, e, f, g)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym3 d1 d2 d3) Source #
SuppressUnusedWarnings (Tuple7Sym3 a6989586621679052394 a6989586621679052395 a6989586621679052396 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym3 a6989586621679052394 a6989586621679052395 a6989586621679052396 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) (a6989586621679052397 :: d) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym3 a6989586621679052394 a6989586621679052395 a6989586621679052396 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) (a6989586621679052397 :: d) = Tuple7Sym4 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type

data Tuple7Sym4 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) :: (~>) e ((~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))) Source #

Instances

Instances details

(SingI d1, SingI d2) => SingI2 (Tuple7Sym4 d1 d2 :: c -> d3 -> TyFun e (f ~> (g ~> (a, b, c, d3, e, f, g))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple7Sym4 d1 d2 x y) Source #
(SingI d1, SingI d2, SingI d3) => SingI1 (Tuple7Sym4 d1 d2 d3 :: d4 -> TyFun e (f ~> (g ~> (a, b, c, d4, e, f, g))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym4 d1 d2 d3 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple7Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (g ~> (a, b, c, d4, e, f, g))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym4 d1 d2 d3 d5) Source #
SuppressUnusedWarnings (Tuple7Sym4 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym4 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) (a6989586621679052398 :: e) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym4 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) (a6989586621679052398 :: e) = Tuple7Sym5 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type

data Tuple7Sym5 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) :: (~>) f ((~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)) Source #

Instances

Instances details

(SingI d1, SingI d2, SingI d3) => SingI2 (Tuple7Sym5 d1 d2 d3 :: d4 -> e -> TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple7Sym5 d1 d2 d3 x y) Source #
(SingI d1, SingI d2, SingI d3, SingI d5) => SingI1 (Tuple7Sym5 d1 d2 d3 d5 :: e -> TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym5 d1 d2 d3 d5 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple7Sym5 d1 d2 d3 d5 d6 :: TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym5 d1 d2 d3 d5 d6) Source #
SuppressUnusedWarnings (Tuple7Sym5 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym5 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) (a6989586621679052399 :: f) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym5 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) (a6989586621679052399 :: f) = Tuple7Sym6 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 a6989586621679052399 :: TyFun g (a, b, c, d, e, f, g) -> Type

data Tuple7Sym6 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) (a6989586621679052399 :: f) :: (~>) g (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type) Source #

Instances

Instances details

(SingI d1, SingI d2, SingI d3, SingI d5) => SingI2 (Tuple7Sym6 d1 d2 d3 d5 :: e -> f -> TyFun g (a, b, c, d4, e, f, g) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Tuple7Sym6 d1 d2 d3 d5 x y) Source #
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI1 (Tuple7Sym6 d1 d2 d3 d5 d6 :: f -> TyFun g (a, b, c, d4, e, f, g) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods liftSing :: forall (x :: k1). Sing x -> Sing (Tuple7Sym6 d1 d2 d3 d5 d6 x) Source #
(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d1 d2 d3 d5 d6 d7 :: TyFun g (a, b, c, d4, e, f, g) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods sing :: Sing (Tuple7Sym6 d1 d2 d3 d5 d6 d7) Source #
SuppressUnusedWarnings (Tuple7Sym6 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 a6989586621679052399 :: TyFun g (a, b, c, d, e, f, g) -> Type) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (Tuple7Sym6 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 a6989586621679052399 :: TyFun k7 (k1, k2, k3, k4, k5, k6, k7) -> Type) (a6989586621679052400 :: k7) Source #
Instance details Defined in Data.Singletons.Base.Instances type Apply (Tuple7Sym6 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 a6989586621679052399 :: TyFun k7 (k1, k2, k3, k4, k5, k6, k7) -> Type) (a6989586621679052400 :: k7) = '(a6989586621679052394, a6989586621679052395, a6989586621679052396, a6989586621679052397, a6989586621679052398, a6989586621679052399, a6989586621679052400)

type family Tuple7Sym7 (a6989586621679052394 :: a) (a6989586621679052395 :: b) (a6989586621679052396 :: c) (a6989586621679052397 :: d) (a6989586621679052398 :: e) (a6989586621679052399 :: f) (a6989586621679052400 :: g) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type) where ... Source #

Equations

Tuple7Sym7 a6989586621679052394 a6989586621679052395 a6989586621679052396 a6989586621679052397 a6989586621679052398 a6989586621679052399 a6989586621679052400 = '(a6989586621679052394, a6989586621679052395, a6989586621679052396, a6989586621679052397, a6989586621679052398, a6989586621679052399, a6989586621679052400)

data FstSym0 :: (~>) (a, b) a Source #

Instances

Instances details

SingI (FstSym0 :: TyFun (a, b) a -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing FstSym0 Source #
SuppressUnusedWarnings (FstSym0 :: TyFun (a, b) a -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (FstSym0 :: TyFun (a, b) a -> Type) (a6989586621679180883 :: (a, b)) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (FstSym0 :: TyFun (a, b) a -> Type) (a6989586621679180883 :: (a, b)) = Fst a6989586621679180883

type family FstSym1 (a6989586621679180883 :: (a, b)) :: a where ... Source #

Equations

FstSym1 a6989586621679180883 = Fst a6989586621679180883

data SndSym0 :: (~>) (a, b) b Source #

Instances

Instances details

SingI (SndSym0 :: TyFun (a, b) b -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing SndSym0 Source #
SuppressUnusedWarnings (SndSym0 :: TyFun (a, b) b -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (SndSym0 :: TyFun (a, b) b -> Type) (a6989586621679180879 :: (a, b)) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (SndSym0 :: TyFun (a, b) b -> Type) (a6989586621679180879 :: (a, b)) = Snd a6989586621679180879

type family SndSym1 (a6989586621679180879 :: (a, b)) :: b where ... Source #

Equations

SndSym1 a6989586621679180879 = Snd a6989586621679180879

data CurrySym0 :: (~>) ((~>) (a, b) c) ((~>) a ((~>) b c)) Source #

Instances

Instances details

SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing CurrySym0 Source #
SuppressUnusedWarnings (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) (a6989586621679180871 :: (a, b) ~> c) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) (a6989586621679180871 :: (a, b) ~> c) = CurrySym1 a6989586621679180871

data CurrySym1 (a6989586621679180871 :: (~>) (a, b) c) :: (~>) a ((~>) b c) Source #

Instances

Instances details

SingI1 (CurrySym1 :: ((a, b) ~> c) -> TyFun a (b ~> c) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (CurrySym1 x) Source #
SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing (CurrySym1 d) Source #
SuppressUnusedWarnings (CurrySym1 a6989586621679180871 :: TyFun a (b ~> c) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (CurrySym1 a6989586621679180871 :: TyFun a (b ~> c) -> Type) (a6989586621679180872 :: a) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (CurrySym1 a6989586621679180871 :: TyFun a (b ~> c) -> Type) (a6989586621679180872 :: a) = CurrySym2 a6989586621679180871 a6989586621679180872

data CurrySym2 (a6989586621679180871 :: (~>) (a, b) c) (a6989586621679180872 :: a) :: (~>) b c Source #

Instances

Instances details

SingI d => SingI1 (CurrySym2 d :: a -> TyFun b c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (CurrySym2 d x) Source #
SingI2 (CurrySym2 :: ((a, b) ~> c) -> a -> TyFun b c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (CurrySym2 x y) Source #
(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing (CurrySym2 d1 d2) Source #
SuppressUnusedWarnings (CurrySym2 a6989586621679180871 a6989586621679180872 :: TyFun b c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (CurrySym2 a6989586621679180871 a6989586621679180872 :: TyFun b c -> Type) (a6989586621679180873 :: b) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (CurrySym2 a6989586621679180871 a6989586621679180872 :: TyFun b c -> Type) (a6989586621679180873 :: b) = Curry a6989586621679180871 a6989586621679180872 a6989586621679180873

type family CurrySym3 (a6989586621679180871 :: (~>) (a, b) c) (a6989586621679180872 :: a) (a6989586621679180873 :: b) :: c where ... Source #

Equations

CurrySym3 a6989586621679180871 a6989586621679180872 a6989586621679180873 = Curry a6989586621679180871 a6989586621679180872 a6989586621679180873

data UncurrySym0 :: (~>) ((~>) a ((~>) b c)) ((~>) (a, b) c) Source #

Instances

Instances details

SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing UncurrySym0 Source #
SuppressUnusedWarnings (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) (a6989586621679180863 :: a ~> (b ~> c)) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) (a6989586621679180863 :: a ~> (b ~> c)) = UncurrySym1 a6989586621679180863

data UncurrySym1 (a6989586621679180863 :: (~>) a ((~>) b c)) :: (~>) (a, b) c Source #

Instances

Instances details

SingI1 (UncurrySym1 :: (a ~> (b ~> c)) -> TyFun (a, b) c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (UncurrySym1 x) Source #
SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing (UncurrySym1 d) Source #
SuppressUnusedWarnings (UncurrySym1 a6989586621679180863 :: TyFun (a, b) c -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (UncurrySym1 a6989586621679180863 :: TyFun (a, b) c -> Type) (a6989586621679180864 :: (a, b)) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (UncurrySym1 a6989586621679180863 :: TyFun (a, b) c -> Type) (a6989586621679180864 :: (a, b)) = Uncurry a6989586621679180863 a6989586621679180864

type family UncurrySym2 (a6989586621679180863 :: (~>) a ((~>) b c)) (a6989586621679180864 :: (a, b)) :: c where ... Source #

Equations

UncurrySym2 a6989586621679180863 a6989586621679180864 = Uncurry a6989586621679180863 a6989586621679180864

data SwapSym0 :: (~>) (a, b) (b, a) Source #

Instances

Instances details

SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods sing :: Sing SwapSym0 Source #
SuppressUnusedWarnings (SwapSym0 :: TyFun (a, b) (b, a) -> Type) Source #
Instance details Defined in Data.Tuple.Singletons Methods suppressUnusedWarnings :: () Source #
type Apply (SwapSym0 :: TyFun (a, b) (b, a) -> Type) (a6989586621679180857 :: (a, b)) Source #
Instance details Defined in Data.Tuple.Singletons type Apply (SwapSym0 :: TyFun (a, b) (b, a) -> Type) (a6989586621679180857 :: (a, b)) = Swap a6989586621679180857

type family SwapSym1 (a6989586621679180857 :: (a, b)) :: (b, a) where ... Source #

Equations

SwapSym1 a6989586621679180857 = Swap a6989586621679180857

Singleton definitions

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Singletons from Data.Tuple

Defunctionalization symbols

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Singletons from `Data.Tuple`