{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DeriveGeneric            #-}
{-# LANGUAGE DeriveTraversable        #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE InstanceSigs             #-}
{-# LANGUAGE KindSignatures           #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilyDependencies   #-}
{-# LANGUAGE TypeInType               #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE ViewPatterns             #-}

-- |
-- Module      : Data.Type.Functor.Product
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Generalized functor products based on lifted 'Foldable's.
--
-- For example, @'Rec' f '[a,b,c]@ from /vinyl/ contains an @f a@, @f b@,
-- and @f c@.
--
-- @'PMaybe' f ('Just a)@ contains an @f a@ and @'PMaybe' f 'Nothing@
-- contains nothing.
--
-- Also provide data types for "indexing" into each foldable.

module Data.Type.Functor.Product (
  -- * Classes
    FProd(..), Shape
  , PureProd(..), pureShape
  , PureProdC(..), ReifyConstraintProd(..)
  , AllConstrainedProd
  -- ** Functions
  , indexProd, mapProd, foldMapProd, hmap, zipProd
  , imapProd, itraverseProd, ifoldMapProd
  , generateProd, generateProdA
  , selectProd, indices
  , eqProd, compareProd
  -- *** Over singletons
  , indexSing, singShape
  , foldMapSing, ifoldMapSing
  -- * Instances
  , Rec(..), Index(..), withPureProdList
  , PMaybe(..), IJust(..)
  , PEither(..), IRight(..)
  , NERec(..), NEIndex(..), withPureProdNE
  , PTup(..), ISnd(..)
  , PIdentity(..), IIdentity(..)
  , sameIndexVal, sameNEIndexVal
  -- ** Interfacing with vinyl
  , rElemIndex, indexRElem, toCoRec
  -- * Singletons
  , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIIdentity(..)
  -- * Defunctionalization symbols
  , ElemSym0, ElemSym1, ElemSym2
  , ProdSym0, ProdSym1, ProdSym2
  ) where

import           Control.Applicative
import           Data.Either.Singletons
import           Data.Foldable.Singletons hiding  (Elem, ElemSym0, ElemSym1, ElemSym2)
import           Data.Function.Singletons
import           Data.Functor.Classes
import           Data.Functor.Identity
import           Data.Functor.Identity.Singletons
import           Data.Functor.Singletons
import           Data.Kind
import           Data.List.NonEmpty               (NonEmpty(..))
import           Data.List.Singletons hiding      (Elem, ElemSym0, ElemSym1, ElemSym2)
import           Data.Maybe
import           Data.Maybe.Singletons
import           Data.Semigroup
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Tuple.Singletons
import           Data.Vinyl hiding                ((:~:))
import           Data.Vinyl.CoRec
import           GHC.Generics                     ((:*:)(..))
import           Lens.Micro hiding                ((%~))
import           Lens.Micro.Extras
import           Text.Show.Singletons
import           Unsafe.Coerce
import qualified Data.List.NonEmpty.Singletons    as NE
import qualified Data.Text                        as T
import qualified Data.Vinyl.Functor               as V
import qualified Data.Vinyl.TypeLevel             as V

fmapIdent :: Fmap IdSym0 as :~: as
fmapIdent :: forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent = forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl

-- | Simply witness the /shape/ of an argument (ie, @'Shape' [] as@
-- witnesses the length of @as@, and @'Shape' Maybe as@ witnesses whether
-- or not @as@ is 'Just' or 'Nothing').
type Shape f = (Prod f Proxy :: f k -> Type)

-- | Unify different functor products over a Foldable @f@.
class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where
    type Elem  f = (i :: f k -> k -> Type) | i -> f
    type Prod  f = (p :: (k -> Type) -> f k -> Type) | p -> f

    -- | You can convert a singleton of a foldable value into a foldable product of
    -- singletons.  This essentially "breaks up" the singleton into its
    -- individual items.  Should be an inverse with 'prodSing'.
    singProd :: Sing as -> Prod f Sing as

    -- | Collect a collection of singletons back into a single singleton.
    -- Should be an inverse with 'singProd'.
    prodSing :: Prod f Sing as -> Sing as

    -- | Pair up each item in a foldable product with its index.
    withIndices
        :: Prod f g as
        -> Prod f (Elem f as :*: g) as

    -- | Traverse a foldable functor product with a RankN applicative function,
    -- mapping over each value and sequencing the effects.
    --
    -- This is the generalization of 'rtraverse'.
    traverseProd
        :: forall g h as m. Applicative m
        => (forall a. g a -> m (h a))
        -> Prod f g as
        -> m (Prod f h as)
    traverseProd = case forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent @as of
      Fmap IdSym0 as :~: as
Refl -> forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
       (g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse (forall {k} (a :: k). SingI a => Sing a
sing @IdSym0)

    -- | Zip together two foldable functor products with a Rank-N function.
    zipWithProd
        :: (forall a. g a -> h a -> j a)
        -> Prod f g as
        -> Prod f h as
        -> Prod f j as
    zipWithProd forall (a :: k). g a -> h a -> j a
f Prod f g as
xs Prod f h as
ys = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd (\Elem f as a
i g a
x -> forall (a :: k). g a -> h a -> j a
f g a
x (forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i Prod f h as
ys)) Prod f g as
xs

    -- | Traverse a foldable functor product with a type-changing function.
    htraverse
        :: Applicative m
        => Sing ff
        -> (forall a. g a -> m (h (ff @@ a)))
        -> Prod f g as
        -> m (Prod f h (Fmap ff as))

    -- | A 'Lens' into an item in a foldable functor product, given its
    -- index.
    --
    -- This roughly generalizes 'rlens'.
    ixProd
        :: Elem f as a
        -> Lens' (Prod f g as) (g a)

    -- | Fold a functor product into a 'Rec'.
    toRec :: Prod f g as -> Rec g (ToList as)

    -- | Get a 'PureProd' instance from a foldable functor product
    -- providing its shape.
    withPureProd
        :: Prod f g as
        -> (PureProd f as => r)
        -> r

-- | Create @'Prod' f@ if you can give a @g a@ for every slot.
class PureProd f as where
    pureProd :: (forall a. g a) -> Prod f g as

-- | Create @'Prod' f@ if you can give a @g a@ for every slot, given some
-- constraint.
class PureProdC f c as where
    pureProdC :: (forall a. c a => g a) -> Prod f g as

-- | Pair up each item in a @'Prod' f@ with a witness that @f a@ satisfies
-- some constraint.
class ReifyConstraintProd f c g as where
    reifyConstraintProd :: Prod f g as -> Prod f (Dict c V.:. g) as

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

data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> f k ~> Type
data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type
type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as

type instance Apply (ProdSym0 f) g = ProdSym1 f g
type instance Apply (ProdSym1 f g) as = Prod f g as

-- | A convenient wrapper over 'V.AllConstrained' that works for any
-- Foldable @f@.
type AllConstrainedProd c as = V.AllConstrained c (ToList as)

-- | Create a 'Shape' given an instance of 'PureProd'.
pureShape :: PureProd f as => Shape f as
pureShape :: forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall {k} (t :: k). Proxy t
Proxy

-- | Generate a 'Prod' of indices for an @as@.
indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
indices :: forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall a b. a -> b -> a
const forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape

-- | Convert a @'Sing' as@ into a @'Shape' f as@, witnessing the shape of
-- of @as@ but dropping all of its values.
singShape
    :: FProd f
    => Sing as
    -> Shape f as
singShape :: forall {k} (f :: * -> *) (as :: f k).
FProd f =>
Sing as -> Shape f as
singShape = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall a b. a -> b -> a
const forall {k} (t :: k). Proxy t
Proxy) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd

-- | Map a RankN function over a 'Prod'.  The generalization of 'rmap'.
mapProd
    :: FProd f
    => (forall a. g a -> h a)
    -> Prod f g as
    -> Prod f h as
mapProd :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). g a -> h a
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). g a -> h a
f)

-- | Zip together the values in two 'Prod's.
zipProd
    :: FProd f
    => Prod f g as
    -> Prod f h as
    -> Prod f (g :*: h) as
zipProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k) (h :: k -> *).
FProd f =>
Prod f g as -> Prod f h as -> Prod f (g :*: h) as
zipProd = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)

