Data.Singletons.TypeRepStar

This module defines singleton instances making Typeable the singleton for the kind *. The definitions don't fully line up with what is expected within the singletons library, so expect unusual results!

Documentation

data family Sing (a :: k)

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing *

data Sing * where

• STypeRep :: Sing * a

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

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

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a, b, c) z

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

Here is the definition of the singleton for *:

data instance Sing (a :: *) where
  STypeRep :: Typeable a => Sing a

Instances for SingI, SingKind, SEq, SDecide, and TestCoercion are also supplied.

Orphan instances

SingKind Type

Associated Types

type DemoteRep Type :: *

Methods

fromSing :: Sing Type a -> DemoteRep Type

toSing :: DemoteRep Type -> SomeSing Type

SDecide Type

Methods

(%~) :: Sing Type a -> Sing Type b -> Decision ((Type :~: a) b)

SEq Type

Methods

(%:==) :: Sing Type a -> Sing Type b -> Sing Bool ((Type :== a) b)

(%:/=) :: Sing Type a -> Sing Type b -> Sing Bool ((Type :/= a) b)

Typeable * a => SingI * a

Methods

sing :: Sing a a

PEq Type (Proxy * Type)

Associated Types

type ((Proxy * Type) :== (x :: Proxy * Type)) (y :: Proxy * Type) :: Bool

type ((Proxy * Type) :/= (x :: Proxy * Type)) (y :: Proxy * Type) :: Bool

TestCoercion * (Sing *)

Methods

testCoercion :: f a -> f b -> Maybe (Coercion (Sing *) a b)