Data.Singletons.TypeRepStar

This module defines singleton instances making TypeRep 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 (z :: Bool)

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (a :: Type)

data Sing (a :: Type) = STypeRep (TypeRep a)

data Sing (n :: Nat)

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

data Sing (z :: Void)

data Sing (z :: [a])

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [k])
• SCons :: Sing (n ': n)

data Sing (z :: Maybe a)

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n :| n)

data Sing (z :: Either a b)

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

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

• STuple2 :: Sing ((,) n n)

data Sing (f :: k1 ~> k2)

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

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

}

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

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

• STuple3 :: Sing ((,,) n n n)

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

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

• STuple4 :: Sing ((,,,) n n n n)

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

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

• STuple5 :: Sing ((,,,,) n n n n n)

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

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

• STuple6 :: Sing ((,,,,,) n n n n n n)

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

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

• STuple7 :: Sing ((,,,,,,) n n n n n n n)

Here is the definition of the singleton for *:

newtype instance Sing :: Type -> Type where
  STypeRep :: TypeRep a -> Sing a

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

data SomeTypeRepStar where

A variant of SomeTypeRep whose underlying TypeRep is restricted to kind *.

Constructors

SomeTypeRepStar :: forall (a :: *). !(TypeRep a) -> SomeTypeRepStar

Instances

Eq SomeTypeRepStar

Methods

(==) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool

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

Ord SomeTypeRepStar

Methods

compare :: SomeTypeRepStar -> SomeTypeRepStar -> Ordering

(<) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool

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

(>) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool

(>=) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool

max :: SomeTypeRepStar -> SomeTypeRepStar -> SomeTypeRepStar

min :: SomeTypeRepStar -> SomeTypeRepStar -> SomeTypeRepStar

Show SomeTypeRepStar

Methods

showsPrec :: Int -> SomeTypeRepStar -> ShowS

show :: SomeTypeRepStar -> String

showList :: [SomeTypeRepStar] -> ShowS

Orphan instances

SingKind Type

Associated Types

type Demote Type = (r :: *)

Methods

fromSing :: Sing a -> Demote Type

toSing :: Demote Type -> SomeSing Type

SDecide Type

Methods

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

PEq Type

Associated Types

type x == y :: Bool

type x /= y :: Bool

SEq Type

Methods

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

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

ShowSing Type

Methods

showsSingPrec :: Int -> Sing a -> ShowS

Typeable a => SingI (a :: *)

Methods

sing :: Sing a

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Ord (Sing a)

Methods

compare :: Sing a -> Sing a -> Ordering

(<) :: Sing a -> Sing a -> Bool

(<=) :: Sing a -> Sing a -> Bool

(>) :: Sing a -> Sing a -> Bool

(>=) :: Sing a -> Sing a -> Bool

max :: Sing a -> Sing a -> Sing a

min :: Sing a -> Sing a -> Sing a

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS