    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MagicHash #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilyDependencies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE ViewPatterns #-}

    #if __GLASGOW_HASKELL__ >= 806
    {-# LANGUAGE QuantifiedConstraints #-}
    #else
    {-# LANGUAGE TypeInType #-}
    #endif

    #if __GLASGOW_HASKELL__ >= 810
    {-# LANGUAGE StandaloneKindSignatures #-}
    #endif

    #if __GLASGOW_HASKELL__ >= 910
    {-# LANGUAGE TypeAbstractions #-}
    #endif

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons
    -- Copyright   :  (C) 2013 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- 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 (
      -- * Main singleton definitions

      Sing, SLambda(..), (@@),

      SingI(..),
      SingI1(..), sing1,
      SingI2(..), sing2,
      SingKind(..),

      -- * Working with singletons
      KindOf, SameKind,
      SingInstance(..), SomeSing(..),
      singInstance, pattern Sing, withSingI,
      withSomeSing, pattern FromSing,
      usingSingI1, usingSingI2,
      singByProxy, singByProxy1, singByProxy2,
      demote, demote1, demote2,

      singByProxy#, singByProxy1#, singByProxy2#,
      withSing, withSing1, withSing2,
      singThat, singThat1, singThat2,

      -- ** @WrappedSing@
      WrappedSing(..), SWrappedSing(..), UnwrapSing,
      -- $SingletonsOfSingletons

      -- ** Defunctionalization
      TyFun, type (~>),
      TyCon1, TyCon2, TyCon3, TyCon4, TyCon5, TyCon6, TyCon7, TyCon8,
      Apply, type (@@),
    #if __GLASGOW_HASKELL__ >= 806
      TyCon, ApplyTyCon, ApplyTyConAux1, ApplyTyConAux2,
    #endif

      -- ** Defunctionalized singletons
      -- | When calling a higher-order singleton function, you need to use a
      -- @singFun...@ function to wrap it. See 'singFun1'.
      singFun1, singFun2, singFun3, singFun4, singFun5, singFun6, singFun7,
      singFun8,
      unSingFun1, unSingFun2, unSingFun3, unSingFun4, unSingFun5,
      unSingFun6, unSingFun7, unSingFun8,
      -- $SLambdaPatternSynonyms
      pattern SLambda2, applySing2,
      pattern SLambda3, applySing3,
      pattern SLambda4, applySing4,
      pattern SLambda5, applySing5,
      pattern SLambda6, applySing6,
      pattern SLambda7, applySing7,
      pattern SLambda8, applySing8,

      -- | These type synonyms are exported only to improve error messages; users
      -- should not have to mention them.
      SingFunction1, SingFunction2, SingFunction3, SingFunction4, SingFunction5,
      SingFunction6, SingFunction7, SingFunction8,

      -- * Auxiliary functions
      Proxy(..),

      -- * Defunctionalization symbols
      DemoteSym0, DemoteSym1,
      SameKindSym0, SameKindSym1, SameKindSym2,
      KindOfSym0, KindOfSym1,
      type (~>@#@$), type (~>@#@$$), type (~>@#@$$$),
      ApplySym0, ApplySym1, ApplySym2,
      type (@@@#@$), type (@@@#@$$), type (@@@#@$$$)
      ) where

    import Data.Kind (Constraint, Type)
    import Data.Proxy (Proxy(..))
    import GHC.Exts (Proxy#)
    import Unsafe.Coerce (unsafeCoerce)

    #if MIN_VERSION_base(4,17,0)
    import GHC.Exts (withDict)
    #endif

    -- | Convenient synonym to refer to the kind of a type variable:
    -- @type KindOf (a :: k) = k@
    #if __GLASGOW_HASKELL__ >= 810
    type KindOf :: k -> Type
    #endif
    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.
    #if __GLASGOW_HASKELL__ >= 810
    type SameKind :: k -> k -> Constraint
    #endif
    type SameKind (a :: k) (b :: k) = (() :: Constraint)

    ----------------------------------------------------------------------
    ---- Sing & friends --------------------------------------------------
    ----------------------------------------------------------------------

    -- | The singleton kind-indexed type family.
    #if __GLASGOW_HASKELL__ >= 810
    type Sing :: k -> Type
    #endif
    #if __GLASGOW_HASKELL__ >= 910
    type family Sing @k :: k -> Type
    #else
    type family Sing :: k -> Type
    #endif

    {-
    Note [The kind of Sing]
    ~~~~~~~~~~~~~~~~~~~~~~~
    It is important to define Sing like this:

      type Sing :: k -> Type
      type family Sing

    Or, equivalently,

      type family Sing :: k -> Type

    There are other conceivable ways to define Sing, but they all suffer from
    various drawbacks:

    * type family Sing :: forall k. k -> Type

      Surprisingly, this is /not/ equivalent to `type family Sing :: k -> Type`.
      The difference lies in their arity, i.e., the number of arguments that must
      be supplied in order to apply Sing. The former declaration has arity 0, while
      the latter has arity 1 (this is more obvious if you write the declaration as
      GHCi would display it with -fprint-explicit-kinds enabled:
      `type family Sing @k :: k -> Type`).

      The former declaration having arity 0 is actually what makes it useless. If
      we were to adopt an arity-0 definition of `Sing`, then in order to write
      `type instance Sing = SFoo`, GHC would require that `SFoo` must have the kind
      `forall k. k -> Type`, and moreover, the kind /must/ be polymorphic in `k`.
      This is undesirable, because in practice, every single `Sing` instance in the
      wild must monomorphize `k` (e.g., `SBool` monomorphizes it to `Bool`), so an
      arity-0 `Sing` simply won't work. In contrast, the current arity-1 definition
      of `Sing` /does/ let you monomorphize `k` in type family instances.

    * type family Sing (a :: k) = (r :: Type) | r -> a

      Again, this is not equivalent to `type family Sing :: k -> Type`. This
      version of `Sing` has arity 2, since one must supply both `k` and `a` in
      order to apply it. While an arity-2 `Sing` is not suffer from the same
      polymorphism issues as the arity-0 `Sing` in the previous bullet point, it
      does suffer from another issue in that it cannot be partially applied. This
      is because its `a` argument /must/ be supplied, whereas with the arity-1
      `Sing`, it is perfectly admissible to write `Sing` without an explicit `a`
      argument. (Its invisible `k` argument is filled in automatically behind the
      scenes.)

    * type family Sing = (r :: k -> Type) | r -> k

      This is the same as `type family Sing :: k -> Type`, but with an injectivity
      annotation. Technically, this definition isn't /wrong/, but the injectivity
      annotation is actually unnecessary. Because the return kind of `Sing` is
      declared to be `k -> Type`, the `Sing` type constructor is automatically
      injective, so `Sing a1 ~ Sing a2` implies `a1 ~~ a2`.

      Another way of phrasing this, using the terminology of Dependent Haskell, is
      that the arrow in `Sing`'s return kind is /matchable/, which implies that
      `Sing` is an injective type constructor as a consequence.
    -}

    -- | 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 v'Sing' pattern synonym.
    #if __GLASGOW_HASKELL__ >= 900
    type SingI :: forall {k}. k -> Constraint
    #endif
    class SingI a where
      -- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
      -- extension to use this method the way you want.
      sing :: Sing a

    -- | A version of the 'SingI' class lifted to unary type constructors.
    #if __GLASGOW_HASKELL__ >= 900
    type SingI1 :: forall {k1} {k2}. (k1 -> k2) -> Constraint
    #endif
    class
    #if __GLASGOW_HASKELL__ >= 806
      (forall x. SingI x => SingI (f x)) =>
    #endif
        SingI1 f where
      -- | 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 :: 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)
    sing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    sing1 = Sing x -> Sing (f x)
    forall (x :: k1). Sing x -> Sing (f x)
    forall {k1} {k2} (f :: k1 -> k2) (x :: k1).
    SingI1 f =>
    Sing x -> Sing (f x)
    liftSing Sing x
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | A version of the 'SingI' class lifted to binary type constructors.
    #if __GLASGOW_HASKELL__ >= 900
    type SingI2 :: forall {k1} {k2} {k3}. (k1 -> k2 -> k3) -> Constraint
    #endif
    class
    #if __GLASGOW_HASKELL__ >= 806
      (forall x y. (SingI x, SingI y) => SingI (f x y)) =>
    #endif
        SingI2 f where
      -- | Lift explicit singletons through a binary type constructor.
      -- You will likely need the @ScopedTypeVariables@ extension to use this
      -- method the way you want.
      liftSing2 :: 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)
    sing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2 = Sing x -> Sing y -> Sing (f x y)
    forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (f x y)
    forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
    SingI2 f =>
    Sing x -> Sing y -> Sing (f x y)
    liftSing2 Sing x
    forall {k} (a :: k). SingI a => Sing a
    sing Sing y
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | 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.
    #if __GLASGOW_HASKELL__ >= 802
    {-# COMPLETE Sing #-}
    #endif
    pattern Sing :: forall k (a :: k). () => SingI a => Sing a
    pattern $mSing :: forall {r} {k} {a :: k}.
    Sing a -> (SingI a => r) -> ((# #) -> r) -> r
    $bSing :: forall {k} (a :: k). SingI a => Sing a
    Sing <- (singInstance -> SingInstance)
      where Sing = Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | 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'
    -- @
    #if __GLASGOW_HASKELL__ >= 810
    type SingKind :: Type -> Constraint
    #endif
    class SingKind k where
      -- | Get a base type from the promoted kind. For example,
      -- @Demote Bool@ will be the type @Bool@. Rarely, the type and kind do not
      -- match. For example, @Demote Nat@ is @Natural@.
      type Demote k = (r :: Type) | r -> k

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

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

    -- | 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'.
    #if __GLASGOW_HASKELL__ >= 810
    type SomeSing :: Type -> Type
    #endif
    data SomeSing k where
      SomeSing :: Sing (a :: k) -> SomeSing k

    -- | 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)
    -- @
    #if __GLASGOW_HASKELL__ >= 802
    {-# COMPLETE FromSing #-}
    #endif
    pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
    pattern $mFromSing :: forall {r} {k}.
    SingKind k =>
    Demote k -> (forall {a :: k}. Sing a -> r) -> ((# #) -> r) -> r
    $bFromSing :: forall k (a :: k). SingKind k => Sing a -> Demote k
    FromSing sng <- ((\Demote k
    demotedVal -> Demote k -> (forall (a :: k). Sing a -> SomeSing k) -> SomeSing k
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote k
    demotedVal Sing a -> SomeSing k
    forall (a :: k). Sing a -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing) -> SomeSing sng)
      where FromSing Sing a
    sng = Sing a -> Demote k
    forall (a :: k). Sing a -> Demote k
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing a
    sng

    ----------------------------------------------------------------------
    ---- WrappedSing -----------------------------------------------------
    ----------------------------------------------------------------------

    -- | 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)@.
    #if __GLASGOW_HASKELL__ >= 810
    type WrappedSing :: k -> Type
    #endif
    newtype WrappedSing :: forall k. k -> Type where
      WrapSing :: forall k (a :: k). { forall k (a :: k). WrappedSing a -> Sing a
    unwrapSing :: Sing a } -> WrappedSing a

    -- | The singleton for 'WrappedSing's. Informally, this is the singleton type
    -- for other singletons.
    #if __GLASGOW_HASKELL__ >= 810
    type SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
    #endif
    newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
      SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
                   { forall k (a :: k) (ws :: WrappedSing a). SWrappedSing ws -> Sing a
    sUnwrapSing :: Sing a } -> SWrappedSing ws
    #if __GLASGOW_HASKELL__ >= 808
    type instance Sing @(WrappedSing a) =
    #else
    type instance Sing =
    #endif
      SWrappedSing

    #if __GLASGOW_HASKELL__ >= 810
    type UnwrapSing :: forall k (a :: k). WrappedSing a -> Sing a
    #endif
    type family UnwrapSing (ws :: WrappedSing (a :: k)) :: Sing a where
      UnwrapSing ('WrapSing s) = s

    instance SingKind (WrappedSing a) where
      type Demote (WrappedSing a) = WrappedSing a
      fromSing :: forall (a :: WrappedSing a). Sing a -> Demote (WrappedSing a)
    fromSing (SWrapSing Sing a
    s) = Sing a -> WrappedSing a
    forall k (a :: k). Sing a -> WrappedSing a
    WrapSing Sing a
    s
      toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)
    toSing (WrapSing Sing a
    s) = Sing (ZonkAny 1) -> SomeSing (WrappedSing a)
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing (ZonkAny 1) -> SomeSing (WrappedSing a))
    -> Sing (ZonkAny 1) -> SomeSing (WrappedSing a)
    forall a b. (a -> b) -> a -> b
    $ Sing a -> SWrappedSing (ZonkAny 1)
    forall k (a :: k) (ws :: WrappedSing a). Sing a -> SWrappedSing ws
    SWrapSing Sing a
    s

    instance forall a (s :: Sing a). SingI a => SingI ('WrapSing s) where
      sing :: Sing ('WrapSing s)
    sing = Sing a -> SWrappedSing ('WrapSing s)
    forall k (a :: k) (ws :: WrappedSing a). Sing a -> SWrappedSing ws
    SWrapSing Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing

    ----------------------------------------------------------------------
    ---- SingInstance ----------------------------------------------------
    ----------------------------------------------------------------------

    -- | A 'SingInstance' wraps up a 'SingI' instance for explicit handling.
    #if __GLASGOW_HASKELL__ >= 810
    type SingInstance :: k -> Type
    #endif
    data SingInstance (a :: k) where
      SingInstance :: SingI a => SingInstance a

    -- | Get an implicit singleton (a 'SingI' instance) from an explicit one.
    singInstance :: forall k (a :: k). Sing a -> SingInstance a
    singInstance :: forall k (a :: k). Sing a -> SingInstance a
    singInstance Sing a
    s = (SingI a => SingInstance a) -> SingInstance a
    with_sing_i SingInstance a
    SingI a => SingInstance a
    forall {k} (a :: k). SingI a => SingInstance a
    SingInstance
      where
        with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
    #if MIN_VERSION_base(4,17,0)
        with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
    with_sing_i = forall (cls :: Constraint) meth r.
    WithDict cls meth =>
    meth -> (cls => r) -> r
    withDict @(SingI a) @(Sing a) Sing a
    s
    #else
        with_sing_i si = unsafeCoerce (Don'tInstantiate si) s

    -- dirty implementation of explicit-to-implicit conversion
    #if __GLASGOW_HASKELL__ >= 810
    type DI :: k -> Type
    #endif
    newtype DI a = Don'tInstantiate (SingI a => SingInstance a)
    #endif

    ----------------------------------------------------------------------
    ---- Defunctionalization ---------------------------------------------
    ----------------------------------------------------------------------

    -- | 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.
    #if __GLASGOW_HASKELL__ >= 810
    type TyFun :: Type -> Type -> Type
    #endif
    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
    -- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@.
    --
    -- The singleton for things of kind @a '~>' b@ is 'SLambda'. 'SLambda' values
    -- can be constructed in one of two ways:
    --
    -- 1. 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@.
    --
    -- 2. 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'@).
    #if __GLASGOW_HASKELL__ >= 810
    type (~>) :: Type -> Type -> Type
    #endif
    type a ~> b = TyFun a b -> Type
    infixr 0 ~>

    -- | Type level function application
    #if __GLASGOW_HASKELL__ >= 810
    type Apply :: (k1 ~> k2) -> k1 -> k2
    #endif
    type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

    -- | An infix synonym for `Apply`
    #if __GLASGOW_HASKELL__ >= 810
    type (@@) :: (k1 ~> k2) -> k1 -> k2
    #endif
    type a @@ b = Apply a b
    infixl 9 @@

    #if __GLASGOW_HASKELL__ >= 806
    -- | 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.
    #if __GLASGOW_HASKELL__ >= 810
    type TyCon :: (k1 -> k2) -> unmatchable_fun
    #endif
    data family TyCon :: (k1 -> k2) -> unmatchable_fun
    -- That unmatchable_fun should really be a function of k1 and k2,
    -- but GHC 8.4 doesn't support type family calls in the result kind
    -- of a data family. It should. See GHC#14645.

    -- The result kind of this is also a bit wrong; it should line
    -- up with unmatchable_fun above. However, we can't do that
    -- because GHC is too stupid to remember that f's kind can't
    -- have more than one argument when kind-checking the RHS of
    -- the second equation. Note that this infelicity is independent
    -- of the problem in the kind of TyCon. There is no GHC ticket
    -- here because dealing with inequality like this is hard, and
    -- I (Richard) wasn't sure what concrete value the ticket would
    -- have, given that we don't know how to begin fixing it.

    -- | An \"internal\" definition used primary in the 'Apply' instance for
    -- 'TyCon'.
    --
    -- Note that this only defined on GHC 8.6 or later.
    #if __GLASGOW_HASKELL__ >= 810
    type ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
    #endif
    #if __GLASGOW_HASKELL__ >= 910
    type family ApplyTyCon @k1 @k2 @unmatchable_fun :: (k1 -> k2) -> (k1 ~> unmatchable_fun) where
    #else
    type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun) where
    #endif
    #if __GLASGOW_HASKELL__ >= 808
      ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2
      ApplyTyCon @k1 @k2         @k2              = ApplyTyConAux1
    #else
      ApplyTyCon = (ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun))
      ApplyTyCon = (ApplyTyConAux1 :: (k1 -> k2)       -> (k1 ~> k2))
    #endif
    -- Upon first glance, the definition of ApplyTyCon (as well as the
    -- corresponding Apply instance for TyCon) seems a little indirect. One might
    -- wonder why these aren't defined like so:
    --
    --   type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where
    --     ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x)
    --     ApplyTyCon f x                     = f x
    --
    --   type instance Apply (TyCon f) x = ApplyTyCon f x
    --
    -- This also works, but it requires that ApplyTyCon always be applied to a
    -- minimum of two arguments. In particular, this rules out a trick that we use
    -- elsewhere in the library to write SingI instances for different TyCons,
    -- which relies on partial applications of ApplyTyCon:
    --
    --   instance forall k1 k2 (f :: k1 -> k2).
    --            ( forall a. SingI a => SingI (f a)
    --            , (ApplyTyCon :: (k1 -> k2) -> (k1 ~> k2)) ~ ApplyTyConAux1
    --            ) => SingI (TyCon1 f) where
    #if __GLASGOW_HASKELL__ >= 808
    type instance Apply @k1 @k3 (TyCon @k1 @k2 @(k1 ~> k3) f) x =
    #else
    type instance Apply (TyCon f) x =
    #endif
      ApplyTyCon f @@ x

    -- | 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.
    #if __GLASGOW_HASKELL__ >= 810
    type ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
    #endif
    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.
    #if __GLASGOW_HASKELL__ >= 810
    type ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)
    #endif
    data ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)

    type instance Apply (ApplyTyConAux1 f) x = f x
    type instance Apply (ApplyTyConAux2 f) x = TyCon (f x)

    #if __GLASGOW_HASKELL__ >= 810
    type TyCon1          :: (k1 -> k2) -> (k1 ~> k2)
    type TyCon2          :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3)
    type TyCon3          :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4)
    type TyCon4          :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5)
    type TyCon5          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6)
    type TyCon6          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7)
    type TyCon7          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8)
    type TyCon8          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9)
    #endif

    -- | 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]
    #if __GLASGOW_HASKELL__ >= 910
    type TyCon1 @k1 @k2 = (TyCon :: (k1 -> k2) -> (k1 ~> k2))

    -- | Similar to 'TyCon1', but for two-parameter type constructors.
    type TyCon2 @k1 @k2 @k3 =
                  (TyCon :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3))
    type TyCon3 @k1 @k2 @k3 @k4 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4))
    type TyCon4 @k1 @k2 @k3 @k4 @k5 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5))
    type TyCon5 @k1 @k2 @k3 @k4 @k5 @k6 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6))
    type TyCon6 @k1 @k2 @k3 @k4 @k5 @k6 @k7 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7))
    type TyCon7 @k1 @k2 @k3 @k4 @k5 @k6 @k7 @k8 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8))
    type TyCon8 @k1 @k2 @k3 @k4 @k5 @k6 @k7 @k8 @k9 =
                  (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
                         -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9))
    #else
    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))
    #endif
    #else
    -- | 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]
    data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)

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

    type instance Apply (TyCon1 f) x = f x
    type instance Apply (TyCon2 f) x = TyCon1 (f x)
    type instance Apply (TyCon3 f) x = TyCon2 (f x)
    type instance Apply (TyCon4 f) x = TyCon3 (f x)
    type instance Apply (TyCon5 f) x = TyCon4 (f x)
    type instance Apply (TyCon6 f) x = TyCon5 (f x)
    type instance Apply (TyCon7 f) x = TyCon6 (f x)
    type instance Apply (TyCon8 f) x = TyCon7 (f x)
    #endif

    ----------------------------------------------------------------------
    ---- Defunctionalized Sing instance and utilities --------------------
    ----------------------------------------------------------------------

    -- | 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@.
    #if __GLASGOW_HASKELL__ >= 810
    type SLambda :: (k1 ~> k2) -> Type
    #endif
    newtype SLambda (f :: k1 ~> k2) =
      SLambda { forall k1 k2 (f :: k1 ~> k2).
    SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
    applySing :: forall t. Sing t -> Sing (f @@ t) }
    #if __GLASGOW_HASKELL__ >= 808
    type instance Sing @(k1 ~> k2) =
    #else
    type instance Sing =
    #endif
      SLambda

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

    -- | Note that this instance's 'toSing' implementation crucially relies on the fact
    -- that the 'SingKind' instances for 'k1' and 'k2' both satisfy the 'SingKind' laws.
    -- If they don't, 'toSing' might produce strange results!
    instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
      type Demote (k1 ~> k2) = Demote k1 -> Demote k2
      fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2)
    fromSing Sing a
    sFun Demote k1
    x = Demote k1 -> (forall (a :: k1). Sing a -> Demote k2) -> Demote k2
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote k1
    x (Sing (Apply a a) -> Demote k2
    forall (a :: k2). Sing a -> Demote k2
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing (Apply a a) -> Demote k2)
    -> (Sing a -> Sing (Apply a a)) -> Sing a -> Demote k2
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SLambda a -> forall (t :: k1). Sing t -> Sing (a @@ t)
    forall k1 k2 (f :: k1 ~> k2).
    SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
    applySing SLambda a
    Sing a
    sFun)
      toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)
    toSing Demote (k1 ~> k2)
    f = Sing (ZonkAny 0) -> SomeSing (k1 ~> k2)
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing Sing (ZonkAny 0)
    forall (f :: k1 ~> k2). Sing f
    slam
        where
          -- Here, we are essentially "manufacturing" a type-level version of the
          -- function f. As long as k1 and k2 obey the SingKind laws, this is a
          -- perfectly fine thing to do, since the computational content of Sing f
          -- will be isomorphic to that of the function f.
          slam :: forall (f :: k1 ~> k2). Sing f
          slam :: forall (f :: k1 ~> k2). Sing f
    slam = forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    forall (f :: k1 ~> k2). SingFunction1 f -> Sing f
    singFun1 @f Sing t -> Sing (f @@ t)
    forall (t :: k1). Sing t -> Sing (f @@ t)
    lam
            where
              -- Here's the tricky part. We need to demote the argument Sing, apply the
              -- term-level function f to it, and promote it back to a Sing. However,
              -- we don't have a way to convince the typechecker that for all argument
              -- types t, f @@ t should be the same thing as res, which motivates the
              -- use of unsafeCoerce.
              lam :: forall (t :: k1). Sing t -> Sing (f @@ t)
              lam :: forall (t :: k1). Sing t -> Sing (f @@ t)
    lam Sing t
    x = Demote k2
    -> (forall (a :: k2). Sing a -> Sing (Apply f t))
    -> Sing (Apply f t)
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing (Demote (k1 ~> k2)
    Demote k1 -> Demote k2
    f (Sing t -> Demote k1
    forall (a :: k1). Sing a -> Demote k1
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    x)) (\(Sing a
    r :: Sing res) -> Sing a -> Sing (Apply f t)
    forall a b. a -> b
    unsafeCoerce Sing a
    r)

    #if __GLASGOW_HASKELL__ >= 810
    type SingFunction1 :: (a1 ~> b) -> Type
    type SingFunction2 :: (a1 ~> a2 ~> b) -> Type
    type SingFunction3 :: (a1 ~> a2 ~> a3 ~> b) -> Type
    type SingFunction4 :: (a1 ~> a2 ~> a3 ~> a4 ~> b) -> Type
    type SingFunction5 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) -> Type
    type SingFunction6 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) -> Type
    type SingFunction7 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) -> Type
    type SingFunction8 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) -> Type
    #endif

    type SingFunction1 (f :: a1 ~> b) =
      forall t. Sing t -> Sing (f @@ t)

    -- | 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
    singFun1 :: forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 SingFunction1 f
    f = SingFunction1 f -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda Sing t -> Sing (f @@ t)
    SingFunction1 f
    f

    type SingFunction2 (f :: a1 ~> a2 ~> b) =
      forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
    singFun2 :: forall f. SingFunction2 f -> Sing f
    singFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    SingFunction2 f -> Sing f
    singFun2 SingFunction2 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction1 (f @@ t) -> Sing (f @@ t)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> Sing t -> Sing (Apply (f @@ t) t)
    SingFunction2 f
    f Sing t
    x))

    type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) =
         forall t1 t2 t3.
         Sing t1 -> Sing t2 -> Sing t3
      -> Sing (f @@ t1 @@ t2 @@ t3)
    singFun3 :: forall f. SingFunction3 f -> Sing f
    singFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    SingFunction3 f -> Sing f
    singFun3 SingFunction3 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction2 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    SingFunction2 f -> Sing f
    singFun2 (Sing t -> Sing t1 -> Sing t2 -> Sing (Apply (Apply (f @@ t) t1) t2)
    SingFunction3 f
    f Sing t
    x))

    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)
    singFun4 :: forall f. SingFunction4 f -> Sing f
    singFun4 :: forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    SingFunction4 f -> Sing f
    singFun4 SingFunction4 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction3 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    SingFunction3 f -> Sing f
    singFun3 (Sing t
    -> Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing (Apply (Apply (Apply (f @@ t) t1) t2) t3)
    SingFunction4 f
    f Sing t
    x))

    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)
    singFun5 :: forall f. SingFunction5 f -> Sing f
    singFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    SingFunction5 f -> Sing f
    singFun5 SingFunction5 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction4 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    SingFunction4 f -> Sing f
    singFun4 (Sing t
    -> Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing (Apply (Apply (Apply (Apply (f @@ t) t1) t2) t3) t4)
    SingFunction5 f
    f Sing t
    x))

    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)
    singFun6 :: forall f. SingFunction6 f -> Sing f
    singFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    SingFunction6 f -> Sing f
    singFun6 SingFunction6 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction5 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    SingFunction5 f -> Sing f
    singFun5 (Sing t
    -> Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing
         (Apply (Apply (Apply (Apply (Apply (f @@ t) t1) t2) t3) t4) t5)
    SingFunction6 f
    f Sing t
    x))

    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)
    singFun7 :: forall f. SingFunction7 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
    singFun7 SingFunction7 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction6 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    SingFunction6 f -> Sing f
    singFun6 (Sing t
    -> Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing t6
    -> Sing
         (Apply
            (Apply (Apply (Apply (Apply (Apply (f @@ t) t1) t2) t3) t4) t5) t6)
    SingFunction7 f
    f Sing t
    x))

    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)
    singFun8 :: forall f. SingFunction8 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
    singFun8 SingFunction8 f
    f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
    forall k1 k2 (f :: k1 ~> k2).
    (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
    SLambda (\Sing t
    x -> SingFunction7 (f @@ t) -> Sing (f @@ t)
    forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    SingFunction7 f -> Sing f
    singFun7 (Sing t
    -> Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing t6
    -> Sing t7
    -> Sing
         (Apply
            (Apply
               (Apply (Apply (Apply (Apply (Apply (f @@ t) t1) t2) t3) t4) t5) t6)
            t7)
    SingFunction8 f
    f Sing t
    x))

    -- | This is the inverse of 'singFun1', and likewise for the other
    -- @unSingFun...@ functions.
    unSingFun1 :: forall f. Sing f -> SingFunction1 f
    unSingFun1 :: forall {a1} {b} (f :: a1 ~> b). Sing f -> SingFunction1 f
    unSingFun1 Sing f
    sf = SLambda f -> forall (t :: a1). Sing t -> Sing (f @@ t)
    forall k1 k2 (f :: k1 ~> k2).
    SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
    applySing SLambda f
    Sing f
    sf

    unSingFun2 :: forall f. Sing f -> SingFunction2 f
    unSingFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    Sing f -> SingFunction2 f
    unSingFun2 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction1 (Apply f t1)
    forall {a1} {b} (f :: a1 ~> b). Sing f -> SingFunction1 f
    unSingFun1 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun3 :: forall f. Sing f -> SingFunction3 f
    unSingFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    Sing f -> SingFunction3 f
    unSingFun3 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction2 (Apply f t1)
    forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    Sing f -> SingFunction2 f
    unSingFun2 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun4 :: forall f. Sing f -> SingFunction4 f
    unSingFun4 :: forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    Sing f -> SingFunction4 f
    unSingFun4 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction3 (Apply f t1)
    forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    Sing f -> SingFunction3 f
    unSingFun3 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun5 :: forall f. Sing f -> SingFunction5 f
    unSingFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    Sing f -> SingFunction5 f
    unSingFun5 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction4 (Apply f t1)
    forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    Sing f -> SingFunction4 f
    unSingFun4 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun6 :: forall f. Sing f -> SingFunction6 f
    unSingFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    Sing f -> SingFunction6 f
    unSingFun6 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction5 (Apply f t1)
    forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    Sing f -> SingFunction5 f
    unSingFun5 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun7 :: forall f. Sing f -> SingFunction7 f
    unSingFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    Sing f -> SingFunction7 f
    unSingFun7 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction6 (Apply f t1)
    forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    Sing f -> SingFunction6 f
    unSingFun6 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    unSingFun8 :: forall f. Sing f -> SingFunction8 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
    unSingFun8 Sing f
    sf Sing t1
    x = Sing (Apply f t1) -> SingFunction7 (Apply f t1)
    forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    Sing f -> SingFunction7 f
    unSingFun7 (Sing f
    sf Sing f -> Sing t1 -> Sing (Apply f t1)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing t1
    x)

    #if __GLASGOW_HASKELL__ >= 802
    {-# COMPLETE SLambda2 #-}
    {-# COMPLETE SLambda3 #-}
    {-# COMPLETE SLambda4 #-}
    {-# COMPLETE SLambda5 #-}
    {-# COMPLETE SLambda6 #-}
    {-# COMPLETE SLambda7 #-}
    {-# COMPLETE SLambda8 #-}
    #endif

    pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
    pattern $mSLambda2 :: forall {r} {a1} {a2} {b} {f :: a1 ~> (a2 ~> b)}.
    Sing f -> (SingFunction2 f -> r) -> ((# #) -> r) -> r
    $bSLambda2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    SingFunction2 f -> Sing f
    SLambda2 {forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    Sing f -> SingFunction2 f
    applySing2} <- (unSingFun2 -> applySing2)
      where SLambda2 SingFunction2 f
    lam2         = SingFunction2 f -> Sing f
    forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
    SingFunction2 f -> Sing f
    singFun2 Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)
    SingFunction2 f
    lam2

    pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
    pattern $mSLambda3 :: forall {r} {a1} {a2} {a3} {b} {f :: a1 ~> (a2 ~> (a3 ~> b))}.
    Sing f -> (SingFunction3 f -> r) -> ((# #) -> r) -> r
    $bSLambda3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    SingFunction3 f -> Sing f
    SLambda3 {forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    Sing f -> SingFunction3 f
    applySing3} <- (unSingFun3 -> applySing3)
      where SLambda3 SingFunction3 f
    lam3         = SingFunction3 f -> Sing f
    forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
    SingFunction3 f -> Sing f
    singFun3 Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)
    SingFunction3 f
    lam3

    pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
    pattern $mSLambda4 :: forall {r} {a1} {a2} {a3} {a4} {b}
           {f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))}.
    Sing f -> (SingFunction4 f -> r) -> ((# #) -> r) -> r
    $bSLambda4 :: forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    SingFunction4 f -> Sing f
    SLambda4 {forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    Sing f -> SingFunction4 f
    applySing4} <- (unSingFun4 -> applySing4)
      where SLambda4 SingFunction4 f
    lam4         = SingFunction4 f -> Sing f
    forall {a1} {a2} {a3} {a4} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
    SingFunction4 f -> Sing f
    singFun4 Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)
    SingFunction4 f
    lam4

    pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
    pattern $mSLambda5 :: forall {r} {a1} {a2} {a3} {a4} {a5} {b}
           {f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))}.
    Sing f -> (SingFunction5 f -> r) -> ((# #) -> r) -> r
    $bSLambda5 :: forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    SingFunction5 f -> Sing f
    SLambda5 {forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    Sing f -> SingFunction5 f
    applySing5} <- (unSingFun5 -> applySing5)
      where SLambda5 SingFunction5 f
    lam5         = SingFunction5 f -> Sing f
    forall {a1} {a2} {a3} {a4} {a5} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
    SingFunction5 f -> Sing f
    singFun5 Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
    SingFunction5 f
    lam5

    pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
    pattern $mSLambda6 :: forall {r} {a1} {a2} {a3} {a4} {a5} {a6} {b}
           {f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))}.
    Sing f -> (SingFunction6 f -> r) -> ((# #) -> r) -> r
    $bSLambda6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    SingFunction6 f -> Sing f
    SLambda6 {forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    Sing f -> SingFunction6 f
    applySing6} <- (unSingFun6 -> applySing6)
      where SLambda6 SingFunction6 f
    lam6         = SingFunction6 f -> Sing f
    forall {a1} {a2} {a3} {a4} {a5} {a6} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
    SingFunction6 f -> Sing f
    singFun6 Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing t6
    -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
    SingFunction6 f
    lam6

    pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
    pattern $mSLambda7 :: forall {r} {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           {f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))}.
    Sing f -> (SingFunction7 f -> r) -> ((# #) -> r) -> r
    $bSLambda7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    SingFunction7 f -> Sing f
    SLambda7 {forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    Sing f -> SingFunction7 f
    applySing7} <- (unSingFun7 -> applySing7)
      where SLambda7 SingFunction7 f
    lam7         = SingFunction7 f -> Sing f
    forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b}
           (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
    SingFunction7 f -> Sing f
    singFun7 Sing t1
    -> Sing t2
    -> Sing t3
    -> Sing t4
    -> Sing t5
    -> Sing t6
    -> Sing t7
    -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
    SingFunction7 f
    lam7

    pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
    pattern $mSLambda8 :: forall {r} {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b}
           {f :: a1
                 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))}.
    Sing f -> (SingFunction8 f -> r) -> ((# #) -> r) -> r
    $bSLambda8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b}
           (f :: a1
                 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))).
    SingFunction8 f -> Sing f
    SLambda8 {forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b}
           (f :: a1
                 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))).
    Sing f -> SingFunction8 f
    applySing8} <- (unSingFun8 -> applySing8)
      where SLambda8 SingFunction8 f
    lam8         = SingFunction8 f -> Sing f
    forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b}
           (f :: a1
                 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))).
    SingFunction8 f -> Sing f
    singFun8 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)
    SingFunction8 f
    lam8

    ----------------------------------------------------------------------
    ---- Convenience -----------------------------------------------------
    ----------------------------------------------------------------------

    -- | Convenience function for creating a context with an implicit singleton
    -- available.
    withSingI :: Sing n -> (SingI n => r) -> r
    withSingI :: forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    withSingI Sing n
    sn SingI n => r
    r =
      case Sing n -> SingInstance n
    forall k (a :: k). Sing a -> SingInstance a
    singInstance Sing n
    sn of
        SingInstance n
    SingInstance -> r
    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                          -- ^ The original datatype
                 -> (forall (a :: k). Sing a -> r)    -- ^ Function expecting a singleton
                 -> r
    withSomeSing :: forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote k
    x forall (a :: k). Sing a -> r
    f =
      case Demote k -> SomeSing k
    forall k. SingKind k => Demote k -> SomeSing k
    toSing Demote k
    x of
        SomeSing Sing a
    x' -> Sing a -> r
    forall (a :: k). Sing a -> r
    f Sing a
    x'

    -- | 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
    usingSingI1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) r.
    (SingI1 f, SingI x) =>
    (SingI (f x) => r) -> r
    usingSingI1 SingI (f x) => r
    k = Sing (f x) -> (SingI (f x) => r) -> r
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    withSingI (forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    forall (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Sing (f x)
    sing1 @f @x) r
    SingI (f x) => r
    k

    -- | 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
    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
    usingSingI2 SingI (f x y) => r
    k = Sing (f x y) -> (SingI (f x y) => r) -> r
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    withSingI (forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    forall (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2 @f @x @y) r
    SingI (f x y) => r
    k

    -- | 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
    withSing :: forall {k} (a :: k) b. SingI a => (Sing a -> b) -> b
    withSing Sing a -> b
    f = Sing a -> b
    f Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | 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
    withSing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) b.
    (SingI1 f, SingI x) =>
    (Sing (f x) -> b) -> b
    withSing1 Sing (f x) -> b
    f = Sing (f x) -> b
    f Sing (f x)
    forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    sing1

    -- | 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
    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
    withSing2 Sing (f x y) -> b
    f = Sing (f x y) -> b
    f Sing (f x y)
    forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2

    -- | 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)
    singThat :: forall k (a :: k).
    (SingKind k, SingI a) =>
    (Demote k -> Bool) -> Maybe (Sing a)
    singThat Demote k -> Bool
    p = (Sing a -> Maybe (Sing a)) -> Maybe (Sing a)
    forall {k} (a :: k) b. SingI a => (Sing a -> b) -> b
    withSing ((Sing a -> Maybe (Sing a)) -> Maybe (Sing a))
    -> (Sing a -> Maybe (Sing a)) -> Maybe (Sing a)
    forall a b. (a -> b) -> a -> b
    $ \Sing a
    x -> if Demote k -> Bool
    p (Sing a -> Demote k
    forall (a :: k). Sing a -> Demote k
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing a
    x) then Sing a -> Maybe (Sing a)
    forall a. a -> Maybe a
    Just Sing a
    x else Maybe (Sing a)
    forall a. Maybe a
    Nothing

    -- | 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))
    singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1).
    (SingKind k2, SingI1 f, SingI x) =>
    (Demote k2 -> Bool) -> Maybe (Sing (f x))
    singThat1 Demote k2 -> Bool
    p = (Sing (f x) -> Maybe (Sing (f x))) -> Maybe (Sing (f x))
    forall {k1} {k} (f :: k1 -> k) (x :: k1) b.
    (SingI1 f, SingI x) =>
    (Sing (f x) -> b) -> b
    withSing1 ((Sing (f x) -> Maybe (Sing (f x))) -> Maybe (Sing (f x)))
    -> (Sing (f x) -> Maybe (Sing (f x))) -> Maybe (Sing (f x))
    forall a b. (a -> b) -> a -> b
    $ \Sing (f x)
    x -> if Demote k2 -> Bool
    p (Sing (f x) -> Demote k2
    forall (a :: k2). Sing a -> Demote k2
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing (f x)
    x) then Sing (f x) -> Maybe (Sing (f x))
    forall a. a -> Maybe a
    Just Sing (f x)
    x else Maybe (Sing (f x))
    forall a. Maybe a
    Nothing

    -- | 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))
    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))
    singThat2 Demote k3 -> Bool
    p = (Sing (f x y) -> Maybe (Sing (f x y))) -> Maybe (Sing (f x y))
    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
    withSing2 ((Sing (f x y) -> Maybe (Sing (f x y))) -> Maybe (Sing (f x y)))
    -> (Sing (f x y) -> Maybe (Sing (f x y))) -> Maybe (Sing (f x y))
    forall a b. (a -> b) -> a -> b
    $ \Sing (f x y)
    x -> if Demote k3 -> Bool
    p (Sing (f x y) -> Demote k3
    forall (a :: k3). Sing a -> Demote k3
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing (f x y)
    x) then Sing (f x y) -> Maybe (Sing (f x y))
    forall a. a -> Maybe a
    Just Sing (f x y)
    x else Maybe (Sing (f x y))
    forall a. Maybe a
    Nothing

    -- | Allows creation of a singleton when a proxy is at hand.
    singByProxy :: SingI a => proxy a -> Sing a
    singByProxy :: forall {k} (a :: k) (proxy :: k -> *). SingI a => proxy a -> Sing a
    singByProxy proxy a
    _ = Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | 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)
    singByProxy1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) (proxy :: k -> *).
    (SingI1 f, SingI x) =>
    proxy (f x) -> Sing (f x)
    singByProxy1 proxy (f x)
    _ = Sing (f x)
    forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    sing1

    -- | 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)
    singByProxy2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2)
           (proxy :: k -> *).
    (SingI2 f, SingI x, SingI y) =>
    proxy (f x y) -> Sing (f x y)
    singByProxy2 proxy (f x y)
    _ = Sing (f x y)
    forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2

    -- | Allows creation of a singleton when a @proxy#@ is at hand.
    singByProxy# :: SingI a => Proxy# a -> Sing a
    singByProxy# :: forall {k} (a :: k). SingI a => Proxy# a -> Sing a
    singByProxy# Proxy# a
    _ = Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | 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)
    singByProxy1# :: forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Proxy# (f x) -> Sing (f x)
    singByProxy1# Proxy# (f x)
    _ = Sing (f x)
    forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    sing1

    -- | 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)
    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)
    singByProxy2# Proxy# (f x y)
    _ = Sing (f x y)
    forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2

    -- | 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 ::
    #if __GLASGOW_HASKELL__ >= 900
      forall {k} (a :: k). (SingKind k, SingI a) => Demote k
    #else
      forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
    #endif
    demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k
    demote = Sing a -> Demote k
    forall (a :: k). Sing a -> Demote k
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (forall (a :: k). SingI a => Sing a
    forall {k} (a :: k). SingI a => Sing a
    sing @a)

    -- | 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 ::
    #if __GLASGOW_HASKELL__ >= 900
      forall {k1} {k2} (f :: k1 -> k2) (x :: k1).
      (SingKind k2, SingI1 f, SingI x) =>
      Demote k2
    #else
      forall f x.
      (SingKind (KindOf (f x)), SingI1 f, SingI x) =>
      Demote (KindOf (f x))
    #endif
    demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1).
    (SingKind k2, SingI1 f, SingI x) =>
    Demote k2
    demote1 = Sing (f x) -> Demote k2
    forall (a :: k2). Sing a -> Demote k2
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (forall {k1} {k} (f :: k1 -> k) (x :: k1).
    (SingI1 f, SingI x) =>
    Sing (f x)
    forall (f :: k1 -> k2) (x :: k1). (SingI1 f, SingI x) => Sing (f x)
    sing1 @f @x)

    -- | 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 ::
    #if __GLASGOW_HASKELL__ >= 900
      forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
      (SingKind k3, SingI2 f, SingI x, SingI y) =>
      Demote k3
    #else
      forall f x y.
      (SingKind (KindOf (f x y)), SingI2 f, SingI x, SingI y) =>
      Demote (KindOf (f x y))
    #endif
    demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
    (SingKind k3, SingI2 f, SingI x, SingI y) =>
    Demote k3
    demote2 = Sing (f x y) -> Demote k3
    forall (a :: k3). Sing a -> Demote k3
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    forall (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
    (SingI2 f, SingI x, SingI y) =>
    Sing (f x y)
    sing2 @f @x @y)

    ----------------------------------------------------------------------
    ---- SingI TyCon{N} instances ----------------------------------------
    ----------------------------------------------------------------------

    #if __GLASGOW_HASKELL__ >= 806
    instance forall k1 kr (f :: k1 -> kr).
             ( forall a. SingI a => SingI (f a)
             ,   (ApplyTyCon :: (k1 -> kr) -> (k1 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon1 f) where
      sing :: Sing (TyCon1 f)
    sing = SingFunction1 (TyCon1 f) -> Sing (TyCon1 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon1 f @@ t)) -> Sing (TyCon1 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (f t)
    Sing (TyCon1 f @@ t)
    SingI t => Sing (TyCon1 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 kr (f :: k1 -> k2 -> kr).
             ( forall a b. (SingI a, SingI b) => SingI (f a b)
             ,   (ApplyTyCon :: (k2 -> kr) -> (k2 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon2 f) where
      sing :: Sing (TyCon2 f)
    sing = SingFunction1 (TyCon2 f) -> Sing (TyCon2 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon2 f @@ t)) -> Sing (TyCon2 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon2 f @@ t)
    SingI t => Sing (TyCon2 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 kr (f :: k1 -> k2 -> k3 -> kr).
             ( forall a b c. (SingI a, SingI b, SingI c) => SingI (f a b c)
             ,   (ApplyTyCon :: (k3 -> kr) -> (k3 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon3 f) where
      sing :: Sing (TyCon3 f)
    sing = SingFunction1 (TyCon3 f) -> Sing (TyCon3 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon3 f @@ t)) -> Sing (TyCon3 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon3 f @@ t)
    SingI t => Sing (TyCon3 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 k4 kr (f :: k1 -> k2 -> k3 -> k4 -> kr).
             ( forall a b c d. (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d)
             ,   (ApplyTyCon :: (k4 -> kr) -> (k4 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon4 f) where
      sing :: Sing (TyCon4 f)
    sing = SingFunction1 (TyCon4 f) -> Sing (TyCon4 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon4 f @@ t)) -> Sing (TyCon4 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon4 f @@ t)
    SingI t => Sing (TyCon4 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 k4 k5 kr
                    (f :: k1 -> k2 -> k3 -> k4 -> k5 -> kr).
             ( forall a b c d e.
                  (SingI a, SingI b, SingI c, SingI d, SingI e)
               => SingI (f a b c d e)
             ,   (ApplyTyCon :: (k5 -> kr) -> (k5 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon5 f) where
      sing :: Sing (TyCon5 f)
    sing = SingFunction1 (TyCon5 f) -> Sing (TyCon5 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon5 f @@ t)) -> Sing (TyCon5 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon5 f @@ t)
    SingI t => Sing (TyCon5 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 k4 k5 k6 kr
                    (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> kr).
             ( forall a b c d e f'.
                  (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f')
               => SingI (f a b c d e f')
             ,   (ApplyTyCon :: (k6 -> kr) -> (k6 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon6 f) where
      sing :: Sing (TyCon6 f)
    sing = SingFunction1 (TyCon6 f) -> Sing (TyCon6 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon6 f @@ t)) -> Sing (TyCon6 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon6 f @@ t)
    SingI t => Sing (TyCon6 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 k4 k5 k6 k7 kr
                    (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> kr).
             ( forall a b c d e f' g.
                  (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g)
               => SingI (f a b c d e f' g)
             ,   (ApplyTyCon :: (k7 -> kr) -> (k7 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon7 f) where
      sing :: Sing (TyCon7 f)
    sing = SingFunction1 (TyCon7 f) -> Sing (TyCon7 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon7 f @@ t)) -> Sing (TyCon7 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon7 f @@ t)
    SingI t => Sing (TyCon7 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    instance forall k1 k2 k3 k4 k5 k6 k7 k8 kr
                    (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> kr).
             ( forall a b c d e f' g h.
                  (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h)
               => SingI (f a b c d e f' g h)
             ,   (ApplyTyCon :: (k8 -> kr) -> (k8 ~> kr))
               ~ ApplyTyConAux1
             ) => SingI (TyCon8 f) where
      sing :: Sing (TyCon8 f)
    sing = SingFunction1 (TyCon8 f) -> Sing (TyCon8 f)
    forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
    singFun1 (Sing t -> (SingI t => Sing (TyCon8 f @@ t)) -> Sing (TyCon8 f @@ t)
    forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
    `withSingI` Sing (TyCon (f t))
    Sing (TyCon8 f @@ t)
    SingI t => Sing (TyCon8 f @@ t)
    forall {k} (a :: k). SingI a => Sing a
    sing)
    #endif

    ----------------------------------------------------------------------
    ---- Defunctionalization symbols -------------------------------------
    ----------------------------------------------------------------------

    -- $(genDefunSymbols [''Demote, ''SameKind, ''KindOf, ''(~>), ''Apply, ''(@@)])
    -- WrapSing, UnwrapSing, and SingFunction1 et al. are not defunctionalizable
    -- at the moment due to GHC#9269

    #if __GLASGOW_HASKELL__ >= 810
    type DemoteSym0 :: Type ~> Type
    type DemoteSym1 :: Type -> Type
    #endif

    data DemoteSym0 :: Type ~> Type
    type DemoteSym1 x = Demote x

    type instance Apply DemoteSym0 x = Demote x

    -----

    #if __GLASGOW_HASKELL__ >= 810
    type SameKindSym0 :: forall k. k ~> k ~> Constraint
    type SameKindSym1 :: forall k. k -> k ~> Constraint
    type SameKindSym2 :: forall k. k -> k -> Constraint
    #endif

    data SameKindSym0 :: forall k. k ~> k ~> Constraint
    data SameKindSym1 :: forall k. k -> k ~> Constraint
    type SameKindSym2 (x :: k) (y :: k) = SameKind x y

    type instance Apply SameKindSym0 x = SameKindSym1 x
    type instance Apply (SameKindSym1 x) y = SameKind x y

    -----

    #if __GLASGOW_HASKELL__ >= 810
    type KindOfSym0 :: forall k. k ~> Type
    type KindOfSym1 :: forall k. k -> Type
    #endif

    data KindOfSym0 :: forall k. k ~> Type
    type KindOfSym1 (x :: k) = KindOf x

    type instance Apply KindOfSym0 x = KindOf x

    -----

    infixr 0 ~>@#@$, ~>@#@$$, ~>@#@$$$

    #if __GLASGOW_HASKELL__ >= 810
    type (~>@#@$)  :: Type ~> Type ~> Type
    type (~>@#@$$) :: Type -> Type ~> Type
    type (~>@#@$$$) :: Type -> Type -> Type
    #endif

    data (~>@#@$)  :: Type ~> Type ~> Type
    data (~>@#@$$) :: Type -> Type ~> Type
    type x ~>@#@$$$ y = x ~> y

    type instance Apply (~>@#@$) x = (~>@#@$$) x
    type instance Apply ((~>@#@$$) x) y = x ~> y

    -----

    #if __GLASGOW_HASKELL__ >= 810
    type ApplySym0 :: forall a b. (a ~> b) ~> a ~> b
    type ApplySym1 :: forall a b. (a ~> b) -> a ~> b
    type ApplySym2 :: forall a b. (a ~> b) -> a -> b
    #endif

    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

    type instance Apply ApplySym0 f = ApplySym1 f
    type instance Apply (ApplySym1 f) x = Apply f x

    -----

    infixl 9 @@@#@$, @@@#@$$, @@@#@$$$

    #if __GLASGOW_HASKELL__ >= 810
    type (@@@#@$)  :: forall a b. (a ~> b) ~> a ~> b
    type (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b
    type (@@@#@$$$) :: forall a b. (a ~> b) -> a -> b
    #endif

    data (@@@#@$)  :: forall a b. (a ~> b) ~> a ~> b
    data (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b
    type (f :: a ~> b) @@@#@$$$ (x :: a) = f @@ x

    type instance Apply (@@@#@$) f = (@@@#@$$) f
    type instance Apply ((@@@#@$$) f) x = f @@ x

    {- $SingletonsOfSingletons

    Aside from being a data type to hang instances off of, 'WrappedSing' has
    another purpose as a general-purpose mechanism for allowing one to write
    code that uses singletons of other singletons. For instance, suppose you
    had the following data type:

    @
    data T :: Type -> Type where
      MkT :: forall a (x :: a). 'Sing' x -> F a -> T a
    @

    A naïve attempt at defining a singleton for @T@ would look something like
    this:

    @
    data ST :: forall a. T a -> Type where
      SMkT :: forall a (x :: a) (sx :: 'Sing' x) (f :: F a).
              'Sing' sx -> 'Sing' f -> ST (MkT sx f)
    @

    But there is a problem here: what exactly /is/ @'Sing' sx@? If @x@ were 'True',
    for instance, then @sx@ would be 'STrue', but it's not clear what
    @'Sing' 'STrue'@ should be. One could define @SSBool@ to be the singleton of
    'SBool's, but in order to be thorough, one would have to generate a singleton
    for /every/ singleton type out there. Plus, it's not clear when to stop. Should
    we also generate @SSSBool@, @SSSSBool@, etc.?

    Instead, 'WrappedSing' and its singleton 'SWrappedSing' provide a way to talk
    about singletons of other arbitrary singletons without the need to generate a
    bazillion instances. For reference, here is the definition of 'SWrappedSing':

    @
    newtype 'SWrappedSing' :: forall k (a :: k). 'WrappedSing' a -> Type where
      'SWrapSing' :: forall k (a :: k) (ws :: 'WrappedSing' a).
                     { 'sUnwrapSing' :: 'Sing' a } -> 'SWrappedSing' ws
    type instance 'Sing' \@('WrappedSing' a) = 'SWrappedSing'
    @

    'SWrappedSing' is a bit of an unusual singleton in that its field is a
    singleton for @'Sing' \@k@, not @'WrappedSing' \@k@. But that's exactly the
    point—a singleton of a singleton contains as much type information as the
    underlying singleton itself, so we can get away with just @'Sing' \@k@.

    As an example of this in action, here is how you would define the singleton
    for the earlier @T@ type:

    @
    data ST :: forall a. T a -> Type where
      SMkT :: forall a (x :: a) (sx :: 'Sing' x) (f :: F a).
              'Sing' ('WrapSing' sx) -> 'Sing' f -> ST (MkT sx f)
    @

    With this technique, we won't need anything like @SSBool@ in order to
    instantiate @x@ with 'True'. Instead, the field of type
    @'Sing' ('WrapSing' sx)@ will simply be a newtype around 'SBool'. In general,
    you'll need /n/ layers of 'WrapSing' if you wish to single a singleton /n/
    times.

    Note that this is not the only possible way to define a singleton for @T@.
    An alternative approach that does not make use of singletons-of-singletons is
    discussed at some length
    <https://github.com/goldfirere/singletons/issues/366#issuecomment-489469086 here>.
    Due to the technical limitations of this approach, however, we do not use it
    in @singletons@ at the moment, instead favoring the
    slightly-clunkier-but-more-reliable 'WrappedSing' approach.
    -}

    {- $SLambdaPatternSynonyms

    @SLambda{2...8}@ are explicitly bidirectional pattern synonyms for
    defunctionalized singletons (@'Sing' (f :: k '~>' k' '~>' k'')@).

    As __constructors__: Same as @singFun{2..8}@. For example, one can turn a
    binary function on singletons @sTake :: 'SingFunction2' TakeSym0@ into a
    defunctionalized singleton @'Sing' (TakeSym :: Nat '~>' [a] '~>' [a])@:

    @
    >>> import Data.List.Singletons
    >>> :set -XTypeApplications
    >>>
    >>> :t 'SLambda2'
    'SLambda2' :: 'SingFunction2' f -> 'Sing' f
    >>> :t 'SLambda2' \@TakeSym0
    'SLambda2' :: 'SingFunction2' TakeSym0 -> 'Sing' TakeSym0
    >>> :t 'SLambda2' \@TakeSym0 sTake
    'SLambda2' :: 'Sing' TakeSym0
    @

    This is useful for functions on singletons that expect a defunctionalized
    singleton as an argument, such as @sZipWith :: 'SingFunction3' ZipWithSym0@:

    @
    sZipWith :: Sing (f :: a '~>' b '~>' c) -> Sing (xs :: [a]) -> Sing (ys :: [b]) -> Sing (ZipWith f xs ys :: [c])
    sZipWith ('SLambda2' \@TakeSym0 sTake) :: Sing (xs :: [Nat]) -> Sing (ys :: [[a]]) -> Sing (ZipWith TakeSym0 xs ys :: [[a]])
    @

    As __patterns__: Same as @unSingFun{2..8}@. Gets a binary term-level
    Haskell function on singletons
    @'Sing' (x :: k) -> 'Sing' (y :: k') -> 'Sing' (f \@\@ x \@\@ y)@
    from a defunctionalised @'Sing' f@. Alternatively, as a record field accessor:

    @
    applySing2 :: 'Sing' (f :: k '~>' k' '~>' k'') -> 'SingFunction2' f
    @
    -}