-- | Map a type-changing function over every item in a 'Prod'.
hmap
    :: FProd f
    => Sing ff
    -> (forall a. g a -> h (ff @@ a))
    -> Prod f g as
    -> Prod f h (Fmap ff as)
hmap :: forall {a} {k} (f :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: f a).
FProd f =>
Sing ff
-> (forall (a :: a). g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap Sing ff
ff forall (a :: a). g a -> h (ff @@ a)
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
       (g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: a). g a -> h (ff @@ a)
f)

-- | 'mapProd', but with access to the index at each element.
imapProd
    :: FProd f
    => (forall a. Elem f as a -> g a -> h a)
    -> Prod f g as
    -> Prod f h as
imapProd :: forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall (a :: k). Elem f as a -> g a -> h a
f = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Elem f as a
i :*: g a
x) -> forall (a :: k). Elem f as a -> g a -> h a
f Elem f as a
i g a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices

-- | Extract the item from the container witnessed by the 'Elem'
indexSing
    :: forall f as a. FProd f
    => Elem f as a        -- ^ Witness
    -> Sing as            -- ^ Collection
    -> Sing a
indexSing :: forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i = forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd

-- | Use an 'Elem' to index a value out of a 'Prod'.
indexProd
    :: FProd f
    => Elem f as a
    -> Prod f g as
    -> g a
indexProd :: forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i = forall a s. Getting a s a -> s -> a
view (forall (f :: * -> *) {k} (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Elem f as a
i)

-- | 'traverseProd', but with access to the index at each element.
itraverseProd
    :: (FProd f, Applicative m)
    => (forall a. Elem f as a -> g a -> m (h a))
    -> Prod f g as
    -> m (Prod f h as)
itraverseProd :: forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
       (h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd forall (a :: k). Elem f as a -> g a -> m (h a)
f = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (\(Elem f as a
i :*: g a
x) -> forall (a :: k). Elem f as a -> g a -> m (h a)
f Elem f as a
i g a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices

-- | 'foldMapProd', but with access to the index at each element.
ifoldMapProd
    :: (FProd f, Monoid m)
    => (forall a. Elem f as a -> g a -> m)
    -> Prod f g as
    -> m
ifoldMapProd :: forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd forall (a :: k). Elem f as a -> g a -> m
f = forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
       (h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd (\Elem f as a
i -> forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Elem f as a -> g a -> m
f Elem f as a
i)

-- | Map a RankN function over a 'Prod' and collect the results as
-- a 'Monoid'.
foldMapProd
    :: (FProd f, Monoid m)
    => (forall a. g a -> m)
    -> Prod f g as
    -> m
foldMapProd :: forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall (a :: k). g a -> m
f = forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd (forall a b. a -> b -> a
const forall (a :: k). g a -> m
f)

-- | 'foldMapSing' but with access to the index.
ifoldMapSing
    :: forall f k (as :: f k) m. (FProd f, Monoid m)
    => (forall a. Elem f as a -> Sing a -> m)
    -> Sing as
    -> m
ifoldMapSing :: forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing forall (a :: k). Elem f as a -> Sing a -> m
f = forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd forall (a :: k). Elem f as a -> Sing a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd

-- | A 'foldMap' over all items in a collection.
foldMapSing
    :: forall f k (as :: f k) m. (FProd f, Monoid m)
    => (forall (a :: k). Sing a -> m)
    -> Sing as
    -> m
foldMapSing :: forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Sing a -> m) -> Sing as -> m
foldMapSing forall (a :: k). Sing a -> m
f = forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing (forall a b. a -> b -> a
const forall (a :: k). Sing a -> m
f)

-- | Rearrange or permute the items in a 'Prod' based on a 'Prod' of
-- indices.
--
-- @
-- 'selectProd' ('IS' 'IZ' ':&' IZ :& 'RNil') ("hi" :& "bye" :& "ok" :& RNil)
--      == "bye" :& "hi" :& RNil
-- @
selectProd
    :: FProd f
    => Prod f (Elem f as) bs
    -> Prod f g as
    -> Prod f g bs
selectProd :: forall {k} (f :: * -> *) (as :: f k) (bs :: f k) (g :: k -> *).
FProd f =>
Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs
selectProd Prod f (Elem f as) bs
is Prod f g as
xs = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
`indexProd` Prod f g as
xs) Prod f (Elem f as) bs
is

-- | An implementation of equality testing for all 'FProd' instances, as
-- long as each of the items are instances of 'Eq'.
eqProd
    :: (FProd f, ReifyConstraintProd f Eq g as)
    => Prod f g as
    -> Prod f g as
    -> Bool
eqProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Eq g as) =>
Prod f g as -> Prod f g as -> Bool
eqProd Prod f g as
xs = All -> Bool
getAll
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall {k} a (b :: k). Const a b -> a
getConst
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict g a
x)) g a
y -> forall {k} a (b :: k). a -> Const a b
Const (Bool -> All
All (g a
x forall a. Eq a => a -> a -> Bool
== g a
y)))
                (forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
       (as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Eq Prod f g as
xs)

-- | An implementation of order comparison for all 'FProd' instances, as
-- long as each of the items are instances of 'Ord'.
compareProd
    :: (FProd f, ReifyConstraintProd f Ord g as)
    => Prod f g as
    -> Prod f g as
    -> Ordering
compareProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Ord g as) =>
Prod f g as -> Prod f g as -> Ordering
compareProd Prod f g as
xs = forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall {k} a (b :: k). Const a b -> a
getConst
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict g a
x)) g a
y -> forall {k} a (b :: k). a -> Const a b
Const (forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y))
                  (forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
       (as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Ord Prod f g as
xs)

-- | Construct a 'Prod' purely by providing a generating function for each
-- index.
generateProd
    :: (FProd f, PureProd f as)
    => (forall a. Elem f as a -> g a)
    -> Prod f g as
generateProd :: forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
(FProd f, PureProd f as) =>
(forall (a :: k). Elem f as a -> g a) -> Prod f g as
generateProd forall (a :: k). Elem f as a -> g a
f = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Elem f as a -> g a
f forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices

-- | Construct a 'Prod' in an 'Applicative' context by providing
-- a generating function for each index.
generateProdA
    :: (FProd f, PureProd f as, Applicative m)
    => (forall a. Elem f as a -> m (g a))
    -> m (Prod f g as)
generateProdA :: forall {k} (f :: * -> *) (as :: f k) (m :: * -> *) (g :: k -> *).
(FProd f, PureProd f as, Applicative m) =>
(forall (a :: k). Elem f as a -> m (g a)) -> m (Prod f g as)
generateProdA forall (a :: k). Elem f as a -> m (g a)
f = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). Elem f as a -> m (g a)
f forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices


-- | Witness an item in a type-level list by providing its index.
--
-- The number of 'IS's correspond to the item's position in the list.
--
-- @
-- 'IZ'         :: 'Index' '[5,10,2] 5
-- 'IS' 'IZ'      :: 'Index' '[5,10,2] 10
-- 'IS' ('IS' 'IZ') :: 'Index' '[5,10,2] 2
-- @
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)
deriving instance Eq (Index as a)
deriving instance Ord (Index as a)

-- | Kind-indexed singleton for 'Index'.
data SIndex (as :: [k]) (a :: k) :: Index as a -> Type where
    SIZ :: SIndex (a ': as) a 'IZ
    SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)

deriving instance Show (SIndex as a i)

type instance Sing = SIndex as a :: Index as a -> Type

instance SingI 'IZ where
    sing :: Sing 'IZ
sing = forall {k} (a :: k) (a :: [k]). SIndex (a : a) a 'IZ
SIZ

instance SingI i => SingI ('IS i) where
    sing :: Sing ('IS i)
sing = forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS forall {k} (a :: k). SingI a => Sing a
sing

instance SingKind (Index as a) where
    type Demote (Index as a) = Index as a
    fromSing :: forall (a :: Index as a). Sing a -> Demote (Index as a)
fromSing = \case
       Sing a
SIndex as a a
SIZ   -> forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ
       SIS SIndex bs a i
j -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SIndex bs a i
j)
    toSing :: Demote (Index as a) -> SomeSing (Index as a)
toSing Demote (Index as a)
i = forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Demote (Index as a)
i forall k (a :: k). Sing a -> SomeSing k
SomeSing
      where
        go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
        go :: forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go = \case
          Index bs b
IZ   -> (forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) (a :: [k]). SIndex (a : a) a 'IZ
SIZ)
          IS Index bs b
j -> \forall (i :: Index bs b). SIndex bs b i -> r
f -> forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Index bs b
j (forall (i :: Index bs b). SIndex bs b i -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS)

instance SDecide (Index as a) where
    %~ :: forall (a :: Index as a) (b :: Index as a).
Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
      Sing a
SIndex as a a
SIZ -> \case
        Sing b
SIndex (a : as) a b
SIZ   -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
        SIS SIndex bs a i
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
      SIS SIndex bs a i
i' -> \case
        Sing b
SIndex (b : bs) a b
SIZ   -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
        SIS SIndex bs a i
j' -> case SIndex bs a i
i' forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SIndex bs a i
j' of
          Proved i :~: i
Refl -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
          Disproved Refuted (i :~: i)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v forall {k} (a :: k). a :~: a
Refl

instance FProd [] where
    type Elem [] = Index
    type Prod [] = Rec

    singProd :: forall {k} (as :: [k]). Sing as -> Prod [] Sing as
singProd = \case
      Sing as
SList as
SNil         -> forall {u} (a :: u -> *). Rec a '[]
RNil
      Sing n1
x `SCons` Sing n2
xs -> Sing n1
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs

    prodSing :: forall {k} (as :: [k]). Prod [] Sing as -> Sing as
prodSing = \case
      Rec Sing as
Prod [] Sing as
RNil    -> forall a. SList '[]
SNil
      Sing r
x :& Rec Sing rs
xs -> Sing r
x forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing rs
xs

    traverseProd
        :: forall g h m as. Applicative m
        => (forall a. g a -> m (h a))
        -> Prod [] g as
        -> m (Prod [] h as)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (m :: * -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
traverseProd forall (a :: k). g a -> m (h a)
f = forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go
      where
        go :: Prod [] g bs -> m (Prod [] h bs)
        go :: forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go = \case
          Rec g bs
Prod [] g bs
RNil    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (a :: u -> *). Rec a '[]
RNil
          g r
x :& Rec g rs
xs -> forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go Rec g rs
xs

    zipWithProd
        :: forall g h j as. ()
        => (forall a. g a -> h a -> j a)
        -> Prod [] g as
        -> Prod [] h as
        -> Prod [] j as
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: [k]).
(forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go
      where
        go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
        go :: forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go = \case
          Rec g bs
Prod [] g bs
RNil -> \case
            Rec h '[]
Prod [] h bs
RNil -> forall {u} (a :: u -> *). Rec a '[]
RNil
          g r
x :& Rec g rs
xs -> \case
            h r
y :& Rec h rs
ys -> forall (a :: k). g a -> h a -> j a
f g r
x h r
y forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go Rec g rs
xs Rec h rs
ys

    htraverse
        :: forall ff g h as m. Applicative m
        => Sing ff
        -> (forall a. g a -> m (h (ff @@ a)))
        -> Prod [] g as
        -> m (Prod [] h (Fmap ff as))
    htraverse :: forall {a} {k} (ff :: a ~> k) (g :: a -> *) (h :: k -> *)
       (as :: [a]) (m :: * -> *).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go
      where
        go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
        go :: forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go = \case
          Rec g bs
Prod [] g bs
RNil    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (a :: u -> *). Rec a '[]
RNil
          g r
x :& Rec g rs
xs -> forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
xs

    withIndices :: forall {k} (g :: k -> *) (as :: [k]).
Prod [] g as -> Prod [] (Elem [] as :*: g) as
withIndices = \case
        Rec g as
Prod [] g as
RNil    -> forall {u} (a :: u -> *). Rec a '[]
RNil
        g r
x :& Rec g rs
xs -> (forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
x) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Index rs a
i :*: g a
y) -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS Index rs a
i forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g rs
xs)

    ixProd
        :: forall g as a. ()
        => Elem [] as a
        -> Lens' (Prod [] g as) (g a)
    ixProd :: forall {k} (g :: k -> *) (as :: [k]) (a :: k).
