    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}

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

    #if __GLASGOW_HASKELL__ >= 810
    {-# LANGUAGE StandaloneKindSignatures #-}
    #else
    {-# LANGUAGE ImpredicativeTypes #-} -- See Note [Impredicative Σ?]
    #endif

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Sigma
    -- Copyright   :  (C) 2017 Ryan Scott
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines 'Sigma', a dependent pair data type, and related functions.
    --
    ----------------------------------------------------------------------------

    module Data.Singletons.Sigma
        ( -- * The 'Sigma' type
          Sigma(..), Σ
        , Sing, SSigma(..), SΣ

          -- * Operations over 'Sigma'
        , fstSigma, FstSigma, sndSigma, SndSigma
        , projSigma1, projSigma2
        , mapSigma, zipSigma
        , currySigma, uncurrySigma

    #if __GLASGOW_HASKELL__ >= 806
          -- * Internal utilities
          -- $internalutilities
        , ShowApply,  ShowSingApply
        , ShowApply', ShowSingApply'
    #endif
        ) where

    import Data.Kind
    import Data.Singletons
    #if __GLASGOW_HASKELL__ >= 806
    import Data.Singletons.ShowSing
    #endif

    -- | A dependent pair.
    #if __GLASGOW_HASKELL__ >= 810
    type Sigma :: forall s -> (s ~> Type) -> Type
    #endif
    data Sigma (s :: Type) :: (s ~> Type) -> Type where
      (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
    infixr 4 :&:

    -- | Unicode shorthand for 'Sigma'.
    #if __GLASGOW_HASKELL__ >= 810
    type Σ :: forall s -> (s ~> Type) -> Type
    #endif
    type Σ = Sigma

    {-
    Note [Impredicative Σ?]
    ~~~~~~~~~~~~~~~~~~~~~~~
    The following definition alone:

      type Σ = Sigma

    will not typecheck without the use of ImpredicativeTypes. There isn't a
    fundamental reason that this should be the case, and the only reason that GHC
    currently requires this is due to GHC#13408. Thankfully, giving Σ a standalone
    kind signature works around GHC#13408, so we only have to enable
    ImpredicativeTypes on pre-8.10 versions of GHC.
    -}

    -- | The singleton type for 'Sigma'.
    #if __GLASGOW_HASKELL__ >= 810
    type SSigma :: Sigma s t -> Type
    #endif
    data SSigma :: forall s t. Sigma s t -> Type where
      (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
                Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t)
    infixr 4 :%&:
    #if __GLASGOW_HASKELL__ >= 808
    type instance Sing @(Sigma s t) =
    #else
    type instance Sing =
    #endif
      SSigma

    instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst).
           (SingI fst, SingI b)
        => SingI (a ':&: b :: Sigma s t) where
      sing :: Sing (a ':&: b)
    sing = Sing ('WrapSing a)
    forall {k} (a :: k). SingI a => Sing a
    sing Sing ('WrapSing a) -> Sing b -> SSigma (a ':&: b)
    forall s (t :: s ~> *) (fst :: s) (sfst :: Sing fst)
           (snd :: t @@ fst).
    Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd)
    :%&: Sing b
    forall {k} (a :: k). SingI a => Sing a
    sing

    -- | Unicode shorthand for 'SSigma'.
    #if __GLASGOW_HASKELL__ >= 810
    type SΣ :: Sigma s t -> Type
    #endif
    type SΣ = SSigma

    -- | Project the first element out of a dependent pair.
    fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
    fstSigma :: forall s (t :: s ~> *). SingKind s => Sigma s t -> Demote s
    fstSigma (Sing fst
    a :&: t @@ fst
    _) = Sing fst -> Demote s
    forall (a :: s). Sing a -> Demote s
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing fst
    a

    -- | Project the first element out of a dependent pair.
    #if __GLASGOW_HASKELL__ >= 810
    type FstSigma :: Sigma s t -> s
    #endif
    type family FstSigma (sig :: Sigma s t) :: s where
      FstSigma ((_ :: Sing fst) ':&: _) = fst

    -- | Project the second element out of a dependent pair.
    sndSigma :: forall s t (sig :: Sigma s t).
                SingKind (t @@ FstSigma sig)
             => SSigma sig -> Demote (t @@ FstSigma sig)
    sndSigma :: forall s (t :: s ~> *) (sig :: Sigma s t).
    SingKind (t @@ FstSigma sig) =>
    SSigma sig -> Demote (t @@ FstSigma sig)
    sndSigma (Sing ('WrapSing sfst)
    _ :%&: Sing snd
    b) = Sing snd -> Demote (Apply t fst)
    forall k (a :: k). SingKind k => Sing a -> Demote k
    forall (a :: Apply t fst). Sing a -> Demote (Apply t fst)
    fromSing Sing snd
    b

    -- | Project the second element out of a dependent pair.
    #if __GLASGOW_HASKELL__ >= 810
    type SndSigma :: forall s t. forall (sig :: Sigma s t) -> t @@ FstSigma sig
    #endif
    type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig where
      SndSigma (_ ':&: b) = b

    -- | Project the first element out of a dependent pair using
    -- continuation-passing style.
    projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
    projSigma1 :: forall s r (t :: s ~> *).
    (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
    projSigma1 forall (fst :: s). Sing fst -> r
    f (Sing fst
    a :&: t @@ fst
    _) = Sing fst -> r
    forall (fst :: s). Sing fst -> r
    f Sing fst
    a

    -- | Project the second element out of a dependent pair using
    -- continuation-passing style.
    projSigma2 :: forall s t r. (forall (fst :: s). t @@ fst -> r) -> Sigma s t -> r
    projSigma2 :: forall s (t :: s ~> *) r.
    (forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r
    projSigma2 forall (fst :: s). (t @@ fst) -> r
    f ((Sing fst
    _ :: Sing (fst :: s)) :&: t @@ fst
    b) = forall (fst :: s). (t @@ fst) -> r
    f @fst t @@ fst
    b

    -- | Map across a 'Sigma' value in a dependent fashion.
    mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). p @@ x -> q @@ (f @@ x))
             -> Sigma a p -> Sigma b q
    mapSigma :: forall a b (f :: a ~> b) (p :: a ~> *) (q :: b ~> *).
    Sing f
    -> (forall (x :: a). (p @@ x) -> q @@ (f @@ x))
    -> Sigma a p
    -> Sigma b q
    mapSigma Sing f
    f forall (x :: a). (p @@ x) -> q @@ (f @@ x)
    g ((Sing fst
    x :: Sing (fst :: a)) :&: p @@ fst
    y) = (Sing f
    f Sing f -> Sing fst -> Sing (Apply f fst)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing fst
    x) Sing (Apply f fst) -> (q @@ Apply f fst) -> Sigma b q
    forall s (t :: s ~> *) (fst :: s).
    Sing fst -> (t @@ fst) -> Sigma s t
    :&: (forall (x :: a). (p @@ x) -> q @@ (f @@ x)
    g @fst p @@ fst
    y)

    -- | Zip two 'Sigma' values together in a dependent fashion.
    zipSigma :: Sing (f :: a ~> b ~> c)
             -> (forall (x :: a) (y :: b). p @@ x -> q @@ y -> r @@ (f @@ x @@ y))
             -> Sigma a p -> Sigma b q -> Sigma c r
    zipSigma :: forall a b c (f :: a ~> (b ~> c)) (p :: a ~> *) (q :: b ~> *)
           (r :: c ~> *).
    Sing f
    -> (forall (x :: a) (y :: b).
        (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y))
    -> Sigma a p
    -> Sigma b q
    -> Sigma c r
    zipSigma Sing f
    f forall (x :: a) (y :: b).
    (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)
    g ((Sing fst
    a :: Sing (fstA :: a)) :&: p @@ fst
    p) ((Sing fst
    b :: Sing (fstB :: b)) :&: q @@ fst
    q) =
      (Sing f
    f Sing f -> Sing fst -> Sing (Apply f fst)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing fst
    a Sing (Apply f fst) -> Sing fst -> Sing (Apply (Apply f fst) fst)
    forall k1 k2 (f :: k1 ~> k2) (t :: k1).
    Sing f -> Sing t -> Sing (f @@ t)
    @@ Sing fst
    b) Sing (Apply (Apply f fst) fst)
    -> (r @@ Apply (Apply f fst) fst) -> Sigma c r
    forall s (t :: s ~> *) (fst :: s).
    Sing fst -> (t @@ fst) -> Sigma s t
    :&: (forall (x :: a) (y :: b).
    (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)
    g @fstA @fstB p @@ fst
    p q @@ fst
    q)

    -- | Convert an uncurried function on 'Sigma' to a curried one.
    --
    -- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism such that
    -- the following identities hold:
    --
    -- @
    -- id1 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type).
    --        (forall (p :: Sigma a b). 'SSigma' p -> c @@ p)
    --     -> (forall (p :: Sigma a b). 'SSigma' p -> c @@ p)
    -- id1 f = 'uncurrySigma' @a @b @c ('currySigma' @a @b @c f)
    --
    -- id2 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type).
    --        (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y))
    --     -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y))
    -- id2 f = 'currySigma' @a @b @c ('uncurrySigma' @a @b @c f)
    -- @
    currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
                  (forall (p :: Sigma a b). SSigma p -> c @@ p)
               -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
                     Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y))
    currySigma :: forall a (b :: a ~> *) (c :: Sigma a b ~> *).
    (forall (p :: Sigma a b). SSigma p -> c @@ p)
    -> forall (x :: a) (sx :: Sing x) (y :: b @@ x).
       Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
    currySigma forall (p :: Sigma a b). SSigma p -> c @@ p
    f Sing ('WrapSing sx)
    x Sing y
    y = SSigma (sx ':&: y) -> Apply c (sx ':&: y)
    forall (p :: Sigma a b). SSigma p -> c @@ p
    f (Sing ('WrapSing sx)
    x Sing ('WrapSing sx) -> Sing y -> SSigma (sx ':&: y)
    forall s (t :: s ~> *) (fst :: s) (sfst :: Sing fst)
           (snd :: t @@ fst).
    Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd)
    :%&: Sing y
    y)

    -- | Convert a curried function on 'Sigma' to an uncurried one.
    --
    -- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism.
    -- (Refer to the documentation for 'currySigma' for more details.)
    uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
                    (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
                       Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y))
                 -> (forall (p :: Sigma a b). SSigma p -> c @@ p)
    uncurrySigma :: forall a (b :: a ~> *) (c :: Sigma a b ~> *).
    (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
     Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y))
    -> forall (p :: Sigma a b). SSigma p -> c @@ p
    uncurrySigma forall (x :: a) (sx :: Sing x) (y :: b @@ x).
    Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
    f (Sing ('WrapSing sfst)
    x :%&: Sing snd
    y) = Sing ('WrapSing sfst) -> Sing snd -> c @@ (sfst ':&: snd)
    forall (x :: a) (sx :: Sing x) (y :: b @@ x).
    Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
    f Sing ('WrapSing sfst)
    x Sing snd
    y

    #if __GLASGOW_HASKELL__ >= 806
    instance (ShowSing s, ShowApply t) => Show (Sigma s t) where
      showsPrec :: Int -> Sigma s t -> ShowS
    showsPrec Int
    p ((Sing fst
    a :: Sing (fst :: s)) :&: t @@ fst
    b) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    5) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        Int -> Sing fst -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    5 Sing fst
    a ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :&: " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> (t @@ fst) -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    5 t @@ fst
    b
          :: ShowApply' t fst => ShowS

    instance forall s (t :: s ~> Type) (sig :: Sigma s t).
             (ShowSing s, ShowSingApply t)
          => Show (SSigma sig) where
      showsPrec :: Int -> SSigma sig -> ShowS
    showsPrec Int
    p ((Sing ('WrapSing sfst)
    sa :: Sing ('WrapSing (sfst :: Sing fst))) :%&: (Sing snd
    sb :: Sing snd)) =
        Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    5) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
          Int -> SWrappedSing ('WrapSing sfst) -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    5 SWrappedSing ('WrapSing sfst)
    Sing ('WrapSing sfst)
    sa ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :&: " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Sing snd -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    5 Sing snd
    sb
            :: ShowSingApply' t fst snd => ShowS

    ------------------------------------------------------------
    -- Internal utilities
    ------------------------------------------------------------

    {- $internal-utilities

    See the documentation in "Data.Singletons.ShowSing"—in particular, the
    Haddocks for 'ShowSing' and `ShowSing'`—for an explanation for why these
    classes exist.

    Note that these classes are only defined on GHC 8.6 or later.
    -}

    #if __GLASGOW_HASKELL__ >= 810
    type ShowApply :: (a ~> Type) -> Constraint
    #endif
    class    (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
    instance (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)

    #if __GLASGOW_HASKELL__ >= 810
    type ShowApply' :: (a ~> Type) -> a -> Constraint
    #endif
    class    Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
    instance Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)

    #if __GLASGOW_HASKELL__ >= 810
    type ShowSingApply :: (a ~> Type) -> Constraint
    #endif
    class    (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
    instance (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)

    #if __GLASGOW_HASKELL__ >= 810
    type ShowSingApply' :: forall a. forall (f :: a ~> Type) (x :: a) -> Apply f x -> Constraint
    #endif
    class    Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)
    instance Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)
    #endif