Copyright	(C) 2017 Ryan Scott
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Void

Contents

The Void singleton
Singletons from Data.Void
Defunctionalization symbols

Description

Defines functions and datatypes relating to the singleton for Void, including a singleton version of all the definitions in Data.Void.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in Data.Void. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

data family Sing (a :: k)
type SVoid = (Sing :: Void -> Type)
type family Absurd (a :: Void) :: a where ...
sAbsurd :: forall (t :: Void). Sing t -> Sing (Apply AbsurdSym0 t :: a)
data AbsurdSym0 (l :: TyFun Void a6989586621679303847)
type AbsurdSym1 (t :: Void) = Absurd t

The `Void` singleton

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)

Just as Void has no constructors, the Sing instance above also has no constructors.

type SVoid = (Sing :: Void -> Type) Source #

SVoid is a kind-restricted synonym for Sing: type SVoid (a :: Void) = Sing a

Singletons from `Data.Void`

type family Absurd (a :: Void) :: a where ... Source #

Equations

Absurd a = Case_6989586621679303855 a a

sAbsurd :: forall (t :: Void). Sing t -> Sing (Apply AbsurdSym0 t :: a) Source #

Defunctionalization symbols

data AbsurdSym0 (l :: TyFun Void a6989586621679303847) Source #

Instances

SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679303847 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () Source #
type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) Source #
Instance details Defined in Data.Singletons.Prelude.Void type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) = (Absurd l :: k2)

type AbsurdSym1 (t :: Void) = Absurd t Source #

The Void singleton

Singletons from Data.Void

Defunctionalization symbols

The `Void` singleton

Singletons from `Data.Void`