Data.Proxy.Singletons

Exports promoted and singled versions of the definitions in Data.Proxy.

The Proxy singleton

type family Sing :: k -> Type

Instances

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SVoid

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SAll

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SAny

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SOrdering

type Sing

Defined in Data.Singletons.Base.TypeError

type Sing = SErrorMessage

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SNat

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple0

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SBool

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SChar

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SSymbol

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SMax :: Max a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SMin :: Min a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SIdentity :: Identity a -> Type

type Sing

Defined in Data.Monoid.Singletons

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Monoid.Singletons

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Ord.Singletons

type Sing = SDown :: Down a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SDual :: Dual a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SProduct :: Product a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type Sing = SSum :: Sum a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SMaybe :: Maybe a -> Type

type Sing

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

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

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

Defined in Data.Singletons.Base.TypeRepTYPE

type Sing = TypeRep :: TYPE rep -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SList :: [a] -> Type

type Sing

Defined in Data.Semigroup.Singletons

type Sing = SArg :: Arg a b -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SEither :: Either a b -> Type

type Sing

Defined in Data.Proxy.Singletons

type Sing = SProxy :: Proxy t -> Type

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 Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple2 :: (a, b) -> Type

type Sing

Defined in Data.Functor.Const.Singletons

type Sing = SConst :: Const a b -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple3 :: (a, b, c) -> Type

type Sing

Defined in Data.Functor.Product.Singletons

type Sing = SProduct :: Product f g a -> Type

type Sing

Defined in Data.Functor.Sum.Singletons

type Sing = SSum :: Sum f g a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple4 :: (a, b, c, d) -> Type

type Sing

Defined in Data.Functor.Compose.Singletons

type Sing = SCompose :: Compose f g a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple5 :: (a, b, c, d, e) -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple6 :: (a, b, c, d, e, f) -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SProxy (a :: Proxy t) where

Constructors

SProxy :: forall {k} (t :: k). SProxy ('Proxy :: Proxy t)

Instances

TestCoercion (SProxy :: Proxy t -> Type)

Defined in Data.Proxy.Singletons

Methods

testCoercion :: forall (a :: Proxy t) (b :: Proxy t). SProxy a -> SProxy b -> Maybe (Coercion a b)

TestEquality (SProxy :: Proxy t -> Type)

Defined in Data.Proxy.Singletons

Methods

testEquality :: forall (a :: Proxy t) (b :: Proxy t). SProxy a -> SProxy b -> Maybe (a :~: b)

Show (SProxy z)

Defined in Data.Proxy.Singletons

Methods

showsPrec :: Int -> SProxy z -> ShowS

show :: SProxy z -> String

showList :: [SProxy z] -> ShowS

Eq (SProxy z)

Defined in Data.Proxy.Singletons

Methods

(==) :: SProxy z -> SProxy z -> Bool

(/=) :: SProxy z -> SProxy z -> Bool

Ord (SProxy z)

Defined in Data.Proxy.Singletons

Methods

compare :: SProxy z -> SProxy z -> Ordering

(<) :: SProxy z -> SProxy z -> Bool

(<=) :: SProxy z -> SProxy z -> Bool

(>) :: SProxy z -> SProxy z -> Bool

(>=) :: SProxy z -> SProxy z -> Bool

max :: SProxy z -> SProxy z -> SProxy z

min :: SProxy z -> SProxy z -> SProxy z

type family AsProxyTypeOf (a1 :: a) (a2 :: proxy a) :: a where ...

Equations

AsProxyTypeOf (a_6989586621679900545 :: k2) (a_6989586621679900547 :: proxy k2) = Apply (Apply (ConstSym0 :: TyFun k2 (proxy k2 ~> k2) -> Type) a_6989586621679900545) a_6989586621679900547

sAsProxyTypeOf :: forall a (proxy :: Type -> Type) (t1 :: a) (t2 :: proxy a). Sing t1 -> Sing t2 -> Sing (AsProxyTypeOf t1 t2)

Defunctionalization symbols

type family ProxySym0 :: Proxy t where ...

Equations

ProxySym0 = 'Proxy :: Proxy t

data AsProxyTypeOfSym0 (a1 :: TyFun a (proxy a ~> a))

Instances

SingI (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type)

Defined in Data.Proxy.Singletons

Methods

sing :: Sing (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type)

SuppressUnusedWarnings (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type)

Defined in Data.Proxy.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621679900552 :: a)

Defined in Data.Proxy.Singletons

type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621679900552 :: a) = AsProxyTypeOfSym1 a6989586621679900552 :: TyFun (proxy a) a -> Type

