Data.Singletons.TH

This module contains basic functionality for deriving your own singletons via Template Haskell. Note that this module does not define any singled definitions on its own. For a version of this module that comes pre-equipped with several singled definitions based on the Prelude, see Data.Singletons.Base.TH from the singletons-base library.

Primary Template Haskell generation functions

singletons :: OptionsMonad q => q [Dec] -> q [Dec]

Make promoted and singled versions of all declarations given, retaining the original declarations. See the README for further explanation.

singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec]

Make promoted and singled versions of all declarations given, discarding the original declarations. Note that a singleton based on a datatype needs the original datatype, so this will fail if it sees any datatype declarations. Classes, instances, and functions are all fine.

genSingletons :: OptionsMonad q => [Name] -> q [Dec]

Generate singled definitions for each of the provided type-level declaration Names. For example, the singletons-th package itself uses

$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])

to generate singletons for Prelude types.

promote :: OptionsMonad q => q [Dec] -> q [Dec]

Promote every declaration given to the type level, retaining the originals. See the README for further explanation.

promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]

Promote each declaration, discarding the originals. Note that a promoted datatype uses the same definition as an original datatype, so this will not work with datatypes. Classes, instances, and functions are all fine.

genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]

Generate defunctionalization symbols for each of the provided type-level declaration Names. See the "Promotion and partial application" section of the singletons README for further explanation.

genPromotions :: OptionsMonad q => [Name] -> q [Dec]

Generate promoted definitions for each of the provided type-level declaration Names. This is generally only useful with classes.

Functions to generate equality instances

promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEq from the given types

promoteEqInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEq from the given type

singEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEq for the given types

singEqInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEq for the given type

singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SDecide, Eq, TestEquality, and TestCoercion for each type in the list.

singDecideInstance :: OptionsMonad q => Name -> q [Dec]

Create instances of SDecide, Eq, TestEquality, and TestCoercion for the given type.

Functions to generate Ord instances

promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for POrd from the given types

promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for POrd from the given type

singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SOrd for the given types

singOrdInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SOrd for the given type

Functions to generate Bounded instances

promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PBounded from the given types

promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PBounded from the given type

singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SBounded for the given types

singBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SBounded for the given type

Functions to generate Enum instances

promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEnum from the given types

promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEnum from the given type

singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEnum for the given types

singEnumInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEnum for the given type

Functions to generate Show instances

promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PShow from the given types

promoteShowInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PShow from the given type

singShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SShow for the given types

(Not to be confused with showSingInstances.)

singShowInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SShow for the given type

(Not to be confused with showShowInstance.)

showSingInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of Show for the given singleton types

(Not to be confused with singShowInstances.)

showSingInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of Show for the given singleton type

(Not to be confused with singShowInstance.)

Utility functions

singITyConInstances :: DsMonad q => [Int] -> q [Dec]

Create an instance for SingI TyCon{N}, where N is the positive number provided as an argument.

Note that the generated code requires the use of the QuantifiedConstraints language extension.

singITyConInstance :: DsMonad q => Int -> q Dec

Create an instance for SingI TyCon{N}, where N is the positive number provided as an argument.

Note that the generated code requires the use of the QuantifiedConstraints language extension.

cases

Arguments

:: DsMonad q

=> Name

The head of the type of the scrutinee. (e.g., ''SBool)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp

sCases

Arguments

:: OptionsMonad q

=> Name

The head of the type the scrutinee's type is based on. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp

The function sCases generates a case expression where each right-hand side is identical. This may be useful if the type-checker requires knowledge of which constructor is used to satisfy equality or type-class constraints, but where each constructor is treated the same.

For sCases, unlike cases, the scrutinee is a singleton. But make sure to pass in the name of the original datatype, preferring ''Maybe over ''SMaybe. In other words, sCases ''Maybe is equivalent to cases ''SMaybe.

Basic singleton definitions

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

pattern FromSing :: forall k (a :: k). SingKind k => Sing a -> Demote k

pattern SLambda2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f

pattern SLambda3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). SingFunction3 f -> Sing f

pattern SLambda4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). SingFunction4 f -> Sing f

