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