data AsProxyTypeOfSym1 (a6989586621679900552 :: a) (b :: TyFun (proxy a) a)

Instances

SingI1 (AsProxyTypeOfSym1 :: a -> TyFun (proxy a) a -> Type)

Defined in Data.Proxy.Singletons

Methods

liftSing :: forall (x :: a). Sing x -> Sing (AsProxyTypeOfSym1 x :: TyFun (proxy a) a -> Type)

SingI d => SingI (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type)

Defined in Data.Proxy.Singletons

Methods

sing :: Sing (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type)

SuppressUnusedWarnings (AsProxyTypeOfSym1 a6989586621679900552 :: TyFun (proxy a) a -> Type)

Defined in Data.Proxy.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (AsProxyTypeOfSym1 a6989586621679900552 :: TyFun (proxy a) a -> Type) (a6989586621679900553 :: proxy a)

Defined in Data.Proxy.Singletons

type Apply (AsProxyTypeOfSym1 a6989586621679900552 :: TyFun (proxy a) a -> Type) (a6989586621679900553 :: proxy a) = AsProxyTypeOf a6989586621679900552 a6989586621679900553

type family AsProxyTypeOfSym2 (a6989586621679900552 :: a) (a6989586621679900553 :: proxy a) :: a where ...

Equations

AsProxyTypeOfSym2 (a6989586621679900552 :: a) (a6989586621679900553 :: proxy a) = AsProxyTypeOf a6989586621679900552 a6989586621679900553

Orphan instances

PAlternative (Proxy :: Type -> Type)

Associated Types

type Empty

Defined in Data.Proxy.Singletons

type Empty

type (a2 :: Proxy a1) <|> (a3 :: Proxy a1)

Defined in Data.Proxy.Singletons

type (a2 :: Proxy a1) <|> (a3 :: Proxy a1)

PApplicative (Proxy :: Type -> Type)

Associated Types

type Pure (a2 :: a1)

Defined in Data.Proxy.Singletons

type Pure (a2 :: a1)

type (a2 :: Proxy (a1 ~> b)) <*> (a3 :: Proxy a1)

Defined in Data.Proxy.Singletons

type (a2 :: Proxy (a1 ~> b)) <*> (a3 :: Proxy a1)

type LiftA2 (arg :: a ~> (b ~> c)) (arg1 :: Proxy a) (arg2 :: Proxy b)

Defined in Data.Proxy.Singletons

type LiftA2 (arg :: a ~> (b ~> c)) (arg1 :: Proxy a) (arg2 :: Proxy b)

type (arg :: Proxy a) *> (arg1 :: Proxy b)

Defined in Data.Proxy.Singletons

type (arg :: Proxy a) *> (arg1 :: Proxy b)

type (arg :: Proxy a) <* (arg1 :: Proxy b)

Defined in Data.Proxy.Singletons

type (arg :: Proxy a) <* (arg1 :: Proxy b)

PFunctor (Proxy :: Type -> Type)

Associated Types

type Fmap (a2 :: a1 ~> b) (a3 :: Proxy a1)

Defined in Data.Proxy.Singletons

type Fmap (a2 :: a1 ~> b) (a3 :: Proxy a1)

type (arg :: a) <$ (arg1 :: Proxy b)

Defined in Data.Proxy.Singletons

type (arg :: a) <$ (arg1 :: Proxy b)

PMonad (Proxy :: Type -> Type)

Associated Types

type (a2 :: Proxy a1) >>= (a3 :: a1 ~> Proxy b)

Defined in Data.Proxy.Singletons

type (a2 :: Proxy a1) >>= (a3 :: a1 ~> Proxy b)

type (arg :: Proxy a) >> (arg1 :: Proxy b)

Defined in Data.Proxy.Singletons

type (arg :: Proxy a) >> (arg1 :: Proxy b)

type Return (arg :: a)

Defined in Data.Proxy.Singletons

type Return (arg :: a)

PMonadPlus (Proxy :: Type -> Type)

Associated Types

type Mzero

Defined in Data.Proxy.Singletons

type Mzero

type Mplus (arg :: Proxy a) (arg1 :: Proxy a)

Defined in Data.Proxy.Singletons

type Mplus (arg :: Proxy a) (arg1 :: Proxy a)

SAlternative (Proxy :: Type -> Type)

Methods

sEmpty :: Sing (Empty :: Proxy a)

(%<|>) :: forall a (t1 :: Proxy a) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (t1 <|> t2)

SApplicative (Proxy :: Type -> Type)

Methods

sPure :: forall a (t :: a). Sing t -> Sing (Pure t :: Proxy a)

