    {-# LANGUAGE PolyKinds, StandaloneDeriving #-}
    #if __GLASGOW_HASKELL__ < 806
    -- Before GHC 8.6, TypeInType was required to explicitly quantify kind variables.
    -- After GHC 8.6, this feature was incorporated into PolyKinds.
    {-# LANGUAGE TypeInType #-}
    #endif
    -- | Singleton types corresponding to type-level data structures.
    --
    -- The implementation is similar, but subtly different to that of the
    -- @<https://hackage.haskell.org/package/singletons singletons>@ package.
    -- See the <http://www.andres-loeh.de/TrueSumsOfProducts "True Sums of Products">
    -- paper for details.
    --
    module Data.SOP.Sing
      ( -- * Singletons
        SList(..)
      , SListI
      , sList
      , para_SList
      , case_SList
        -- ** Shape of type-level lists
      , Shape(..)
      , shape
      , lengthSList
      ) where

    import Data.Kind (Type)
    import Data.Proxy (Proxy(..))

    import Data.SOP.Constraint

    -- * Singletons

    -- | Explicit singleton list.
    --
    -- A singleton list can be used to reveal the structure of
    -- a type-level list argument that the function is quantified
    -- over. For every type-level list @xs@, there is one non-bottom
    -- value of type @'SList' xs@.
    --
    -- Note that these singleton lists are polymorphic in the
    -- list elements; we do not require a singleton representation
    -- for them.
    --
    -- @since 0.2
    --
    data SList :: [k] -> Type where
      SNil  :: SList '[]
      SCons :: SListI xs => SList (x ': xs)

    deriving instance Show (SList (xs :: [k]))
    deriving instance Eq   (SList (xs :: [k]))
    deriving instance Ord  (SList (xs :: [k]))

    -- | Paramorphism for a type-level list.
    --
    -- @since 0.4.0.0
    --
    para_SList ::
         SListI xs
      => r '[]
      -> (forall y ys . (SListI ys) => r ys -> r (y ': ys))
      -> r xs
    para_SList :: forall {a} (xs :: [a]) (r :: [a] -> *).
    SListI xs =>
    r '[]
    -> (forall (y :: a) (ys :: [a]). SListI ys => r ys -> r (y : ys))
    -> r xs
    para_SList r '[]
    nil forall (y :: a) (ys :: [a]). SListI ys => r ys -> r (y : ys)
    cons =
      Proxy Top
    -> r '[]
    -> (forall (y :: a) (ys :: [a]).
        (Top y, All Top ys) =>
        r ys -> r (y : ys))
    -> r xs
    forall k (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (r :: [k] -> *).
    All c xs =>
    proxy c
    -> r '[]
    -> (forall (y :: k) (ys :: [k]).
        (c y, All c ys) =>
        r ys -> r (y : ys))
    -> r xs
    forall (proxy :: (a -> Constraint) -> *) (r :: [a] -> *).
    proxy Top
    -> r '[]
    -> (forall (y :: a) (ys :: [a]).
        (Top y, All Top ys) =>
        r ys -> r (y : ys))
    -> r xs
    cpara_SList (Proxy Top
    forall {k}. Proxy Top
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy Top) r '[]
    nil r ys -> r (y : ys)
    forall (y :: a) (ys :: [a]).
    (Top y, All Top ys) =>
    r ys -> r (y : ys)
    forall (y :: a) (ys :: [a]). SListI ys => r ys -> r (y : ys)
    cons
    {-# INLINE para_SList #-}

    -- | Case distinction on a type-level list.
    --
    -- @since 0.4.0.0
    --
    case_SList ::
         SListI xs
      => r '[]
      -> (forall y ys . (SListI ys) => r (y ': ys))
      -> r xs
    case_SList :: forall {a} (xs :: [a]) (r :: [a] -> *).
    SListI xs =>
    r '[]
    -> (forall (y :: a) (ys :: [a]). SListI ys => r (y : ys)) -> r xs
    case_SList r '[]
    nil forall (y :: a) (ys :: [a]). SListI ys => r (y : ys)
    cons =
      Proxy Top
    -> r '[]
    -> (forall (y :: a) (ys :: [a]). (Top y, All Top ys) => r (y : ys))
    -> r xs
    forall {a} (c :: a -> Constraint) (xs :: [a])
           (proxy :: (a -> Constraint) -> *) (r :: [a] -> *).
    All c xs =>
    proxy c
    -> r '[]
    -> (forall (y :: a) (ys :: [a]). (c y, All c ys) => r (y : ys))
    -> r xs
    ccase_SList (Proxy Top
    forall {k}. Proxy Top
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy Top) r '[]
    nil r (y : ys)
    forall (y :: a) (ys :: [a]). (Top y, All Top ys) => r (y : ys)
    forall (y :: a) (ys :: [a]). SListI ys => r (y : ys)
    cons
    {-# INLINE case_SList #-}

    -- | Get hold of an explicit singleton (that one can then
    -- pattern match on) for a type-level list
    --
    sList :: SListI xs => SList xs
    sList :: forall {k} (xs :: [k]). SListI xs => SList xs
    sList = Proxy Top
    -> SList '[]
    -> (forall (y :: k) (ys :: [k]).
        (Top y, All Top ys) =>
        SList (y : ys))
    -> SList xs
    forall {a} (c :: a -> Constraint) (xs :: [a])
           (proxy :: (a -> Constraint) -> *) (r :: [a] -> *).
    All c xs =>
    proxy c
    -> r '[]
    -> (forall (y :: a) (ys :: [a]). (c y, All c ys) => r (y : ys))
    -> r xs
    ccase_SList (Proxy Top
    forall {k}. Proxy Top
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy Top) SList '[]
    forall {k}. SList '[]
    SNil SList (y : ys)
    forall (y :: k) (ys :: [k]). (Top y, All Top ys) => SList (y : ys)
    forall {k} (xs :: [k]) (x :: k). SListI xs => SList (x : xs)
    SCons

    -- * Shape of type-level lists

    -- | Occasionally it is useful to have an explicit, term-level, representation
    -- of type-level lists (esp because of https://ghc.haskell.org/trac/ghc/ticket/9108 )
    --
    data Shape :: [k] -> Type where
      ShapeNil  :: Shape '[]
      ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)

    deriving instance Show (Shape xs)
    deriving instance Eq   (Shape xs)
    deriving instance Ord  (Shape xs)

    -- | The shape of a type-level list.
    shape :: forall k (xs :: [k]). SListI xs => Shape xs
    shape :: forall k (xs :: [k]). SListI xs => Shape xs
    shape = case SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList :: SList xs of
              SList xs
    SNil  -> Shape xs
    Shape '[]
    forall {k}. Shape '[]
    ShapeNil
              SList xs
    SCons -> Shape xs -> Shape (x : xs)
    forall {k} (xs :: [k]) (x :: k).
    SListI xs =>
    Shape xs -> Shape (x : xs)
    ShapeCons Shape xs
    forall k (xs :: [k]). SListI xs => Shape xs
    shape

    -- | The length of a type-level list.
    --
    -- @since 0.2
    --
    lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int
    lengthSList :: forall k (xs :: [k]) (proxy :: [k] -> *).
    SListI xs =>
    proxy xs -> Int
    lengthSList proxy xs
    _ = Shape xs -> Int
    forall {k} (xs' :: [k]). Shape xs' -> Int
    lengthShape (Shape xs
    forall k (xs :: [k]). SListI xs => Shape xs
    shape :: Shape xs)
      where
        lengthShape :: forall xs'. Shape xs' -> Int
        lengthShape :: forall {k} (xs' :: [k]). Shape xs' -> Int
    lengthShape Shape xs'
    ShapeNil      = Int
    0
        lengthShape (ShapeCons Shape xs
    s) = Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Shape xs -> Int
    forall {k} (xs' :: [k]). Shape xs' -> Int
    lengthShape Shape xs
    s