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

Data.Singletons.TH

Contents

Primary Template Haskell generation functions
Basic singleton definitions
Auxiliary definitions

Description

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.

Synopsis

singletons :: OptionsMonad q => q [Dec] -> q [Dec]
singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec]
genSingletons :: OptionsMonad q => [Name] -> q [Dec]
promote :: OptionsMonad q => q [Dec] -> q [Dec]
promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]
genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]
genPromotions :: OptionsMonad q => [Name] -> q [Dec]
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
singEqInstances :: OptionsMonad q => [Name] -> q [Dec]
singEqInstance :: OptionsMonad q => Name -> q [Dec]
singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]
singDecideInstance :: OptionsMonad q => Name -> q [Dec]
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]
singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
singOrdInstance :: OptionsMonad q => Name -> q [Dec]
promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]
singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
singBoundedInstance :: OptionsMonad q => Name -> q [Dec]
promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]
singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
singEnumInstance :: OptionsMonad q => Name -> q [Dec]
promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteShowInstance :: OptionsMonad q => Name -> q [Dec]
singShowInstances :: OptionsMonad q => [Name] -> q [Dec]
singShowInstance :: OptionsMonad q => Name -> q [Dec]
showSingInstances :: OptionsMonad q => [Name] -> q [Dec]
showSingInstance :: OptionsMonad q => Name -> q [Dec]
singITyConInstances :: DsMonad q => [Int] -> q [Dec]
singITyConInstance :: DsMonad q => Int -> q Dec
cases :: DsMonad q => Name -> q Exp -> q Exp -> q Exp
sCases :: OptionsMonad q => Name -> q Exp -> q Exp -> q Exp
data family TyCon :: (k1 -> k2) -> unmatchable_fun
data Proxy (t :: k) = Proxy
class SingKind k where
- type Demote k = (r :: Type) | r -> k
- fromSing :: forall (a :: k). Sing a -> Demote k
- toSing :: Demote k -> SomeSing k
class SingI (a :: k) where
- sing :: Sing a
type family Sing :: k -> Type
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
type (~>) a b = TyFun a b -> Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type family ApplyTyCon :: (k1 -> k2) -> TyFun k1 unmatchable_fun -> Type where ...
data ApplyTyConAux1 (a :: k1 -> k2) (b :: TyFun k1 k2)
class (forall (x :: k1). SingI x => SingI (f x)) => SingI1 (f :: k1 -> k2) where
- 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
- liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (f x y)
type family Demote k = (r :: Type) | r -> k
withSingI :: forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
data SomeSing k where
- SomeSing :: forall k (a :: k). Sing a -> SomeSing k
newtype SLambda (f :: k1 ~> k2) = SLambda {
- applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)
}
type SameKind (a :: k) (b :: k) = ()
demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k
type (@@) (a :: k1 ~> k2) (b :: k1) = Apply a b
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
data (@@@#@$) (a1 :: TyFun (a ~> b) (a ~> b))
data (a1 :: a ~> b) @@@#@$$ (b1 :: TyFun a b)
type (@@@#@$$$) (f :: a ~> b) (x :: a) = f @@ x
data (~>@#@$) (a :: TyFun Type (Type ~> Type))
data a ~>@#@$$ (b :: TyFun Type Type)
type (~>@#@$$$) x y = x ~> y
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
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
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
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
data ApplySym0 (a1 :: TyFun (a ~> b) (a ~> b))
data ApplySym1 (a1 :: a ~> b) (b1 :: TyFun a b)
type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
data ApplyTyConAux2 (a :: k1 -> k2 -> k3) (b :: TyFun k1 unmatchable_fun)
data DemoteSym0 (a :: TyFun Type Type)
type DemoteSym1 x = Demote x
type KindOf (a :: k) = k
data KindOfSym0 (a :: TyFun k Type)
type KindOfSym1 (x :: k) = KindOf x
newtype SWrappedSing (a1 :: WrappedSing a) where
- SWrapSing :: forall k (a :: k) (a1 :: WrappedSing a). {..} -> SWrappedSing a1
data SameKindSym0 (a :: TyFun k (k ~> Constraint))
data SameKindSym1 (a :: k) (b :: TyFun k Constraint)
type SameKindSym2 (x :: k) (y :: k) = SameKind x y
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)
data SingInstance (a :: k) where
- SingInstance :: forall {k} (a :: k). SingI a => SingInstance a
type TyCon1 = TyCon :: (k1 -> k2) -> k1 ~> k2
type TyCon2 = TyCon :: (k1 -> k2 -> k3) -> k1 ~> (k2 ~> k3)
type TyCon3 = TyCon :: (k1 -> k2 -> k3 -> k4) -> k1 ~> (k2 ~> (k3 ~> k4))
type TyCon4 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> k5)))
type TyCon5 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k6))))
type TyCon6 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k7)))))
type TyCon7 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k8))))))
type TyCon8 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k9)))))))
data TyFun a b
type family UnwrapSing (ws :: WrappedSing a) :: Sing a where ...
newtype WrappedSing (a :: k) where
- WrapSing :: forall k (a :: k). {..} -> WrappedSing a
class SDecide k where
- (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
data (a :: k) :~: (b :: k) where
- Refl :: forall {k} (a :: k). a :~: a
data Void
type Refuted a = a -> Void
data Decision a
- = Proved a
- | Disproved (Refuted a)
class SuppressUnusedWarnings (t :: k) where
- suppressUnusedWarnings :: ()

Primary Template Haskell generation functions

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

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] Source #

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] Source #

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] Source #

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

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

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] Source #

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] Source #

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] Source #

