Copyright | (C) 2017 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Void
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
- type family Sing :: k -> Type
- data SVoid :: Void -> Type
- type family Absurd (a :: Void) :: a where ...
- sAbsurd :: forall a (t :: Void). Sing t -> Sing (Apply AbsurdSym0 t :: a)
- data AbsurdSym0 :: forall a6989586621679365194. (~>) Void a6989586621679365194
- type AbsurdSym1 (a6989586621679365197 :: Void) = Absurd a6989586621679365197
The Void
singleton
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SVoid :: Void -> Type Source #
Instances
TestCoercion SVoid Source # | |
Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SVoid a -> SVoid b -> Maybe (Coercion a b) | |
TestEquality SVoid Source # | |
Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SVoid a -> SVoid b -> Maybe (a :~: b) | |
Show (SVoid z) | |
Singletons from Data.Void
type family Absurd (a :: Void) :: a where ... Source #
Equations
Absurd a = Case_6989586621679365200 a a |
Defunctionalization symbols
data AbsurdSym0 :: forall a6989586621679365194. (~>) Void a6989586621679365194 Source #
Instances
SingI (AbsurdSym0 :: TyFun Void a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Void Methods sing :: Sing AbsurdSym0 Source # | |
SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679365194 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () Source # | |
type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679365197 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Void |
type AbsurdSym1 (a6989586621679365197 :: Void) = Absurd a6989586621679365197 Source #