    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MagicHash #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE QuantifiedConstraints #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_GHC -Wno-orphans #-}

    -----------------------------------------------------------------------------
    -- |
    -- 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. For routine
    -- use, consider importing 'Data.Singletons.Prelude', which exports constructors
    -- for singletons based on types in the @Prelude@.
    --
    -- You may also want to read
    -- the original papers presenting this library, available at
    -- <http://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf>
    -- and <http://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf>.
    --
    ----------------------------------------------------------------------------

    module Data.Singletons (
      -- * Main singleton definitions

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

      SingI(..), SingKind(..),

      -- * Working with singletons
      KindOf, SameKind,
      SingInstance(..), SomeSing(..),
      singInstance, pattern Sing, withSingI,
      withSomeSing, pattern FromSing,
      singByProxy, demote,

      singByProxy#,
      withSing, singThat,

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

      -- ** Defunctionalization
      TyFun, type (~>),
      TyCon1, TyCon2, TyCon3, TyCon4, TyCon5, TyCon6, TyCon7, TyCon8,
      TyCon, Apply, type (@@),

      -- ** 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, pattern SLambda3, pattern SLambda4, pattern SLambda5,
      pattern SLambda6, pattern SLambda7, pattern SLambda8,

      -- | 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.Singletons.Internal
    import Data.Singletons.Prelude.Enum
    import Data.Singletons.Prelude.Eq
    import Data.Singletons.Prelude.Instances
    import Data.Singletons.Prelude.IsString
    import Data.Singletons.Prelude.Monoid
    import Data.Singletons.Prelude.Num
    import Data.Singletons.Prelude.Ord
    import Data.Singletons.Prelude.Semigroup
    import Data.Singletons.Promote
    import Data.Singletons.ShowSing
    import Data.Singletons.Single (singITyConInstances)
    import Data.String
    import qualified Data.Text as T (pack)

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

    {-
    Generates SingI instances for TyCon1 through TyCon8:

      instance (forall a.    SingI a           => SingI (f a),   ...) => SingI (TyCon1 f)
      instance (forall a b. (SingI a, SingI b) => SingI (f a b), ...) => SingI (TyCon2 f)
      ...
    -}
    $(singITyConInstances [1..8])

    ----------------------------------------------------------------------
    ---- SomeSing instances ----------------------------------------------
    ----------------------------------------------------------------------

    instance SEq k => Eq (SomeSing k) where
      SomeSing a :: Sing a
    a == :: SomeSing k -> SomeSing k -> Bool
    == SomeSing b :: Sing a
    b = Sing (a == a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (a == a)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a == b)
    %== Sing a
    b)
      SomeSing a :: Sing a
    a /= :: SomeSing k -> SomeSing k -> Bool
    /= SomeSing b :: Sing a
    b = Sing (a /= a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (a /= a)
    forall k (a :: k) (b :: k).
    SEq k =>
    Sing a -> Sing b -> Sing (a /= b)
    %/= Sing a
    b)

    instance SOrd k => Ord (SomeSing k) where
      SomeSing a :: Sing a
    a compare :: SomeSing k -> SomeSing k -> Ordering
    `compare` SomeSing b :: Sing a
    b = Sing (Compare a a) -> Demote Ordering
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
    `sCompare` Sing a
    b)
      SomeSing a :: Sing a
    a < :: SomeSing k -> SomeSing k -> Bool
    <         SomeSing b :: Sing a
    b = Sing (a < a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (<@#@$) a) a)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)
    %<  Sing a
    b)
      SomeSing a :: Sing a
    a <= :: SomeSing k -> SomeSing k -> Bool
    <=        SomeSing b :: Sing a
    b = Sing (a <= a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (<=@#@$) a) a)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)
    %<= Sing a
    b)
      SomeSing a :: Sing a
    a > :: SomeSing k -> SomeSing k -> Bool
    >         SomeSing b :: Sing a
    b = Sing (a > a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (>@#@$) a) a)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)
    %>  Sing a
    b)
      SomeSing a :: Sing a
    a >= :: SomeSing k -> SomeSing k -> Bool
    >=        SomeSing b :: Sing a
    b = Sing (a >= a) -> Demote Bool
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (>=@#@$) a) a)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)
    %>= Sing a
    b)

    instance SBounded k => Bounded (SomeSing k) where
      minBound :: SomeSing k
    minBound = Sing MinBound -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing Sing MinBound
    forall a. SBounded a => Sing MinBoundSym0
    sMinBound
      maxBound :: SomeSing k
    maxBound = Sing MaxBound -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing Sing MaxBound
    forall a. SBounded a => Sing MaxBoundSym0
    sMaxBound

    instance SEnum k => Enum (SomeSing k) where
      succ :: SomeSing k -> SomeSing k
    succ (SomeSing a :: Sing a
    a) = Sing (Succ a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a -> Sing (Apply SuccSym0 a)
    forall a (t :: a). SEnum a => Sing t -> Sing (Apply SuccSym0 t)
    sSucc Sing a
    a)
      pred :: SomeSing k -> SomeSing k
    pred (SomeSing a :: Sing a
    a) = Sing (Pred a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a -> Sing (Apply PredSym0 a)
    forall a (t :: a). SEnum a => Sing t -> Sing (Apply PredSym0 t)
    sPred Sing a
    a)
      toEnum :: Int -> SomeSing k
    toEnum n :: Int
    n = Demote Nat
    -> (forall (a :: Nat). Sing a -> SomeSing k) -> SomeSing k
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing (Int -> Demote Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    n) (Sing (ToEnum a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing (ToEnum a) -> SomeSing k)
    -> (SNat a -> Sing (ToEnum a)) -> SNat a -> SomeSing k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SNat a -> Sing (ToEnum a)
    forall a (t :: Nat). SEnum a => Sing t -> Sing (Apply ToEnumSym0 t)
    sToEnum)
      fromEnum :: SomeSing k -> Int
    fromEnum (SomeSing a :: Sing a
    a) = Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Sing (FromEnum a) -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing (Sing a -> Sing (Apply FromEnumSym0 a)
    forall a (t :: a). SEnum a => Sing t -> Sing (Apply FromEnumSym0 t)
    sFromEnum Sing a
    a))
      enumFromTo :: SomeSing k -> SomeSing k -> [SomeSing k]
    enumFromTo (SomeSing from :: Sing a
    from) (SomeSing to :: Sing a
    to) =
        SList (EnumFromTo a a) -> [SomeSing k]
    forall a (x :: [a]). SList x -> [SomeSing a]
    listFromSingShallow (Sing a -> Sing a -> Sing (Apply (Apply EnumFromToSym0 a) a)
    forall a (t :: a) (t :: a).
    SEnum a =>
    Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t)
    sEnumFromTo Sing a
    from Sing a
    to)
      enumFromThenTo :: SomeSing k -> SomeSing k -> SomeSing k -> [SomeSing k]
    enumFromThenTo (SomeSing from :: Sing a
    from) (SomeSing then_ :: Sing a
    then_) (SomeSing to :: Sing a
    to) =
        SList (EnumFromThenTo a a a) -> [SomeSing k]
    forall a (x :: [a]). SList x -> [SomeSing a]
    listFromSingShallow (Sing a
    -> Sing a
    -> Sing a
    -> Sing (Apply (Apply (Apply EnumFromThenToSym0 a) a) a)
    forall a (t :: a) (t :: a) (t :: a).
    SEnum a =>
    Sing t
    -> Sing t
    -> Sing t
    -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t)
    sEnumFromThenTo Sing a
    from Sing a
    then_ Sing a
    to)

    -- Like the 'fromSing' implementation for lists, but bottoms out at
    -- 'SomeSing' instead of recursively invoking 'fromSing'.
    listFromSingShallow :: SList (x :: [a]) -> [SomeSing a]
    listFromSingShallow :: SList x -> [SomeSing a]
    listFromSingShallow SNil         = []
    listFromSingShallow (SCons x :: Sing n
    x xs :: Sing n
    xs) = Sing n -> SomeSing a
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing Sing n
    x SomeSing a -> [SomeSing a] -> [SomeSing a]
    forall a. a -> [a] -> [a]
    : SList n -> [SomeSing a]
    forall a (x :: [a]). SList x -> [SomeSing a]
    listFromSingShallow Sing n
    SList n
    xs

    instance SNum k => Num (SomeSing k) where
      SomeSing a :: Sing a
    a + :: SomeSing k -> SomeSing k -> SomeSing k
    + SomeSing b :: Sing a
    b = Sing (a + a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (+@#@$) a) a)
    forall a (t :: a) (t :: a).
    SNum a =>
    Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t)
    %+ Sing a
    b)
      SomeSing a :: Sing a
    a - :: SomeSing k -> SomeSing k -> SomeSing k
    - SomeSing b :: Sing a
    b = Sing (a - a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (-@#@$) a) a)
    forall a (t :: a) (t :: a).
    SNum a =>
    Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t)
    %- Sing a
    b)
      SomeSing a :: Sing a
    a * :: SomeSing k -> SomeSing k -> SomeSing k
    * SomeSing b :: Sing a
    b = Sing (a * a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (*@#@$) a) a)
    forall a (t :: a) (t :: a).
    SNum a =>
    Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t)
    %* Sing a
    b)
      negate :: SomeSing k -> SomeSing k
    negate (SomeSing a :: Sing a
    a) = Sing (Negate a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a -> Sing (Apply NegateSym0 a)
    forall a (t :: a). SNum a => Sing t -> Sing (Apply NegateSym0 t)
    sNegate Sing a
    a)
      abs :: SomeSing k -> SomeSing k
    abs    (SomeSing a :: Sing a
    a) = Sing (Abs a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a -> Sing (Apply AbsSym0 a)
    forall a (t :: a). SNum a => Sing t -> Sing (Apply AbsSym0 t)
    sAbs Sing a
    a)
      signum :: SomeSing k -> SomeSing k
    signum (SomeSing a :: Sing a
    a) = Sing (Signum a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a -> Sing (Apply SignumSym0 a)
    forall a (t :: a). SNum a => Sing t -> Sing (Apply SignumSym0 t)
    sSignum Sing a
    a)
      fromInteger :: Integer -> SomeSing k
    fromInteger n :: Integer
    n = Demote Nat
    -> (forall (a :: Nat). Sing a -> SomeSing k) -> SomeSing k
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing (Integer -> Demote Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    n) (Sing (FromInteger a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing (FromInteger a) -> SomeSing k)
    -> (SNat a -> Sing (FromInteger a)) -> SNat a -> SomeSing k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SNat a -> Sing (FromInteger a)
    forall a (t :: Nat).
    SNum a =>
    Sing t -> Sing (Apply FromIntegerSym0 t)
    sFromInteger)

    instance ShowSing k => Show (SomeSing k) where
      showsPrec :: Int -> SomeSing k -> ShowS
    showsPrec p :: Int
    p (SomeSing (s :: Sing a)) =
        Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 10) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    showString "SomeSing " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Sing a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec 11 Sing a
    s
          :: ShowSing' a => ShowS

    instance SSemigroup k => Semigroup (SomeSing k) where
      SomeSing a :: Sing a
    a <> :: SomeSing k -> SomeSing k -> SomeSing k
    <> SomeSing b :: Sing a
    b = Sing (a <> a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    a Sing a -> Sing a -> Sing (Apply (Apply (<>@#@$) a) a)
    forall a (t :: a) (t :: a).
    SSemigroup a =>
    Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t)
    %<> Sing a
    b)

    instance SMonoid k => Monoid (SomeSing k) where
      mempty :: SomeSing k
    mempty = Sing Mempty -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing Sing Mempty
    forall a. SMonoid a => Sing MemptySym0
    sMempty

    instance SIsString k => IsString (SomeSing k) where
      fromString :: String -> SomeSing k
    fromString s :: String
    s = Demote Symbol
    -> (forall (a :: Symbol). Sing a -> SomeSing k) -> SomeSing k
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing (String -> Text
    T.pack String
    s) (Sing (FromString a) -> SomeSing k
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing (FromString a) -> SomeSing k)
    -> (SSymbol a -> Sing (FromString a)) -> SSymbol a -> SomeSing k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SSymbol a -> Sing (FromString a)
    forall a (t :: Symbol).
    SIsString a =>
    Sing t -> Sing (Apply FromStringSym0 t)
    sFromString)

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

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

    {- $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.Singletons.Prelude.List
    >>> :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
    @
    -}