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

-----------------------------------------------------------------------------
-- |
-- 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 (a :: k) = k

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

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

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

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

  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'
-- @
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'.
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 sng :: 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)@.
newtype WrappedSing :: forall k. k -> Type 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.
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
  SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
               { SWrappedSing ws -> Sing a
sUnwrapSing :: Sing a } -> SWrappedSing ws
type instance Sing = SWrappedSing

type family UnwrapSing (ws :: WrappedSing a) :: Sing a 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.
data SingInstance (a :: k) where
  SingInstance :: SingI a => SingInstance a

-- dirty implementation of explicit-to-implicit conversion
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 s :: 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 si :: 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.
data TyFun :: Type -> Type -> Type

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

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

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

-- | Workhorse for the 'TyCon1', etc., types. This can be used directly
-- in place of any of the @TyConN@ types, but it will work only with
-- /monomorphic/ types. When GHC#14645 is fixed, this should fully supersede
-- the @TyConN@ types.
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.
type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun) 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.
data ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
-- | An \"internal\" defunctionalization symbol used primarily in the
-- definition of 'ApplyTyCon'.
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)

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

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

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

newtype SLambda (f :: k1 ~> k2) =
  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 sFun :: Sing a
sFun x :: 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 f :: 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 k1 k (f :: k1 ~> k). 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 x :: 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 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 f :: 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 f = forall t. Sing t -> SingFunction1 (f @@ t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 :: SingFunction2 f -> Sing f
singFun2 f :: SingFunction2 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction1 (Apply f t) -> Sing (Apply f t)
forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
singFun1 (Sing t -> SingFunction1 (Apply f t)
SingFunction2 f
f Sing t
x))

type SingFunction3 f = forall t. Sing t -> SingFunction2 (f @@ t)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 :: SingFunction3 f -> Sing f
singFun3 f :: SingFunction3 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction2 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k (f :: k1 ~> (k1 ~> k)). SingFunction2 f -> Sing f
singFun2 (Sing t -> SingFunction2 (Apply f t)
SingFunction3 f
f Sing t
x))

type SingFunction4 f = forall t. Sing t -> SingFunction3 (f @@ t)
singFun4 :: forall f. SingFunction4 f -> Sing f
singFun4 :: SingFunction4 f -> Sing f
singFun4 f :: SingFunction4 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction3 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> k))).
SingFunction3 f -> Sing f
singFun3 (Sing t -> SingFunction3 (Apply f t)
SingFunction4 f
f Sing t
x))

type SingFunction5 f = forall t. Sing t -> SingFunction4 (f @@ t)
singFun5 :: forall f. SingFunction5 f -> Sing f
singFun5 :: SingFunction5 f -> Sing f
singFun5 f :: SingFunction5 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction4 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))).
SingFunction4 f -> Sing f
singFun4 (Sing t -> SingFunction4 (Apply f t)
SingFunction5 f
f Sing t
x))

type SingFunction6 f = forall t. Sing t -> SingFunction5 (f @@ t)
singFun6 :: forall f. SingFunction6 f -> Sing f
singFun6 :: SingFunction6 f -> Sing f
singFun6 f :: SingFunction6 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction5 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))).
SingFunction5 f -> Sing f
singFun5 (Sing t -> SingFunction5 (Apply f t)
SingFunction6 f
f Sing t
x))

type SingFunction7 f = forall t. Sing t -> SingFunction6 (f @@ t)
singFun7 :: forall f. SingFunction7 f -> Sing f
singFun7 :: SingFunction7 f -> Sing f
singFun7 f :: SingFunction7 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction6 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))))).
SingFunction6 f -> Sing f
singFun6 (Sing t -> SingFunction6 (Apply f t)
SingFunction7 f
f Sing t
x))

type SingFunction8 f = forall t. Sing t -> SingFunction7 (f @@ t)
singFun8 :: forall f. SingFunction8 f -> Sing f
singFun8 :: SingFunction8 f -> Sing f
singFun8 f :: SingFunction8 f
f = (forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\x :: Sing t
x -> SingFunction7 (Apply f t) -> Sing (Apply f t)
forall k1 k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))))).
SingFunction7 f -> Sing f
singFun7 (Sing t -> SingFunction7 (Apply f t)
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 sf :: 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 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction1 (Apply f t)
forall k1 k (f :: k1 ~> k). Sing f -> SingFunction1 f
unSingFun1 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun3 :: forall f. Sing f -> SingFunction3 f
unSingFun3 :: Sing f -> SingFunction3 f
unSingFun3 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction2 (Apply f t)
forall k1 k1 k (f :: k1 ~> (k1 ~> k)). Sing f -> SingFunction2 f
unSingFun2 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun4 :: forall f. Sing f -> SingFunction4 f
unSingFun4 :: Sing f -> SingFunction4 f
unSingFun4 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction3 (Apply f t)
forall k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> k))).
Sing f -> SingFunction3 f
unSingFun3 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun5 :: forall f. Sing f -> SingFunction5 f
unSingFun5 :: Sing f -> SingFunction5 f
unSingFun5 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction4 (Apply f t)
forall k1 k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))).
Sing f -> SingFunction4 f
unSingFun4 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun6 :: forall f. Sing f -> SingFunction6 f
unSingFun6 :: Sing f -> SingFunction6 f
unSingFun6 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction5 (Apply f t)
forall k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))).
Sing f -> SingFunction5 f
unSingFun5 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun7 :: forall f. Sing f -> SingFunction7 f
unSingFun7 :: Sing f -> SingFunction7 f
unSingFun7 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction6 (Apply f t)
forall k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))))).
Sing f -> SingFunction6 f
unSingFun6 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

unSingFun8 :: forall f. Sing f -> SingFunction8 f
unSingFun8 :: Sing f -> SingFunction8 f
unSingFun8 sf :: Sing f
sf x :: Sing t
x = Sing (Apply f t) -> SingFunction7 (Apply f t)
forall k1 k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))))).
Sing f -> SingFunction7 f
unSingFun7 (Sing f
sf Sing f -> Sing t -> Sing (Apply f t)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t
x)

{-# COMPLETE SLambda2 #-}
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
pattern $bSLambda2 :: SingFunction2 f -> Sing f
$mSLambda2 :: forall r k1 k2 k (f :: k1 ~> (k2 ~> k)).
Sing f -> (SingFunction2 f -> r) -> (Void# -> r) -> r
SLambda2 {Sing f -> forall (t :: k1). Sing t -> SingFunction1 (f @@ t)
applySing2} <- (unSingFun2 -> applySing2)
  where SLambda2 lam2 :: SingFunction2 f
lam2         = SingFunction2 f -> Sing f
forall k1 k1 k (f :: k1 ~> (k1 ~> k)). 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 k1 k2 k3 k (f :: k1 ~> (k2 ~> (k3 ~> k))).
Sing f -> (SingFunction3 f -> r) -> (Void# -> r) -> r
SLambda3 {Sing f -> forall (t :: k1). Sing t -> SingFunction2 (f @@ t)
applySing3} <- (unSingFun3 -> applySing3)
  where SLambda3 lam3 :: SingFunction3 f
lam3         = SingFunction3 f -> Sing f
forall k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> k))).
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 k1 k2 k3 k4 k (f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> k)))).
Sing f -> (SingFunction4 f -> r) -> (Void# -> r) -> r
SLambda4 {Sing f -> forall (t :: k1). Sing t -> SingFunction3 (f @@ t)
applySing4} <- (unSingFun4 -> applySing4)
  where SLambda4 lam4 :: SingFunction4 f
lam4         = SingFunction4 f -> Sing f
forall k1 k1 k1 k1 k (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))).
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 k1 k2 k3 k4 k5 k
       (f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k))))).
Sing f -> (SingFunction5 f -> r) -> (Void# -> r) -> r
SLambda5 {Sing f -> forall (t :: k1). Sing t -> SingFunction4 (f @@ t)
applySing5} <- (unSingFun5 -> applySing5)
  where SLambda5 lam5 :: SingFunction5 f
lam5         = SingFunction5 f -> Sing f
forall k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))).
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 k1 k2 k3 k4 k5 k6 k
       (f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k)))))).
Sing f -> (SingFunction6 f -> r) -> (Void# -> r) -> r
SLambda6 {Sing f -> forall (t :: k1). Sing t -> SingFunction5 (f @@ t)
applySing6} <- (unSingFun6 -> applySing6)
  where SLambda6 lam6 :: SingFunction6 f
lam6         = SingFunction6 f -> Sing f
forall k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))))).
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 k1 k2 k3 k4 k5 k6 k7 k
       (f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k))))))).
Sing f -> (SingFunction7 f -> r) -> (Void# -> r) -> r
SLambda7 {Sing f -> forall (t :: k1). Sing t -> SingFunction6 (f @@ t)
applySing7} <- (unSingFun7 -> applySing7)
  where SLambda7 lam7 :: SingFunction7 f
lam7         = SingFunction7 f -> Sing f
forall k1 k1 k1 k1 k1 k1 k1 k
       (f :: k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k))))))).
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 k1 k2 k3 k4 k5 k6 k7 k8 k
       (f :: k1
             ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k)))))))).
Sing f -> (SingFunction8 f -> r) -> (Void# -> r) -> r
SLambda8 {Sing f -> forall (t :: k1). Sing t -> SingFunction7 (f @@ t)
applySing8} <- (unSingFun8 -> applySing8)
  where SLambda8 lam8 :: SingFunction8 f
lam8         = SingFunction8 f -> Sing f
forall k1 k1 k1 k1 k1 k1 k1 k1 k
       (f :: k1
             ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k)))))))).
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 sn :: Sing n
sn r :: SingI n => r
r =
  case Sing n -> SingInstance n
forall k (a :: k). Sing a -> SingInstance a
singInstance Sing n
sn of
    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 x :: Demote k
x f :: 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 x' :: 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 f :: 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 p :: 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
$ \x :: 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 _ = 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# _ = 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)