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


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


-- | This module exports the basic definitions to use singletons. See also
--   <tt>Prelude.Singletons</tt> from the <tt>singletons-base</tt> library,
--   which re-exports this module alongside many singled definitions based
--   on the <a>Prelude</a>.
--   
--   You may also want to read the original papers presenting this library,
--   available at
--   <a>https://richarde.dev/papers/2012/singletons/paper.pdf</a> and
--   <a>https://richarde.dev/papers/2014/promotion/promotion.pdf</a>.
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 <tt>singletons</tt> (see the Haddocks for
--   <tt>(<a>~&gt;</a>)</tt> for more information about this), and as a
--   result, the <a>Sing</a> instance for <a>SLambda</a> is one of the only
--   such instances defined in the <tt>singletons</tt> library rather than,
--   say, <tt>singletons-base</tt>.
newtype SLambda (f :: k1 ~> k2)
SLambda :: (forall (t :: k1). () => Sing t -> Sing (f @@ t)) -> SLambda (f :: k1 ~> k2)
[applySing] :: SLambda (f :: k1 ~> k2) -> forall (t :: k1). () => Sing t -> Sing (f @@ t)

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

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

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

-- | A version of the <a>SingI</a> class lifted to unary type constructors.
class forall (x :: k1). SingI x => SingI f x => SingI1 (f :: k1 -> k2)

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

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

-- | A version of the <a>SingI</a> class lifted to binary type
--   constructors.
class forall (x :: k1) (y :: k2). (SingI x, SingI y) => SingI f x y => SingI2 (f :: k1 -> k2 -> k3)

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

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

-- | The <a>SingKind</a> class is a <i>kind</i> 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 <a>SingKind</a> instance to be well behaved, it should obey the
--   following laws:
--   
--   <pre>
--   <a>toSing</a> . <a>fromSing</a> ≡ <a>SomeSing</a>
--   (\x -&gt; <a>withSomeSing</a> x <a>fromSing</a>) ≡ <a>id</a>
--   </pre>
--   
--   The final law can also be expressed in terms of the <a>FromSing</a>
--   pattern synonym:
--   
--   <pre>
--   (\(<a>FromSing</a> sing) -&gt; <a>FromSing</a> sing) ≡ <a>id</a>
--   </pre>
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 :: forall (a :: k). SingKind k => Sing a -> 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: <tt>type
--   KindOf (a :: k) = k</tt>
type KindOf (a :: k) = k

-- | Force GHC to unify the kinds of <tt>a</tt> and <tt>b</tt>. Note that
--   <tt>SameKind a b</tt> is different from <tt>KindOf a ~ KindOf b</tt>
--   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) = ()

-- | A <a>SingInstance</a> wraps up a <a>SingI</a> instance for explicit
--   handling.
data SingInstance (a :: k)
[SingInstance] :: forall {k} (a :: k). SingI a => SingInstance a

-- | An <i>existentially-quantified</i> 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:
--   
--   <pre>
--   foo :: Bool -&gt; ...
--   foo b = case toSing b of
--             SomeSing sb -&gt; {- fancy dependently-typed code with sb -}
--   </pre>
--   
--   An example like the one above may be easier to write using
--   <a>withSomeSing</a>.
data SomeSing k
[SomeSing] :: forall k (a :: k). Sing a -> SomeSing k

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

-- | An explicitly bidirectional pattern synonym for implicit singletons.
--   
--   As an <b>expression</b>: Constructs a singleton <tt>Sing a</tt> given
--   a implicit singleton constraint <tt>SingI a</tt>.
--   
--   As a <b>pattern</b>: Matches on an explicit <tt>Sing a</tt> witness
--   bringing an implicit <tt>SingI a</tt> 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 :: forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r