Elem [] as a -> Lens' (Prod [] g as) (g a)
ixProd Elem [] as a
i0 (g a -> f (g a)
f :: g a -> h (g a)) = forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Elem [] as a
i0
      where
        go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
        go :: forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go = \case
          Index bs a
Elem [] bs a
IZ -> \case
            g r
x :& Rec g rs
xs -> (forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g rs
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g r
x
          IS Index bs a
i -> \case
            g r
x :& Rec g rs
xs -> (g r
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Index bs a
i Rec g rs
xs

    toRec :: forall {a} (g :: a -> *) (as :: [a]).
Prod [] g as -> Rec g (ToList as)
toRec = forall a. a -> a
id

    withPureProd :: forall {k} (g :: k -> *) (as :: [k]) r.
Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList

-- | A stronger version of 'withPureProd' for 'Rec', providing
-- a 'RecApplicative' instance as well.
withPureProdList
    :: Rec f as
    -> ((RecApplicative as, PureProd [] as) => r)
    -> r
withPureProdList :: forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList = \case
    Rec f as
RNil    -> forall a. a -> a
id
    f r
_ :& Rec f rs
xs -> forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f rs
xs

instance RecApplicative as => PureProd [] as where
    pureProd :: forall (g :: k -> *). (forall (a :: k). g a) -> Prod [] g as
pureProd = forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure

instance RPureConstrained c as => PureProdC [] c as where
    pureProdC :: forall (g :: k -> *). (forall (a :: k). c a => g a) -> Prod [] g as
pureProdC = forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
rpureConstrained @c

instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where
    reifyConstraintProd :: Prod [] f as -> Prod [] (Dict c :. f) as
reifyConstraintProd = forall {u} (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint @c

-- | 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)
deriving instance Read (IJust ('Just a) a)
deriving instance Eq (IJust as a)
deriving instance Ord (IJust as a)

-- | Kind-indexed singleton for 'IJust'.
data SIJust (as :: Maybe k) (a :: k) :: IJust as a -> Type where
    SIJust :: SIJust ('Just a) a 'IJust

deriving instance Show (SIJust as a i)

type instance Sing = SIJust as a :: IJust as a -> Type

instance SingI 'IJust where
    sing :: Sing 'IJust
sing = forall {k} (a :: k). SIJust ('Just a) a 'IJust
SIJust

instance SingKind (IJust as a) where
    type Demote (IJust as a) = IJust as a
    fromSing :: forall (a :: IJust as a). Sing a -> Demote (IJust as a)
fromSing Sing a
SIJust as a a
SIJust = forall {k} (a :: k). IJust ('Just a) a
IJust
    toSing :: Demote (IJust as a) -> SomeSing (IJust as a)
toSing Demote (IJust as a)
IJust as a
IJust = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k). SIJust ('Just a) a 'IJust
SIJust

instance SDecide (IJust as a) where
    Sing a
SIJust as a a
SIJust %~ :: forall (a :: IJust as a) (b :: IJust as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIJust ('Just a) a b
SIJust = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl

-- | A @'PMaybe' f 'Nothing@ contains nothing, and a @'PMaybe' f ('Just a)@
-- contains an @f a@.
--
-- In practice this can be useful to write polymorphic
-- functions/abstractions that contain an argument that can be "turned off"
-- for different instances.
data PMaybe :: (k -> Type) -> Maybe k -> Type where
    PNothing :: PMaybe f 'Nothing
    PJust    :: f a -> PMaybe f ('Just a)

instance ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) where
    showsPrec :: Int -> PMaybe f as -> ShowS
showsPrec Int
d PMaybe f as
xs = case forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
       (as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PMaybe f as
xs of
      PMaybe (Dict Show :. f) as
Prod Maybe (Dict Show :. f) as
PNothing                   -> String -> ShowS
showString String
"PNothing"
      PJust (V.Compose (Dict f a
x)) -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall a. Show a => Int -> a -> ShowS
showsPrec String
"PJust" Int
d f a
x
instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
    == :: PMaybe f as -> PMaybe f as -> Bool
(==) = forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Eq g as) =>
Prod f g as -> Prod f g as -> Bool
eqProd
instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where
    compare :: PMaybe f as -> PMaybe f as -> Ordering
compare = forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Ord g as) =>
Prod f g as -> Prod f g as -> Ordering
compareProd

instance FProd Maybe where
    type instance Elem Maybe = IJust
    type instance Prod Maybe = PMaybe

    singProd :: forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
singProd = \case
      Sing as
SMaybe as
SNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
      SJust Sing n
x  -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust Sing n
x
    prodSing :: forall {k} (as :: Maybe k). Prod Maybe Sing as -> Sing as
prodSing = \case
      PMaybe Sing as
Prod Maybe Sing as
PNothing -> forall a. SMaybe 'Nothing
SNothing
      PJust Sing a
x  -> forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust Sing a
x
    withIndices :: forall {k} (g :: k -> *) (as :: Maybe k).
Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as
withIndices = \case
      PMaybe g as
Prod Maybe g as
PNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust g a
x  -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall {k} (a :: k). IJust ('Just a) a
IJust forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Maybe k)
       (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod Maybe g as -> m (Prod Maybe h as)
traverseProd forall (a :: k). g a -> m (h a)
f = \case
      PMaybe g as
Prod Maybe g as
PNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust g a
x  -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: Maybe k).
(forall (a :: k). g a -> h a -> j a)
-> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = \case
      PMaybe g as
Prod Maybe g as
PNothing -> \case
        PMaybe h 'Nothing
Prod Maybe h as
PNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust g a
x -> \case
        PJust h a
y -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
    htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: Maybe a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod Maybe g as
-> m (Prod Maybe h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = \case
      PMaybe g as
Prod Maybe g as
PNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust g a
x  -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: forall {k} (as :: Maybe k) (a :: k) (g :: k -> *).
Elem Maybe as a -> Lens' (Prod Maybe g as) (g a)
ixProd = \case
      IJust as a
Elem Maybe as a
IJust -> \g a -> f (g a)
f -> \case
        PJust g a
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
    toRec :: forall {a} (g :: a -> *) (as :: Maybe a).
Prod Maybe g as -> Rec g (ToList as)
toRec = \case
      PMaybe g as
Prod Maybe g as
PNothing -> forall {u} (a :: u -> *). Rec a '[]
RNil
      PJust g a
x  -> g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
    withPureProd :: forall {k} (g :: k -> *) (as :: Maybe k) r.
Prod Maybe g as -> (PureProd Maybe as => r) -> r
withPureProd = \case
      PMaybe g as
Prod Maybe g as
PNothing -> forall a. a -> a
id
      PJust g a
_  -> forall a. a -> a
id

instance PureProd Maybe 'Nothing where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Maybe g 'Nothing
pureProd forall (a :: k). g a
_ = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance PureProd Maybe ('Just a) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Maybe g ('Just a)
pureProd forall (a :: k). g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (a :: k). g a
x

instance PureProdC Maybe c 'Nothing where
    pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod Maybe g 'Nothing
pureProdC forall (a :: k). c a => g a
_ = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c a => PureProdC Maybe c ('Just a) where
    pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
pureProdC forall (a :: a). c a => g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (a :: a). c a => g a
x

instance ReifyConstraintProd Maybe c g 'Nothing where
    reifyConstraintProd :: Prod Maybe g 'Nothing -> Prod Maybe (Dict c :. g) 'Nothing
reifyConstraintProd PMaybe g 'Nothing
Prod Maybe g 'Nothing
PNothing = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where
    reifyConstraintProd :: Prod Maybe g ('Just a) -> Prod Maybe (Dict c :. g) ('Just a)
reifyConstraintProd (PJust g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
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)
deriving instance Read (IRight ('Right a) a)
deriving instance Eq (IRight as a)
deriving instance Ord (IRight as a)

-- | Kind-indexed singleton for 'IRight'.
data SIRight (as :: Either j k) (a :: k) :: IRight as a -> Type where
    SIRight :: SIRight ('Right a) a 'IRight

deriving instance Show (SIRight as a i)

type instance Sing = SIRight as a :: IRight as a -> Type

instance SingI 'IRight where
    sing :: Sing 'IRight
sing = forall {k} {j} (a :: k). SIRight ('Right a) a 'IRight
SIRight

instance SingKind (IRight as a) where
    type Demote (IRight as a) = IRight as a
    fromSing :: forall (a :: IRight as a). Sing a -> Demote (IRight as a)
fromSing Sing a
SIRight as a a
SIRight = forall {k} {j} (a :: k). IRight ('Right a) a
IRight
    toSing :: Demote (IRight as a) -> SomeSing (IRight as a)
toSing Demote (IRight as a)
IRight as a
IRight = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} {j} (a :: k). SIRight ('Right a) a 'IRight
SIRight

instance SDecide (IRight as a) where
    Sing a
SIRight as a a
SIRight %~ :: forall (a :: IRight as a) (b :: IRight as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIRight ('Right a) a b
SIRight = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl

-- | A @'PEither' f ('Left e)@ contains @'Sing' e@, and a @'PMaybe' f ('Right a)@
-- contains an @f a@.
--
-- In practice this can be useful in the same situatinos that 'PMaybe' can,
-- but with an extra value in the case where value @f@ is "turned off" with
-- 'Left'.
data PEither :: (k -> Type) -> Either j k -> Type where
    PLeft  :: Sing e -> PEither f ('Left e)
    PRight :: f a -> PEither f ('Right a)

instance (SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as) where
    showsPrec :: Int -> PEither f as -> ShowS
showsPrec Int
d PEither f as
xs = case forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
       (as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PEither f as
xs of
        PLeft Sing e
e                     -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall {a} {a} {t2 :: a}.
(Integral a, SShow a) =>
a -> Sing t2 -> ShowS
go         String
"PLeft" Int
d Sing e
e
        PRight (V.Compose (Dict f a
x)) -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall a. Show a => Int -> a -> ShowS
showsPrec String
"PRight" Int
d f a
x
      where
        go :: a -> Sing t2 -> ShowS
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral->FromSing Sing a
i) Sing t2
x (String -> Text
T.pack->FromSing Sing a
str) = Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing forall a b. (a -> b) -> a -> b
$ forall a (t1 :: Natural) (t2 :: a) (t3 :: Symbol).
SShow a =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
sShowsPrec Sing a
i Sing t2
x Sing a
str

instance FProd (Either j) where
    type instance Elem (Either j) = IRight
    type instance Prod (Either j) = PEither

    singProd :: forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
singProd = \case
      SLeft  Sing n
e -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing n
e
      SRight Sing n
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight Sing n
x
    prodSing :: forall {k} (as :: Either j k). Prod (Either j) Sing as -> Sing as
prodSing = \case
      PLeft Sing e
e  -> forall a b (n :: a). Sing n -> SEither ('Left n)
SLeft Sing e
e
      PRight Sing a
x -> forall a b (n :: b). Sing n -> SEither ('Right n)
SRight Sing a
x
    withIndices :: forall {k} (g :: k -> *) (as :: Either j k).
Prod (Either j) g as
-> Prod (Either j) (Elem (Either j) as :*: g) as
withIndices = \case
      PLeft Sing e
e  -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
      PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall {k} {j} (a :: k). IRight ('Right a) a
IRight forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Either j k)
       (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod (Either j) g as -> m (Prod (Either j) h as)
traverseProd forall (a :: k). g a -> m (h a)
f = \case
      PLeft Sing e
e  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
      PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: Either j k).
(forall (a :: k). g a -> h a -> j a)
-> Prod (Either j) g as
-> Prod (Either j) h as
-> Prod (Either j) j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = \case
      PLeft Sing e
e -> \case
        PLeft Sing e
_ -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
      PRight g a
x -> \case
        PRight h a
y -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
    htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: Either j a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod (Either j) g as
-> m (Prod (Either j) h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = \case
      PLeft Sing e
e  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
      PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: forall {k} (as :: Either j k) (a :: k) (g :: k -> *).
Elem (Either j) as a -> Lens' (Prod (Either j) g as) (g a)
ixProd = \case
      IRight as a
Elem (Either j) as a
IRight -> \g a -> f (g a)
f -> \case
        PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
    toRec :: forall {a} (g :: a -> *) (as :: Either j a).
Prod (Either j) g as -> Rec g (ToList as)
toRec = \case
      PLeft Sing e
_  -> forall {u} (a :: u -> *). Rec a '[]
RNil
      PRight g a
x -> g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
    withPureProd :: forall {k} (g :: k -> *) (as :: Either j k) r.
Prod (Either j) g as -> (PureProd (Either j) as => r) -> r
withPureProd = \case
      PLeft Sing e
Sing -> forall a. a -> a
id
      PRight g a
_   -> forall a. a -> a
id

instance SingI e => PureProd (Either j) ('Left e) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod (Either j) g ('Left e)
pureProd forall (a :: k). g a
_ = forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft forall {k} (a :: k). SingI a => Sing a
sing
instance PureProd (Either j) ('Right a) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod (Either j) g ('Right a)
pureProd forall (a :: k). g a
x = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (a :: k). g a
x

instance SingI e => PureProdC (Either j) c ('Left e) where
    pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod (Either j) g ('Left e)
pureProdC forall (a :: k). c a => g a
_ = (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft forall {k} (a :: k). SingI a => Sing a
sing)
instance c a => PureProdC (Either j) c ('Right a) where
    pureProdC :: forall (g :: b -> *).
(forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
pureProdC forall (a :: b). c a => g a
x = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (a :: b). c a => g a
x

instance ReifyConstraintProd (Either j) c g ('Left e) where
    reifyConstraintProd :: Prod (Either j) g ('Left e)
-> Prod (Either j) (Dict c :. g) ('Left e)
reifyConstraintProd (PLeft Sing e
e) = forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where
    reifyConstraintProd :: Prod (Either j) g ('Right a)
-> Prod (Either j) (Dict c :. g) ('Right a)
reifyConstraintProd (PRight g a
x) = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
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)
deriving instance Eq (NEIndex as a)
deriving instance Ord (NEIndex as a)

-- | Kind-indexed singleton for 'NEIndex'.
data SNEIndex (as :: NonEmpty k) (a :: k) :: NEIndex as a -> Type where
    SNEHead :: SNEIndex (a ':| as) a 'NEHead
    SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)

deriving instance Show (SNEIndex as a i)

type instance Sing = SNEIndex as a :: NEIndex as a -> Type

instance SingI 'NEHead where
    sing :: Sing 'NEHead
sing = forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead

instance SingI i => SingI ('NETail i) where
    sing :: Sing ('NETail i)
sing = forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail forall {k} (a :: k). SingI a => Sing a
sing

instance SingKind (NEIndex as a) where
    type Demote (NEIndex as a) = NEIndex as a
    fromSing :: forall (a :: NEIndex as a). Sing a -> Demote (NEIndex as a)
fromSing = \case
      Sing a
SNEIndex as a a
SNEHead   -> forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead
      SNETail SIndex as a i
i -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail forall a b. (a -> b) -> a -> b
$ forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SIndex as a i
i
    toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)
toSing = \case
      Demote (NEIndex as a)
NEIndex as a
NEHead   -> forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
      NETail Index as a
i -> forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Index as a
i forall a b. (a -> b) -> a -> b
$ forall k (a :: k). Sing a -> SomeSing k
SomeSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail

instance SDecide (NEIndex as a) where
    %~ :: forall (a :: NEIndex as a) (b :: NEIndex as a).
Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
      Sing a
SNEIndex as a a
SNEHead -> \case
        Sing b
SNEIndex (a ':| as) a b
SNEHead   -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
        SNETail SIndex as a i
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
      SNETail SIndex as a i
i -> \case
        Sing b
SNEIndex (b ':| as) a b
SNEHead -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
        SNETail SIndex as a i
j -> case SIndex as a i
i forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SIndex as a i
j of
          Proved i :~: i
Refl -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
          Disproved Refuted (i :~: i)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v forall {k} (a :: k). a :~: a
Refl

-- | A non-empty version of 'Rec'.
data NERec :: (k -> Type) -> NonEmpty k -> Type where
    (:&|) :: f a -> Rec f as -> NERec f (a ':| as)
infixr 5 :&|

deriving instance (Show (f a), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a ':| as))
deriving instance (Eq (f a), Eq (Rec f as)) => Eq (NERec f (a ':| as))
deriving instance (Ord (f a), Ord (Rec f as)) => Ord (NERec f (a ':| as))

instance FProd NonEmpty where
    type instance Elem NonEmpty = NEIndex
    type instance Prod NonEmpty = NERec

    singProd :: forall {k} (as :: NonEmpty k). Sing as -> Prod NonEmpty Sing as
singProd (Sing n1
x NE.:%| Sing n2
xs) = Sing n1
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
    prodSing :: forall {k} (as :: NonEmpty k). Prod NonEmpty Sing as -> Sing as
prodSing (Sing a
x :&| Rec Sing as
xs) = Sing a
x forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing as
xs
    withIndices :: forall {k} (g :: k -> *) (as :: NonEmpty k).
Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as
withIndices (g a
x :&| Rec g as
xs) =
          (forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
      forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Index as a
i :*: g a
y) -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail Index as a
i forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g as
xs)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: NonEmpty k)
       (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod NonEmpty g as -> m (Prod NonEmpty h as)
traverseProd forall (a :: k). g a -> m (h a)
f (g a
x :&| Rec g as
xs) =
        forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
       (m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). g a -> m (h a)
f Rec g as
xs
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: NonEmpty k).
(forall (a :: k). g a -> h a -> j a)
-> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (g a
x :&| Rec g as
xs) (h a
y :&| Rec h as
ys) = forall (a :: k). g a -> h a -> j a
f g a
x h a
y forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall (a :: k). g a -> h a -> j a
f Rec g as
xs Rec h as
ys
    htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: NonEmpty a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod NonEmpty g as
-> m (Prod NonEmpty h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a). g a -> m (h (ff @@ a))
f (g a
x :&| Rec g as
xs) =
        forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
       (g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a). g a -> m (h (ff @@ a))
f Rec g as
xs
    ixProd :: forall {k} (as :: NonEmpty k) (a :: k) (g :: k -> *).
Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a)
ixProd = \case
      NEIndex as a
Elem NonEmpty as a
NEHead -> \g a -> f (g a)
f -> \case
        g a
x :&| Rec g as
xs -> (forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| Rec g as
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
      NETail Index as a
i -> \g a -> f (g a)
f -> \case
        g a
x :&| Rec g as
xs -> (g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) {k} (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Index as a
i g a -> f (g a)
f Rec g as
xs
    toRec :: forall {a} (g :: a -> *) (as :: NonEmpty a).
Prod NonEmpty g as -> Rec g (ToList as)
toRec (g a
x :&| Rec g as
xs) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g as
xs
    withPureProd :: forall {k} (g :: k -> *) (as :: NonEmpty k) r.
Prod NonEmpty g as -> (PureProd NonEmpty as => r) -> r
withPureProd (g a
x :&| Rec g as
xs) = forall {k} (f :: k -> *) (a :: k) (as :: [k]) r.
f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE g a
x Rec g as
xs

-- | A stronger version of 'withPureProd' for 'NERec', providing
-- a 'RecApplicative' instance as well.
withPureProdNE
    :: f a
    -> Rec f as
    -> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
    -> r
withPureProdNE :: forall {k} (f :: k -> *) (a :: k) (as :: [k]) r.
f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE f a
_ Rec f as
xs = forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f as
xs

instance RecApplicative as => PureProd NonEmpty (a ':| as) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod NonEmpty g (a ':| as)
pureProd forall (a :: k). g a
x = forall (a :: k). g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall (a :: k). g a
x

instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where
    pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod NonEmpty g (a ':| as)
pureProdC forall (a :: a). c a => g a
x = forall (a :: a). c a => g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (c :: k -> Constraint) (as :: f k)
       (g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @c forall (a :: a). c a => g a
x

instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where
    reifyConstraintProd :: Prod NonEmpty g (a ':| as)
-> Prod NonEmpty (Dict c :. g) (a ':| as)
reifyConstraintProd (g a
x :&| Rec g as
xs) = forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
                                 forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
       (as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @c Rec g as
xs

-- | Test if two indices point to the same item in a list.
--
-- We have to return a 'Maybe' here instead of a 'Decision', because it
-- might be the case that the same item might be duplicated in a list.
-- Therefore, even if two indices are different, we cannot prove that the
-- values they point to are different.
sameIndexVal
    :: Index as a
    -> Index as b
    -> Maybe (a :~: b)
sameIndexVal :: forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal = \case
    Index as a
IZ -> \case
      Index as b
IZ   -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
      IS Index bs b
_ -> forall a. Maybe a
Nothing
    IS Index bs a
i -> \case
      Index as b
IZ   -> forall a. Maybe a
Nothing
      IS Index bs b
j -> forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index bs a
i Index bs b
j forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl


-- | Test if two indices point to the same item in a non-empty list.
--
-- We have to return a 'Maybe' here instead of a 'Decision', because it
-- might be the case that the same item might be duplicated in a list.
-- Therefore, even if two indices are different, we cannot prove that the
-- values they point to are different.
sameNEIndexVal
    :: NEIndex as a
    -> NEIndex as b
    -> Maybe (a :~: b)
sameNEIndexVal :: forall {k} (as :: NonEmpty k) (a :: k) (b :: k).
NEIndex as a -> NEIndex as b -> Maybe (a :~: b)
sameNEIndexVal = \case
    NEIndex as a
NEHead -> \case
      NEIndex as b
NEHead   -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
      NETail Index as b
_ -> forall a. Maybe a
Nothing
    NETail Index as a
i -> \case
      NEIndex as b
NEHead   -> forall a. Maybe a
Nothing
      NETail Index as b
j -> forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index as a
i Index as b
j forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl

-- | 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)
deriving instance Read (ISnd '(a, b) b)
deriving instance Eq (ISnd as a)
deriving instance Ord (ISnd as a)

-- | Kind-indexed singleton for 'ISnd'.
data SISnd (as :: (j, k)) (a :: k) :: ISnd as a -> Type where
    SISnd :: SISnd '(a, b) b 'ISnd

deriving instance Show (SISnd as a i)

type instance Sing = SISnd as a :: ISnd as a -> Type

instance SingI 'ISnd where
    sing :: Sing 'ISnd
sing = forall {j} {k} (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd

instance SingKind (ISnd as a) where
    type Demote (ISnd as a) = ISnd as a
    fromSing :: forall (a :: ISnd as a). Sing a -> Demote (ISnd as a)
fromSing Sing a
SISnd as a a
SISnd = forall {j} {k} (a :: j) (b :: k). ISnd '(a, b) b
ISnd
    toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)
toSing Demote (ISnd as a)
ISnd as a
ISnd = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {j} {k} (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd

instance SDecide (ISnd as a) where
    Sing a
SISnd as a a
SISnd %~ :: forall (a :: ISnd as a) (b :: ISnd as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SISnd '(a, a) a b
SISnd = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl

-- | A 'PTup' tuples up some singleton with some value; a @'PTup' f '(w,
-- a)@ contains a @'Sing' w@ and an @f a@.
--
-- This can be useful for carrying along some witness aside a functor
-- value.
data PTup :: (k -> Type) -> (j, k) -> Type where
    PTup :: Sing w -> f a -> PTup f '(w, a)

deriving instance (Show (Sing w), Show (f a)) => Show (PTup f '(w, a))
deriving instance (Read (Sing w), Read (f a)) => Read (PTup f '(w, a))
deriving instance (Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a))
deriving instance (Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a))

instance FProd ((,) j) where
    type instance Elem ((,) j) = ISnd
    type instance Prod ((,) j) = PTup

    singProd :: forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
singProd (STuple2 Sing n1
w Sing n2
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing n1
w Sing n2
x
    prodSing :: forall {k} (as :: (j, k)). Prod ((,) j) Sing as -> Sing as
prodSing (PTup Sing w
w Sing a
x) = forall a b (n1 :: a) (n2 :: b).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing w
w Sing a
x
    withIndices :: forall {k} (g :: k -> *) (as :: (j, k)).
Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as
withIndices (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (forall {j} {k} (a :: j) (b :: k). ISnd '(a, b) b
ISnd forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: (j, k))
       (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod ((,) j) g as -> m (Prod ((,) j) h as)
traverseProd forall (a :: k). g a -> m (h a)
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: (j, k)).
(forall (a :: k). g a -> h a -> j a)
-> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (PTup Sing w
w g a
x) (PTup Sing w
_ h a
y) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
    htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: (j, a)).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod ((,) j) g as
-> m (Prod ((,) j) h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: forall {k} (as :: (j, k)) (a :: k) (g :: k -> *).
Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a)
ixProd ISnd as a
Elem ((,) j) as a
ISnd g a -> f (g a)
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
    toRec :: forall {a} (g :: a -> *) (as :: (j, a)).
Prod ((,) j) g as -> Rec g (ToList as)
toRec (PTup Sing w
_ g a
x) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
    withPureProd :: forall {k} (g :: k -> *) (as :: (j, k)) r.
Prod ((,) j) g as -> (PureProd ((,) j) as => r) -> r
withPureProd (PTup Sing w
Sing g a
_) PureProd ((,) j) as => r
x = PureProd ((,) j) as => r
x

instance SingI w => PureProd ((,) j) '(w, a) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod ((,) j) g '(w, a)
pureProd forall (a :: k). g a
x = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup forall {k} (a :: k). SingI a => Sing a
sing forall (a :: k). g a
x

instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
    pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod ((,) j) g '(w, a)
pureProdC forall (a :: k). c a => g a
x = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup forall {k} (a :: k). SingI a => Sing a
sing forall (a :: k). c a => g a
x

instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where
    reifyConstraintProd :: Prod ((,) j) g '(w, a) -> Prod ((,) j) (Dict c :. g) '(w, a)
reifyConstraintProd (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall a b. (a -> b) -> a -> b
$ forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)

-- | 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)
deriving instance Read (IIdentity ('Identity a) a)
deriving instance Eq (IIdentity as a)
deriving instance Ord (IIdentity as a)

-- | Kind-indexed singleton for 'IIdentity'.
--
-- @since 0.1.5.0
data SIIdentity (as :: Identity k) (a :: k) :: IIdentity as a -> Type where
    SIId :: SIIdentity ('Identity a) a 'IId

deriving instance Show (SIIdentity as a i)

type instance Sing = SIIdentity as a :: IIdentity as a -> Type

instance SingI 'IId where
    sing :: Sing 'IId
sing = forall {k} (a :: k). SIIdentity ('Identity a) a 'IId
SIId

instance SingKind (IIdentity as a) where
    type Demote (IIdentity as a) = IIdentity as a
    fromSing :: forall (a :: IIdentity as a). Sing a -> Demote (IIdentity as a)
fromSing Sing a
SIIdentity as a a
SIId = forall {k} (x :: k). IIdentity ('Identity x) x
IId
    toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)
toSing Demote (IIdentity as a)
IIdentity as a
IId = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k). SIIdentity ('Identity a) a 'IId
SIId

instance SDecide (IIdentity as a) where
    Sing a
SIIdentity as a a
SIId %~ :: forall (a :: IIdentity as a) (b :: IIdentity as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIIdentity ('Identity a) a b
SIId = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl

-- | A 'PIdentity' is a trivial functor product; it is simply the functor,
-- itself, alone.  @'PIdentity' f ('Identity' a)@ is simply @f a@.  This
-- may be useful in conjunction with other combinators.
data PIdentity :: (k -> Type) -> Identity k -> Type where
    PIdentity :: f a -> PIdentity f ('Identity a)

deriving instance Show (f a) => Show (PIdentity f ('Identity a))
deriving instance Read (f a) => Read (PIdentity f ('Identity a))
deriving instance Eq (f a) => Eq (PIdentity f ('Identity a))
deriving instance Ord (f a) => Ord (PIdentity f ('Identity a))

instance FProd Identity where
    type Elem Identity = IIdentity
    type Prod Identity = PIdentity

    singProd :: forall {k} (as :: Identity k). Sing as -> Prod Identity Sing as
singProd (SIdentity Sing n
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity Sing n
x
    prodSing :: forall {k} (as :: Identity k). Prod Identity Sing as -> Sing as
prodSing (PIdentity Sing a
x) = forall a (n :: a). Sing n -> SIdentity ('Identity n)
SIdentity Sing a
x
    withIndices :: forall {k} (g :: k -> *) (as :: Identity k).
Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as
withIndices (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (forall {k} (x :: k). IIdentity ('Identity x) x
IId forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Identity k)
       (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod Identity g as -> m (Prod Identity h as)
traverseProd forall (a :: k). g a -> m (h a)
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
       (as :: Identity k).
(forall (a :: k). g a -> h a -> j a)
-> Prod Identity g as -> Prod Identity h as -> Prod Identity j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (PIdentity g a
x) (PIdentity h a
y) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
    htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: Identity a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod Identity g as
-> m (Prod Identity h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: forall {k} (as :: Identity k) (a :: k) (g :: k -> *).
Elem Identity as a -> Lens' (Prod Identity g as) (g a)
ixProd IIdentity as a
Elem Identity as a
IId g a -> f (g a)
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
    toRec :: forall {a} (g :: a -> *) (as :: Identity a).
Prod Identity g as -> Rec g (ToList as)
toRec (PIdentity g a
x) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
    withPureProd :: forall {k} (g :: k -> *) (as :: Identity k) r.
Prod Identity g as -> (PureProd Identity as => r) -> r
withPureProd (PIdentity g a
_) PureProd Identity as => r
x = PureProd Identity as => r
x

instance PureProd Identity ('Identity a) where
    pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Identity g ('Identity a)
pureProd forall (a :: k). g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (a :: k). g a
x

instance c a => PureProdC Identity c ('Identity a) where
    pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
pureProdC forall (a :: a). c a => g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (a :: a). c a => g a
x

instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where
    reifyConstraintProd :: Prod Identity g ('Identity a)
-> Prod Identity (Dict c :. g) ('Identity a)
reifyConstraintProd (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall a b. (a -> b) -> a -> b
$ forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)

-- | Produce an 'Index' from an 'RElem' constraint.
rElemIndex
    :: forall r rs i. (RElem r rs i, PureProd [] rs)
    => Index rs r
rElemIndex :: forall {k} (r :: k) (rs :: [k]) (i :: Nat).
(RElem r rs i, PureProd [] rs) =>
Index rs r
rElemIndex = forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f, r ~ r') =>
record f rs -> f r
rgetC forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices

-- | Use an 'Index' to inject an @f a@ into a 'CoRec'.
toCoRec
    :: forall k (as :: [k]) a f. (RecApplicative as, FoldRec as as)
    => Index as a
    -> f a
    -> CoRec f as
toCoRec :: forall k (as :: [k]) (a :: k) (f :: k -> *).
(RecApplicative as, FoldRec as as) =>
Index as a -> f a -> CoRec f as
toCoRec = \case
    Index as a
IZ   -> forall {k} (a1 :: k) (b :: [k]) (a :: k -> *).
RElem a1 b (RIndex a1 b) =>
a a1 -> CoRec a b
CoRec
    IS Index bs a
i -> \f a
x -> forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField forall a b. (a -> b) -> a -> b
$ forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall (bs :: [k]) (b :: k) (c :: k).
Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go Index bs a
i f a
x) forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
  where
    go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c
    go :: forall (bs :: [k]) (b :: k) (c :: k).
Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go Index bs a
i f a
x Index (b : bs) c
j = case forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal (forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS Index bs a
i) Index (b : bs) c
j of
      Just a :~: c
Refl -> forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall a. a -> Maybe a
Just f a
x)
      Maybe (a :~: c)
Nothing  ->  forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose  forall a. Maybe a
Nothing

-- | If we have @'Index' as a@, we should also be able to create an item
-- that would require @'RElem' a as ('V.RIndex' as a)@.  Along with
-- 'rElemIndex', this essentially converts between the indexing system in
-- this library and the indexing system of /vinyl/.
indexRElem
    :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as)
    => Index as a
    -> (RElem a as (V.RIndex a as) => r)
    -> r
indexRElem :: forall k (a :: k) (as :: [k]) r.
(SDecide k, SingI a, RecApplicative as, FoldRec as as) =>
Index as a -> (RElem a as (RIndex a as) => r) -> r
indexRElem Index as a
i = case forall k (as :: [k]) (a :: k) (f :: k -> *).
(RecApplicative as, FoldRec as as) =>
Index as a -> f a -> CoRec f as
toCoRec Index as a
i Sing a
x of
    CoRec Sing a1
y -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
      Proved a :~: a1
Refl -> forall a. a -> a
id
      Disproved Refuted (a :~: a1)
_ -> \RElem a as (RIndex a as) => r
_ -> forall a. String -> a
errorWithoutStackTrace String
"why :|"
  where
    x :: Sing a
x = forall {k} (a :: k). SingI a => Sing a
sing