Produce instances for PEq from the given types

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

Produce an instance for PEq from the given type

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

Create instances of SEq for the given types

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

Create instance of SEq for the given type

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

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

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

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

Functions to generate `Ord` instances

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

Produce instances for POrd from the given types

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

Produce an instance for POrd from the given type

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

Create instances of SOrd for the given types

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

Create instance of SOrd for the given type

Functions to generate `Bounded` instances

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

Produce instances for PBounded from the given types

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

Produce an instance for PBounded from the given type

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

Create instances of SBounded for the given types

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

Create instance of SBounded for the given type

Functions to generate `Enum` instances

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

Produce instances for PEnum from the given types

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

Produce an instance for PEnum from the given type

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

Create instances of SEnum for the given types

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

Create instance of SEnum for the given type

Functions to generate `Show` instances

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

Produce instances for PShow from the given types

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

Produce an instance for PShow from the given type

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

Create instances of SShow for the given types

(Not to be confused with showSingInstances.)

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

Create instance of SShow for the given type

(Not to be confused with showShowInstance.)

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

Create instances of Show for the given singleton types

(Not to be confused with singShowInstances.)

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

Create instance of Show for the given singleton type

(Not to be confused with singShowInstance.)

Utility functions

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

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 Source #

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 Source #

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 Source #

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

data family TyCon :: (k1 -> k2) -> unmatchable_fun #

Instances

Instances details

(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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon8 f) #
type Apply (TyCon f :: k1 ~> k5) (x :: k1)
Instance details Defined in Data.Singletons type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x

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

Instances details

Generic1 (Proxy :: k -> Type)

Instance details

Defined in GHC.Generics

Associated Types

type Rep1 (Proxy :: k -> Type)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> Type) = D1 ('MetaData "Proxy" "Data.Proxy" "base" '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 #

MonadZip (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Control.Monad.Zip

Methods

mzip :: Proxy a -> Proxy b -> Proxy (a, b) #

mzipWith :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c #

munzip :: Proxy (a, b) -> (Proxy a, Proxy b) #

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in 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 #

Eq1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

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

Instance details

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

Instance details

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

Instance details

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)

Instance details

Defined in Data.Functor.Contravariant

Methods

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

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

Traversable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in 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) #

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in 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

Instance details

Defined in 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

Instance details

Defined in 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

Instance details

Defined in 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

Instance details

Defined in Data.Proxy

Methods

mzero :: Proxy a #

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

NFData1 (Proxy :: Type -> Type)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

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

Data t => Data (Proxy t)

Since: base-4.7.0.0

Instance details

Defined in 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) #

