singletons-2.5.1: A framework for generating singleton types

Copyright | (C) 2018 Ryan Scott
License | BSD-style (see LICENSE)
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu)
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.Prelude.Const

Contents

- The `Const` singleton
- Defunctionalization symbols
- Orphan instances

Description

Exports the promoted and singled versions of the `Const` data type.

Synopsis

- data family Sing :: k -> Type
- type SConst = (Sing :: Const a b -> Type)
- type family GetConst (x :: Const a b) :: a where ...
- data ConstSym0 :: forall (a6989586621679091214 :: Type) k6989586621679091213 (b6989586621679091215 :: k6989586621679091213). (~>) a6989586621679091214 (Const (a6989586621679091214 :: Type) (b6989586621679091215 :: k6989586621679091213))
- type ConstSym1 (t6989586621680705928 :: a6989586621679091214) = Const t6989586621680705928
- data GetConstSym0 :: forall a6989586621680706243 b6989586621680706244. (~>) (Const a6989586621680706243 b6989586621680706244) a6989586621680706243
- type GetConstSym1 (x6989586621680706245 :: Const a6989586621680706243 b6989586621680706244) = GetConst x6989586621680706245

# The `Const` singleton

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

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

data Sing (a :: Ordering) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

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

data Sing (n :: Nat) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

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

data Sing (n :: Symbol) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

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

data Sing (a :: Any) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

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

data Sing (a :: PErrorMessage) Source # |

Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

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

newtype Sing (a :: TYPE rep) Source #

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

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

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

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

Instance details

Defined in Data.Singletons.Internal

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

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

}

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

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

Instance details

Defined in Data.Singletons.Prelude.Instances

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

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

type SConst = (Sing :: Const a b -> Type) Source #

type family GetConst (x :: Const a b) :: a where ... Source #

Equations

GetConst (Const x) = x |

# Defunctionalization symbols

data ConstSym0 :: forall (a6989586621679091214 :: Type) k6989586621679091213 (b6989586621679091215 :: k6989586621679091213). (~>) a6989586621679091214 (Const (a6989586621679091214 :: Type) (b6989586621679091215 :: k6989586621679091213)) Source #

Instances

