{-# 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.Functor.Classes
import           Data.Functor.Identity
import           Data.Kind
import           Data.List.NonEmpty                      (NonEmpty(..))
import           Data.Maybe
import           Data.Semigroup
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Singletons.Prelude hiding          (Elem, ElemSym0, ElemSym1, ElemSym2)
import           Data.Singletons.Prelude.Foldable hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
import           Data.Singletons.Prelude.Identity
import           Data.Vinyl hiding                       ((:~:))
import           Data.Vinyl.CoRec
import           GHC.Generics                            ((:*:)(..))
import           Lens.Micro hiding                       ((%~))
import           Lens.Micro.Extras
import           Unsafe.Coerce
import qualified Data.Singletons.Prelude.List.NonEmpty   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 :: Fmap IdSym0 as :~: as
fmapIdent = (Any :~: Any) -> Fmap IdSym0 as :~: as
forall a b. a -> b
unsafeCoerce Any :~: Any
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 Fmap IdSym0 as :~: as
forall (f0 :: * -> *) b0 (as :: f0 b0). Fmap IdSym0 as :~: as
fmapIdent @as of
      Refl -> Sing IdSym0
-> (forall (a :: k). g a -> m (h (IdSym0 @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap IdSym0 as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
       (g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse (SingI IdSym0 => Sing IdSym0
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 f :: forall (a :: k). g a -> h a -> j a
f xs :: Prod f g as
xs ys :: Prod f h as
ys = (forall (a :: k). Elem f as a -> g a -> j a)
-> Prod f g as -> Prod f j as
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 (\i :: Elem f as a
i x :: g a
x -> g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x (Elem f as a -> Prod f h as -> h a
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 :: Shape f as
pureShape = (forall (a :: k). Proxy a) -> Shape f as
forall k (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall (a :: k). Proxy a
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 :: Prod f (Elem f as) as
indices = (forall (a :: k). Elem f as a -> Proxy a -> Elem f as a)
-> Prod f Proxy as -> Prod f (Elem f as) as
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 -> Proxy a -> Elem f as a
forall a b. a -> b -> a
const Prod f Proxy as
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 :: Sing as -> Shape f as
singShape = (forall (a :: k). Sing a -> Proxy a)
-> Prod f Sing as -> Shape f as
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 (Proxy a -> Sing a -> Proxy a
forall a b. a -> b -> a
const Proxy a
forall k (t :: k). Proxy t
Proxy) (Prod f Sing as -> Shape f as)
-> (Sing as -> Prod f Sing as) -> Sing as -> Shape f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
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 (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd f :: forall (a :: k). g a -> h a
f = Identity (Prod f h as) -> Prod f h as
forall a. Identity a -> a
runIdentity (Identity (Prod f h as) -> Prod f h as)
-> (Prod f g as -> Identity (Prod f h as))
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). g a -> Identity (h a))
-> Prod f g as -> Identity (Prod f h as)
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 (h a -> Identity (h a)
forall a. a -> Identity a
Identity (h a -> Identity (h a)) -> (g a -> h a) -> g a -> Identity (h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h a
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 :: Prod f g as -> Prod f h as -> Prod f (g :*: h) as
zipProd = (forall (a :: k). g a -> h a -> (:*:) g h a)
-> Prod f g as -> Prod f h as -> Prod f (g :*: h) as
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 -> (:*:) g h a
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 :: Sing ff
-> (forall (a :: a0). g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap ff :: Sing ff
ff f :: forall (a :: a0). g a -> h (ff @@ a)
f = Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as)
forall a. Identity a -> a
runIdentity (Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as))
-> (Prod f g as -> Identity (Prod f h (Fmap ff as)))
-> Prod f g as
-> Prod f h (Fmap ff as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing ff
-> (forall (a :: a0). g a -> Identity (h (ff @@ a)))
-> Prod f g as
-> Identity (Prod f h (Fmap ff as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
       (g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff (h (Apply ff a) -> Identity (h (Apply ff a))
forall a. a -> Identity a
Identity (h (Apply ff a) -> Identity (h (Apply ff a)))
-> (g a -> h (Apply ff a)) -> g a -> Identity (h (Apply ff a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h (Apply ff a)
forall (a :: a0). 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 (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd f :: forall (a :: k). Elem f as a -> g a -> h a
f = (forall (a :: k). (:*:) (Elem f as) g a -> h a)
-> Prod f (Elem f as :*: g) as -> Prod f h as
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 (\(i :*: x) -> Elem f as a -> g a -> h a
forall (a :: k). Elem f as a -> g a -> h a
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> Prod f h as)
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
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 :: Elem f as a -> Sing as -> Sing a
indexSing i :: Elem f as a
i = Elem f as a -> Prod f Sing as -> Sing a
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 Sing as -> Sing a)
-> (Sing as -> Prod f Sing as) -> Sing as -> Sing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
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 :: Elem f as a -> Prod f g as -> g a
indexProd i :: Elem f as a
i = Getting (g a) (Prod f g as) (g a) -> Prod f g as -> g a
forall a s. Getting a s a -> s -> a
view (Elem f as a -> Lens' (Prod f g as) (g a)
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 (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd f :: forall (a :: k). Elem f as a -> g a -> m (h a)
f = (forall (a :: k). (:*:) (Elem f as) g a -> m (h a))
-> Prod f (Elem f as :*: g) as -> m (Prod f h as)
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 (\(i :*: x) -> Elem f as a -> g a -> m (h a)
forall (a :: k). Elem f as a -> g a -> m (h a)
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> m (Prod f h as))
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> m (Prod f h as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
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 (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd f :: forall (a :: k). Elem f as a -> g a -> m
f = Const m (Prod f Any as) -> m
forall a k (b :: k). Const a b -> a
getConst (Const m (Prod f Any as) -> m)
-> (Prod f g as -> Const m (Prod f Any as)) -> Prod f g as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Elem f as a -> g a -> Const m (Any a))
-> Prod f g as -> Const m (Prod f Any as)
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 (\i :: Elem f as a
i -> m -> Const m (Any a)
forall k a (b :: k). a -> Const a b
Const (m -> Const m (Any a)) -> (g a -> m) -> g a -> Const m (Any a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> g a -> m
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 (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd f :: forall (a :: k). g a -> m
f = (forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
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 ((g a -> m) -> Elem f as a -> g a -> m
forall a b. a -> b -> a
const g a -> m
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 (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing f :: forall (a :: k). Elem f as a -> Sing a -> m
f = (forall (a :: k). Elem f as a -> Sing a -> m)
-> Prod f Sing as -> m
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 (Prod f Sing as -> m)
-> (Sing as -> Prod f Sing as) -> Sing as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
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 (a :: k). Sing a -> m) -> Sing as -> m
foldMapSing f :: forall (a :: k). Sing a -> m
f = (forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
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 ((Sing a -> m) -> Elem f as a -> Sing a -> m
forall a b. a -> b -> a
const Sing a -> m
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 :: Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs
selectProd is :: Prod f (Elem f as) bs
is xs :: Prod f g as
xs = (forall (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) bs -> Prod f g bs
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 -> Prod f g as -> g a
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 :: Prod f g as -> Prod f g as -> Bool
eqProd xs :: Prod f g as
xs = All -> Bool
getAll
          (All -> Bool) -> (Prod f g as -> All) -> Prod f g as -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Const All a -> All)
-> Prod f (Const All) as -> All
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). Const All a -> All
forall a k (b :: k). Const a b -> a
getConst
          (Prod f (Const All) as -> All)
-> (Prod f g as -> Prod f (Const All) as) -> Prod f g as -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Eq) g a -> g a -> Const All a)
-> Prod f (Dict Eq :. g) as -> Prod f g as -> Prod f (Const All) as
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 x)) y :: g a
y -> All -> Const All a
forall k a (b :: k). a -> Const a b
Const (Bool -> All
All (g a
x g a -> g a -> Bool
forall a. Eq a => a -> a -> Bool
== g a
y)))
                (Prod f g as -> Prod f (Dict Eq :. g) as
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 :: Prod f g as -> Prod f g as -> Ordering
compareProd xs :: Prod f g as
xs = (forall (a :: k). Const Ordering a -> Ordering)
-> Prod f (Const Ordering) as -> Ordering
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). Const Ordering a -> Ordering
forall a k (b :: k). Const a b -> a
getConst
            (Prod f (Const Ordering) as -> Ordering)
-> (Prod f g as -> Prod f (Const Ordering) as)
-> Prod f g as
-> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Ord) g a -> g a -> Const Ordering a)
-> Prod f (Dict Ord :. g) as
-> Prod f g as
-> Prod f (Const Ordering) as
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 x)) y :: g a
y -> Ordering -> Const Ordering a
forall k a (b :: k). a -> Const a b
Const (g a -> g a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y))
                  (Prod f g as -> Prod f (Dict Ord :. g) as
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 (a :: k). Elem f as a -> g a) -> Prod f g as
generateProd f :: forall (a :: k). Elem f as a -> g a
f = (forall (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) as -> Prod f g as
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 Prod f (Elem f as) as
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 (a :: k). Elem f as a -> m (g a)) -> m (Prod f g as)
generateProdA f :: forall (a :: k). Elem f as a -> m (g a)
f = (forall (a :: k). Elem f as a -> m (g a))
-> Prod f (Elem f as) as -> m (Prod f g as)
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 Prod f (Elem f as) as
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 a :: 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 = Sing 'IZ
forall k (a :: k) (as :: [k]). SIndex (a : as) a 'IZ
SIZ

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

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

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

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

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

    prodSing :: Prod [] Sing as -> Sing as
prodSing = \case
      RNil    -> Sing as
forall a0. SList '[]
SNil
      x :& xs -> Sing r
x Sing r -> Sing rs -> SList (r : rs)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` Prod [] Sing rs -> Sing rs
forall (f :: * -> *) k (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing rs
Prod [] 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 (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f = Prod [] g as -> m (Prod [] h as)
forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go
      where
        go :: Prod [] g bs -> m (Prod [] h bs)
        go :: Prod [] g bs -> m (Prod [] h bs)
go = \case
          RNil    -> Rec h '[] -> m (Rec h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall u (a :: u -> *). Rec a '[]
RNil
          x :& xs -> h r -> Rec h rs -> Rec h (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h r -> Rec h rs -> Rec h (r : rs))
-> m (h r) -> m (Rec h rs -> Rec h (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h r)
forall (a :: k). g a -> m (h a)
f g r
x m (Rec h rs -> Rec h (r : rs))
-> m (Rec h rs) -> m (Rec h (r : rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h rs)
forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go Rec g rs
Prod [] 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 (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f = Prod [] g as -> Prod [] h as -> Prod [] j as
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 :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go = \case
          RNil -> \case
            RNil -> Prod [] j bs
forall u (a :: u -> *). Rec a '[]
RNil
          x :& xs -> \case
            y :& ys -> g r -> h r -> j r
forall (a :: k). g a -> h a -> j a
f g r
x h r
h r
y j r -> Rec j rs -> Rec j (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Prod [] g rs -> Prod [] h rs -> Prod [] j rs
forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go Rec g rs
Prod [] g rs
xs Rec h rs
Prod [] 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 :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f = Prod [] g as -> m (Prod [] h (Fmap ff as))
forall (bs :: [a0]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go
      where
        go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
        go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go = \case
          RNil    -> Rec h '[] -> m (Rec h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall u (a :: u -> *). Rec a '[]
RNil
          x :& xs -> h (Apply ff r)
-> Rec h (Fmap_6989586621680022960 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h (Apply ff r)
 -> Rec h (Fmap_6989586621680022960 ff rs)
 -> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
-> m (h (Apply ff r))
-> m (Rec h (Fmap_6989586621680022960 ff rs)
      -> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h (Apply ff r))
forall (a :: a0). g a -> m (h (ff @@ a))
f g r
x m (Rec h (Fmap_6989586621680022960 ff rs)
   -> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
-> m (Rec h (Fmap_6989586621680022960 ff rs))
-> m (Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h (Fmap ff rs))
forall (bs :: [a0]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
Prod [] g rs
xs

    withIndices :: Prod [] g as -> Prod [] (Elem [] as :*: g) as
withIndices = \case
        RNil    -> Prod [] (Elem [] as :*: g) as
forall u (a :: u -> *). Rec a '[]
RNil
        x :& xs -> (Index (r : rs) r
forall k (a :: k) (as :: [k]). Index (a : as) a
IZ Index (r : rs) r -> g r -> (:*:) (Index (r : rs)) g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
x) (:*:) (Index (r : rs)) g r
-> Rec (Index (r : rs) :*: g) rs
-> Rec (Index (r : rs) :*: g) (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (a :: k).
 (:*:) (Index rs) g a -> (:*:) (Index (r : rs)) g a)
-> Prod [] (Index rs :*: g) rs -> Prod [] (Index (r : rs) :*: g) 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 (\(i :*: y) -> Index rs a -> Index (r : rs) a
forall k (bs :: [k]) (a :: k) (b :: k).
Index bs a -> Index (b : bs) a
IS Index rs a
i Index (r : rs) a -> g a -> (:*:) (Index (r : rs)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g rs -> Prod [] (Elem [] rs :*: g) rs
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
Prod [] g rs
xs)

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

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

    withPureProd :: Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = Prod [] g as -> (PureProd [] as => r) -> r
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 :: Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList = \case
    RNil    -> ((RecApplicative as, PureProd [] as) => r) -> r
forall a. a -> a
id
    _ :& xs :: Rec f rs
xs -> Rec f rs -> ((RecApplicative rs, PureProd [] rs) => r) -> r
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 (a :: k). g a) -> Prod [] g as
pureProd = (forall (a :: k). g a) -> Prod [] g as
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 (a :: k). c a => g a) -> Prod [] g as
pureProdC = forall (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *).
RPureConstrained c ts =>
(forall (a :: u). 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
forall (f :: k -> *) (rs :: [k]).
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 a :: 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 = Sing 'IJust
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 :: Sing a -> Demote (IJust as a)
fromSing SIJust = Demote (IJust as a)
forall k (a :: k). IJust ('Just a) a
IJust
    toSing :: Demote (IJust as a) -> SomeSing (IJust as a)
toSing IJust = Sing 'IJust -> SomeSing (IJust as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IJust
forall k (a :: k). SIJust ('Just a) a 'IJust
SIJust

instance SDecide (IJust as a) where
    SIJust %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIJust = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
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 d :: Int
d xs :: PMaybe f as
xs = case Prod Maybe f as -> Prod Maybe (Dict Show :. f) as
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
Prod Maybe f as
xs of
      PNothing                   -> String -> ShowS
showString "PNothing"
      PJust (V.Compose (Dict x)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec "PJust" Int
d f a
x
instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
    == :: PMaybe f as -> PMaybe f as -> Bool
(==) = 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 = PMaybe f as -> PMaybe f as -> Ordering
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 :: Sing as -> Prod Maybe Sing as
singProd = \case
      SNothing -> Prod Maybe Sing as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
      SJust x  -> Sing n -> PMaybe Sing ('Just n)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust Sing n
x
    prodSing :: Prod Maybe Sing as -> Sing as
prodSing = \case
      PNothing -> Sing as
forall a0. SMaybe 'Nothing
SNothing
      PJust x  -> Sing a -> SMaybe ('Just a)
forall a0 (n :: a0). Sing n -> SMaybe ('Just n)
SJust Sing a
x
    withIndices :: Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as
withIndices = \case
      PNothing -> Prod Maybe (Elem Maybe as :*: g) as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust x  -> (:*:) (IJust ('Just a)) g a
-> PMaybe (IJust ('Just a) :*: g) ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (IJust ('Just a) a
forall k (a :: k). IJust ('Just a) a
IJust IJust ('Just a) a -> g a -> (:*:) (IJust ('Just a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod Maybe g as -> m (Prod Maybe h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f = \case
      PNothing -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust x  -> h a -> PMaybe h ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (h a -> PMaybe h ('Just a)) -> m (h a) -> m (PMaybe h ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f = \case
      PNothing -> \case
        PNothing -> Prod Maybe j as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust x -> \case
        PJust y -> j a -> PMaybe j ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
    htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod Maybe g as
-> m (Prod Maybe h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f = \case
      PNothing -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
      PJust x  -> h (Apply ff a) -> PMaybe h ('Just (Apply ff a))
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (h (Apply ff a) -> PMaybe h ('Just (Apply ff a)))
-> m (h (Apply ff a)) -> m (PMaybe h ('Just (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: Elem Maybe as a -> Lens' (Prod Maybe g as) (g a)
ixProd = \case
      IJust -> \f :: g a -> f (g a)
f -> \case
        PJust x -> g a -> PMaybe g ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (g a -> PMaybe g ('Just a)) -> f (g a) -> f (PMaybe g ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
    toRec :: Prod Maybe g as -> Rec g (ToList as)
toRec = \case
      PNothing -> Rec g (ToList as)
forall u (a :: u -> *). Rec a '[]
RNil
      PJust x  -> g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
    withPureProd :: Prod Maybe g as -> (PureProd Maybe as => r) -> r
withPureProd = \case
      PNothing -> (PureProd Maybe as => r) -> r
forall a. a -> a
id
      PJust _  -> (PureProd Maybe as => r) -> r
forall a. a -> a
id

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

instance PureProdC Maybe c 'Nothing where
    pureProdC :: (forall (a :: k). c a => g a) -> Prod Maybe g 'Nothing
pureProdC _ = Prod Maybe g 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c a => PureProdC Maybe c ('Just a) where
    pureProdC :: (forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
pureProdC x :: forall (a :: a). c a => g a
x = g a -> PMaybe g ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust g a
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 PNothing = Prod Maybe (Dict c :. g) 'Nothing
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 x) = Compose (Dict c) g a -> PMaybe (Dict c :. g) ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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 a :: 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 = Sing 'IRight
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 :: Sing a -> Demote (IRight as a)
fromSing SIRight = Demote (IRight as a)
forall k j (a :: k). IRight ('Right a) a
IRight
    toSing :: Demote (IRight as a) -> SomeSing (IRight as a)
toSing IRight = Sing 'IRight -> SomeSing (IRight as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IRight
forall k j (a :: k). SIRight ('Right a) a 'IRight
SIRight

instance SDecide (IRight as a) where
    SIRight %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIRight = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
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 d :: Int
d xs :: PEither f as
xs = case Prod (Either j) f as -> Prod (Either j) (Dict Show :. f) as
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
Prod (Either j) f as
xs of
        PLeft e                     -> (Int -> Sing e -> ShowS) -> String -> Int -> Sing e -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> Sing e -> ShowS
forall a a (t2 :: a).
(Integral a, SShow a) =>
a -> Sing t2 -> ShowS
go         "PLeft" Int
d Sing e
e
        PRight (V.Compose (Dict x)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec "PRight" Int
d f a
x
      where
        go :: a -> Sing t2 -> ShowS
go (a -> Demote Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral->FromSing i) x :: Sing t2
x (String -> Text
T.pack->FromSing str) = Text -> String
T.unpack (Text -> String)
-> (SSymbol (ShowsPrec a t2 a) -> Text)
-> SSymbol (ShowsPrec a t2 a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SSymbol (ShowsPrec a t2 a) -> Text
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SSymbol (ShowsPrec a t2 a) -> String)
-> SSymbol (ShowsPrec a t2 a) -> String
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing t2
-> Sing a
-> Sing (Apply (Apply (Apply ShowsPrecSym0 a) t2) a)
forall a (t1 :: Nat) (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
        go _ _ _ = String
forall a. HasCallStack => a
undefined

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

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

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

instance SingI e => PureProdC (Either j) c ('Left e) where
    pureProdC :: (forall (a :: k). c a => g a) -> Prod (Either j) g ('Left e)
pureProdC _ = (Sing e -> PEither g ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
forall k (a :: k). SingI a => Sing a
sing)
instance c a => PureProdC (Either j) c ('Right a) where
    pureProdC :: (forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
pureProdC x :: forall (a :: b). c a => g a
x = g a -> PEither g ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight g a
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 e) = Sing e -> PEither (Dict c :. g) ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
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 x) = Compose (Dict c) g a -> PEither (Dict c :. g) ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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 a :: 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 = Sing 'NEHead
forall k (a :: k) (as :: [k]). SNEIndex (a ':| as) a 'NEHead
SNEHead

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

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

instance SDecide (NEIndex as a) where
    %~ :: Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
      SNEHead -> \case
        SNEHead   -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
        SNETail _ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
      SNETail i -> \case
        SNEHead -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
        SNETail j -> case Sing i
SIndex as a i
i Sing i -> Sing i -> Decision (i :~: i)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex as a i
j of
          Proved Refl -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
          Disproved v :: Refuted (i :~: i)
v -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case Refl -> Refuted (i :~: i)
v i :~: i
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 :: Sing as -> Prod NonEmpty Sing as
singProd (x NE.:%| xs) = Sing n1
x Sing n1 -> Rec Sing n2 -> NERec Sing (n1 ':| n2)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Sing n2 -> Prod [] Sing n2
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
    prodSing :: Prod NonEmpty Sing as -> Sing as
prodSing (x :&| xs) = Sing a
x Sing a -> Sing as -> SNonEmpty (a ':| as)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| Prod [] Sing as -> Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing as
Prod [] Sing as
xs
    withIndices :: Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as
withIndices (x :&| xs) =
          (NEIndex (a ':| as) a
forall k (a :: k) (as :: [k]). NEIndex (a ':| as) a
NEHead NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
      (:*:) (NEIndex (a ':| as)) g a
-> Rec (NEIndex (a ':| as) :*: g) as
-> NERec (NEIndex (a ':| as) :*: g) (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k).
 (:*:) (Index as) g a -> (:*:) (NEIndex (a ':| as)) g a)
-> Prod [] (Index as :*: g) as
-> Prod [] (NEIndex (a ':| as) :*: g) as
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 (\(i :*: y) -> Index as a -> NEIndex (a ':| as) a
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> NEIndex (b ':| as) a
NETail Index as a
i NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g as -> Prod [] (Elem [] as :*: g) as
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
Prod [] g as
xs)
    traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod NonEmpty g as -> m (Prod NonEmpty h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (x :&| xs) =
        h a -> Rec h as -> NERec h (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
(:&|) (h a -> Rec h as -> NERec h (a ':| as))
-> m (h a) -> m (Rec h as -> NERec h (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x m (Rec h as -> NERec h (a ':| as))
-> m (Rec h as) -> m (NERec h (a ':| as))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
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
Prod [] g as
xs
    zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (x :&| xs) (y :&| ys) = g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y j a -> Rec j as -> NERec j (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
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
Prod [] g as
xs Rec h as
Prod [] h as
ys
    htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod NonEmpty g as
-> m (Prod NonEmpty h (Fmap ff as))
htraverse ff :: Sing ff
ff f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (x :&| xs) =
        h (Apply ff a)
-> Rec h (Fmap_6989586621680022960 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
(:&|) (h (Apply ff a)
 -> Rec h (Fmap_6989586621680022960 ff as)
 -> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
-> m (h (Apply ff a))
-> m (Rec h (Fmap_6989586621680022960 ff as)
      -> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x m (Rec h (Fmap_6989586621680022960 ff as)
   -> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
-> m (Rec h (Fmap_6989586621680022960 ff as))
-> m (NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
       (g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a0). g a -> m (h (ff @@ a))
f Rec g as
Prod [] g as
xs
    ixProd :: Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a)
ixProd = \case
      NEHead -> \f :: g a -> f (g a)
f -> \case
        x :&| xs -> (g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Rec g as
xs) (g a -> NERec g (a ':| as)) -> f (g a) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
      NETail i -> \f :: g a -> f (g a)
f -> \case
        x :&| xs -> (g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&|) (Rec g as -> NERec g (a ':| as))
-> f (Rec g as) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem [] as a
-> (g a -> f (g a)) -> Prod [] g as -> f (Prod [] g as)
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
Elem [] as a
i g a -> f (g a)
f Rec g as
Prod [] g as
xs
    toRec :: Prod NonEmpty g as -> Rec g (ToList as)
toRec (x :&| xs) = g a
x g a -> Rec g as -> Rec g (a : as)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g as
xs
    withPureProd :: Prod NonEmpty g as -> (PureProd NonEmpty as => r) -> r
withPureProd (x :&| xs) = g a
-> Rec g as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
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 :: f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE _ xs :: Rec f as
xs = Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
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 (a :: k). g a) -> Prod NonEmpty g (a ':| as)
pureProd x :: forall (a :: k). g a
x = g a
forall (a :: k). g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k). g a) -> Prod [] g as
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 (a :: a). c a => g a) -> Prod NonEmpty g (a ':| as)
pureProdC x :: forall (a :: a). c a => g a
x = g a
forall (a :: a). c a => g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: a). c a => g a) -> Prod [] g as
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 (x :&| xs) = Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
                                 Compose (Dict c) g a
-> Rec (Dict c :. g) as -> NERec (Dict c :. g) (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Prod [] g as -> Prod [] (Dict c :. g) as
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
Prod [] 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 :: Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal = \case
    IZ -> \case
      IZ   -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
      IS _ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
    IS i :: Index bs a
i -> \case
      IZ   -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      IS j :: Index bs b
j -> Index bs a -> Index bs b -> Maybe (a :~: b)
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
Index bs b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case Refl -> a :~: b
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 :: NEIndex as a -> NEIndex as b -> Maybe (a :~: b)
sameNEIndexVal = \case
    NEHead -> \case
      NEHead   -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
      NETail _ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
    NETail i :: Index as a
i -> \case
      NEHead   -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      NETail j :: Index as b
j -> Index as a -> Index as b -> Maybe (a :~: b)
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
Index as b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case Refl -> a :~: b
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 a :: 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 = Sing 'ISnd
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 :: Sing a -> Demote (ISnd as a)
fromSing SISnd = Demote (ISnd as a)
forall j k (a :: j) (b :: k). ISnd '(a, b) b
ISnd
    toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)
toSing ISnd = Sing 'ISnd -> SomeSing (ISnd as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'ISnd
forall j k (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd

instance SDecide (ISnd as a) where
    SISnd %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SISnd = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
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 :: Sing as -> Prod ((,) j) Sing as
singProd (STuple2 w x) = Sing n1 -> Sing n2 -> PTup Sing '(n1, n2)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing n1
w Sing n2
x
    prodSing :: Prod ((,) j) Sing as -> Sing as
prodSing (PTup w x) = Sing w -> Sing a -> STuple2 '(w, a)
forall a0 b0 (n1 :: a0) (n2 :: b0).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing w
w Sing a
x
    withIndices :: Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as
withIndices (PTup w x) = Sing w
-> (:*:) (ISnd '(w, a)) g a -> PTup (ISnd '(w, a) :*: g) '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (ISnd '(w, a) a
forall j k (a :: j) (b :: k). ISnd '(a, b) b
ISnd ISnd '(w, a) a -> g a -> (:*:) (ISnd '(w, a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod ((,) j) g as -> m (Prod ((,) j) h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (PTup w x) = Sing w -> h a -> PTup h '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (h a -> PTup h '(w, a)) -> m (h a) -> m (PTup h '(w, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (PTup w x) (PTup _ y) = Sing w -> j a -> PTup j '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
    htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod ((,) j) g as
-> m (Prod ((,) j) h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (PTup w x) = Sing w -> h (Apply ff a) -> PTup h '(w, Apply ff a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (h (Apply ff a) -> PTup h '(w, Apply ff a))
-> m (h (Apply ff a)) -> m (PTup h '(w, Apply ff a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a)
ixProd ISnd f :: g a -> f (g a)
f (PTup w x) = Sing a -> g a -> PTup g '(a, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing a
Sing w
w (g a -> PTup g '(a, a)) -> f (g a) -> f (PTup g '(a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
    toRec :: Prod ((,) j) g as -> Rec g (ToList as)
toRec (PTup _ x) = g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
    withPureProd :: Prod ((,) j) g as -> (PureProd ((,) j) as => r) -> r
withPureProd (PTup Sing _) x :: PureProd ((,) j) as => r
x = r
PureProd ((,) j) as => r
x

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

instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
    pureProdC :: (forall (a :: k). c a => g a) -> Prod ((,) j) g '(w, a)
pureProdC x :: forall (a :: k). c a => g a
x = Sing w -> g a -> PTup g '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
forall k (a :: k). SingI a => Sing a
sing g a
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 w x) = Sing w -> Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
Sing w
w (Compose (Dict c) g a -> Prod ((,) j) (Dict c :. g) '(w, a))
-> Compose (Dict c) g a -> Prod ((,) j) (Dict c :. g) '(w, a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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 a :: 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 = Sing 'IId
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 :: Sing a -> Demote (IIdentity as a)
fromSing SIId = Demote (IIdentity as a)
forall k (x :: k). IIdentity ('Identity x) x
IId
    toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)
toSing IId = Sing 'IId -> SomeSing (IIdentity as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IId
forall k (a :: k). SIIdentity ('Identity a) a 'IId
SIId

instance SDecide (IIdentity as a) where
    SIId %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIId = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
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 :: Sing as -> Prod Identity Sing as
singProd (SIdentity x) = Sing n -> PIdentity Sing ('Identity n)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity Sing n
x
    prodSing :: Prod Identity Sing as -> Sing as
prodSing (PIdentity x) = Sing a -> SIdentity ('Identity a)
forall a0 (n :: a0). Sing n -> SIdentity ('Identity n)
SIdentity Sing a
x
    withIndices :: Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as
withIndices (PIdentity x) = (:*:) (IIdentity ('Identity a)) g a
-> PIdentity (IIdentity ('Identity a) :*: g) ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (IIdentity ('Identity a) a
forall k (x :: k). IIdentity ('Identity x) x
IId IIdentity ('Identity a) a
-> g a -> (:*:) (IIdentity ('Identity a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
    traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod Identity g as -> m (Prod Identity h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (PIdentity x) = h a -> PIdentity h ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (h a -> PIdentity h ('Identity a))
-> m (h a) -> m (PIdentity h ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
    zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod Identity g as -> Prod Identity h as -> Prod Identity j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (PIdentity x) (PIdentity y) = j a -> PIdentity j ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
    htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod Identity g as
-> m (Prod Identity h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (PIdentity x) = h (Apply ff a) -> PIdentity h ('Identity (Apply ff a))
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (h (Apply ff a) -> PIdentity h ('Identity (Apply ff a)))
-> m (h (Apply ff a)) -> m (PIdentity h ('Identity (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
    ixProd :: Elem Identity as a -> Lens' (Prod Identity g as) (g a)
ixProd IId f :: g a -> f (g a)
f (PIdentity x) = g a -> PIdentity g ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (g a -> PIdentity g ('Identity a))
-> f (g a) -> f (PIdentity g ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
    toRec :: Prod Identity g as -> Rec g (ToList as)
toRec (PIdentity x) = g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
    withPureProd :: Prod Identity g as -> (PureProd Identity as => r) -> r
withPureProd (PIdentity _) x :: PureProd Identity as => r
x = r
PureProd Identity as => r
x

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

instance c a => PureProdC Identity c ('Identity a) where
    pureProdC :: (forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
pureProdC x :: forall (a :: a). c a => g a
x = g a -> PIdentity g ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity g a
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 x) = Compose (Dict c) g a -> Prod Identity (Dict c :. g) ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (Compose (Dict c) g a -> Prod Identity (Dict c :. g) ('Identity a))
-> Compose (Dict c) g a
-> Prod Identity (Dict c :. g) ('Identity a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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 :: Index rs r
rElemIndex = Rec (Index rs) rs -> Index rs r
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 Rec (Index rs) rs
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 as a f. (RecApplicative as, FoldRec as as)
    => Index as a
    -> f a
    -> CoRec f as
toCoRec :: Index as a -> f a -> CoRec f as
toCoRec = \case
    IZ   -> f a -> CoRec f as
forall k (a1 :: k) (b :: [k]) (a :: k -> *).
RElem a1 b (RIndex a1 b) =>
a a1 -> CoRec a b
CoRec
    IS i :: Index bs a
i -> \x :: f a
x -> Maybe (CoRec f as) -> CoRec f as
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CoRec f as) -> CoRec f as)
-> (Rec (Maybe :. f) as -> Maybe (CoRec f as))
-> Rec (Maybe :. f) as
-> CoRec f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. f) as -> Maybe (CoRec f as)
forall k (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField (Rec (Maybe :. f) as -> CoRec f as)
-> Rec (Maybe :. f) as -> CoRec f as
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Index (b : bs) a -> (:.) Maybe f a)
-> Prod [] (Index (b : bs)) (b : bs)
-> Prod [] (Maybe :. f) (b : bs)
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 bs a -> f a -> Index (b : bs) a -> Compose Maybe f a
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) Prod [] (Index (b : bs)) (b : bs)
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 :: Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go i :: Index bs a
i x :: f a
x j :: Index (b : bs) c
j = case Index (b : bs) a -> Index (b : bs) c -> Maybe (a :~: c)
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal (Index bs a -> Index (b : bs) a
forall k (bs :: [k]) (a :: k) (b :: k).
Index bs a -> Index (b : bs) a
IS Index bs a
i) Index (b : bs) c
j of
      Just Refl -> Maybe (f a) -> Compose Maybe f a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (f a -> Maybe (f a)
forall a. a -> Maybe a
Just f a
x)
      Nothing  ->  Maybe (f c) -> Compose Maybe f c
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose  Maybe (f c)
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 :: Index as a -> (RElem a as (RIndex a as) => r) -> r
indexRElem i :: Index as a
i = case Index as a -> Sing a -> CoRec Sing as
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 y :: Sing a1
y -> case Sing a
x Sing a -> Sing a1 -> Decision (a :~: a1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
      Proved Refl -> (RElem a as (RIndex a as) => r) -> r
forall a. a -> a
id
      Disproved _ -> String -> (RElem a as (RIndex a as) => r) -> r
forall a. String -> a
errorWithoutStackTrace "why :|"
  where
    x :: Sing a
x = Sing a
forall k (a :: k). SingI a => Sing a
sing