pattern SLambda5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). SingFunction5 f -> Sing f

pattern SLambda6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). SingFunction6 f -> Sing f

pattern SLambda7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). SingFunction7 f -> Sing f

pattern SLambda8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). SingFunction8 f -> Sing f

pattern Sing :: forall k (a :: k). () => SingI a => Sing a

applySing2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f

applySing3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f

applySing4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f

applySing5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f

applySing6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f

applySing7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f

applySing8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f

demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k

demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => Demote k2

demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => Demote k3

sing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Sing (f x)

sing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2). (SingI2 f, SingI x, SingI y) => Sing (f x y)

singByProxy :: forall {k} (a :: k) proxy. SingI a => proxy a -> Sing a

singByProxy# :: forall {k} (a :: k). SingI a => Proxy# a -> Sing a

singByProxy1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) proxy. (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)

singByProxy1# :: forall {k1} {k} (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)

singByProxy2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) proxy. (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)

singByProxy2# :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2). (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)

singFun1 :: forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f

singFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f

singFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). SingFunction3 f -> Sing f

singFun4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). SingFunction4 f -> Sing f

singFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). SingFunction5 f -> Sing f

singFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). SingFunction6 f -> Sing f

singFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). SingFunction7 f -> Sing f

singFun8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). SingFunction8 f -> Sing f

singInstance :: forall k (a :: k). Sing a -> SingInstance a

singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)

singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x))

singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y))

unSingFun1 :: forall {a1} {b} (f :: a1 ~> b). Sing f -> SingFunction1 f

unSingFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f

unSingFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f

unSingFun4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f

unSingFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f

unSingFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f

unSingFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f

unSingFun8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f

usingSingI1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r

usingSingI2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r

withSing :: forall {k} (a :: k) b. SingI a => (Sing a -> b) -> b

withSing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) b. (SingI1 f, SingI x) => (Sing (f x) -> b) -> b

withSing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) b. (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b

withSingI :: forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r

withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r

data Proxy (t :: k)

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the undefined :: a idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> Type)

Defined in GHC.Internal.Generics

Associated Types

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Defined in GHC.Internal.Generics

type Rep1 (Proxy :: k -> Type) = D1 ('MetaData "Proxy" "GHC.Internal.Data.Proxy" "ghc-internal" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: k -> Type))

Methods

from1 :: forall (a :: k). Proxy a -> Rep1 (Proxy :: k -> Type) a

to1 :: forall (a :: k). Rep1 (Proxy :: k -> Type) a -> Proxy a

Eq1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftEq :: (a -> b -> Bool) -> Proxy a -> Proxy b -> Bool

Ord1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftCompare :: (a -> b -> Ordering) -> Proxy a -> Proxy b -> Ordering

Read1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Proxy a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Proxy a]

Show1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy a] -> ShowS

Contravariant (Proxy :: Type -> Type)

Defined in Data.Functor.Contravariant

Methods

contramap :: (a' -> a) -> Proxy a -> Proxy a'

(>$) :: b -> Proxy b -> Proxy a

NFData1 (Proxy :: Type -> Type)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a -> ()) -> Proxy a -> ()

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in GHC.Internal.Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

pure :: a -> Proxy a

(<*>) :: Proxy (a -> b) -> Proxy a -> Proxy b

liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c

(*>) :: Proxy a -> Proxy b -> Proxy b

(<*) :: Proxy a -> Proxy b -> Proxy a

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in GHC.Internal.Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Foldable

Methods

fold :: Monoid m => Proxy m -> m

foldMap :: Monoid m => (a -> m) -> Proxy a -> m

foldMap' :: Monoid m => (a -> m) -> Proxy a -> m

foldr :: (a -> b -> b) -> b -> Proxy a -> b

foldr' :: (a -> b -> b) -> b -> Proxy a -> b

foldl :: (b -> a -> b) -> b -> Proxy a -> b

foldl' :: (b -> a -> b) -> b -> Proxy a -> b

foldr1 :: (a -> a -> a) -> Proxy a -> a

foldl1 :: (a -> a -> a) -> Proxy a -> a

toList :: Proxy a -> [a]

null :: Proxy a -> Bool

length :: Proxy a -> Int