SingI (ConstSym0 :: TyFun a6989586621679091214 (Const a6989586621679091214 b6989586621679091215) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 Source #
SuppressUnusedWarnings (ConstSym0 :: TyFun a6989586621679091214 (Const a6989586621679091214 b6989586621679091215) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () Source #
type Apply (ConstSym0 :: TyFun a (Const a b6989586621679091215) -> Type) (t6989586621680705928 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Apply (ConstSym0 :: TyFun a (Const a b6989586621679091215) -> Type) (t6989586621680705928 :: a) = (Const t6989586621680705928 :: Const a b6989586621679091215)

type ConstSym1 (t6989586621680705928 :: a6989586621679091214) = Const t6989586621680705928 Source #

data GetConstSym0 :: forall a6989586621680706243 b6989586621680706244. (~>) (Const a6989586621680706243 b6989586621680706244) a6989586621680706243 Source #

Instances

SuppressUnusedWarnings (GetConstSym0 :: TyFun (Const a6989586621680706243 b6989586621680706244) a6989586621680706243 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () Source #
type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680706245 :: Const a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680706245 :: Const a b) = GetConst x6989586621680706245

type GetConstSym1 (x6989586621680706245 :: Const a6989586621680706243 b6989586621680706244) = GetConst x6989586621680706245 Source #

# Orphan instances

SMonoid m => SApplicative (Const m :: Type -> Type) Source # |
Instance details Methods sPure :: Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source #
SFunctor (Const m :: Type -> Type) Source # |
Instance details Methods sFmap :: Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
PApplicative (Const m :: Type -> Type) Source # |
Instance details Associated Types type Pure arg :: f a Source # type arg <*> arg :: f b Source # type LiftA2 arg arg arg :: f c Source # type arg *> arg :: f b Source # type arg <* arg :: f a Source #
PFunctor (Const m :: Type -> Type) Source # |
Instance details Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
SFoldable (Const m :: Type -> Type) Source # |

Instance details

Methods

sFold :: SMonoid m0 => Sing t -> Sing (Apply FoldSym0 t) Source #

sFoldMap :: SMonoid m0 => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source #

sFoldr :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source #

sFoldr' :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source #

sFoldl :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source #

sFoldl' :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source #

sFoldr1 :: Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source #

sFoldl1 :: Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source #

sToList :: Sing t -> Sing (Apply ToListSym0 t) Source #

sNull :: Sing t -> Sing (Apply NullSym0 t) Source #

sLength :: Sing t -> Sing (Apply LengthSym0 t) Source #

sElem :: SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source #

sMaximum :: SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source #

sMinimum :: SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source #

sSum :: SNum a => Sing t -> Sing (Apply SumSym0 t) Source #

sProduct :: SNum a => Sing t -> Sing (Apply ProductSym0 t) Source #

PFoldable (Const m :: Type -> Type) Source # |

Instance details

Associated Types

type Fold arg :: m Source #

type FoldMap arg arg :: m Source #

type Foldr arg arg arg :: b Source #

type Foldr' arg arg arg :: b Source #

type Foldl arg arg arg :: b Source #

type Foldl' arg arg arg :: b Source #

type Foldr1 arg arg :: a Source #

type Foldl1 arg arg :: a Source #

type ToList arg :: [a] Source #

type Null arg :: Bool Source #

type Length arg :: Nat Source #

type Elem arg arg :: Bool Source #

type Maximum arg :: a Source #

type Minimum arg :: a Source #

type Sum arg :: a Source #

type Product arg :: a Source #

SingI (TyCon1 (Const :: k1 -> Const k1 b) :: k1 ~> Const k1 b) Source # |
Instance details Methods sing :: Sing (TyCon1 Const0) Source #
SingKind a => SingKind (Const a b) Source # |
Instance details Associated Types type Demote (Const a b) = (r :: Type) Source # Methods fromSing :: Sing a0 -> Demote (Const a b) Source # toSing :: Demote (Const a b) -> SomeSing (Const a b) Source #
SDecide a => SDecide (Const a b) Source # |
Instance details Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
PEq (Const a b) Source # |
Instance details Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq a => SEq (Const a b) Source # |
Instance details Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #
SOrd a => SOrd (Const a b) Source # |

Instance details

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

POrd (Const a b) Source # |
Instance details Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SNum a => SNum (Const a b) Source # |

Instance details

Methods

(%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source #

(%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source #

(%*) :: Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) Source #

sNegate :: Sing t -> Sing (Apply NegateSym0 t) Source #

sAbs :: Sing t -> Sing (Apply AbsSym0 t) Source #

sSignum :: Sing t -> Sing (Apply SignumSym0 t) Source #

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) Source #

PNum (Const a b) Source # |
Instance details Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
SBounded a => SBounded (Const a b) Source # |
Instance details Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
PBounded (Const a b) Source # |
Instance details Associated Types type MinBound :: a Source # type MaxBound :: a Source #
SEnum a => SEnum (Const a b) Source # |

Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) Source #

sPred :: Sing t -> Sing (Apply PredSym0 t) Source #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) Source #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) Source #

sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source #

sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #

PEnum (Const a b) Source # |
Instance details Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
SSemigroup a => SSemigroup (Const a b) Source # |
Instance details Methods (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: Sing t -> Sing (Apply SconcatSym0 t) Source #
PSemigroup (Const a b) Source # |
Instance details Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow a => SShow (Const a b) Source # |
Instance details Methods sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow (Const a b) Source # |
Instance details Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
SMonoid a => SMonoid (Const a b) Source # |
Instance details Methods sMempty :: Sing MemptySym0 Source # sMappend :: Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) Source # sMconcat :: Sing t -> Sing (Apply MconcatSym0 t) Source #
PMonoid (Const a b) Source # |
Instance details Associated Types type Mempty :: a Source # type Mappend arg arg :: a Source # type Mconcat arg :: a Source #
SingI a2 => SingI (Const a2 :: Const a1 b) Source # |
Instance details Methods sing :: Sing (Const0 a2) Source #