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 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!

Synopsis

data family Sing (a :: k)
data SomeTypeRepStar where
- SomeTypeRepStar :: forall (a :: *). !(TypeRep a) -> SomeTypeRepStar

Documentation

data family Sing (a :: k) Source #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar 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 z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (z :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Bool) where SFalse :: Sing False STrue :: Sing True
data Sing (z :: Ordering) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Ordering) where SLT :: Sing LT SEQ :: Sing EQ SGT :: Sing GT
data Sing (a :: Type) Source #
Instance details Defined in Data.Singletons.TypeRepStar data Sing (a :: Type) = STypeRep (TypeRep a)
data Sing (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: Sing n
data Sing (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: Sing n
data Sing (z :: ()) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: ()) where STuple0 :: Sing ()
data Sing (z :: Void) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Void)
data Sing (z :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: [a]) where SNil :: Sing ([] :: [k]) SCons :: Sing (n ': n)
data Sing (z :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Maybe a) where SNothing :: Sing (Nothing :: Maybe a) SJust :: Sing (Just n)
data Sing (z :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: NonEmpty a) where (:%\|) :: Sing (n :\| n)
data Sing (z :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances 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)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b)) where STuple2 :: Sing ((,) n n)
data Sing (f :: k1 ~> k2) Source #
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (z :: (a, b, c)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c)) where STuple3 :: Sing ((,,) n n n)
data Sing (z :: (a, b, c, d)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d)) where STuple4 :: Sing ((,,,) n n n n)
data Sing (z :: (a, b, c, d, e)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances 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)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances 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)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances 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 Source #

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

Constructors

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

Instances

Eq SomeTypeRepStar Source #
Instance details Defined in Data.Singletons.TypeRepStar Methods (==) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool # (/=) :: SomeTypeRepStar -> SomeTypeRepStar -> Bool #
Ord SomeTypeRepStar Source #
Instance details Defined in Data.Singletons.TypeRepStar 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 Source #
Instance details Defined in Data.Singletons.TypeRepStar Methods showsPrec :: Int -> SomeTypeRepStar -> ShowS # show :: SomeTypeRepStar -> String # showList :: [SomeTypeRepStar] -> ShowS #

Orphan instances

SingKind Type Source #
Instance details Associated Types type Demote Type = (r :: *) Source # Methods fromSing :: Sing a -> Demote Type Source # toSing :: Demote Type -> SomeSing Type Source #
SDecide Type Source #
Instance details Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Type Source #
Instance details Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Type Source #
Instance details Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
ShowSing Type Source #
Instance details Methods showsSingPrec :: Int -> Sing a -> ShowS Source #
Typeable a => SingI (a :: *) Source #
Instance details Methods sing :: Sing a Source #
Eq (Sing a) Source #
Instance details Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) Source #
Instance details 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) Source #
Instance details Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #