{-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds,
             FlexibleContexts, FlexibleInstances,
             TypeFamilies, TypeOperators, TypeFamilyDependencies,
             UndecidableInstances, ConstraintKinds,
             ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes,
             PatternSynonyms, ViewPatterns, StandaloneKindSignatures #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Internal
-- 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. This module
-- exists since we need to define instances for 'SomeSing' in
-- "Data.Singletons", as defining them elsewhere would almost inevitably lead
-- to import cycles.
--
----------------------------------------------------------------------------

module Data.Singletons.Internal (
    module Data.Singletons.Internal
  , Proxy(..)
  ) where

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

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

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

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

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

{-
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.
-- If you need to satisfy this constraint with an explicit singleton, please
-- see 'withSingI' or the 'Sing' pattern synonym.
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

-- | 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.
{-# COMPLETE Sing #-}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern $bSing :: Sing a
$mSing :: forall r k (a :: k). Sing a -> (SingI a => r) -> (Void# -> r) -> r
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'
-- @
type SingKind :: Type -> Constraint
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'.
type SomeSing :: Type -> Type
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)
-- @
{-# COMPLETE FromSing #-}
pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
pattern $bFromSing :: Sing a -> Demote k
$mFromSing :: forall r k.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> (Void# -> r) -> r
FromSing sng <- ((\demotedVal -> withSomeSing demotedVal SomeSing) -> SomeSing sng)
  where FromSing Sing a
sng = 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)@.
type WrappedSing :: k -> Type
newtype WrappedSing a where
  WrapSing :: 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.
type SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
newtype SWrappedSing ws where
  SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
               { SWrappedSing ws -> Sing a
sUnwrapSing :: Sing a } -> SWrappedSing ws
type instance Sing = SWrappedSing

type UnwrapSing :: WrappedSing a -> Sing a
type family UnwrapSing ws where
  UnwrapSing ('WrapSing s) = s

instance SingKind (WrappedSing a) where
  type Demote (WrappedSing a) = WrappedSing a
  fromSing :: Sing a -> Demote (WrappedSing a)
fromSing (SWrapSing 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 s) = Sing Any -> SomeSing (WrappedSing a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing Any -> SomeSing (WrappedSing a))
-> Sing Any -> SomeSing (WrappedSing a)
forall a b. (a -> b) -> a -> b
$ Sing a -> SWrappedSing Any
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.
type SingInstance :: k -> Type
data SingInstance a where
  SingInstance :: SingI a => SingInstance a

-- dirty implementation of explicit-to-implicit conversion
type DI :: k -> Type
newtype DI a = Don'tInstantiate (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 :: Sing a -> SingInstance a
singInstance Sing a
s = (SingI a => SingInstance a) -> SingInstance a
with_sing_i SingI a => SingInstance a
forall k (a :: k). SingI a => SingInstance a
SingInstance
  where
    with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
    with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
with_sing_i SingI a => SingInstance a
si = DI a -> Sing a -> SingInstance a
forall a b. a -> b
unsafeCoerce ((SingI a => SingInstance a) -> DI a
forall k (a :: k). (SingI a => SingInstance a) -> DI a
Don'tInstantiate SingI a => SingInstance a
si) Sing a
s

----------------------------------------------------------------------
---- 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.
type TyFun :: Type -> Type -> Type
data TyFun a b

-- | Something of kind `a ~> b` is a defunctionalized type function that is
-- not necessarily generative or injective.
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

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

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

-- | Workhorse for the 'TyCon1', etc., types. This can be used directly
-- in place of any of the @TyConN@ types, but it will work only with
-- /monomorphic/ types. When GHC#14645 is fixed, this should fully supersede
-- the @TyConN@ types.
type TyCon :: (k1 -> k2) -> unmatchable_fun
data family TyCon
-- 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.
type ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
type family ApplyTyCon where
  ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2
  ApplyTyCon @k1 @k2         @k2              = ApplyTyConAux1
-- 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
type instance Apply (TyCon f) x = ApplyTyCon f @@ x

-- | An \"internal\" defunctionalization symbol used primarily in the
-- definition of 'ApplyTyCon', as well as the 'SingI' instances for 'TyCon1',
-- 'TyCon2', etc.
type ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
data ApplyTyConAux1 f z
-- | An \"internal\" defunctionalization symbol used primarily in the
-- definition of 'ApplyTyCon'.
type ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)
data ApplyTyConAux2 f z
type instance Apply (ApplyTyConAux1 f) x = f x
type instance Apply (ApplyTyConAux2 f) x = TyCon (f x)

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

-- | Similar to 'TyCon1', but for two-parameter type constructors.
type TyCon2 :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3)
type TyCon2 = TyCon

type TyCon3 :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4)
type TyCon3 = TyCon

type TyCon4 :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5)
type TyCon4 = TyCon

type TyCon5 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6)
type TyCon5 = TyCon

type TyCon6 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7)
type TyCon6 = TyCon

type TyCon7 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8)
type TyCon7 = TyCon

type TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9)
type TyCon8 = TyCon

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

type SLambda :: (k1 ~> k2) -> Type
newtype SLambda f =
  SLambda { SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing :: forall t. Sing t -> Sing (f @@ t) }
type instance Sing = SLambda

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

-- | 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 :: 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 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 Any -> SomeSing (k1 ~> k2)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing Any
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 :: Sing f
slam = SingFunction1 f -> Sing f
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 @f SingFunction1 f
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 :: Sing t -> Sing (f @@ t)
lam Sing t
x = Demote k2
-> (forall (a :: k2). Sing a -> Sing (f @@ t)) -> Sing (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 k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
x)) (\(r :: Sing res) -> Sing a -> Sing (f @@ t)
forall a b. a -> b
unsafeCoerce Sing a
r)

type SingFunction1 :: (a1 ~> b) -> Type
type SingFunction1 f = 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 :: 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 SingFunction1 f
f

type SingFunction2 :: (a1 ~> a2 ~> b) -> Type
type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 :: 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 ((f @@ t) @@ t)
SingFunction2 f
f Sing t
x))

type SingFunction3 :: (a1 ~> a2 ~> a3 ~> b) -> Type
type SingFunction3 f = forall t1 t2 t3.
                       Sing t1 -> Sing t2 -> Sing t3
                    -> Sing (f @@ t1 @@ t2 @@ t3)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 :: 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 (((f @@ t) @@ t1) @@ t2)
SingFunction3 f
f Sing t
x))

type SingFunction4 :: (a1 ~> a2 ~> a3 ~> a4 ~> b) -> Type
type SingFunction4 f = 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 :: 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 ((((f @@ t) @@ t1) @@ t2) @@ t3)
SingFunction4 f
f Sing t
x))

type SingFunction5 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) -> Type
type SingFunction5 f = 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 :: 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 (((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4)
SingFunction5 f
f Sing t
x))

type SingFunction6 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) -> Type
type SingFunction6 f = 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 :: 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 ((((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
SingFunction6 f
f Sing t
x))

type SingFunction7 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) -> Type
type SingFunction7 f = 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 :: 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 (((((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
SingFunction7 f
f Sing t
x))

type SingFunction8 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) -> Type
type SingFunction8 f = 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 :: 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
     ((((((((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 :: Sing f -> SingFunction1 f
unSingFun1 Sing f
sf = SLambda f -> SingFunction1 f
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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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)

{-# COMPLETE SLambda2 #-}
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
pattern $bSLambda2 :: SingFunction2 f -> Sing f
$mSLambda2 :: forall r a1 a2 b (f :: a1 ~> (a2 ~> b)).
Sing f -> (SingFunction2 f -> r) -> (Void# -> r) -> r
SLambda2 {Sing f
-> forall (t1 :: a1) (t2 :: a2).
   Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)
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 SingFunction2 f
lam2

{-# COMPLETE SLambda3 #-}
pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
pattern $bSLambda3 :: SingFunction3 f -> Sing f
$mSLambda3 :: forall r a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))).
Sing f -> (SingFunction3 f -> r) -> (Void# -> r) -> r
SLambda3 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3).
   Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)
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 SingFunction3 f
lam3

{-# COMPLETE SLambda4 #-}
pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
pattern $bSLambda4 :: SingFunction4 f -> Sing f
$mSLambda4 :: forall r a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
Sing f -> (SingFunction4 f -> r) -> (Void# -> r) -> r
SLambda4 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4).
   Sing t1
   -> Sing t2
   -> Sing t3
   -> Sing t4
   -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)
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 SingFunction4 f
lam4

{-# COMPLETE SLambda5 #-}
pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
pattern $bSLambda5 :: SingFunction5 f -> Sing f
$mSLambda5 :: forall r a1 a2 a3 a4 a5 b
       (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
Sing f -> (SingFunction5 f -> r) -> (Void# -> r) -> r
SLambda5 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5).
   Sing t1
   -> Sing t2
   -> Sing t3
   -> Sing t4
   -> Sing t5
   -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
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 SingFunction5 f
lam5

{-# COMPLETE SLambda6 #-}
pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
pattern $bSLambda6 :: SingFunction6 f -> Sing f
$mSLambda6 :: forall r a1 a2 a3 a4 a5 a6 b
       (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
Sing f -> (SingFunction6 f -> r) -> (Void# -> r) -> r
SLambda6 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
          (t6 :: a6).
   Sing t1
   -> Sing t2
   -> Sing t3
   -> Sing t4
   -> Sing t5
   -> Sing t6
   -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
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 SingFunction6 f
lam6

{-# COMPLETE SLambda7 #-}
pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
pattern $bSLambda7 :: SingFunction7 f -> Sing f
$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) -> (Void# -> r) -> r
SLambda7 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
          (t6 :: a6) (t7 :: a7).
   Sing t1
   -> Sing t2
   -> Sing t3
   -> Sing t4
   -> Sing t5
   -> Sing t6
   -> Sing t7
   -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
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 SingFunction7 f
lam7

{-# COMPLETE SLambda8 #-}
pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
pattern $bSLambda8 :: SingFunction8 f -> Sing f
$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) -> (Void# -> r) -> r
SLambda8 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
          (t6 :: a6) (t7 :: a7) (t8 :: a8).
   Sing t1
   -> Sing t2
   -> Sing t3
   -> Sing t4
   -> Sing t5
   -> Sing t6
   -> Sing t7
   -> Sing t8
   -> Sing
        ((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8)
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 SingFunction8 f
lam8

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

-- | Convenience function for creating a context with an implicit singleton
-- available.
withSingI :: Sing n -> (SingI n => r) -> r
withSingI :: 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 :: 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'

-- | 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 :: (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 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 :: (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 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

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

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

-- | 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 :: forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
demote :: Demote (KindOf a)
demote = Sing a -> Demote (KindOf a)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SingI a => Sing a
forall k (a :: k). SingI a => Sing a
sing @a)