-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Basic singleton types and definitions
--   
--   singletons contains the basic types and definitions needed to
--   support dependently typed programming techniques in Haskell. This
--   library was originally presented in Dependently Typed Programming
--   with Singletons, published at the Haskell Symposium, 2012.
--   (https://richarde.dev/papers/2012/singletons/paper.pdf)
--   
--   singletons is intended to be a small, foundational library on
--   which other projects can build. As such, singletons has a
--   minimal dependency footprint and supports GHCs dating back to GHC 8.0.
--   For more information, consult the singletons
--   README.
--   
--   You may also be interested in the following related libraries:
--   
--   
--   
- The singletons-th library defines Template Haskell
--   functionality that allows promotion of term-level functions to
--   type-level equivalents and singling functions to dependently
--   typed equivalents.
--   
- The singletons-base library uses singletons-th
--   to define promoted and singled functions from the base
--   library, including the Prelude.
--   
@package singletons
@version 3.0.3

-- | This module exports the basic definitions to use singletons. See also
--   Prelude.Singletons from the singletons-base library,
--   which re-exports this module alongside many singled definitions based
--   on the Prelude.
--   
--   You may also want to read the original papers presenting this library,
--   available at
--   https://richarde.dev/papers/2012/singletons/paper.pdf and
--   https://richarde.dev/papers/2014/promotion/promotion.pdf.
module Data.Singletons

-- | The singleton kind-indexed type family.
type family Sing :: k -> Type

-- | The singleton type for functions. Functions have somewhat special
--   treatment in singletons (see the Haddocks for
--   (~>) for more information about this), and as a
--   result, the Sing instance for SLambda is one of the only
--   such instances defined in the singletons library rather than,
--   say, singletons-base.
newtype SLambda (f :: k1 ~> k2)
SLambda :: (forall t. Sing t -> Sing (f @@ t)) -> SLambda (f :: k1 ~> k2)
[applySing] :: SLambda (f :: k1 ~> k2) -> forall t. Sing t -> Sing (f @@ t)

-- | An infix synonym for applySing
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
infixl 9 @@

-- | A SingI constraint is essentially an implicitly-passed
--   singleton.
--   
--   In contrast to the SingKind class, which is parameterized over
--   data types promoted to the kind level, the SingI class is
--   parameterized over values promoted to the type level. To explain this
--   distinction another way, consider this code:
--   
--   
--   f = fromSing (sing @(T :: K))
--   
--   
--   Here, f uses methods from both SingI and
--   SingKind. However, the shape of each constraint is rather
--   different: using sing requires a 'SingI T' constraint, whereas
--   using fromSing requires a 'SingKind K' constraint.
--   
--   If you need to satisfy this constraint with an explicit singleton,
--   please see withSingI or the Sing pattern synonym.
class SingI a

-- | Produce the singleton explicitly. You will likely need the
--   ScopedTypeVariables extension to use this method the way you
--   want.
sing :: SingI a => Sing a

-- | A version of the SingI class lifted to unary type constructors.
class (forall x. SingI x => SingI (f x)) => SingI1 f

-- | Lift an explicit singleton through a unary type constructor. You will
--   likely need the ScopedTypeVariables extension to use this
--   method the way you want.
liftSing :: SingI1 f => Sing x -> Sing (f x)

-- | Produce a singleton explicitly using implicit SingI1 and
--   SingI constraints. You will likely need the
--   ScopedTypeVariables extension to use this method the way you
--   want.
sing1 :: (SingI1 f, SingI x) => Sing (f x)

-- | A version of the SingI class lifted to binary type
--   constructors.
class (forall x y. (SingI x, SingI y) => SingI (f x y)) => SingI2 f

-- | Lift explicit singletons through a binary type constructor. You will
--   likely need the ScopedTypeVariables extension to use this
--   method the way you want.
liftSing2 :: SingI2 f => Sing x -> Sing y -> Sing (f x y)

-- | Produce a singleton explicitly using implicit SingI2 and
--   SingI constraints. You will likely need the
--   ScopedTypeVariables extension to use this method the way you
--   want.
sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y)

-- | The SingKind class is 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.
--   
--   For a SingKind instance to be well behaved, it should obey the
--   following laws:
--   
--   
--   toSing . fromSing ≡ SomeSing
--   (\x -> withSomeSing x fromSing) ≡ id
--   
--   
--   The final law can also be expressed in terms of the FromSing
--   pattern synonym:
--   
--   
--   (\(FromSing sing) -> FromSing sing) ≡ id
--   
class SingKind k where {
    