-- | Convert a normal datatype (like <a>Bool</a>) to a singleton for that
--   datatype, passing it into a continuation.
withSomeSing :: 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 <b>expression</b>: this takes a singleton to its demoted (base)
--   type.
--   
--   <pre>
--   &gt;&gt;&gt; :t FromSing \@Bool
--   FromSing \@Bool :: Sing a -&gt; Bool
--   
--   &gt;&gt;&gt; FromSing SFalse
--   False
--   </pre>
--   
--   As a <b>pattern</b>: It extracts a singleton from its demoted (base)
--   type.
--   
--   <pre>
--   singAnd :: <a>Bool</a> -&gt; <a>Bool</a> -&gt; <a>SomeSing</a> <a>Bool</a>
--   singAnd (<a>FromSing</a> singBool1) (<a>FromSing</a> singBool2) =
--     <a>SomeSing</a> (singBool1 %&amp;&amp; singBool2)
--   </pre>
--   
--   instead of writing it with <a>withSomeSing</a>:
--   
--   <pre>
--   singAnd bool1 bool2 =
--     <a>withSomeSing</a> bool1 $ singBool1 -&gt;
--       <a>withSomeSing</a> bool2 $ singBool2 -&gt;
--         <a>SomeSing</a> (singBool1 %&amp;&amp; singBool2)
--   </pre>
pattern FromSing :: forall k (a :: k). SingKind k => Sing a -> Demote k

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

-- | Convert a group of <a>SingI2</a> and <a>SingI</a> constraints
--   (representing a function to apply and its arguments, respectively)
--   into a single <a>SingI</a> constraint representing the application.
--   You will likely need the <tt>ScopedTypeVariables</tt> extension to use
--   this method the way you want.
usingSingI2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) 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 :: forall {k} (a :: k) proxy. SingI a => proxy a -> Sing a

