Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.TypeRepStar

Contents

Orphan instances

Description

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!

Synopsis

Documentation

data family Sing (a :: k) Source #

The singleton kind-indexed data family.

Instances

data Sing Bool Source #
data Sing Bool where SFalse :: Sing Bool z STrue :: Sing Bool z
data Sing Ordering Source #
data Sing Ordering where SLT :: Sing Ordering z SEQ :: Sing Ordering z SGT :: Sing Ordering z
data Sing * Source #
data Sing * where STypeRep :: Sing * a
data Sing Nat Source #
data Sing Nat where SNat :: Sing Nat n
data Sing Symbol Source #
data Sing Symbol where SSym :: Sing Symbol n
data Sing () Source #
data Sing () where STuple0 :: Sing () z
data Sing [a0] Source #
data Sing [a0] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a0) Source #
data Sing (Maybe a0) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a0) Source #
data Sing (NonEmpty a0) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a0 b0) Source #
data Sing (Either a0 b0) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a0, b0) Source #
data Sing (a0, b0) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2) Source #
data Sing ((~>) k1 k2) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a0, b0, c0) Source #
data Sing (a0, b0, c0) where STuple3 :: Sing (a, b, c) z
data Sing (a0, b0, c0, d0) Source #
data Sing (a0, b0, c0, d0) where STuple4 :: Sing (a, b, c, d) z
data Sing (a0, b0, c0, d0, e0) Source #
data Sing (a0, b0, c0, d0, e0) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a0, b0, c0, d0, e0, f0) Source #
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) Source #
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 Source #
Associated Types type DemoteRep Type :: * Source # Methods fromSing :: Sing Type a -> DemoteRep Type Source # toSing :: DemoteRep Type -> SomeSing Type Source #
SDecide Type Source #
Methods (%~) :: Sing Type a -> Sing Type b -> Decision ((Type :~: a) b) Source #
SEq Type Source #
Methods (%:==) :: Sing Type a -> Sing Type b -> Sing Bool ((Type :== a) b) Source # (%:/=) :: Sing Type a -> Sing Type b -> Sing Bool ((Type :/= a) b) Source #
Typeable * a => SingI * a Source #
Methods sing :: Sing a a Source #
PEq Type (Proxy * Type) Source #
Associated Types type ((Proxy * Type) :== (x :: Proxy * Type)) (y :: Proxy * Type) :: Bool Source # type ((Proxy * Type) :/= (x :: Proxy * Type)) (y :: Proxy * Type) :: Bool Source #
TestCoercion * (Sing *) Source #
Methods testCoercion :: f a -> f b -> Maybe (Coercion (Sing *) a b) #