elem :: Eq a => a -> Proxy a -> Bool

maximum :: Ord a => Proxy a -> a

minimum :: Ord a => Proxy a -> a

sum :: Num a => Proxy a -> a

product :: Num a => Proxy a -> a

Traversable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b)

sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a)

mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b)

sequence :: Monad m => Proxy (m a) -> m (Proxy a)

Hashable1 (Proxy :: Type -> Type)

Defined in Data.Hashable.Class

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Proxy a -> Int

NFData (Proxy a)

Since: deepseq-1.4.0.0

Defined in Control.DeepSeq

Methods

rnf :: Proxy a -> ()

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in GHC.Internal.Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Data t => Data (Proxy t)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy t -> c (Proxy t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy t)

toConstr :: Proxy t -> Constr

dataTypeOf :: Proxy t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Proxy t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Proxy t))

gmapT :: (forall b. Data b => b -> b) -> Proxy t -> Proxy t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQ :: (forall d. Data d => d -> u) -> Proxy t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

succ :: Proxy s -> Proxy s

pred :: Proxy s -> Proxy s

toEnum :: Int -> Proxy s

fromEnum :: Proxy s -> Int

enumFrom :: Proxy s -> [Proxy s]

enumFromThen :: Proxy s -> Proxy s -> [Proxy s]

enumFromTo :: Proxy s -> Proxy s -> [Proxy s]

enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s]

Generic (Proxy t)

Defined in GHC.Internal.Generics

Associated Types

type Rep (Proxy t)

Since: base-4.6.0.0

Defined in GHC.Internal.Generics

type Rep (Proxy t) = D1 ('MetaData "Proxy" "GHC.Internal.Data.Proxy" "ghc-internal" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Proxy t -> Rep (Proxy t) x

to :: Rep (Proxy t) x -> Proxy t

Ix (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

Read (Proxy t)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

readsPrec :: Int -> ReadS (Proxy t)

readList :: ReadS [Proxy t]

readPrec :: ReadPrec (Proxy t)

readListPrec :: ReadPrec [Proxy t]

Show (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Eq (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Ord (Proxy s)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering

(<) :: Proxy s -> Proxy s -> Bool

(<=) :: Proxy s -> Proxy s -> Bool

(>) :: Proxy s -> Proxy s -> Bool

(>=) :: Proxy s -> Proxy s -> Bool

max :: Proxy s -> Proxy s -> Proxy s

min :: Proxy s -> Proxy s -> Proxy s

Hashable (Proxy a)

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> Proxy a -> Int

hash :: Proxy a -> Int

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Defined in GHC.Internal.Generics

type Rep1 (Proxy :: k -> Type) = D1 ('MetaData "Proxy" "GHC.Internal.Data.Proxy" "ghc-internal" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: k -> Type))

type Rep (Proxy t)

Since: base-4.6.0.0

Defined in GHC.Internal.Generics

type Rep (Proxy t) = D1 ('MetaData "Proxy" "GHC.Internal.Data.Proxy" "ghc-internal" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: Type -> Type))

type (@@) (a :: k1 ~> k2) (b :: k1) = Apply a b

data (@@@#@$) (a1 :: TyFun (a ~> b) (a ~> b))

Instances

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f

data (a1 :: a ~> b) @@@#@$$ (b1 :: TyFun a b)

Instances

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) = f @@ x

type (@@@#@$$$) (f :: a ~> b) (x :: a) = f @@ x

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

Instances

type Apply DemoteSym0 (x :: Type)

Defined in Data.Singletons

type Apply DemoteSym0 (x :: Type) = Demote x

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)

Defined in Data.Singletons

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)

Defined in Data.Singletons

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k)

Defined in Data.Singletons

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) = SameKind x y

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) = f @@ x

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) = Apply f x

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

type Apply (TyCon f :: k1 ~> k3) (x :: k1)

Defined in Data.Singletons

type Apply (TyCon f :: k1 ~> k3) (x :: k1) = ApplyTyCon f @@ x

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4)

Defined in Data.Singletons

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

Defined in Data.Singletons

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

data ApplySym0 (a1 :: TyFun (a ~> b) (a ~> b))

Instances

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

