{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE TypeOperators       #-}

-- |
-- Module      : Data.Type.Universe
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- A type family for "containers", intended for allowing lifting of
-- predicates on @k@ to be predicates on containers @f k@.
--
module Data.Type.Universe (
  -- * Universe
    Elem, In, Universe(..)
  -- ** Instances
  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
  , CompElem(..), SumElem(..)
  -- ** Predicates
  , All, WitAll(..), NotAll
  , Any, WitAny(..), None
  , Null, NotNull
  -- *** Specialized
  , IsJust, IsNothing, IsRight, IsLeft
  -- * Decisions and manipulations
  , decideAny, decideAll, genAllA, genAll, igenAll
  , foldMapUni, ifoldMapUni, index, pickElem
  -- * Universe Combination
  , Sing (SComp, SInL, SInR)
  -- ** Universe Composition
  , (:.:)(..), sGetComp, GetComp
  , allComp, compAll, anyComp, compAny
  -- ** Universe Disjunction
  , (:+:)(..)
  , anySumL, anySumR, sumLAny, sumRAny
  , allSumL, allSumR, sumLAll, sumRAll
  -- * Defunctionalization symbols
  , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
  ) where

import           Control.Applicative
import           Data.Functor.Identity
import           Data.Kind
import           Data.List.NonEmpty                    (NonEmpty(..))
import           Data.Proxy
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not)
import           Data.Type.Predicate
import           Data.Type.Predicate.Logic
import           Data.Typeable                         (Typeable)
import           GHC.Generics                          (Generic)
import           Prelude hiding                        (any, all)
import qualified Data.Singletons.Prelude.List.NonEmpty as NE

#if MIN_VERSION_singletons(2,5,0)
import           Data.Singletons.Prelude.Identity
#else
import           Data.Singletons.TH
genSingletons [''Identity]
#endif

-- | A witness for membership of a given item in a type-level collection
type family Elem (f :: Type -> Type) :: f k -> k -> Type

data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a

type instance Apply (ElemSym0 f) as = ElemSym1 f as
type instance Apply (ElemSym1 f as) a = Elem f as a

-- | @'In' f as@ is a predicate that a given input @a@ is a member of
-- collection @as@.
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as

-- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
-- type-level collection @as@, the predicate @p a@ is true.
data WitAny f :: (k ~> Type) -> f k -> Type where
    WitAny :: Elem f as a -> p @@ a -> WitAny f p as

-- | An @'Any' f p@ is a predicate testing a collection @as :: f a@ for the
-- fact that at least one item in @as@ satisfies @p@.  Represents the
-- "exists" quantifier over a given universe.
--
-- This is mostly useful for its 'Decidable' and 'TFunctor' instances,
-- which lets you lift predicates on @p@ to predicates on @'Any' f p@.
data Any f :: Predicate k -> Predicate (f k)
type instance Apply (Any f p) as = WitAny f p as

-- | A @'WitAll' p as@ is a witness that the predicate @p a@ is true for all
-- items @a@ in the type-level collection @as@.
newtype WitAll f p (as :: f k) = WitAll { runWitAll :: forall a. Elem f as a -> p @@ a }

-- | An @'All' f p@ is a predicate testing a collection @as :: f a@ for the
-- fact that /all/ items in @as@ satisfy @p@.  Represents the "forall"
-- quantifier over a given universe.
--
-- This is mostly useful for its 'Decidable', 'Provable', and 'TFunctor'
-- instances, which lets you lift predicates on @p@ to predicates on @'All'
-- f p@.
data All f :: Predicate k -> Predicate (f k)
type instance Apply (All f p) as = WitAll f p as

instance (Universe f, Decidable p) => Decidable (Any f p) where
    decide = decideAny @f @_ @p $ decide @p

instance (Universe f, Decidable p) => Decidable (All f p) where
    decide = decideAll @f @_ @p $ decide @p

instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where

instance Provable p => Provable (NotNull f ==> Any f p) where
    prove _ (WitAny i s) = WitAny i (prove @p s)

instance (Universe f, Provable p) => Provable (All f p) where
    prove xs = WitAll $ \i -> prove @p (index i xs)

instance Universe f => TFunctor (Any f) where
    tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)

instance Universe f => TFunctor (All f) where
    tmap f xs a = WitAll $ \i -> f (index i xs) (runWitAll a i)