-- | Allows creation of a singleton for a unary type constructor when a
--   proxy is at hand.
singByProxy1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) proxy. (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 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) proxy. (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 <a>SingKind</a> and
--   <a>SingI</a> behind the scenes, so <tt><a>demote</a> = <a>fromSing</a>
--   <a>sing</a></tt>.
--   
--   This function is intended to be used with <tt>TypeApplications</tt>.
--   For example:
--   
--   <pre>
--   &gt;&gt;&gt; demote @True
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; demote @(Nothing :: Maybe Ordering)
--   Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; demote @(Just EQ)
--   Just EQ
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; demote @'(True,EQ)
--   (True,EQ)
--   </pre>
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 <a>SingKind</a>,
--   <a>SingI1</a>, and <a>SingI</a> behind the scenes, so
--   <tt><a>demote1</a> = <a>fromSing</a> <a>sing1</a></tt>.
--   
--   This function is intended to be used with <tt>TypeApplications</tt>.
--   For example:
--   
--   <pre>
--   &gt;&gt;&gt; demote1 @Just @EQ
--   Just EQ
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; demote1 @('(,) True) @EQ
--   (True,EQ)
--   </pre>
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 <a>SingKind</a>,
--   <a>SingI2</a>, and <a>SingI</a> behind the scenes, so
--   <tt><a>demote2</a> = <a>fromSing</a> <a>sing2</a></tt>.
--   
--   This function is intended to be used with <tt>TypeApplications</tt>.
--   For example:
--   
--   <pre>
--   &gt;&gt;&gt; demote2 @'(,) @True @EQ
--   (True,EQ)
--   </pre>
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 <tt>proxy#</tt> is at hand.
singByProxy# :: forall {k} (a :: k). SingI a => Proxy# a -> Sing a

-- | Allows creation of a singleton for a unary type constructor when a
--   <tt>proxy#</tt> is at hand.
singByProxy1# :: forall {k1} {k} (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)

-- | Allows creation of a singleton for a binary type constructor when a
--   <tt>proxy#</tt> is at hand.
singByProxy2# :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2). (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 <a>sing</a> could
--   potentially refer to a different singleton, and one has to use type
--   signatures (often with <tt>ScopedTypeVariables</tt>) to ensure that
--   they are the same.
withSing :: forall {k} (a :: k) b. 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 <a>sing1</a> could potentially refer to a different
--   singleton, and one has to use type signatures (often with
--   <tt>ScopedTypeVariables</tt>) to ensure that they are the same.
withSing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) b. (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 <a>sing1</a> could potentially refer to a different
--   singleton, and one has to use type signatures (often with
--   <tt>ScopedTypeVariables</tt>) to ensure that they are the same.
withSing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) b. (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 <a>Nothing</a>. 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 <a>Nothing</a>. 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 <a>Nothing</a>. 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 <a>Sing</a>.
--   
--   Since <a>Sing</a> is a type family, it cannot be used directly in type
--   class instances. As one example, one cannot write a catch-all
--   <tt>instance <tt>SDecide</tt> k =&gt; <tt>TestEquality</tt>
--   (<a>Sing</a> k)</tt>. On the other hand, <a>WrappedSing</a> is a
--   perfectly ordinary data type, which means that it is quite possible to
--   define an <tt>instance <tt>SDecide</tt> k =&gt; <tt>TestEquality</tt>
--   (<a>WrappedSing</a> k)</tt>.
newtype WrappedSing (a :: k)
[WrapSing] :: forall k (a :: k). Sing a -> WrappedSing a

-- | The singleton for <a>WrappedSing</a>s. Informally, this is the
--   singleton type for other singletons.
newtype SWrappedSing (a1 :: WrappedSing a)
[SWrapSing] :: forall k (a :: k) (a1 :: WrappedSing a). Sing a -> SWrappedSing a1
type family UnwrapSing (ws :: WrappedSing a) :: 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 a b

-- | Something of kind <tt>a <a>~&gt;</a> b</tt> 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 <tt><a>README</a></tt>.
--   
--   The singleton for things of kind <tt>a <a>~&gt;</a> b</tt> is
--   <a>SLambda</a>. <a>SLambda</a> values can be constructed in one of two
--   ways:
--   
--   <ol>
--   <li>With the <tt>singFun*</tt> family of combinators (e.g.,
--   <a>singFun1</a>). For example, if you have:</li>
--   </ol>
--   
--   <pre>
--   type Id :: a -&gt; a
--   sId :: Sing a -&gt; Sing (Id a)
--   
--   </pre>
--   
--   Then you can construct a value of type <tt><a>Sing</a> @(a
--   <a>~&gt;</a> a)</tt> (that is, <tt><a>SLambda</a> @a @a</tt> like so:
--   
--   <pre>
--   sIdFun :: <a>Sing</a> @(a <a>~&gt;</a> a) IdSym0
--   sIdFun = singFun1 @IdSym0 sId
--   
--   </pre>
--   
--   Where <tt>IdSym0 :: a <a>~&gt;</a> a</tt> is the defunctionlized
--   version of <tt>Id</tt>.
--   
--   <ol>
--   <li>Using the <a>SingI</a> class. For example, <tt><a>sing</a>
--   @IdSym0</tt> is another way of defining <tt>sIdFun</tt> above. The
--   <tt>singletons-th</tt> library automatically generates <a>SingI</a>
--   instances for defunctionalization symbols such as
--   <tt>IdSym0</tt>.</li>
--   </ol>
--   
--   Normal type-level arrows <tt>(-&gt;)</tt> can be converted into
--   defunctionalization arrows <tt>(<a>~&gt;</a>)</tt> by the use of the
--   <a>TyCon</a> family of types. (Refer to the Haddocks for <a>TyCon1</a>
--   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 <tt>a -&gt; b</tt>, as they can be used in
--   defunctionalized settings by simply applying <tt>TyCon{N}</tt> with an
--   appropriate <tt>N</tt>.
--   
--   This includes the <tt>(-&gt;)</tt> type constructor itself, which is
--   of kind <tt><a>Type</a> -&gt; <a>Type</a> -&gt; <a>Type</a></tt>. One
--   can turn it into something of kind <tt><a>Type</a> <a>~&gt;</a>
--   <a>Type</a> <a>~&gt;</a> <a>Type</a></tt> by writing <tt><a>TyCon2</a>
--   (-&gt;)</tt>, or something of kind <tt><a>Type</a> -&gt; <a>Type</a>
--   <a>~&gt;</a> <a>Type</a></tt> by writing <tt><a>TyCon1</a> ((-&gt;)
--   t)</tt> (where <tt>t :: <a>Type</a></tt>).
type a ~> b = TyFun a b -> Type
infixr 0 ~>

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

-- | Similar to <a>TyCon1</a>, but for two-parameter type constructors.
type TyCon2 = TyCon
type TyCon3 = TyCon
type TyCon4 = TyCon
type TyCon5 = TyCon
type TyCon6 = TyCon
type TyCon7 = TyCon
type TyCon8 = TyCon

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

-- | An infix synonym for <a>Apply</a>
type (a :: k1 ~> k2) @@ (b :: k1) = Apply a b
infixl 9 @@

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

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

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

-- | An "internal" defunctionalization symbol used primarily in the
--   definition of <a>ApplyTyCon</a>.
--   
--   Note that this is only defined on GHC 8.6 or later.
data ApplyTyConAux2 (a :: k1 -> k2 -> k3) (b :: TyFun 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:
--   
--   <pre>
--   falses = sMap (singFun1 @NotSym0 sNot)
--                 (STrue `SCons` STrue `SCons` SNil)
--   </pre>
--   
--   There are a family of <tt>singFun...</tt> functions, keyed by the
--   number of parameters of the function.
singFun1 :: forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). SingFunction3 f -> Sing f
singFun4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). SingFunction4 f -> Sing f
singFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). SingFunction5 f -> Sing f
singFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). SingFunction6 f -> Sing f
singFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). SingFunction7 f -> Sing f
singFun8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). SingFunction8 f -> Sing f

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