    -- | Get a base type from the promoted kind. For example, <tt>Demote
    --   Bool</tt> will be the type <tt>Bool</tt>. Rarely, the type and kind do
    --   not match. For example, <tt>Demote Nat</tt> is <tt>Natural</tt>.
    type Demote k = (r :: Type) | r -> k;
}

-- | Convert a singleton to its unrefined version.
fromSing :: SingKind k => Sing (a :: k) -> Demote k

-- | Convert an unrefined type to an existentially-quantified singleton
--   type.
toSing :: SingKind k => Demote k -> SomeSing k

-- | Convenient synonym to refer to the kind of a type variable: type
--   KindOf (a :: k) = k
type KindOf (a :: k) = k

-- | Force GHC to unify the kinds of a and b. Note that
--   SameKind a b is different from KindOf a ~ KindOf b
--   in that the former makes the kinds unify immediately, whereas the
--   latter is a proposition that GHC considers as possibly false.
type SameKind (a :: k) (b :: k) = (() :: Constraint)

-- | A SingInstance wraps up a SingI instance for explicit
--   handling.
data SingInstance (a :: k)
[SingInstance] :: SingI a => 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 k
[SomeSing] :: Sing (a :: k) -> SomeSing k

-- | Get an implicit singleton (a SingI instance) from an explicit
--   one.
singInstance :: forall k (a :: k). Sing a -> SingInstance a

-- | An explicitly bidirectional pattern synonym for implicit singletons.
--   
--   As an expression: Constructs a singleton Sing a given
--   a implicit singleton constraint SingI a.
--   
--   As a pattern: Matches on an explicit Sing a witness
--   bringing an implicit SingI a constraint into scope.
pattern Sing :: forall k (a :: k). () => SingI a => Sing 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 :: forall k r. SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r

-- | An explicitly bidirectional pattern synonym for going between a
--   singleton and the corresponding demoted term.
--   
--   As an expression: this takes a singleton to its demoted (base)
--   type.
--   
--   
--   >>> :t FromSing \@Bool
--   FromSing \@Bool :: Sing a -> Bool
--   
--   >>> FromSing SFalse
--   False
--   
--   
--   As a pattern: It extracts a singleton from its demoted (base)
--   type.
--   
--   
--   singAnd :: Bool -> Bool -> SomeSing Bool
--   singAnd (FromSing singBool1) (FromSing singBool2) =
--     SomeSing (singBool1 %&& singBool2)
--   
--   
--   instead of writing it with withSomeSing:
--   
--   
--   singAnd bool1 bool2 =
--     withSomeSing bool1 $ singBool1 ->
--       withSomeSing bool2 $ singBool2 ->
--         SomeSing (singBool1 %&& singBool2)
--   
pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k

-- | Convert a group of SingI1 and SingI constraints
--   (representing a function to apply and its argument, respectively) into
--   a single SingI constraint representing the application. You
--   will likely need the ScopedTypeVariables extension to use
--   this method the way you want.
usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r

-- | Convert a group of SingI2 and SingI constraints
--   (representing a function to apply and its arguments, respectively)
--   into a single SingI constraint representing the application.
--   You will likely need the ScopedTypeVariables extension to use
--   this method the way you want.
usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => 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 for a unary type constructor when a
--   proxy is at hand.
singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)

-- | Allows creation of a singleton for a binary type constructor when a
--   proxy is at hand.
singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)

-- | A convenience function that takes a type as input and demotes it to
--   its value-level counterpart as output. This uses SingKind and
--   SingI behind the scenes, so demote = fromSing
--   sing.
--   
--   This function is intended to be used with TypeApplications.
--   For example:
--   
--   
--   >>> demote @True
--   True
--   
--   
--   
--   >>> demote @(Nothing :: Maybe Ordering)
--   Nothing
--   
--   
--   
--   >>> demote @(Just EQ)
--   Just EQ
--   
--   
--   
--   >>> demote @'(True,EQ)
--   (True,EQ)
--   
demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k

-- | A convenience function that takes a unary type constructor and its
--   argument as input, applies them, and demotes the result to its
--   value-level counterpart as output. This uses SingKind,
--   SingI1, and SingI behind the scenes, so
--   demote1 = fromSing sing1.
--   
--   This function is intended to be used with TypeApplications.
--   For example:
--   
--   
--   >>> demote1 @Just @EQ
--   Just EQ
--   
--   
--   
--   >>> demote1 @('(,) True) @EQ
--   (True,EQ)
--   
demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => Demote k2

-- | A convenience function that takes a binary type constructor and its
--   arguments as input, applies them, and demotes the result to its
--   value-level counterpart as output. This uses SingKind,
--   SingI2, and SingI behind the scenes, so
--   demote2 = fromSing sing2.
--   
--   This function is intended to be used with TypeApplications.
--   For example:
--   
--   
--   >>> demote2 @'(,) @True @EQ
--   (True,EQ)
--   
demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => Demote k3

-- | Allows creation of a singleton when a proxy# is at hand.
singByProxy# :: SingI a => Proxy# a -> Sing a

-- | Allows creation of a singleton for a unary type constructor when a
--   proxy# is at hand.
singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)

-- | Allows creation of a singleton for a binary type constructor when a
--   proxy# is at hand.
singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)

-- | 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 useful when we need to name a singleton value
--   for a unary type constructor multiple times. Without this function,
--   each use of sing1 could potentially refer to a different
--   singleton, and one has to use type signatures (often with
--   ScopedTypeVariables) to ensure that they are the same.
withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b

-- | A convenience function useful when we need to name a singleton value
--   for a binary type constructor multiple times. Without this function,
--   each use of sing1 could potentially refer to a different
--   singleton, and one has to use type signatures (often with
--   ScopedTypeVariables) to ensure that they are the same.
withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> 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 :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)

-- | A convenience function that names a singleton for a unary type
--   constructor 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.
singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x))

-- | A convenience function that names a singleton for a binary type
--   constructor 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.
singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y))

-- | A newtype around Sing.
--   
--   Since Sing is a type family, it cannot be used directly in type
--   class instances. As one example, one cannot write a catch-all
--   instance SDecide k => TestEquality
--   (Sing k). On the other hand, WrappedSing is a
--   perfectly ordinary data type, which means that it is quite possible to
--   define an instance SDecide k => TestEquality
--   (WrappedSing k).
newtype WrappedSing :: forall k. k -> Type
[WrapSing] :: forall k (a :: k). Sing a -> WrappedSing a

-- | The singleton for WrappedSings. Informally, this is the
--   singleton type for other singletons.
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
[SWrapSing] :: forall k (a :: k) (ws :: WrappedSing a). Sing a -> SWrappedSing ws
type family UnwrapSing (ws :: WrappedSing (a :: k)) :: Sing a

-- | Representation of the kind of a type-level function. The difference
--   between term-level arrows and this type-level arrow is that at the
--   term level applications can be unsaturated, whereas at the type level
--   all applications have to be fully saturated.
data TyFun :: Type -> Type -> Type