instance Universe f => DFunctor (All f) where
    dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs

-- | Typeclass for a type-level container that you can quantify or lift
-- type-level predicates over.
class Universe (f :: Type -> Type) where
    -- | 'decideAny', but providing an 'Elem'.
    idecideAny
        :: forall k (p :: k ~> Type) (as :: f k). ()
        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
        -> (Sing as -> Decision (Any f p @@ as))                         -- ^ predicate on collection

    -- | 'decideAll', but providing an 'Elem'.
    idecideAll
        :: forall k (p :: k ~> Type) (as :: f k). ()
        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
        -> (Sing as -> Decision (All f p @@ as))                         -- ^ predicate on collection

    -- | 'genAllA', but providing an 'Elem'.
    igenAllA
        :: forall k (p :: k ~> Type) (as :: f k) h. Applicative h
        => (forall a. Elem f as a -> Sing a -> h (p @@ a))        -- ^ predicate on value in context
        -> (Sing as -> h (All f p @@ as))                              -- ^ predicate on collection in context

-- | Predicate that a given @as :: f k@ is empty and has no items in it.
type Null    f = (None f Evident :: Predicate (f k))

-- | Predicate that a given @as :: f k@ is not empty, and has at least one
-- item in it.
type NotNull f = (Any f Evident :: Predicate (f k))

-- | A @'None' f p@ is a predicate on a collection @as@ that no @a@ in @as@
-- satisfies predicate @p@.
type None f p = (Not (Any f p) :: Predicate (f k))

-- | A @'NotAll' f p@ is a predicate on a collection @as@ that at least one
-- @a@ in @as@ does not satisfy predicate @p@.
type NotAll f p = (Not (All f p) :: Predicate (f k))

-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
-- a collection @as@ that is true if and only if /any/ item in @as@
-- satisfies the original predicate.
--
-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
-- of kind @f k ~> Type@.
--
-- Essentially tests existential quantification.
decideAny
    :: forall f k (p :: k ~> Type). Universe f
    => Decide p                                 -- ^ predicate on value
    -> Decide (Any f p)                -- ^ predicate on collection
decideAny f = idecideAny (const f)

-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
-- a collection @as@ that is true if and only if /all/ items in @as@
-- satisfies the original predicate.
--
-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
-- of kind @f k ~> Type@.
--
-- Essentially tests universal quantification.
decideAll
    :: forall f k (p :: k ~> Type). Universe f
    => Decide p                                 -- ^ predicate on value
    -> Decide (All f p)                -- ^ predicate on collection
decideAll f = idecideAll (const f)

-- | If @p a@ is true for all values @a@ in @as@ under some
-- (Applicative) context @h@, then you can create an @'All' p as@ under
-- that Applicative context @h@.
--
-- Can be useful with 'Identity' (which is basically unwrapping and
-- wrapping 'All'), or with 'Maybe' (which can express predicates that
-- are either provably true or not provably false).
--
-- In practice, this can be used to iterate and traverse and sequence
-- actions over all "items" in @as@.
genAllA
    :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
    => (forall a. Sing a -> h (p @@ a))        -- ^ predicate on value in context
    -> (Sing as -> h (All f p @@ as))               -- ^ predicate on collection in context
genAllA f = igenAllA (const f)

-- | 'genAll', but providing an 'Elem'.
igenAll
    :: forall f k (p :: k ~> Type) (as :: f k). Universe f
    => (forall a. Elem f as a -> Sing a -> p @@ a)            -- ^ always-true predicate on value
    -> (Sing as -> All f p @@ as)                                  -- ^ always-true predicate on collection
igenAll f = runIdentity . igenAllA (\i -> Identity . f i)

-- | If @p a@ is true for all values @a@ in @as@, then we have @'All'
-- p as@.  Basically witnesses the definition of 'All'.
genAll
    :: forall f k (p :: k ~> Type). Universe f
    => Prove p                 -- ^ always-true predicate on value
    -> Prove (All f p)         -- ^ always-true predicate on collection
genAll f = igenAll (const f)

-- | Extract the item from the container witnessed by the 'Elem'
index
    :: forall f as a. Universe f
    => Elem f as a        -- ^ Witness
    -> Sing as            -- ^ Collection
    -> Sing a
index i = (`runWitAll` i) . splitSing