-- | <a>Proxy</a> 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, <tt><a>Proxy</a> :: <a>Proxy</a> a</tt> is a safer
--   alternative to the <tt><a>undefined</a> :: a</tt> idiom.
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy (Void, Int -&gt; Int)
--   Proxy
--   </pre>
--   
--   Proxy can even hold types of higher kinds,
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Either
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Functor
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy complicatedStructure
--   Proxy
--   </pre>
data Proxy (t :: k)
Proxy :: Proxy (t :: k)
data DemoteSym0 (a :: TyFun Type Type)
type DemoteSym1 x = Demote x
data SameKindSym0 (a :: TyFun k k ~> Constraint)
data SameKindSym1 (a :: k) (b :: TyFun k Constraint)
type SameKindSym2 (x :: k) (y :: k) = SameKind x y
data KindOfSym0 (a :: TyFun k Type)
type KindOfSym1 (x :: k) = KindOf x
data (a :: TyFun Type Type ~> Type) ~>@#@$
infixr 0 ~>@#@$
data a ~>@#@$$ (b :: TyFun Type Type)
infixr 0 ~>@#@$$
type x ~>@#@$$$ y = x ~> y
infixr 0 ~>@#@$$$
data ApplySym0 (a1 :: TyFun a ~> b a ~> b)
data ApplySym1 (a1 :: a ~> b) (b1 :: TyFun a b)
type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
data (a1 :: TyFun a ~> b a ~> b) @@@#@$
infixl 9 @@@#@$
data (a1 :: a ~> b) @@@#@$$ (b1 :: TyFun a b)
infixl 9 @@@#@$$
type (f :: a ~> b) @@@#@$$$ (x :: a) = f @@ x
infixl 9 @@@#@$$$
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) (s :: Data.Singletons.Sing a). Data.Singletons.SingI a => Data.Singletons.SingI ('Data.Singletons.WrapSing s)
instance (Data.Singletons.SingKind k1, Data.Singletons.SingKind k2) => Data.Singletons.SingKind (k1 Data.Singletons.~> k2)
instance forall k (a :: k). Data.Singletons.SingKind (Data.Singletons.WrappedSing a)


-- | Defines the class <a>SDecide</a>, allowing for decidable equality over
--   singletons.
module Data.Singletons.Decide

-- | Members of the <a>SDecide</a> "kind" class support decidable equality.
--   Instances of this class are generated alongside singleton definitions
--   for datatypes that derive an <a>Eq</a> 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 <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
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 <a>Void</a>, a function
--   that type-checks at <tt>a -&gt; Void</tt> shows that objects of type
--   <tt>a</tt> can never exist. Thus, we say that <tt>a</tt> is
--   <a>Refuted</a>
type Refuted a = a -> Void

-- | A <a>Decision</a> about a type <tt>a</tt> is either a proof of
--   existence or a proof that <tt>a</tt> cannot exist.
data Decision a

-- | Witness for <tt>a</tt>
Proved :: a -> Decision a

-- | Proof that no <tt>a</tt> exists
Disproved :: Refuted a -> Decision a

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

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


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

-- | The workhorse that powers <a>ShowSing</a>. The only reason that
--   <a>ShowSing'</a> exists is to work around GHC's inability to put type
--   families in the head of a quantified constraint (see <a>this GHC
--   issue</a> for more details on this point). In other words, GHC will
--   not let you define <a>ShowSing</a> like so:
--   
--   <pre>
--   class (forall (z :: k). <a>Show</a> (<a>Sing</a> z)) =&gt; <a>ShowSing</a> k
--   </pre>
--   
--   By replacing <tt><a>Show</a> (<a>Sing</a> z)</tt> with <tt>ShowSing'
--   z</tt>, we are able to avoid this restriction for the most part.
--   
--   The superclass of <a>ShowSing'</a> is a bit peculiar:
--   
--   <pre>
--   class (forall (sing :: k -&gt; Type). sing ~ <a>Sing</a> =&gt; <a>Show</a> (sing z)) =&gt; <a>ShowSing'</a> (z :: k)
--   </pre>
--   
--   One might wonder why this superclass is used instead of this seemingly
--   more direct equivalent:
--   
--   <pre>
--   class <a>Show</a> (<a>Sing</a> z) =&gt; <a>ShowSing'</a> (z :: k)
--   </pre>
--   
--   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
--   <a>https://gitlab.haskell.org/ghc/ghc/-/issues/16365#note_189057</a>
--   for more on this point). The former's superclass, on the other hand,
--   does <i>not</i> 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 <a>ShowSing</a> 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
--   <tt><a>Show</a> (sing z)</tt> will match a <a>Show</a> instance for
--   <i>any</i> types <tt>sing :: k -&gt; Type</tt> and <tt>z :: k</tt>,
--   (where <tt>k</tt> is a kind variable), it is possible for GHC's
--   constraint solver to get into a situation where multiple instances
--   match <tt><a>Show</a> (sing z)</tt>, and GHC will get confused as a
--   result. Consider this example:
--   
--   <pre>
--   -- As in <a>Data.Singletons</a>
--   newtype <a>WrappedSing</a> :: forall k. k -&gt; Type where
--     <a>WrapSing</a> :: forall k (a :: k). { <a>unwrapSing</a> :: <a>Sing</a> a } -&gt; <a>WrappedSing</a> a
--   
--   instance <a>ShowSing</a> k =&gt; <a>Show</a> (<a>WrappedSing</a> (a :: k)) where
--     <a>showsPrec</a> _ s = <a>showString</a> "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}'
--   </pre>
--   
--   When typechecking the <a>Show</a> instance for <a>WrappedSing</a>, GHC
--   must fill in a default definition <tt><a>show</a> = defaultShow</tt>,
--   where <tt>defaultShow :: <a>Show</a> (<a>WrappedSing</a> a) =&gt;
--   <a>WrappedSing</a> a -&gt; <a>String</a></tt>. GHC's constraint solver
--   has two possible ways to satisfy the <tt><a>Show</a>
--   (<a>WrappedSing</a> a)</tt> constraint for <tt>defaultShow</tt>:
--   
--   <ol>
--   <li>The top-level instance declaration for <tt><a>Show</a>
--   (<a>WrappedSing</a> (a :: k))</tt> itself, and</li>
--   <li><tt><a>Show</a> (sing (z :: k))</tt> from the head of the
--   quantified constraint arising from <tt><a>ShowSing</a> k</tt>.</li>
--   </ol>
--   
--   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 <tt>Couldn't match type Sing with
--   WrappedSing</tt>. See
--   <a>https://gitlab.haskell.org/ghc/ghc/-/issues/17934</a> for a full
--   diagnosis of the issue.
--   
--   The bad news is that because of GHC#17934, we have to manually define
--   <a>show</a> (and <a>showList</a>) in the <a>Show</a> instance for
--   <a>WrappedSing</a> in order to avoid confusing GHC's constraint
--   solver. In other words, <tt>deriving <a>Show</a></tt> is a no-go for
--   <a>WrappedSing</a>. The good news is that situations like
--   <a>WrappedSing</a> are quite rare in the world of
--   <tt>singletons</tt>—most of the time, <a>Show</a> instances for
--   singleton types do <i>not</i> have the shape <tt><a>Show</a> (sing (z
--   :: k))</tt>, where <tt>k</tt> is a polymorphic kind variable. Rather,
--   most such instances instantiate <tt>k</tt> to a specific kind (e.g.,
--   <tt>Bool</tt>, or <tt>[a]</tt>), which means that they will not
--   overlap the head of the quantified superclass in <a>ShowSing'</a> as
--   observed above.
--   
--   Note that we define the single instance for <a>ShowSing'</a> without
--   the use of a quantified constraint in the instance context:
--   
--   <pre>
--   instance <a>Show</a> (<a>Sing</a> z) =&gt; <a>ShowSing'</a> (z :: k)
--   </pre>
--   
--   We <i>could</i> 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 :: k -> Type => Show sing z => ShowSing' (z :: k)
instance forall k (z :: k). GHC.Internal.Show.Show (Data.Singletons.Sing z) => Data.Singletons.ShowSing.ShowSing' z
instance (forall (z :: k). Data.Singletons.ShowSing.ShowSing' z) => Data.Singletons.ShowSing.ShowSing k
instance forall k (a :: k) (ws :: Data.Singletons.WrappedSing a). Data.Singletons.ShowSing.ShowSing k => GHC.Internal.Show.Show (Data.Singletons.SWrappedSing ws)
instance forall k (a :: k). Data.Singletons.ShowSing.ShowSing k => GHC.Internal.Show.Show (Data.Singletons.WrappedSing a)


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

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

-- | Unicode shorthand for <a>Sigma</a>.
type Σ = Sigma

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

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

-- | Unicode shorthand for <a>SSigma</a>.
type SΣ = SSigma

-- | Project the first element out of a dependent pair.
fstSigma :: forall s (t :: s ~> Type). 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 :: s ~> Type) (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 s r (t :: s ~> Type). (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 :: s ~> Type) r. (forall (fst :: s). () => (t @@ fst) -> r) -> Sigma s t -> r

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

-- | Zip two <a>Sigma</a> values together in a dependent fashion.
zipSigma :: forall a b c (f :: a ~> (b ~> c)) (p :: a ~> Type) (q :: b ~> Type) (r :: c ~> Type). Sing f -> (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 <a>Sigma</a> to a curried one.
--   
--   Together, <a>currySigma</a> and <a>uncurrySigma</a> witness an
--   isomorphism such that the following identities hold:
--   
--   <pre>
--   id1 :: forall a (b :: a ~&gt; Type) (c :: <a>Sigma</a> a b ~&gt; Type).
--          (forall (p :: Sigma a b). <a>SSigma</a> p -&gt; c @<tt> p)
--       -&gt; (forall (p :: Sigma a b). <a>SSigma</a> p -&gt; c </tt><tt> p)
--   id1 f = <a>uncurrySigma</a> </tt>a <tt>b </tt>c (<a>currySigma</a> <tt>a </tt>b <tt>c f)
--   
--   id2 :: forall a (b :: a ~&gt; Type) (c :: <a>Sigma</a> a b ~&gt; Type).
--          (forall (x :: a) (sx :: Sing x) (y :: b </tt><tt> x). Sing (<a>WrapSing</a> sx) -&gt; Sing y -&gt; c </tt><tt> (sx :&amp;: y))
--       -&gt; (forall (x :: a) (sx :: Sing x) (y :: b </tt><tt> x). Sing (<a>WrapSing</a> sx) -&gt; Sing y -&gt; c </tt><tt> (sx :&amp;: y))
--   id2 f = <a>currySigma</a> </tt>a <tt>b </tt>c (<a>uncurrySigma</a> <tt>a </tt>b @c f)
--   </pre>
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 :: WrappedSing x) -> Sing y -> c @@ (sx ':&: y :: Sigma a b)

-- | Convert a curried function on <a>Sigma</a> to an uncurried one.
--   
--   Together, <a>currySigma</a> and <a>uncurrySigma</a> witness an
--   isomorphism. (Refer to the documentation for <a>currySigma</a> 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 :: WrappedSing x) -> Sing y -> c @@ (sx ':&: y :: Sigma a b)) -> 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 a (f :: a Data.Singletons.~> *) (x :: a). GHC.Internal.Show.Show (Data.Singletons.Apply f x) => Data.Singletons.Sigma.ShowApply' f x
instance forall a (f :: a Data.Singletons.~> *). (forall (x :: a). Data.Singletons.Sigma.ShowApply' f x) => Data.Singletons.Sigma.ShowApply f
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.Internal.Show.Show (Data.Singletons.Sigma.SSigma sig)
instance forall s (t :: s Data.Singletons.~> *). (Data.Singletons.ShowSing.ShowSing s, Data.Singletons.Sigma.ShowApply t) => GHC.Internal.Show.Show (Data.Singletons.Sigma.Sigma s t)
instance forall a (f :: a Data.Singletons.~> *) (x :: a) (z :: Data.Singletons.Apply f x). GHC.Internal.Show.Show (Data.Singletons.Sing z) => Data.Singletons.Sigma.ShowSingApply' f x z
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 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)