data ApplySym1 (a1 :: a ~> b) (b1 :: TyFun a b)

Instances

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) = Apply f x

type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x

type family ApplyTyCon :: (k1 -> k2) -> TyFun k1 unmatchable_fun -> Type where ...

Equations

ApplyTyCon = ApplyTyConAux2 :: (k1 -> k2 -> k3) -> TyFun k1 unmatchable_fun -> Type

ApplyTyCon = ApplyTyConAux1 :: (k1 -> k2) -> TyFun k1 k2 -> Type

data ApplyTyConAux1 (a :: k1 -> k2) (b :: TyFun k1 k2)

Instances

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

data ApplyTyConAux2 (a :: k1 -> k2 -> k3) (b :: TyFun k1 unmatchable_fun)

Instances

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4)

Defined in Data.Singletons

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)

type family Demote k = (r :: Type) | r -> k

Instances

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

data DemoteSym0 (a :: TyFun Type Type)

Instances

type Apply DemoteSym0 (x :: Type)

Defined in Data.Singletons

type Apply DemoteSym0 (x :: Type) = Demote x

type DemoteSym1 x = Demote x

type KindOf (a :: k) = k

data KindOfSym0 (a :: TyFun k Type)

Instances

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)

Defined in Data.Singletons

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x

type KindOfSym1 (x :: k) = KindOf x

newtype SLambda (f :: k1 ~> k2)

Constructors

SLambda

Fields

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

newtype SWrappedSing (a1 :: WrappedSing a) where

Constructors

SWrapSing

Fields

• :: forall k (a :: k) (a1 :: WrappedSing a). { sUnwrapSing :: Sing a
•    } -> SWrappedSing a1

type SameKind (a :: k) (b :: k) = ()

data SameKindSym0 (a :: TyFun k (k ~> Constraint))

Instances

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

Defined in Data.Singletons

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

data SameKindSym1 (a :: k) (b :: TyFun k Constraint)

Instances

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k)

Defined in Data.Singletons

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) = SameKind x y

type SameKindSym2 (x :: k) (y :: k) = SameKind x y

type family Sing :: k -> Type

Instances

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type

type SingFunction1 (f :: a1 ~> b) = forall (t :: a1). Sing t -> Sing (f @@ t)

type SingFunction2 (f :: a1 ~> (a2 ~> b)) = forall (t1 :: a1) (t2 :: a2). Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)

type SingFunction3 (f :: a1 ~> (a2 ~> (a3 ~> b))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3). Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)

type SingFunction4 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)

type SingFunction5 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)

type SingFunction6 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)

type SingFunction7 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)

type SingFunction8 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7) (t8 :: a8). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing ((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8)

class SingI (a :: k) where

Methods

sing :: Sing a

Instances

SingI a => SingI ('WrapSing s :: WrappedSing a)

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s :: WrappedSing a)

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(SingI fst, SingI b) => SingI (a ':&: b :: Sigma s t)

Defined in Data.Singletons.Sigma

Methods

sing :: Sing (a ':&: b :: Sigma s t)

(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

class (forall (x :: k1). SingI x => SingI (f x)) => SingI1 (f :: k1 -> k2) where

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (f x)

class (forall (x :: k1) (y :: k2). (SingI x, SingI y) => SingI (f x y)) => SingI2 (f :: k1 -> k2 -> k3) where

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (f x y)

data SingInstance (a :: k) where

Constructors

SingInstance :: forall {k} (a :: k). SingI a => SingInstance a

class SingKind k where

Associated Types

type Demote k = (r :: Type) | r -> k

Methods

fromSing :: forall (a :: k). Sing a -> Demote k

toSing :: Demote k -> SomeSing k

Instances

SingKind (WrappedSing a)

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

Methods

fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a)

toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

Methods

fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2)

toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)

data SomeSing k where

Constructors

SomeSing :: forall k (a :: k). Sing a -> SomeSing k

data family TyCon :: forall k1 k2 unmatchable_fun. (k1 -> k2) -> unmatchable_fun

Instances

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

type Apply (TyCon f :: k1 ~> k3) (x :: k1)

Defined in Data.Singletons

type Apply (TyCon f :: k1 ~> k3) (x :: k1) = ApplyTyCon f @@ x

type TyCon1 = TyCon

type TyCon2 = TyCon

type TyCon3 = TyCon

type TyCon4 = TyCon

type TyCon5 = TyCon

type TyCon6 = TyCon

type TyCon7 = TyCon

type TyCon8 = TyCon

data TyFun a b

Instances

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

Methods

fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2)

toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

type Apply (TyCon f :: k1 ~> k3) (x :: k1)

Defined in Data.Singletons

type Apply (TyCon f :: k1 ~> k3) (x :: k1) = ApplyTyCon f @@ x

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

Defined in Data.Singletons

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

type Sing

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

Defined in Data.Singletons

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

type family UnwrapSing (ws :: WrappedSing a) :: Sing a where ...

Equations

UnwrapSing ('WrapSing s :: WrappedSing a) = s

newtype WrappedSing (a :: k) where

Constructors

WrapSing

Fields

• :: forall k (a :: k). { unwrapSing :: Sing a
•    } -> WrappedSing a

Instances

SingKind (WrappedSing a)

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

Methods

fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a)

toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)

SingI a => SingI ('WrapSing s :: WrappedSing a)

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s :: WrappedSing a)

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

type (~>) a b = TyFun a b -> Type

data (~>@#@$) (a :: TyFun Type (Type ~> Type))

Instances

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

data a ~>@#@$$ (b :: TyFun Type Type)

Instances

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)

Defined in Data.Singletons

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

type (~>@#@$$$) x y = x ~> y

Auxiliary definitions

class SDecide k where

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)

data (a :: k) :~: (b :: k) where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a

Instances

TestCoercion ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: Type -> Type -> Type)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

NFData (a :~: b)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

Eq (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b)

Since: base-4.7.0.0

Defined in GHC.Internal.Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

data Void

Uninhabited data type

Since: base-4.8.0.0

Instances

NFData Void

Defined as rnf = absurd.

Since: deepseq-1.4.0.0

Defined in Control.DeepSeq

Methods

rnf :: Void -> ()

Semigroup Void

Since: base-4.9.0.0

Defined in GHC.Internal.Base

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Data Void

Since: base-4.8.0.0

Defined in GHC.Internal.Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void

toConstr :: Void -> Constr

dataTypeOf :: Void -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void)

gmapT :: (forall b. Data b => b -> b) -> Void -> Void

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQ :: (forall d. Data d => d -> u) -> Void -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

Generic Void

Defined in GHC.Internal.Generics

Associated Types

type Rep Void

Since: base-4.8.0.0

Defined in GHC.Internal.Generics

type Rep Void = D1 ('MetaData "Void" "GHC.Internal.Base" "ghc-internal" 'False) (V1 :: Type -> Type)

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Since: base-4.8.0.0

Defined in GHC.Internal.Read

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Since: base-4.8.0.0

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

Eq Void

Since: base-4.8.0.0

Defined in GHC.Internal.Base

Methods

(==) :: Void -> Void -> Bool

(/=) :: Void -> Void -> Bool

Ord Void

Since: base-4.8.0.0

Defined in GHC.Internal.Base

Methods

compare :: Void -> Void -> Ordering

(<) :: Void -> Void -> Bool

(<=) :: Void -> Void -> Bool

(>) :: Void -> Void -> Bool

(>=) :: Void -> Void -> Bool

max :: Void -> Void -> Void

min :: Void -> Void -> Void

Hashable Void

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> Void -> Int

hash :: Void -> Int

Lift Void

Since: template-haskell-2.15.0.0

Defined in GHC.Internal.TH.Lift

Methods

lift :: Quote m => Void -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Void -> Code m Void

type Rep Void

Since: base-4.8.0.0

Defined in GHC.Internal.Generics

type Rep Void = D1 ('MetaData "Void" "GHC.Internal.Base" "ghc-internal" 'False) (V1 :: Type -> Type)

type Refuted a = a -> Void

data Decision a

Constructors

Proved a

Disproved (Refuted a)

class SuppressUnusedWarnings (t :: k) where

This class (which users should never see) is to be instantiated in order to use an otherwise-unused data constructor, such as the "kind-inference" data constructor for defunctionalization symbols.

Methods

suppressUnusedWarnings :: ()