-- | Something of kind a ~> b is a defunctionalized type
--   function that is not necessarily generative or injective.
--   Defunctionalized type functions (also called "defunctionalization
--   symbols") can be partially applied, even if the original type function
--   cannot be. For more information on how this works, see the "Promotion
--   and partial application" section of the README.
--   
--   The singleton for things of kind a ~> b is
--   SLambda. SLambda values can be constructed in one of two
--   ways:
--   
--   
--   
- With the singFun* family of combinators (e.g.,
--   singFun1). For example, if you have:
--   
--   
--   
--   type Id :: a -> a
--   sId :: Sing a -> Sing (Id a)
--   
--   
--   
--   Then you can construct a value of type Sing @(a
--   ~> a) (that is, SLambda @a @a like so:
--   
--   
--   sIdFun :: Sing @(a ~> a) IdSym0
--   sIdFun = singFun1 @IdSym0 sId
--   
--   
--   
--   Where IdSym0 :: a ~> a is the defunctionlized
--   version of Id.
--   
--   
--   
- Using the SingI class. For example, sing
--   @IdSym0 is another way of defining sIdFun above. The
--   singletons-th library automatically generates SingI
--   instances for defunctionalization symbols such as
--   IdSym0.
--   
--   
--   Normal type-level arrows (->) can be converted into
--   defunctionalization arrows (~>) by the use of the
--   TyCon family of types. (Refer to the Haddocks for TyCon1
--   to see an example of this in practice.) For this reason, we do not
--   make an effort to define defunctionalization symbols for most type
--   constructors of kind a -> b, as they can be used in
--   defunctionalized settings by simply applying TyCon{N} with an
--   appropriate N.
--   
--   This includes the (->) type constructor itself, which is
--   of kind Type -> Type -> Type. One
--   can turn it into something of kind Type ~>
--   Type ~> Type by writing TyCon2
--   (->), or something of kind Type -> Type
--   ~> Type by writing TyCon1 ((->)
--   t) (where t :: Type).
type a ~> b = TyFun a b -> Type
infixr 0 ~>

-- | Wrapper for converting the normal type-level arrow into a
--   ~>. For example, given:
--   
--   
--   data Nat = Zero | Succ Nat
--   type family Map (a :: a ~> b) (a :: [a]) :: [b]
--     Map f '[] = '[]
--     Map f (x ': xs) = Apply f x ': Map f xs
--   
--   
--   We can write:
--   
--   
--   Map (TyCon1 Succ) [Zero, Succ Zero]
--   
type TyCon1 = (TyCon :: (k1 -> k2) -> (k1 ~> k2))

-- | Similar to TyCon1, but for two-parameter type constructors.
type TyCon2 = (TyCon :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3))
type TyCon3 = (TyCon :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4))
type TyCon4 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5))
type TyCon5 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6))
type TyCon6 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7))
type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8))
type TyCon8 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9))

-- | Type level function application
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

-- | An infix synonym for Apply
type a @@ b = Apply a b
infixl 9 @@

-- | Workhorse for the TyCon1, etc., types. This can be used
--   directly in place of any of the TyConN types, but it will
--   work only with monomorphic types. When GHC#14645 is fixed, this
--   should fully supersede the TyConN types.
--   
--   Note that this is only defined on GHC 8.6 or later. Prior to GHC 8.6,
--   TyCon1 et al. were defined as separate data types.
data family TyCon :: (k1 -> k2) -> unmatchable_fun

-- | An "internal" definition used primary in the Apply instance for
--   TyCon.
--   
--   Note that this only defined on GHC 8.6 or later.
type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)

-- | An "internal" defunctionalization symbol used primarily in the
--   definition of ApplyTyCon, as well as the SingI instances
--   for TyCon1, TyCon2, etc.
--   
--   Note that this is only defined on GHC 8.6 or later.
data ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)

-- | An "internal" defunctionalization symbol used primarily in the
--   definition of ApplyTyCon.
--   
--   Note that this is only defined on GHC 8.6 or later.
data ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)

-- | Use this function when passing a function on singletons as a
--   higher-order function. You will need visible type application to get
--   this to work. For example:
--   
--   
--   falses = sMap (singFun1 @NotSym0 sNot)
--                 (STrue `SCons` STrue `SCons` SNil)
--   
--   
--   There are a family of singFun... functions, keyed by the
--   number of parameters of the function.
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun4 :: forall f. SingFunction4 f -> Sing f
singFun5 :: forall f. SingFunction5 f -> Sing f
singFun6 :: forall f. SingFunction6 f -> Sing f
singFun7 :: forall f. SingFunction7 f -> Sing f
singFun8 :: forall f. SingFunction8 f -> Sing f

-- | This is the inverse of singFun1, and likewise for the other
--   unSingFun... functions.
unSingFun1 :: forall f. Sing f -> SingFunction1 f
unSingFun2 :: forall f. Sing f -> SingFunction2 f
unSingFun3 :: forall f. Sing f -> SingFunction3 f
unSingFun4 :: forall f. Sing f -> SingFunction4 f
unSingFun5 :: forall f. Sing f -> SingFunction5 f
unSingFun6 :: forall f. Sing f -> SingFunction6 f
unSingFun7 :: forall f. Sing f -> SingFunction7 f
unSingFun8 :: forall f. Sing f -> SingFunction8 f
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
applySing2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f
pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
applySing3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f
pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
applySing4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f
pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
applySing5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f
pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
applySing6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f
pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
applySing7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f
pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
applySing8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f
type SingFunction1 (f :: a1 ~> b) = forall t. Sing t -> Sing (f @@ t)
type SingFunction2 (f :: a1 ~> a2 ~> b) = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f @@ t1 @@ t2 @@ t3)
type SingFunction4 (f :: a1 ~> a2 ~> a3 ~> a4 ~> b) = forall t1 t2 t3 t4. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4)
type SingFunction5 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) = forall t1 t2 t3 t4 t5. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5)
type SingFunction6 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) = forall t1 t2 t3 t4 t5 t6. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6)
type SingFunction7 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) = forall t1 t2 t3 t4 t5 t6 t7. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7)
type SingFunction8 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) = forall t1 t2 t3 t4 t5 t6 t7 t8. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7 @@ t8)

