-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A framework for generating singleton types
--
@package singletons
@version 0.9.2
-- | This module is a reimplementation of Edward Kmett's void
-- package. It is included within singletons to avoid depending on
-- void and all the packages that depends on (including
-- text). If this causes problems for you (that singletons has
-- its own Void type), please let me (Richard Eisenberg) know at
-- eir at cis.upenn.edu.
module Data.Singletons.Void
-- | A logically uninhabited data type.
data Void
-- | Since Void values logically don't exist, this witnesses the
-- logical reasoning tool of "ex falso quodlibet".
absurd :: Void -> a
-- | If Void is uninhabited then any Functor that holds only
-- values of type Void is holding no values.
vacuous :: Functor f => f Void -> f a
-- | If Void is uninhabited then any Monad that holds values
-- of type Void is holding no values.
vacuousM :: Monad m => m Void -> m a
instance Typeable Void
instance Data Void
instance Generic Void
instance Datatype D1Void
instance Constructor C1_0Void
instance Exception Void
instance Ix Void
instance Read Void
instance Show Void
instance Ord Void
instance Eq Void
-- | Defines and exports types that are useful when working with
-- singletons. Some of these are re-exports from
-- Data.Type.Equality.
module Data.Singletons.Types
-- | Because we can never create a value of type Void, a function
-- that type-checks at a -> Void shows that objects of type
-- a can never exist. Thus, we say that a is
-- Refuted
type Refuted a = a -> Void
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: (Refuted a) -> Decision a
-- | Defines functions and datatypes relating to the singleton for
-- Bool, including a singletons version of all the definitions in
-- Data.Bool.
--
-- 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.Bool. Also, please excuse
-- the apparent repeated variable names. This is due to an interaction
-- between Template Haskell and Haddock.
module Data.Singletons.Bool
-- | The singleton kind-indexed data family.
type SBool (z_aizw :: Bool) = Sing z_aizw
-- | Type-level If. If True a b ==> a; If
-- False a b ==> b
-- | Conditional over singletons
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
-- | Type-level "not"
sNot :: SBool a -> SBool (Not a)
type (:&&) a b = a && b
type (:||) a b = a || b
(%:&&) :: SBool a -> SBool b -> SBool (a :&& b)
(%:||) :: SBool a -> SBool b -> SBool (a :|| b)
sBool_ :: Sing t_anmT -> Sing t_anmU -> Sing t_anmV -> Sing (Bool_ t_anmT t_anmU t_anmV)
type Otherwise = True
sOtherwise :: Sing Otherwise
-- | Defines the SEq singleton version of the Eq type class.
module Data.Singletons.Eq
-- | The singleton analogue of Eq. Unlike the definition for
-- Eq, it is required that instances define a body for '(%:==)'.
-- You may also supply a body for '(%:/=)'.
class kparam ~ KProxy => SEq (kparam :: KProxy k) where a %:/= b = sNot (a %:== b)
(%:==) :: SEq kparam => Sing a -> Sing b -> Sing (a :== b)
(%:/=) :: SEq kparam => Sing a -> Sing b -> Sing (a :/= b)
-- | A type family to compute Boolean equality. Instances are provided only
-- for open kinds, such as * and function kinds.
-- Instances are also provided for datatypes exported from base. A
-- poly-kinded instance is not provided, as a recursive definition
-- for algebraic kinds is generally more useful.
-- | A re-export of the type-level (==) that conforms to the
-- singletons naming convention.
type (:==) a b = a == b
type (:/=) a b = Not (a :== b)
instance (SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy, SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance SEq 'KProxy
instance SEq 'KProxy => SEq 'KProxy
instance SEq 'KProxy
instance (SEq 'KProxy, SEq 'KProxy) => SEq 'KProxy
instance SEq 'KProxy => SEq 'KProxy
instance SEq 'KProxy
-- | This file implements singletonStar, which generates a datatype
-- Rep and associated singleton from a list of types. The
-- promoted version of Rep is kind * and the Haskell
-- types themselves. This is still very experimental, so expect unusual
-- results!
module Data.Singletons.CustomStar
-- | Produce a representation and singleton for the collection of types
-- given.
--
-- A datatype Rep is created, with one constructor per type in
-- the declared universe. When this type is promoted by the singletons
-- library, the constructors become full types in *, not just
-- promoted data constructors.
--
-- For example,
--
--
-- $(singletonStar [''Nat, ''Bool, ''Maybe])
--
--
-- generates the following:
--
--
-- data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)
--
--
-- and its singleton. However, because Rep is promoted to
-- *, the singleton is perhaps slightly unexpected:
--
--
-- data instance Sing (a :: *) where
-- SNat :: Sing Nat
-- SBool :: Sing Bool
-- SMaybe :: SingRep a => Sing a -> Sing (Maybe a)
--
--
-- The unexpected part is that Nat, Bool, and
-- Maybe above are the real Nat, Bool, and
-- Maybe, not just promoted data constructors.
--
-- Please note that this function is very experimental. Use at
-- your own risk.
singletonStar :: Quasi q => [Name] -> q [Dec]
-- | 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!
module Data.Singletons.TypeRepStar
-- | The singleton kind-indexed data family.
instance TestCoercion Sing
instance SDecide 'KProxy
instance SEq 'KProxy
instance SingKind 'KProxy
instance Typeable a => SingI a
-- | This module contains everything you need to derive your own singletons
-- via Template Haskell.
--
-- TURN ON -XScopedTypeVariables IN YOUR MODULE IF YOU WANT THIS
-- TO WORK.
module Data.Singletons.TH
-- | Make promoted and singleton versions of all declarations given,
-- retaining the original declarations. See
-- http://www.cis.upenn.edu/~eir/packages/singletons/README.html
-- for further explanation.
singletons :: Quasi q => q [Dec] -> q [Dec]
-- | Make promoted and singleton versions of all declarations given,
-- discarding the original declarations.
singletonsOnly :: Quasi q => q [Dec] -> q [Dec]
-- | Generate singleton definitions from a type that is already defined.
-- For example, the singletons package itself uses
--
--
-- $(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
--
--
-- to generate singletons for Prelude types.
genSingletons :: Quasi q => [Name] -> q [Dec]
-- | Promote every declaration given to the type level, retaining the
-- originals.
promote :: Quasi q => q [Dec] -> q [Dec]
-- | Promote each declaration, discarding the originals.
promoteOnly :: Quasi q => q [Dec] -> q [Dec]
-- | Produce instances for '(:==)' (type-level equality) from the given
-- types
promoteEqInstances :: Quasi q => [Name] -> q [Dec]
-- | Produce an instance for '(:==)' (type-level equality) from the given
-- type
promoteEqInstance :: Quasi q => Name -> q [Dec]
-- | Create instances of SEq and type-level '(:==)' for each type
-- in the list
singEqInstances :: Quasi q => [Name] -> q [Dec]
-- | Create instance of SEq and type-level '(:==)' for the given
-- type
singEqInstance :: Quasi q => Name -> q [Dec]
-- | Create instances of SEq (only -- no instance for '(:==)',
-- which SEq generally relies on) for each type in the list
singEqInstancesOnly :: Quasi q => [Name] -> q [Dec]
-- | Create instances of SEq (only -- no instance for '(:==)',
-- which SEq generally relies on) for the given type
singEqInstanceOnly :: Quasi q => Name -> q [Dec]
-- | Create instances of SDecide for each type in the list
singDecideInstances :: Quasi q => [Name] -> q [Dec]
-- | Create instance of SDecide for the given type
singDecideInstance :: Quasi q => Name -> q [Dec]
-- | The function cases generates a case expression where each
-- right-hand side is identical. This may be useful if the type-checker
-- requires knowledge of which constructor is used to satisfy equality or
-- type-class constraints, but where each constructor is treated the
-- same.
cases :: Quasi q => Name -> q Exp -> q Exp -> q Exp
-- | The singleton kind-indexed data family.
-- | A SingI constraint is essentially an implicitly-passed
-- singleton. If you need to satisfy this constraint with an explicit
-- singleton, please see withSingI.
class SingI (a :: k)
sing :: SingI a => Sing a
-- | The SingKind class is essentially a kind class. It
-- classifies all kinds for which singletons are defined. The class
-- supports converting between a singleton type and the base (unrefined)
-- type which it is built from.
class kparam ~ KProxy => SingKind (kparam :: KProxy k) where type family DemoteRep kparam :: *
fromSing :: SingKind kparam => Sing (a :: k) -> DemoteRep kparam
toSing :: SingKind kparam => DemoteRep kparam -> SomeSing kparam
-- | Convenient synonym to refer to the kind of a type variable: type
-- KindOf (a :: k) = ('KProxy :: KProxy k)
type KindOf (a :: k) = (KProxy :: KProxy k)
-- | Convenient abbreviation for DemoteRep: type Demote (a :: k)
-- = DemoteRep ('KProxy :: KProxy k)
type Demote (a :: k) = DemoteRep (KProxy :: KProxy k)
-- | A re-export of the type-level (==) that conforms to the
-- singletons naming convention.
type (:==) a b = a == b
-- | Type-level If. If True a b ==> a; If
-- False a b ==> b
-- | Conditional over singletons
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
type (:&&) a b = a && b
-- | The singleton analogue of Eq. Unlike the definition for
-- Eq, it is required that instances define a body for '(%:==)'.
-- You may also supply a body for '(%:/=)'.
class kparam ~ KProxy => SEq (kparam :: KProxy k) where a %:/= b = sNot (a %:== b)
(%:==) :: SEq kparam => Sing a -> Sing b -> Sing (a :== b)
(%:/=) :: SEq kparam => Sing a -> Sing b -> Sing (a :/= b)
-- | The type constructor Any is type to which you can unsafely
-- coerce any lifted type, and back.
--
--
-- - It is lifted, and hence represented by a pointer
-- - It does not claim to be a data type, and that's important
-- for the code generator, because the code gen may enter a data
-- value but never enters a function value.
--
--
-- It's also used to instantiate un-constrained type variables after type
-- checking. For example, length has type
--
--
-- length :: forall a. [a] -> Int
--
--
-- and the list datacon for the empty list has type
--
--
-- [] :: forall a. [a]
--
--
-- In order to compose these two terms as length [] a type
-- application is required, but there is no constraint on the choice. In
-- this situation GHC uses Any:
--
--
-- length (Any *) ([] (Any *))
--
--
-- Note that Any is kind polymorphic, and takes a kind
-- k as its first argument. The kind of Any is thus
-- forall k. k -> k.
data Any :: k
-- | Members of the SDecide "kind" class support decidable equality.
-- Instances of this class are generated alongside singleton definitions
-- for datatypes that derive an Eq instance.
class kparam ~ KProxy => SDecide (kparam :: KProxy k)
(%~) :: SDecide kparam => Sing a -> Sing b -> Decision (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
--
-- Since: 4.7.0.0
data (:~:) (a :: k) (b :: k) :: k -> k -> *
Refl :: (:~:) k a1 a1
-- | A logically uninhabited data type.
data Void
-- | Because we can never create a value of type Void, a function
-- that type-checks at a -> Void shows that objects of type
-- a can never exist. Thus, we say that a is
-- Refuted
type Refuted a = a -> Void
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: (Refuted a) -> Decision a
-- | A concrete, promotable proxy type, for use at the kind level There are
-- no instances for this because it is intended at the kind level only
data KProxy t :: * -> *
KProxy :: KProxy t
-- | An existentially-quantified singleton. This type is useful when
-- you want a singleton type, but there is no way of knowing, at
-- compile-time, what the type index will be. To make use of this type,
-- you will generally have to use a pattern-match:
--
--
-- foo :: Bool -> ...
-- foo b = case toSing b of
-- SomeSing sb -> {- fancy dependently-typed code with sb -}
--
--
-- An example like the one above may be easier to write using
-- withSomeSing.
data SomeSing (kproxy :: KProxy k)
SomeSing :: Sing (a :: k) -> SomeSing (KProxy :: KProxy k)
-- | Defines functions and datatypes relating to the singleton for tuples,
-- including a singletons version of all the definitions in
-- Data.Tuple.
--
-- 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.Tuple. Also, please
-- excuse the apparent repeated variable names. This is due to an
-- interaction between Template Haskell and Haddock.
module Data.Singletons.Tuple
-- | The singleton kind-indexed data family.
type STuple0 (z_aizV :: ()) = Sing z_aizV
type STuple2 (z_aizW :: (,) a_12 b_13) = Sing z_aizW
type STuple3 (z_aiA5 :: (,,) a_12 b_13 c_14) = Sing z_aiA5
type STuple4 (z_aiAi :: (,,,) a_12 b_13 c_14 d_15) = Sing z_aiAi
type STuple5 (z_aiAz :: (,,,,) a_12 b_13 c_14 d_15 e_16) = Sing z_aiAz
type STuple6 (z_aiAU :: (,,,,,) a_12 b_13 c_14 d_15 e_16 f_17) = Sing z_aiAU
type STuple7 (z_aiBj :: (,,,,,,) a_12 b_13 c_14 d_15 e_16 f_17 g_18) = Sing z_aiBj
sFst :: Sing t_aqeV -> Sing (Fst t_aqeV)
sSnd :: Sing t_aqeW -> Sing (Snd t_aqeW)
sCurry :: (forall (t_aqeY :: (a_aqen, b_aqeo)). Sing t_aqeY -> Sing (t_aqeX t_aqeY)) -> Sing t_aqeZ -> Sing t_aqf0 -> Sing (Curry t_aqeX t_aqeZ t_aqf0)
sUncurry :: (forall (t_aqf2 :: a_aqet). Sing t_aqf2 -> forall (t_aqf3 :: b_aqeu). Sing t_aqf3 -> Sing (t_aqf1 t_aqf2 t_aqf3)) -> Sing t_aqf4 -> Sing (Uncurry t_aqf1 t_aqf4)
sSwap :: Sing t_aqf5 -> Sing (Swap t_aqf5)
-- | Defines the class SDecide, allowing for decidable equality over
-- singletons.
module Data.Singletons.Decide
-- | Members of the SDecide "kind" class support decidable equality.
-- Instances of this class are generated alongside singleton definitions
-- for datatypes that derive an Eq instance.
class kparam ~ KProxy => SDecide (kparam :: KProxy k)
(%~) :: SDecide kparam => Sing a -> Sing b -> Decision (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
--
-- Since: 4.7.0.0
data (:~:) (a :: k) (b :: k) :: k -> k -> *
Refl :: (:~:) k a1 a1
-- | A logically uninhabited data type.
data Void
-- | Because we can never create a value of type Void, a function
-- that type-checks at a -> Void shows that objects of type
-- a can never exist. Thus, we say that a is
-- Refuted
type Refuted a = a -> Void
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: (Refuted a) -> Decision a
-- | This module exports the basic definitions to use singletons. For
-- routine use, consider importing Prelude, which exports
-- constructors for singletons based on types in the Prelude.
--
-- You may also want to read
-- http://www.cis.upenn.edu/~eir/packages/singletons/README.html
-- and the original paper presenting this library, available at
-- http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf.
module Data.Singletons
-- | The singleton kind-indexed data family.
-- | A SingI constraint is essentially an implicitly-passed
-- singleton. If you need to satisfy this constraint with an explicit
-- singleton, please see withSingI.
class SingI (a :: k)
sing :: SingI a => Sing a
-- | The SingKind class is essentially a kind class. It
-- classifies all kinds for which singletons are defined. The class
-- supports converting between a singleton type and the base (unrefined)
-- type which it is built from.
class kparam ~ KProxy => SingKind (kparam :: KProxy k) where type family DemoteRep kparam :: *
fromSing :: SingKind kparam => Sing (a :: k) -> DemoteRep kparam
toSing :: SingKind kparam => DemoteRep kparam -> SomeSing kparam
-- | Convenient synonym to refer to the kind of a type variable: type
-- KindOf (a :: k) = ('KProxy :: KProxy k)
type KindOf (a :: k) = (KProxy :: KProxy k)
-- | Convenient abbreviation for DemoteRep: type Demote (a :: k)
-- = DemoteRep ('KProxy :: KProxy k)
type Demote (a :: k) = DemoteRep (KProxy :: KProxy k)
-- | A SingInstance wraps up a SingI instance for explicit
-- handling.
data SingInstance (a :: k)
SingInstance :: SingInstance a
-- | An existentially-quantified singleton. This type is useful when
-- you want a singleton type, but there is no way of knowing, at
-- compile-time, what the type index will be. To make use of this type,
-- you will generally have to use a pattern-match:
--
--
-- foo :: Bool -> ...
-- foo b = case toSing b of
-- SomeSing sb -> {- fancy dependently-typed code with sb -}
--
--
-- An example like the one above may be easier to write using
-- withSomeSing.
data SomeSing (kproxy :: KProxy k)
SomeSing :: Sing (a :: k) -> SomeSing (KProxy :: KProxy k)
-- | Get an implicit singleton (a SingI instance) from an explicit
-- one.
singInstance :: Sing a -> SingInstance a
-- | Convenience function for creating a context with an implicit singleton
-- available.
withSingI :: Sing n -> (SingI n => r) -> r
-- | Convert a normal datatype (like Bool) to a singleton for that
-- datatype, passing it into a continuation.
withSomeSing :: SingKind (KProxy :: KProxy k) => DemoteRep (KProxy :: KProxy k) -> (forall (a :: k). Sing a -> r) -> r
-- | Allows creation of a singleton when a proxy is at hand.
singByProxy :: SingI a => proxy a -> Sing a
-- | Allows creation of a singleton when a proxy# is at hand.
singByProxy# :: SingI a => Proxy# a -> Sing a
-- | A convenience function useful when we need to name a singleton value
-- multiple times. Without this function, each use of sing could
-- potentially refer to a different singleton, and one has to use type
-- signatures (often with ScopedTypeVariables) to ensure that
-- they are the same.
withSing :: SingI a => (Sing a -> b) -> b
-- | A convenience function that names a singleton satisfying a certain
-- property. If the singleton does not satisfy the property, then the
-- function returns Nothing. The property is expressed in terms of
-- the underlying representation of the singleton.
singThat :: (SingKind (KProxy :: KProxy k), SingI a) => (Demote a -> Bool) -> Maybe (Sing a)
-- | GHC 7.8 sometimes warns about incomplete pattern matches when no such
-- patterns are possible, due to GADT constraints. See the bug report at
-- https://ghc.haskell.org/trac/ghc/ticket/3927. In such cases,
-- it's useful to have a catch-all pattern that then has bugInGHC
-- as its right-hand side.
bugInGHC :: a
-- | The promotion of error
-- | The singleton for error
sError :: Sing (str :: Symbol) -> a
-- | A concrete, promotable proxy type, for use at the kind level There are
-- no instances for this because it is intended at the kind level only
data KProxy t :: * -> *
KProxy :: KProxy t
-- | A concrete, poly-kinded proxy type
data Proxy (t :: k) :: k -> *
Proxy :: Proxy
-- | Defines functions and datatypes relating to the singleton for '[]',
-- including a singletons version of a few of the definitions in
-- Data.List.
--
-- 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.List. Also, please excuse
-- the apparent repeated variable names. This is due to an interaction
-- between Template Haskell and Haddock.
module Data.Singletons.List
-- | The singleton kind-indexed data family.
type SList (z_aizM :: [] a_12) = Sing z_aizM
sHead :: Sing t_aqJ2 -> Sing (Head t_aqJ2)
sTail :: Sing t_aqJ3 -> Sing (Tail t_aqJ3)
(%:++) :: Sing t_aqJ0 -> Sing t_aqJ1 -> Sing ((:++) t_aqJ0 t_aqJ1)
sReverse :: Sing t_aqJ4 -> Sing (Reverse t_aqJ4)
-- | Defines functions and datatypes relating to the singleton for
-- Either, including a singletons version of all the definitions
-- in Data.Either.
--
-- 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.Either. Also, please
-- excuse the apparent repeated variable names. This is due to an
-- interaction between Template Haskell and Haddock.
module Data.Singletons.Either
-- | The singleton kind-indexed data family.
type SEither (z_aizC :: Either a_a7md b_a7me) = Sing z_aizC
sEither_ :: (forall (t_ar9A :: a_ar8m). Sing t_ar9A -> Sing (t_ar9z t_ar9A)) -> (forall (t_ar9C :: b_ar8o). Sing t_ar9C -> Sing (t_ar9B t_ar9C)) -> Sing t_ar9D -> Sing (Either_ t_ar9z t_ar9B t_ar9D)
sLefts :: Sing t_ar9E -> Sing (Lefts t_ar9E)
sRights :: Sing t_ar9F -> Sing (Rights t_ar9F)
sPartitionEithers :: Sing t_ar9G -> Sing (PartitionEithers t_ar9G)
sIsLeft :: Sing t_ar9J -> Sing (IsLeft t_ar9J)
sIsRight :: Sing t_ar9K -> Sing (IsRight t_ar9K)
-- | Defines functions and datatypes relating to the singleton for
-- Maybe, including a singletons version of all the definitions in
-- Data.Maybe.
--
-- 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.Maybe. Also, please
-- excuse the apparent repeated variable names. This is due to an
-- interaction between Template Haskell and Haddock.
module Data.Singletons.Maybe
-- | The singleton kind-indexed data family.
type SMaybe (z_aizx :: Maybe a_a4wb) = Sing z_aizx
sMaybe_ :: Sing t_arPW -> (forall (t_arPY :: a_arP0). Sing t_arPY -> Sing (t_arPX t_arPY)) -> Sing t_arPZ -> Sing (Maybe_ t_arPW t_arPX t_arPZ)
sIsJust :: Sing t_arQ0 -> Sing (IsJust t_arQ0)
sIsNothing :: Sing t_arQ1 -> Sing (IsNothing t_arQ1)
sFromJust :: Sing t_arQ2 -> Sing (FromJust t_arQ2)
sFromMaybe :: Sing t_arQ3 -> Sing t_arQ4 -> Sing (FromMaybe t_arQ3 t_arQ4)
sMaybeToList :: Sing t_arQ5 -> Sing (MaybeToList t_arQ5)
sListToMaybe :: Sing t_arQ6 -> Sing (ListToMaybe t_arQ6)
sCatMaybes :: Sing t_arQ7 -> Sing (CatMaybes t_arQ7)
sMapMaybe :: (forall (t_arQ9 :: a_arPj). Sing t_arQ9 -> Sing (t_arQ8 t_arQ9)) -> Sing t_arQa -> Sing (MapMaybe t_arQ8 t_arQa)
-- | Mimics the Haskell Prelude, but with singleton types. Includes the
-- basic singleton definitions. Note: This is currently very incomplete!
--
-- Because many of these definitions are produced by Template Haskell, it
-- is not possible to create proper Haddock documentation. Also, please
-- excuse the apparent repeated variable names. This is due to an
-- interaction between Template Haskell and Haddock.
module Data.Singletons.Prelude
-- | The singleton kind-indexed data family.
type SBool (z_aizw :: Bool) = Sing z_aizw
type SList (z_aizM :: [] a_12) = Sing z_aizM
type SMaybe (z_aizx :: Maybe a_a4wb) = Sing z_aizx
type SEither (z_aizC :: Either a_a7md b_a7me) = Sing z_aizC
type STuple0 (z_aizV :: ()) = Sing z_aizV
type STuple2 (z_aizW :: (,) a_12 b_13) = Sing z_aizW
type STuple3 (z_aiA5 :: (,,) a_12 b_13 c_14) = Sing z_aiA5
type STuple4 (z_aiAi :: (,,,) a_12 b_13 c_14 d_15) = Sing z_aiAi
type STuple5 (z_aiAz :: (,,,,) a_12 b_13 c_14 d_15 e_16) = Sing z_aiAz
type STuple6 (z_aiAU :: (,,,,,) a_12 b_13 c_14 d_15 e_16 f_17) = Sing z_aiAU
type STuple7 (z_aiBj :: (,,,,,,) a_12 b_13 c_14 d_15 e_16 f_17 g_18) = Sing z_aiBj
-- | Type-level If. If True a b ==> a; If
-- False a b ==> b
-- | Conditional over singletons
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
-- | Type-level "not"
sNot :: SBool a -> SBool (Not a)
type (:&&) a b = a && b
type (:||) a b = a || b
(%:&&) :: SBool a -> SBool b -> SBool (a :&& b)
(%:||) :: SBool a -> SBool b -> SBool (a :|| b)
(%:++) :: Sing t_aqJ0 -> Sing t_aqJ1 -> Sing ((:++) t_aqJ0 t_aqJ1)
sMaybe_ :: Sing t_arPW -> (forall (t_arPY :: a_arP0). Sing t_arPY -> Sing (t_arPX t_arPY)) -> Sing t_arPZ -> Sing (Maybe_ t_arPW t_arPX t_arPZ)
sEither_ :: (forall (t_ar9A :: a_ar8m). Sing t_ar9A -> Sing (t_ar9z t_ar9A)) -> (forall (t_ar9C :: b_ar8o). Sing t_ar9C -> Sing (t_ar9B t_ar9C)) -> Sing t_ar9D -> Sing (Either_ t_ar9z t_ar9B t_ar9D)
sFst :: Sing t_aqeV -> Sing (Fst t_aqeV)
sSnd :: Sing t_aqeW -> Sing (Snd t_aqeW)
sCurry :: (forall (t_aqeY :: (a_aqen, b_aqeo)). Sing t_aqeY -> Sing (t_aqeX t_aqeY)) -> Sing t_aqeZ -> Sing t_aqf0 -> Sing (Curry t_aqeX t_aqeZ t_aqf0)
sUncurry :: (forall (t_aqf2 :: a_aqet). Sing t_aqf2 -> forall (t_aqf3 :: b_aqeu). Sing t_aqf3 -> Sing (t_aqf1 t_aqf2 t_aqf3)) -> Sing t_aqf4 -> Sing (Uncurry t_aqf1 t_aqf4)