-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
splitSing
    :: forall f k (as :: f k). Universe f
    => Sing as
    -> All f (TyPred Sing) @@ as
splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)

-- | Automatically generate a witness for a member, if possible
pickElem
    :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
    => Decision (Elem f as a)
pickElem = mapDecision (\case WitAny i Refl -> i)
                       (\case i -> WitAny i Refl)
         . decide @(Any f (TyPred ((:~:) a)))
         $ sing

-- | 'foldMapUni' but with access to the index.
ifoldMapUni
    :: forall f k (as :: f k) m. (Universe f, Monoid m)
    => (forall a. Elem f as a -> Sing a -> m)
    -> Sing as
    -> m
ifoldMapUni f = getConst . igenAllA (\i -> Const . f i)

-- | A 'foldMap' over all items in a collection.
foldMapUni
    :: forall f k (as :: f k) m. (Universe f, Monoid m)
    => (forall (a :: k). Sing a -> m)
    -> Sing as
    -> m
foldMapUni f = ifoldMapUni (const f)

-- | Witness an item in a type-level list by providing its index.
data Index :: [k] -> k -> Type where
    IZ :: Index (a ': as) a
    IS :: Index bs a -> Index (b ': bs) a

deriving instance Show (Index as a)
instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where
    decide x = withSingI x $ pickElem

type instance Elem [] = Index

instance Universe [] where
    idecideAny
        :: forall k (p :: k ~> Type) (as :: [k]). ()
        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
        -> Sing as
        -> Decision (Any [] p @@ as)
    idecideAny f = \case
      SNil -> Disproved $ \case
        WitAny i _ -> case i of {}
      x `SCons` xs -> case f IZ x of
        Proved p    -> Proved $ WitAny IZ p
        Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of
          Proved (WitAny i p) -> Proved $ WitAny (IS i) p
          Disproved vs -> Disproved $ \case
            WitAny IZ     p -> v p
            WitAny (IS i) p -> vs (WitAny i p)

    idecideAll
        :: forall k (p :: k ~> Type) (as :: [k]). ()
        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
        -> Sing as
        -> Decision (All [] p @@ as)
    idecideAll f = \case
      SNil -> Proved $ WitAll $ \case {}
      x `SCons` xs -> case f IZ x of
        Proved p -> case idecideAll @[] @_ @p (f . IS) xs of
          Proved a -> Proved $ WitAll $ \case
            IZ   -> p
            IS i -> runWitAll a i
          Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
        Disproved v -> Disproved $ \a -> v $ runWitAll a IZ

    igenAllA
        :: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h
        => (forall a. Elem [] as a -> Sing a -> h (p @@ a))
        -> Sing as
        -> h (All [] p @@ as)
    igenAllA f = \case
        SNil         -> pure $ WitAll $ \case {}
        x `SCons` xs -> go <$> f IZ x <*> igenAllA (f . IS) xs
      where
        go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)
        go p a = WitAll $ \case
          IZ   -> p
          IS i -> runWitAll a i

-- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
-- 'Just'.
data IJust :: Maybe k -> k -> Type where
    IJust :: IJust ('Just a) a

deriving instance Show (IJust as a)
instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where
    decide x = withSingI x $ pickElem

type instance Elem Maybe = IJust

-- | Test that a 'Maybe' is 'Just'.
--
-- @since 0.1.2.0
type IsJust    = (NotNull Maybe :: Predicate (Maybe k))

-- | Test that a 'Maybe' is 'Nothing'.
--
-- @since 0.1.2.0
type IsNothing = (Null    Maybe :: Predicate (Maybe k))

instance Universe Maybe where
    idecideAny f = \case
      SNothing -> Disproved $ \case WitAny i _ -> case i of {}
      SJust x  -> case f IJust x of
        Proved p    -> Proved $ WitAny IJust p
        Disproved v -> Disproved $ \case
          WitAny IJust p -> v p

    idecideAll f = \case
      SNothing -> Proved $ WitAll $ \case {}
      SJust x  -> case f IJust x of
        Proved p    -> Proved $ WitAll $ \case IJust -> p
        Disproved v -> Disproved $ \a -> v $ runWitAll a IJust

    igenAllA f = \case
      SNothing -> pure $ WitAll $ \case {}
      SJust x  -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x

-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
-- is 'Right'.
data IRight :: Either j k -> k -> Type where
    IRight :: IRight ('Right a) a

deriving instance Show (IRight as a)
instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where
    decide x = withSingI x $ pickElem

type instance Elem (Either j) = IRight

-- | Test that an 'Either' is 'Right'
--
-- @since 0.1.2.0
type IsRight = (NotNull (Either j) :: Predicate (Either j k))

-- | Test that an 'Either' is 'Left'
--
-- @since 0.1.2.0
type IsLeft  = (Null    (Either j) :: Predicate (Either j k))

instance Universe (Either j) where
    idecideAny f = \case
      SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}
      SRight x -> case f IRight x of
        Proved p    -> Proved $ WitAny IRight p
        Disproved v -> Disproved $ \case
          WitAny IRight p -> v p

    idecideAll f = \case
      SLeft  _ -> Proved $ WitAll $ \case {}
      SRight x -> case f IRight x of
        Proved p    -> Proved $ WitAll $ \case IRight -> p
        Disproved v -> Disproved $ \a -> v $ runWitAll a IRight

    igenAllA f = \case
      SLeft  _ -> pure $ WitAll $ \case {}
      SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x

-- | Witness an item in a type-level 'NonEmpty' by either indicating that
-- it is the "head", or by providing an index in the "tail".
data NEIndex :: NonEmpty k -> k -> Type where
    NEHead :: NEIndex (a ':| as) a
    NETail :: Index as a -> NEIndex (b ':| as) a

deriving instance Show (NEIndex as a)
instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where
    decide x = withSingI x $ pickElem

type instance Elem NonEmpty = NEIndex

instance Universe NonEmpty where
    idecideAny
        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
        -> Sing as
        -> Decision (Any NonEmpty p @@ as)
    idecideAny f (x NE.:%| xs) = case f NEHead x of
      Proved p    -> Proved $ WitAny NEHead p
      Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of
        Proved (WitAny i p) -> Proved $ WitAny (NETail i) p
        Disproved vs     -> Disproved $ \case
          WitAny i p -> case i of
            NEHead    -> v p
            NETail i' -> vs (WitAny i' p)

    idecideAll
        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
        -> Sing as
        -> Decision (All NonEmpty p @@ as)
    idecideAll f (x NE.:%| xs) = case f NEHead x of
      Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of
        Proved ps -> Proved $ WitAll $ \case
          NEHead   -> p
          NETail i -> runWitAll ps i
        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
      Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead

    igenAllA
        :: forall k (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
        => (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))
        -> Sing as
        -> h (All NonEmpty p @@ as)
    igenAllA f (x NE.:%| xs) = go <$> f NEHead x <*> igenAllA @[] @_ @p (f . NETail) xs
      where
        go :: p @@ b -> All [] p @@ bs -> All NonEmpty p @@ (b ':| bs)
        go p ps = WitAll $ \case
          NEHead   -> p
          NETail i -> runWitAll ps i

-- | Trivially witness an item in the second field of a type-level tuple.
data ISnd :: (j, k) -> k -> Type where
    ISnd :: ISnd '(a, b) b

deriving instance Show (ISnd as a)
-- TODO: does this interfere with NonNull stuff?
instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where
    decide x = withSingI x $ pickElem

type instance Elem ((,) j) = ISnd

instance Universe ((,) j) where
    idecideAny f (STuple2 _ x) = case f ISnd x of
      Proved p    -> Proved $ WitAny ISnd p
      Disproved v -> Disproved $ \case WitAny ISnd p -> v p

    idecideAll f (STuple2 _ x) = case f ISnd x of
      Proved p    -> Proved $ WitAll $ \case ISnd -> p
      Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd

    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x

-- | There are no items of type @a@ in a @'Proxy' a@.
--
-- @since 0.1.3.0
data IProxy :: Proxy k -> k -> Type

deriving instance Show (IProxy 'Proxy a)

instance Provable (Not (TyPred (IProxy 'Proxy))) where
    prove _ = \case {}

type instance Elem Proxy = IProxy

-- | The null universe
instance Universe Proxy where
    idecideAny _ _ = Disproved $ \case
        WitAny i _ -> case i of {}
    idecideAll _ _ = Proved $ WitAll $ \case {}
    igenAllA   _ _ = pure $ WitAll $ \case {}

-- | Trivially witness the item held in an 'Identity'.
--
-- @since 0.1.3.0
data IIdentity :: Identity k -> k -> Type where
    IId :: IIdentity ('Identity x) x

deriving instance Show (IIdentity as a)

instance (SingI (as :: Identity k), SDecide k) => Decidable (TyPred (IIdentity as)) where
    decide x = withSingI x $ pickElem

type instance Elem Identity = IIdentity

-- | The single-pointed universe.  Note that this instance is really only
-- usable in /singletons-2.5/ and higher (so GHC 8.6).
instance Universe Identity where
    idecideAny f (SIdentity x) = mapDecision (WitAny IId)
                                             (\case WitAny IId p -> p)
                               $ f IId x
    idecideAll f (SIdentity x) = mapDecision (\p -> WitAll $ \case IId -> p)
                                             (`runWitAll` IId)
                               $ f IId x
    igenAllA f (SIdentity x) = (\p -> WitAll $ \case IId -> p) <$> f IId x

-- | Compose two Functors.  Is the same as 'Data.Functor.Compose.Compose'
-- and 'GHC.Generics.:.:', except with a singleton and meant to be used at
-- the type level.  Will be redundant if either of the above gets brought
-- into the singletons library.
--
-- Note that because this is a higher-kinded data constructor, there is no
-- 'SingKind'  instance; if you need 'fromSing' and 'toSing', try going
-- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.
--
-- Note that 'Identity' acts as an identity.
--
-- @since 0.1.2.0
data (f :.: g) a = Comp { getComp :: f (g a) }
    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)

data instance Sing (k :: (f :.: g) a) where
    SComp :: Sing x -> Sing ('Comp x)

-- | 'getComp' lifted to the type level
--
-- @since 0.1.2.0
type family GetComp c where
    GetComp ('Comp a) = a

-- | Singletonized witness for 'GetComp'
--
-- @since 0.1.2.0
sGetComp :: Sing a -> Sing (GetComp a)
sGetComp (SComp x) = x

instance SingI ass => SingI ('Comp ass) where
    sing = SComp sing

data GetCompSym0 :: (f :.: g) k ~> f (g k)
type instance Apply GetCompSym0 ('Comp ass) = ass
type GetCompSym1 a = GetComp a

-- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where
--     type Demote ((f :.: g) a) = (:.:) f' g' a'

-- | A pair of indices allows you to index into a nested structure.
--
-- @since 0.1.2.0
data CompElem :: (f :.: g) k -> k -> Type where
    (:?) :: Elem f ass as
         -> Elem g as  a
         -> CompElem ('Comp ass) a

-- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))
--     => Show (CompElem ('Comp ass :: (f :.: g) k) a)

type instance Elem (f :.: g) = CompElem

instance (Universe f, Universe g) => Universe (f :.: g) where
    idecideAny
        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
        -> Sing ass
        -> Decision (Any (f :.: g) p @@ ass)
    idecideAny f (SComp xss)
        = mapDecision anyComp compAny
        . idecideAny @f @_ @(Any g p) go
        $ xss
      where
        go  :: Elem f (GetComp ass) as
            -> Sing as
            -> Decision (Any g p @@ as)
        go i = idecideAny $ \j -> f (i :? j)

    idecideAll
        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
        -> Sing ass
        -> Decision (All (f :.: g) p @@ ass)
    idecideAll f (SComp xss)
        = mapDecision allComp compAll
        . idecideAll @f @_ @(All g p) go
        $ xss
      where
        go  :: Elem f (GetComp ass) as
            -> Sing as
            -> Decision (All g p @@ as)
        go i = idecideAll $ \j -> f (i :? j)

    igenAllA
        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h
        => (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))
        -> Sing ass
        -> h (All (f :.: g) p @@ ass)
    igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass
      where
        go  :: Elem f (GetComp ass) (as :: g k)
            -> Sing as
            -> h (All g p @@ as)
        go i = igenAllA $ \j -> f (i :? j)

-- | Turn a composition of 'Any' into an 'Any' of a composition.
--
-- @since 0.1.2.0
anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p

-- | Turn an 'Any' of a composition into a composition of 'Any'.
--
-- @since 0.1.2.0
compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)

-- | Turn a composition of 'All' into an 'All' of a composition.
--
-- @since 0.1.2.0
allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j

-- | Turn an 'All' of a composition into a composition of 'All'.
--
-- @since 0.1.2.0
compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)

-- | Disjoint union of two Functors.  Is the same as 'Data.Functor.Sum.Sum'
-- and 'GHC.Generics.:+:', except with a singleton and meant to be used at
-- the type level.  Will be redundant if either of the above gets brought
-- into the singletons library.
--
-- Note that because this is a higher-kinded data constructor, there is no
-- 'SingKind'  instance; if you need 'fromSing' and 'toSing', consider
-- manually pattern matching.
--
-- Note that 'Proxy' acts as an identity.
--
-- @since 0.1.3.0
data (f :+: g) a = InL (f a)
                 | InR (g a)
    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
deriving instance (Traversable f, Traversable g) => Traversable (f :+: g)

data instance Sing (k :: (f :+: g) a) where
    SInL :: Sing x -> Sing ('InL x)
    SInR :: Sing y -> Sing ('InR y)

type family FromL s where
    FromL ('InL a) = a

-- | Index into a disjoint union by providing an index into one of the two
-- possible options.
--
-- @since 0.1.3.0
data SumElem :: (f :+: g) k -> k -> Type where
    IInL :: Elem f as a -> SumElem ('InL as) a
    IInR :: Elem f bs b -> SumElem ('InR bs) b

type instance Elem (f :+: g) = SumElem

instance (Universe f, Universe g) => Universe (f :+: g) where
    idecideAny
        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
        -> Sing abs
        -> Decision (Any (f :+: g) p @@ abs)
    idecideAny f = \case
      SInL xs -> mapDecision anySumL sumLAny
               $ idecideAny @f @_ @p (f . IInL) xs
      SInR ys -> mapDecision anySumR sumRAny
               $ idecideAny @g @_ @p (f . IInR) ys

    idecideAll
        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
        -> Sing abs
        -> Decision (All (f :+: g) p @@ abs)
    idecideAll f = \case
      SInL xs -> mapDecision allSumL sumLAll
               $ idecideAll @f @_ @p (f . IInL) xs
      SInR xs -> mapDecision allSumR sumRAll
               $ idecideAll @g @_ @p (f . IInR) xs

    igenAllA
        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k) h. Applicative h
        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> h (p @@ ab))
        -> Sing abs
        -> h (All (f :+: g) p @@ abs)
    igenAllA f = \case
      SInL xs -> allSumL <$> igenAllA @f @_ @p (f . IInL) xs
      SInR xs -> allSumR <$> igenAllA @g @_ @p (f . IInR) xs

-- | Turn an 'Any' of @f@ into an 'Any' of @f ':+:' g@.
anySumL :: Any f p @@ as -> Any (f :+: g) p @@ 'InL as
anySumL (WitAny i x) = WitAny (IInL i) x

-- | Turn an 'Any' of @g@ into an 'Any' of @f ':+:' g@.
anySumR :: Any g p @@ bs -> Any (f :+: g) p @@ 'InR bs
anySumR (WitAny j y) = WitAny (IInR j) y

-- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @f@.
sumLAny :: Any (f :+: g) p @@ 'InL as -> Any f p @@ as
sumLAny (WitAny (IInL i) x) = WitAny i x

-- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @g@.
sumRAny :: Any (f :+: g) p @@ 'InR bs -> Any g p @@ bs
sumRAny (WitAny (IInR j) y) = WitAny j y

-- | Turn an 'All' of @f@ into an 'All' of @f ':+:' g@.
allSumL :: All f p @@ as -> All (f :+: g) p @@ 'InL as
allSumL a = WitAll $ \case IInL i -> runWitAll a i

-- | Turn an 'All' of @g@ into an 'All' of @f ':+:' g@.
allSumR :: All g p @@ bs -> All (f :+: g) p @@ 'InR bs
allSumR a = WitAll $ \case IInR j -> runWitAll a j

-- | Turn an 'All' of @f ':+:' g@ into an 'All' of @f@.
sumLAll :: All (f :+: g) p @@ 'InL as -> All f p @@ as
sumLAll a = WitAll $ runWitAll a . IInL

-- | Turn an 'All' of @f ':+:' g@ into an 'All' of @g@.
sumRAll :: All (f :+: g) p @@ 'InR bs -> All g p @@ bs
sumRAll a = WitAll $ runWitAll a . IInR