-- | Proxy is a type that holds no data, but has a phantom parameter
--   of arbitrary type (or even kind). Its use is to provide type
--   information, even though there is no value available of that type (or
--   it may be too costly to create one).
--   
--   Historically, Proxy :: Proxy a is a safer
--   alternative to the undefined :: a idiom.
--   
--   
--   >>> Proxy :: Proxy (Void, Int -> Int)
--   Proxy
--   
--   
--   Proxy can even hold types of higher kinds,
--   
--   
--   >>> Proxy :: Proxy Either
--   Proxy
--   
--   
--   
--   >>> Proxy :: Proxy Functor
--   Proxy
--   
--   
--   
--   >>> Proxy :: Proxy complicatedStructure
--   Proxy
--   
data () => Proxy (t :: k)
Proxy :: Proxy (t :: k)
data DemoteSym0 :: Type ~> Type
type DemoteSym1 x = Demote x
data SameKindSym0 :: forall k. k ~> k ~> Constraint
data SameKindSym1 :: forall k. k -> k ~> Constraint
type SameKindSym2 (x :: k) (y :: k) = SameKind x y
data KindOfSym0 :: forall k. k ~> Type
type KindOfSym1 (x :: k) = KindOf x
data (~>@#@$) :: Type ~> Type ~> Type
infixr 0 ~>@#@$
data (~>@#@$$) :: Type -> Type ~> Type
infixr 0 ~>@#@$$
type x ~>@#@$$$ y = x ~> y
infixr 0 ~>@#@$$$
data ApplySym0 :: forall a b. (a ~> b) ~> a ~> b
data ApplySym1 :: forall a b. (a ~> b) -> a ~> b
type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
data (@@@#@$) :: forall a b. (a ~> b) ~> a ~> b
infixl 9 @@@#@$
data (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b
infixl 9 @@@#@$$
type (f :: a ~> b) @@@#@$$$ (x :: a) = f @@ x
infixl 9 @@@#@$$$
instance (Data.Singletons.SingKind k1, Data.Singletons.SingKind k2) => Data.Singletons.SingKind (k1 Data.Singletons.~> k2)
instance forall k1 k2 k3 k4 k5 k6 k7 k8 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f', Data.Singletons.SingI g, Data.Singletons.SingI h) => Data.Singletons.SingI (f a b c d e f' g h), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon8 f)
instance forall k1 k2 k3 k4 k5 k6 k7 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f', Data.Singletons.SingI g) => Data.Singletons.SingI (f a b c d e f' g), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon7 f)
instance forall k1 k2 k3 k4 k5 k6 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f') => Data.Singletons.SingI (f a b c d e f'), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon6 f)
instance forall k1 k2 k3 k4 k5 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e) => Data.Singletons.SingI (f a b c d e), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon5 f)
instance forall k1 k2 k3 k4 kr (f :: k1 -> k2 -> k3 -> k4 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d) => Data.Singletons.SingI (f a b c d), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon4 f)
instance forall k1 k2 k3 kr (f :: k1 -> k2 -> k3 -> kr). (forall (a :: k1) (b :: k2) (c :: k3). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c) => Data.Singletons.SingI (f a b c), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon3 f)
instance forall k1 k2 kr (f :: k1 -> k2 -> kr). (forall (a :: k1) (b :: k2). (Data.Singletons.SingI a, Data.Singletons.SingI b) => Data.Singletons.SingI (f a b), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon2 f)
instance forall k1 kr (f :: k1 -> kr). (forall (a :: k1). Data.Singletons.SingI a => Data.Singletons.SingI (f a), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon1 f)
instance forall k (a :: k). Data.Singletons.SingKind (Data.Singletons.WrappedSing a)
instance forall k (a :: k) (s :: Data.Singletons.Sing a). Data.Singletons.SingI a => Data.Singletons.SingI ('Data.Singletons.WrapSing s)

-- | 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 SDecide k

-- | Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b)
infix 4 %~