(%<*>) :: forall a b (t1 :: Proxy (a ~> b)) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (t1 <*> t2)

sLiftA2 :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: Proxy a) (t3 :: Proxy b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (LiftA2 t1 t2 t3)

(%*>) :: forall a b (t1 :: Proxy a) (t2 :: Proxy b). Sing t1 -> Sing t2 -> Sing (t1 *> t2)

(%<*) :: forall a b (t1 :: Proxy a) (t2 :: Proxy b). Sing t1 -> Sing t2 -> Sing (t1 <* t2)

SFunctor (Proxy :: Type -> Type)

Methods

sFmap :: forall a b (t1 :: a ~> b) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (Fmap t1 t2)

(%<$) :: forall a b (t1 :: a) (t2 :: Proxy b). Sing t1 -> Sing t2 -> Sing (t1 <$ t2)

SMonad (Proxy :: Type -> Type)

Methods

(%>>=) :: forall a b (t1 :: Proxy a) (t2 :: a ~> Proxy b). Sing t1 -> Sing t2 -> Sing (t1 >>= t2)

(%>>) :: forall a b (t1 :: Proxy a) (t2 :: Proxy b). Sing t1 -> Sing t2 -> Sing (t1 >> t2)

sReturn :: forall a (t :: a). Sing t -> Sing (Return t :: Proxy a)

SMonadPlus (Proxy :: Type -> Type)

Methods

sMzero :: Sing (Mzero :: Proxy a)

sMplus :: forall a (t1 :: Proxy a) (t2 :: Proxy a). Sing t1 -> Sing t2 -> Sing (Mplus t1 t2)

SingKind (Proxy t)

Associated Types

type Demote (Proxy t)

Defined in Data.Proxy.Singletons

type Demote (Proxy t) = Proxy t

Methods

fromSing :: forall (a :: Proxy t). Sing a -> Demote (Proxy t)

toSing :: Demote (Proxy t) -> SomeSing (Proxy t)

SDecide (Proxy t)

Methods

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

PEq (Proxy s)

SEq (Proxy s)

Methods

(%==) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 == t2)

(%/=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 /= t2)

PMonoid (Proxy s)

Associated Types

type Mempty

Defined in Data.Proxy.Singletons

type Mempty

SMonoid (Proxy s)

Methods

sMempty :: Sing (Mempty :: Proxy s)

sMappend :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Mappend t1 t2)

sMconcat :: forall (t :: [Proxy s]). Sing t -> Sing (Mconcat t)

POrd (Proxy s)

SOrd (Proxy s)

Methods

sCompare :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Compare t1 t2)

(%<) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 < t2)

(%<=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 <= t2)

(%>) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 > t2)

(%>=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 >= t2)

sMax :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Max t1 t2)

sMin :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Min t1 t2)

PSemigroup (Proxy s)

SSemigroup (Proxy s)

Methods

(%<>) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 <> t2)

sSconcat :: forall (t :: NonEmpty (Proxy s)). Sing t -> Sing (Sconcat t)

PBounded (Proxy s)

Associated Types

type MinBound

Defined in Data.Proxy.Singletons

type MinBound

type MaxBound

Defined in Data.Proxy.Singletons

type MaxBound

PEnum (Proxy s)

SBounded (Proxy s)

Methods

sMinBound :: Sing (MinBound :: Proxy s)

sMaxBound :: Sing (MaxBound :: Proxy s)

SEnum (Proxy s)

Methods

sSucc :: forall (t :: Proxy s). Sing t -> Sing (Succ t)

sPred :: forall (t :: Proxy s). Sing t -> Sing (Pred t)

sToEnum :: forall (t :: Natural). Sing t -> Sing (ToEnum t :: Proxy s)

sFromEnum :: forall (t :: Proxy s). Sing t -> Sing (FromEnum t)

sEnumFromTo :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (EnumFromTo t1 t2)

sEnumFromThenTo :: forall (t1 :: Proxy s) (t2 :: Proxy s) (t3 :: Proxy s). Sing t1 -> Sing t2 -> Sing t3 -> Sing (EnumFromThenTo t1 t2 t3)

PShow (Proxy s)

SShow (Proxy s)

Methods

sShowsPrec :: forall (t1 :: Natural) (t2 :: Proxy s) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (ShowsPrec t1 t2 t3)

sShow_ :: forall (t :: Proxy s). Sing t -> Sing (Show_ t)

sShowList :: forall (t1 :: [Proxy s]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (ShowList t1 t2)

SingI ('Proxy :: Proxy t)

Methods

sing :: Sing ('Proxy :: Proxy t)