Monoid (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in 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

Instance details

Defined in Data.Proxy

Methods

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

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

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

Bounded (Proxy t)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

minBound :: Proxy t #

maxBound :: Proxy t #

Enum (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in 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)

Instance details

Defined in GHC.Generics

Associated Types

type Rep (Proxy t)	Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 ('MetaData "Proxy" "Data.Proxy" "base" '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

Instance details

Defined in 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

Instance details

Defined in 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

Instance details

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS #

show :: Proxy s -> String #

showList :: [Proxy s] -> ShowS #

NFData (Proxy a)

Since: deepseq-1.4.0.0

Instance details

Defined in Control.DeepSeq

Methods

rnf :: Proxy a -> () #

Eq (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

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

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

Ord (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in 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 #

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Instance details

Defined in GHC.Generics

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

type Rep (Proxy t)

Since: base-4.6.0.0

Instance details

Defined in GHC.Generics

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

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

Instances details

SingKind (WrappedSing a)

Instance details

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a)
Instance details 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)

Instance details

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2)
Instance details 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) #

class SingI (a :: k) where #

Methods

sing :: Sing a #

Instances

Instances details

SingI a => SingI ('WrapSing s :: WrappedSing a)
Instance details 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)
Instance details 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)
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon2 f) #
(SingI fst, SingI b) => SingI (a ':&: b :: Sigma s t)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon8 f) #

type family Sing :: k -> Type #

Instances

Instances details

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
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type

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

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

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

Instances

Instances details

type Apply DemoteSym0 (x :: Type)
Instance details Defined in Data.Singletons type Apply DemoteSym0 (x :: Type) = Demote x
type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)
Instance details Defined in Data.Singletons type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y
type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details 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)
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x
type Apply (TyCon f :: k1 ~> k5) (x :: k1)
Instance details Defined in Data.Singletons type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x
type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4)
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)
type Apply (~>@#@$) (x :: Type)
Instance details Defined in Data.Singletons type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x
type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)
Instance details 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)
Instance details 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)
Instance details Defined in Data.Singletons type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

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

Instances details

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1)
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

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) #

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

Instances

Instances details

type Demote (WrappedSing a)
Instance details Defined in Data.Singletons type Demote (WrappedSing a) = WrappedSing a
type Demote (k1 ~> k2)
Instance details Defined in Data.Singletons type Demote (k1 ~> k2) = Demote k1 -> Demote k2

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

data SomeSing k where #

Constructors

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

newtype SLambda (f :: k1 ~> k2) #

Constructors

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

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

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

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

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

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

Instances

Instances details

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)
Instance details 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

Instances details

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1)
Instance details Defined in Data.Singletons type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) = f @@ x

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

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

Instances

Instances details

type Apply (~>@#@$) (x :: Type)
Instance details Defined in Data.Singletons type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

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

Instances

Instances details

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)
Instance details Defined in Data.Singletons type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

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

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 #

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 #

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 #

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

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

Instances

Instances details

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)
Instance details 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

Instances details

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1)
Instance details 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 #

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

Instances

Instances details

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4)
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)

data DemoteSym0 (a :: TyFun Type Type) #

Instances

Instances details

type Apply DemoteSym0 (x :: Type)
Instance details 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

Instances details

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)
Instance details Defined in Data.Singletons type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x

type KindOfSym1 (x :: k) = KindOf x #

newtype SWrappedSing (a1 :: WrappedSing a) where #

Constructors

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

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

Instances

Instances details

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)
Instance details 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

Instances details

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k)
Instance details 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 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) #

data SingInstance (a :: k) where #

Constructors

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

type TyCon1 = TyCon :: (k1 -> k2) -> k1 ~> k2 #

type TyCon2 = TyCon :: (k1 -> k2 -> k3) -> k1 ~> (k2 ~> k3) #

type TyCon3 = TyCon :: (k1 -> k2 -> k3 -> k4) -> k1 ~> (k2 ~> (k3 ~> k4)) #

type TyCon4 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> k5))) #

type TyCon5 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k6)))) #

type TyCon6 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k7))))) #

type TyCon7 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k8)))))) #