-- | 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.
data () => (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:

-- | 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 suitable default implementation for testEquality that
--   leverages SDecide.
decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b)

-- | A suitable default implementation for testCoercion that
--   leverages SDecide.
decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b)
instance Data.Singletons.Decide.SDecide k => Data.Type.Equality.TestEquality Data.Singletons.WrappedSing
instance Data.Singletons.Decide.SDecide k => Data.Type.Coercion.TestCoercion Data.Singletons.WrappedSing

-- | Defines the class ShowSing which is useful for defining
--   Show instances for singleton types. Because ShowSing
--   crucially relies on QuantifiedConstraints, it is only defined
--   if this library is built with GHC 8.6 or later.
module Data.Singletons.ShowSing

-- | In addition to the promoted and singled versions of the Show
--   class that singletons-base provides, it is also useful to be
--   able to directly define Show instances for singleton types
--   themselves. Doing so is almost entirely straightforward, as a derived
--   Show instance does 90 percent of the work. The last 10
--   percent—getting the right instance context—is a bit tricky, and that's
--   where ShowSing comes into play.
--   
--   As an example, let's consider the singleton type for lists. We want to
--   write an instance with the following shape:
--   
--   
--   instance ??? => Show (SList (z :: [k])) where
--     showsPrec p SNil = showString "SNil"
--     showsPrec p (SCons sx sxs) =
--       showParen (p > 10) $ showString "SCons " . showsPrec 11 sx
--                          . showSpace . showsPrec 11 sxs
--   
--   
--   To figure out what should go in place of ???, observe that we
--   require the type of each field to also be Show instances. In
--   other words, we need something like (Show (Sing (a
--   :: k))). But this isn't quite right, as the type variable
--   a doesn't appear in the instance head. In fact, this
--   a type is really referring to an existentially quantified
--   type variable in the SCons constructor, so it doesn't make
--   sense to try and use it like this.
--   
--   Luckily, the QuantifiedConstraints language extension
--   provides a solution to this problem. This lets you write a context of
--   the form (forall a. Show (Sing (a :: k))),
--   which demands that there be an instance for Show
--   (Sing (a :: k)) that is parametric in the use of
--   a. This lets us write something closer to this:
--   
--   
--   instance (forall a. Show (Sing (a :: k))) => SList (Sing (z :: [k])) where ...
--   
--   
--   The ShowSing class is a thin wrapper around (forall a.
--   Show (Sing (a :: k))). With ShowSing, our
--   final instance declaration becomes this:
--   
--   
--   instance ShowSing k => Show (SList (z :: [k])) where ...
--   
--   
--   In fact, this instance can be derived:
--   
--   
--   deriving instance ShowSing k => Show (SList (z :: [k]))
--   
--   
--   (Note that the actual definition of ShowSing is slightly more
--   complicated than what this documentation might suggest. For the full
--   story, refer to the documentation for ShowSing'.)
--   
--   When singling a derived Show instance, singletons-th
--   will also generate a Show instance for the corresponding
--   singleton type using ShowSing. In other words, if you give
--   singletons-th a derived Show instance, then you'll
--   receive the following in return:
--   
--   
--   
- A promoted (PShow) instance
--   
- A singled (SShow) instance
--   
- A Show instance for the singleton type
--   
--   
--   What a bargain!
class (forall (z :: k). ShowSing' z) => ShowSing (k :: Type)

-- | The workhorse that powers ShowSing. The only reason that
--   ShowSing' exists is to work around GHC's inability to put type
--   families in the head of a quantified constraint (see this GHC
--   issue for more details on this point). In other words, GHC will
--   not let you define ShowSing like so:
--   
--   
--   class (forall (z :: k). Show (Sing z)) => ShowSing k
--   
--   
--   By replacing Show (Sing z) with ShowSing'
--   z, we are able to avoid this restriction for the most part.
--   
--   The superclass of ShowSing' is a bit peculiar:
--   
--   
--   class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing' (z :: k)
--   
--   
--   One might wonder why this superclass is used instead of this seemingly
--   more direct equivalent:
--   
--   
--   class Show (Sing z) => ShowSing' (z :: k)
--   
--   
--   Actually, these aren't equivalent! The latter's superclass mentions a
--   type family in its head, and this gives GHC's constraint solver
--   trouble when trying to match this superclass against other
--   constraints. (See the discussion beginning at
--   https://gitlab.haskell.org/ghc/ghc/-/issues/16365#note_189057
--   for more on this point). The former's superclass, on the other hand,
--   does not mention a type family in its head, which allows it to
--   match other constraints more easily. It may sound like a small
--   difference, but it's the only reason that ShowSing is able to
--   work at all without a significant amount of additional workarounds.
--   
--   The quantified superclass has one major downside. Although the head of
--   the quantified superclass is more eager to match, which is usually a
--   good thing, it can bite under certain circumstances. Because
--   Show (sing z) will match a Show instance for
--   any types sing :: k -> Type and z :: k,
--   (where k is a kind variable), it is possible for GHC's
--   constraint solver to get into a situation where multiple instances
--   match Show (sing z), and GHC will get confused as a
--   result. Consider this example:
--   
--   
--   -- As in Data.Singletons
--   newtype WrappedSing :: forall k. k -> Type where
--     WrapSing :: forall k (a :: k). { unwrapSing :: Sing a } -> WrappedSing a
--   
--   instance ShowSing k => Show (WrappedSing (a :: k)) where
--     showsPrec _ s = showString "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}'
--   
--   
--   When typechecking the Show instance for WrappedSing, GHC
--   must fill in a default definition show = defaultShow,
--   where defaultShow :: Show (WrappedSing a) =>
--   WrappedSing a -> String. GHC's constraint solver
--   has two possible ways to satisfy the Show
--   (WrappedSing a) constraint for defaultShow:
--   
--   
--   
- The top-level instance declaration for Show
--   (WrappedSing (a :: k)) itself, and
--   
- Show (sing (z :: k)) from the head of the
--   quantified constraint arising from ShowSing k.
--   
--   
--   In practice, GHC will choose (2), as local quantified constraints
--   shadow global constraints. This confuses GHC greatly, causing it to
--   error out with an error akin to Couldn't match type Sing with
--   WrappedSing. See
--   https://gitlab.haskell.org/ghc/ghc/-/issues/17934 for a full
--   diagnosis of the issue.
--   
--   The bad news is that because of GHC#17934, we have to manually define
--   show (and showList) in the Show instance for
--   WrappedSing in order to avoid confusing GHC's constraint
--   solver. In other words, deriving Show is a no-go for
--   WrappedSing. The good news is that situations like
--   WrappedSing are quite rare in the world of
--   singletons—most of the time, Show instances for
--   singleton types do not have the shape Show (sing (z
--   :: k)), where k is a polymorphic kind variable. Rather,
--   most such instances instantiate k to a specific kind (e.g.,
--   Bool, or [a]), which means that they will not
--   overlap the head of the quantified superclass in ShowSing' as
--   observed above.
--   
--   Note that we define the single instance for ShowSing' without
--   the use of a quantified constraint in the instance context:
--   
--   
--   instance Show (Sing z) => ShowSing' (z :: k)
--   
--   
--   We could define this instance with a quantified constraint in
--   the instance context, and it would be equally as expressive. But it
--   doesn't provide any additional functionality that the non-quantified
--   version gives, so we opt for the non-quantified version, which is
--   easier to read.
class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing' (z :: k)
instance forall k (a :: k) (ws :: Data.Singletons.WrappedSing a). Data.Singletons.ShowSing.ShowSing k => GHC.Show.Show (Data.Singletons.SWrappedSing ws)
instance (forall (z :: k). Data.Singletons.ShowSing.ShowSing' z) => Data.Singletons.ShowSing.ShowSing k
instance forall k (a :: k). Data.Singletons.ShowSing.ShowSing k => GHC.Show.Show (Data.Singletons.WrappedSing a)
instance forall k (z :: k). GHC.Show.Show (Data.Singletons.Sing z) => Data.Singletons.ShowSing.ShowSing' z

-- | Defines Sigma, a dependent pair data type, and related
--   functions.
module Data.Singletons.Sigma

-- | A dependent pair.
data Sigma (s :: Type) :: (s ~> Type) -> Type
[:&:] :: forall s t fst. Sing (fst :: s) -> (t @@ fst) -> Sigma s t
infixr 4 :&:

-- | Unicode shorthand for Sigma.
type Σ = Sigma

-- | The singleton kind-indexed type family.
type family Sing :: k -> Type

-- | The singleton type for Sigma.
data SSigma :: forall s t. Sigma s t -> Type
[:%&:] :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t)
infixr 4 :%&:

-- | Unicode shorthand for SSigma.
type SΣ = SSigma

-- | Project the first element out of a dependent pair.
fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s

-- | Project the first element out of a dependent pair.
type family FstSigma (sig :: Sigma s t) :: s

-- | Project the second element out of a dependent pair.
sndSigma :: forall s t (sig :: Sigma s t). SingKind (t @@ FstSigma sig) => SSigma sig -> Demote (t @@ FstSigma sig)

-- | Project the second element out of a dependent pair.
type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig

-- | Project the first element out of a dependent pair using
--   continuation-passing style.
projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r

-- | Project the second element out of a dependent pair using
--   continuation-passing style.
projSigma2 :: forall s t r. (forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r

-- | Map across a Sigma value in a dependent fashion.
mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). (p @@ x) -> q @@ (f @@ x)) -> Sigma a p -> Sigma b q

-- | Zip two Sigma values together in a dependent fashion.
zipSigma :: Sing (f :: a ~> (b ~> c)) -> (forall (x :: a) (y :: b). (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)) -> Sigma a p -> Sigma b q -> Sigma c r

-- | Convert an uncurried function on Sigma to a curried one.
--   
--   Together, currySigma and uncurrySigma witness an
--   isomorphism such that the following identities hold:
--   
--   
--   id1 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
--          (forall (p :: Sigma a b). SSigma p -> c @ p)
--       -> (forall (p :: Sigma a b). SSigma p -> c  p)
--   id1 f = uncurrySigma a b c (currySigma a b c f)
--   
--   id2 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
--          (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (WrapSing sx) -> Sing y -> c  (sx :&: y))
--       -> (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (WrapSing sx) -> Sing y -> c  (sx :&: y))
--   id2 f = currySigma a b c (uncurrySigma a b @c f)
--   
currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (p :: Sigma a b). SSigma p -> c @@ p) -> forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)

