Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.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) #

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 [a] #
data Sing [a] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a) #
data Sing (Maybe a) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a) #
data Sing (NonEmpty a) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a b) #
data Sing (Either a b) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a, b) #
data Sing (a, b) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2) #
data Sing ((~>) k1 k2) = SLambda { applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a, b, c) #
data Sing (a, b, c) where STuple3 :: Sing (a, b, c) z
data Sing (a, b, c, d) #
data Sing (a, b, c, d) where STuple4 :: Sing (a, b, c, d) z
data Sing (a, b, c, d, e) #
data Sing (a, b, c, d, e) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a, b, c, d, e, f) #
data Sing (a, b, c, d, e, f) where STuple6 :: Sing (a, b, c, d, e, f) z
data Sing (a, b, c, d, e, f, g) #
data Sing (a, b, c, d, e, f, g) 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 Demote Type = (r :: *) # Methods fromSing :: Sing Type a -> Demote Type # toSing :: Demote Type -> SomeSing Type #
SDecide Type #
Methods (%~) :: Sing Type a -> Sing Type b -> Decision ((Type :~: a) b) #
PEq Type #
Associated Types type (Type :== (x :: Type)) (y :: Type) :: Bool # type (Type :/= (x :: Type)) (y :: Type) :: Bool #
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 #
TestCoercion * (Sing *) #
Methods testCoercion :: f a -> f b -> Maybe (Coercion (Sing *) a b) #