type TyCon8 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k9))))))) #

data TyFun a b #

Instances

Instances details

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

Instance details

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2)
Instance details 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)

Instance details

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)

Instance details

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)

Instance details

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)

Instance details

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)

Instance details

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)

Instance details

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)

Instance details

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)

Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f) #

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

Instance details

Defined in Data.Singletons

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

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

Instance details

Defined in Data.Singletons

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

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

Instance details

Defined in Data.Singletons

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

type Demote (k1 ~> k2)

Instance details

Defined in Data.Singletons

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

type Sing

Instance details

Defined in Data.Singletons

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

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

Instance details

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)

Instance details

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

Instances details

SingKind (WrappedSing a)

Instance details

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a)
Instance details 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)

Instance details

Defined in Data.Singletons

Methods

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

type Demote (WrappedSing a)

Instance details

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

type Sing

Instance details

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

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

Instances details

Category ((:~:) :: k -> k -> Type)	Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: forall (a :: k). a :~: a # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c #
TestCoercion ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in 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
Instance details Defined in 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
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () #
NFData1 ((:~:) a)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () #
(a ~ b, Data a) => Data (a :~: b)	Since: base-4.7.0.0
Instance details Defined in 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
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details Defined in 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
Instance details Defined in 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
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #
NFData (a :~: b)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () #
Eq (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)	Since: base-4.7.0.0
Instance details Defined in 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

Instances details

Data Void

Since: base-4.8.0.0

Instance details

Defined in 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 #

Semigroup Void

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty Void -> Void #

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

Exception Void

Since: base-4.8.0.0

Instance details

Defined in GHC.Exception.Type

Methods

toException :: Void -> SomeException #

fromException :: SomeException -> Maybe Void #

displayException :: Void -> String #

Generic Void

Instance details

Defined in GHC.Generics

Associated Types

type Rep Void	Since: base-4.8.0.0
Instance details Defined in GHC.Generics type Rep Void = D1 ('MetaData "Void" "GHC.Base" "base" 'False) (V1 :: Type -> Type)

Methods

from :: Void -> Rep Void x #

to :: Rep Void x -> Void #

Ix Void

Since: base-4.8.0.0

Instance details

Defined in GHC.Ix

Methods

range :: (Void, Void) -> [Void] #

index :: (Void, Void) -> Void -> Int #

unsafeIndex :: (Void, Void) -> Void -> Int #

inRange :: (Void, Void) -> Void -> Bool #

rangeSize :: (Void, Void) -> Int #

unsafeRangeSize :: (Void, Void) -> Int #

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

Instance details

Defined in GHC.Read

Methods

readsPrec :: Int -> ReadS Void #

readList :: ReadS [Void] #

readPrec :: ReadPrec Void #

readListPrec :: ReadPrec [Void] #

Show Void

Since: base-4.8.0.0

Instance details

Defined in GHC.Show

Methods

showsPrec :: Int -> Void -> ShowS #

show :: Void -> String #

showList :: [Void] -> ShowS #

NFData Void

Defined as rnf = absurd.

Since: deepseq-1.4.0.0

Instance details

Defined in Control.DeepSeq

Methods

rnf :: Void -> () #

Eq Void

Since: base-4.8.0.0

Instance details

Defined in GHC.Base

Methods

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

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

Ord Void

Since: base-4.8.0.0

Instance details

Defined in GHC.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 #

Lift Void

Since: template-haskell-2.15.0.0

Instance details

Defined in Language.Haskell.TH.Syntax

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

Instance details

Defined in GHC.Generics

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

type Refuted a = a -> Void #

data Decision a #

Constructors

Proved a
Disproved (Refuted a)

class SuppressUnusedWarnings (t :: k) where Source #

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 :: () Source #

Primary Template Haskell generation functions

Functions to generate equality instances

Functions to generate Ord instances

Functions to generate Bounded instances

Functions to generate Enum instances

Functions to generate Show instances

Utility functions

Basic singleton definitions

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Auxiliary definitions

Instances

Instances

Functions to generate `Ord` instances

Functions to generate `Bounded` instances

Functions to generate `Enum` instances

Functions to generate `Show` instances