-- | Convert a curried function on Sigma to an uncurried one.
--   
--   Together, currySigma and uncurrySigma witness an
--   isomorphism. (Refer to the documentation for currySigma for
--   more details.)
uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)) -> forall (p :: Sigma a b). SSigma p -> c @@ p
class (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
class (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
class Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
class Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)
instance forall s (t :: s Data.Singletons.~> *) (sig :: Data.Singletons.Sigma.Sigma s t). (Data.Singletons.ShowSing.ShowSing s, Data.Singletons.Sigma.ShowSingApply t) => GHC.Show.Show (Data.Singletons.Sigma.SSigma sig)
instance forall a (f :: a Data.Singletons.~> *). (forall (x :: a) (z :: Data.Singletons.Apply f x). Data.Singletons.Sigma.ShowSingApply' f x z) => Data.Singletons.Sigma.ShowSingApply f
instance forall a (f :: a Data.Singletons.~> *) (x :: a) (z :: Data.Singletons.Apply f x). GHC.Show.Show (Data.Singletons.Sing z) => Data.Singletons.Sigma.ShowSingApply' f x z
instance forall s (t :: s Data.Singletons.~> *). (Data.Singletons.ShowSing.ShowSing s, Data.Singletons.Sigma.ShowApply t) => GHC.Show.Show (Data.Singletons.Sigma.Sigma s t)
instance forall a (f :: a Data.Singletons.~> *). (forall (x :: a). Data.Singletons.Sigma.ShowApply' f x) => Data.Singletons.Sigma.ShowApply f
instance forall a (f :: a Data.Singletons.~> *) (x :: a). GHC.Show.Show (Data.Singletons.Apply f x) => Data.Singletons.Sigma.ShowApply' f x
instance forall s (t :: s Data.Singletons.~> *) (fst :: s) (a :: Data.Singletons.Sing fst) (b :: t Data.Singletons.@@ fst). (Data.Singletons.SingI fst, Data.Singletons.SingI b) => Data.Singletons.SingI (a 'Data.Singletons.Sigma.:&: b)
