{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# 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 qualified Data.List.NonEmpty.Singletons as NE
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 qualified Data.Text as T
import Data.Tuple.Singletons
import Data.Vinyl hiding ((:~:))
import Data.Vinyl.CoRec
import qualified Data.Vinyl.Functor as V
import qualified Data.Vinyl.TypeLevel as V
import GHC.Generics ((:*:) (..))
import Lens.Micro hiding ((%~))
import Lens.Micro.Extras
import Text.Show.Singletons
import Unsafe.Coerce

fmapIdent :: Fmap IdSym0 as :~: as
fmapIdent :: forall {f :: * -> *} {b} (as :: f b). 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 forall (as :: f k). Fmap IdSym0 as :~: as
forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent @as of
    Fmap IdSym0 as :~: as
Refl -> Sing IdSym0
-> (forall (a :: k). g a -> m (h (IdSym0 @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap IdSym0 as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: f a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
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
forall (a :: TyFun k 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 (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 (\Elem f as a
i 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 :: forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape = (forall (a :: k). Proxy a) -> Prod f Proxy as
forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
forall (g :: k -> *). (forall (a :: k). g a) -> Prod f g as
pureProd Proxy a
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 :: forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
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 Elem f as a -> Proxy a -> Elem f as a
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 :: forall {k} (f :: * -> *) (as :: f k).
FProd f =>
Sing as -> Shape f as
singShape = (forall (a :: k). Sing a -> Proxy a)
-> Prod f Sing as -> Prod f Proxy 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 -> Prod f Proxy as)
-> (Sing as -> Prod f Sing as) -> Sing as -> Prod f Proxy as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). 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 {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 = 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 {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f 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 (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 :: 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 (a :: k). g a -> h a -> (:*:) g h a)
-> Prod f g as -> Prod f h as -> Prod f (g :*: h) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f 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 g a -> h a -> (:*:) g h a
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 :: 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 = 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 :: a). g a -> Identity (h (ff @@ a)))
-> Prod f g as
-> Identity (Prod f h (Fmap ff as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: f a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
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 (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 :: 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 (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 (\(Elem f as a
i :*: g a
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 {k} (g :: k -> *) (as :: f k).
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 =>
  -- | Witness
  Elem f as a ->
  -- | Collection
  Sing as ->
  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 = 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 {k} (as :: f k). 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 :: 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 = 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 {k} (as :: f k) (a :: k) (g :: k -> *).
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 {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 (a :: k). (:*:) (Elem f as) g a -> m (h a))
-> Prod f (Elem f as :*: g) as -> m (Prod f h as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f 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 (\(Elem f as a
i :*: g a
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 {k} (g :: k -> *) (as :: f k).
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 {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 = Const m (Prod f Any as) -> m
forall {k} a (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 (\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 {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 (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 (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 (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 Elem f as a -> Sing a -> m
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 {k} (as :: f k). 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 (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 (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 :: 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 (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 :: 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
    (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 Const All a -> All
forall (a :: k). Const All a -> All
forall {k} a (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 {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f 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
      (\(V.Compose (Dict g a
x)) 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)))
      (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
forall (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 (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 Const Ordering a -> Ordering
forall (a :: k). Const Ordering a -> Ordering
forall {k} a (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 {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f 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
      (\(V.Compose (Dict g a
x)) 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))
      (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
forall (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 (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 Elem f as a -> g a
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 {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 (a :: k). Elem f as a -> m (g a))
-> Prod f (Elem f as) as -> m (Prod f g as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f 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 Elem f as a -> m (g a)
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 :: [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 = Sing 'IZ
SIndex (a : as) a 'IZ
forall {k} (a :: k) (a :: [k]). SIndex (a : a) 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} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS Sing i
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 :: forall (a :: Index as a). Sing a -> Demote (Index as a)
fromSing = \case
    Sing a
SIndex as a a
SIZ -> Demote (Index as a)
Index (a : as) a
forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ
    SIS SIndex bs a i
j -> Index bs a -> Index (b : bs) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS (Sing i -> Demote (Index bs a)
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Index bs a). Sing a -> Demote (Index bs a)
fromSing Sing i
SIndex bs a i
j)
  toSing :: Demote (Index as a) -> SomeSing (Index as a)
toSing 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 Sing i -> SomeSing (Index as a)
SIndex as a i -> SomeSing (Index as a)
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 :: 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 -> ((SIndex bs b 'IZ -> r) -> SIndex bs b 'IZ -> r
forall a b. (a -> b) -> a -> b
$ SIndex bs b 'IZ
SIndex (b : as) b 'IZ
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 -> 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)
SIndex bs b i -> SIndex (b : bs) b ('IS i)
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 -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      SIS SIndex bs a i
_ -> 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 SIndex bs a i
i' -> \case
      Sing b
SIndex (b : bs) a b
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 SIndex bs a i
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)
forall (a :: Index bs a) (b :: Index bs a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex bs a i
j' of
        Proved i :~: i
Refl -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
        Disproved 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 a :~: b
Refl -> Refuted (i :~: i)
v i :~: i
i :~: i
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 -> Rec Sing '[]
Prod [] Sing as
forall {u} (a :: u -> *). Rec a '[]
RNil
    Sing n1
x `SCons` Sing n2
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 {k} (as :: [k]). Sing as -> Prod [] Sing as
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 -> Sing as
SList '[]
forall a. SList '[]
SNil
    Sing r
x :& Rec Sing rs
xs -> Sing r
x Sing r -> Sing rs -> SList (r : rs)
forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` Prod [] Sing rs -> Sing rs
forall {k} (as :: [k]). Prod [] Sing as -> Sing as
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 {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 = 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 :: forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go = \case
        Rec g bs
Prod [] g bs
RNil -> Rec h '[] -> m (Rec h '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
        g r
x :& Rec g rs
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 a b. m (a -> b) -> m a -> m b
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 {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 = 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 :: 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 -> Rec j '[]
Prod [] j bs
forall {u} (a :: u -> *). Rec a '[]
RNil
        g r
x :& Rec g rs
xs -> \case
          h r
y :& Rec h rs
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 :: 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 = Prod [] g as -> m (Prod [] h (Fmap ff as))
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 -> Rec h '[] -> m (Rec h '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
        g r
x :& Rec g rs
xs -> h (Apply ff r)
-> Rec h (Fmap_6989586621679427133 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621679427133 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_6989586621679427133 ff rs)
 -> Rec h (Apply ff r : Fmap_6989586621679427133 ff rs))
-> m (h (Apply ff r))
-> m (Rec h (Fmap_6989586621679427133 ff rs)
      -> Rec h (Apply ff r : Fmap_6989586621679427133 ff rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h (Apply ff r))
forall (a :: a). g a -> m (h (ff @@ a))
f g r
x m (Rec h (Fmap_6989586621679427133 ff rs)
   -> Rec h (Apply ff r : Fmap_6989586621679427133 ff rs))
-> m (Rec h (Fmap_6989586621679427133 ff rs))
-> m (Rec h (Apply ff r : Fmap_6989586621679427133 ff rs))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h (Fmap ff rs))
forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
Prod [] 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 -> Rec (Index '[] :*: g) '[]
Prod [] (Elem [] as :*: g) as
forall {u} (a :: u -> *). Rec a '[]
RNil
    g r
x :& Rec g rs
xs -> (Index (r : rs) r
forall {k} (a :: k) (a :: [k]). Index (a : a) 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 (\(Index rs a
i :*: g a
y) -> Index rs a -> Index (r : rs) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) 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 {k} (g :: k -> *) (as :: [k]).
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 rs
Prod [] 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)) = 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 :: 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 -> (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 Index bs a
i -> \case
          g r
x :& Rec g rs
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 :: forall {a} (g :: a -> *) (as :: [a]).
Prod [] g as -> Rec g (ToList as)
toRec = Rec g as -> Rec g as
Prod [] g as -> Rec g (ToList as)
forall a. a -> a
id

  withPureProd :: forall {k} (g :: k -> *) (as :: [k]) r.
Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = Rec g as -> ((RecApplicative as, PureProd [] as) => r) -> r
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 :: forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList = \case
  Rec f as
RNil -> r -> r
((RecApplicative as, PureProd [] as) => r) -> r
forall a. a -> a
id
  f r
_ :& 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 (g :: k -> *). (forall (a :: k). g a) -> Prod [] g as
pureProd = (forall (x :: k). g x) -> Rec g as
(forall (x :: k). g x) -> Prod [] g as
forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
forall (f :: k -> *). (forall (x :: k). f x) -> Rec f as
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
forall (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
forall (c :: * -> Constraint) (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 :: 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 = Sing 'IJust
SIJust ('Just a) a '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 :: forall (a :: IJust as a). Sing a -> Demote (IJust as a)
fromSing Sing a
SIJust as a a
SIJust = Demote (IJust as a)
IJust ('Just a) a
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 = Sing 'IJust -> SomeSing (IJust as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IJust
SIJust ('Just a) a 'IJust
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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
forall (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
    PMaybe (Dict Show :. f) as
Prod Maybe (Dict Show :. f) as
PNothing -> String -> ShowS
showString String
"PNothing"
    PJust (V.Compose (Dict f a
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 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
(==) = PMaybe f as -> PMaybe f as -> Bool
Prod Maybe f as -> Prod Maybe 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
Prod Maybe f as -> Prod Maybe 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 Elem Maybe = IJust
  type Prod Maybe = PMaybe

  singProd :: forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
singProd = \case
    Sing as
SMaybe as
SNothing -> PMaybe Sing 'Nothing
Prod Maybe Sing as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
    SJust Sing n
x -> Sing n -> PMaybe Sing ('Just n)
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 -> Sing as
SMaybe 'Nothing
forall a. SMaybe 'Nothing
SNothing
    PJust Sing a
x -> Sing a -> SMaybe ('Just a)
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 -> PMaybe (IJust 'Nothing :*: g) 'Nothing
Prod Maybe (Elem Maybe as :*: g) as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
    PJust g a
x -> (:*:) (IJust ('Just a)) g a
-> PMaybe (IJust ('Just a) :*: g) ('Just a)
forall {k} (f :: k -> *) (a :: k). 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 {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 -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
    PJust g a
x -> h a -> PMaybe h ('Just a)
forall {k} (f :: k -> *) (a :: k). 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 {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 -> PMaybe j 'Nothing
Prod Maybe j as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
    PJust g a
x -> \case
      PJust h a
y -> j a -> PMaybe j ('Just a)
forall {k} (f :: k -> *) (a :: k). 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 :: 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 -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
    PJust g a
x -> h (Apply ff a) -> PMaybe h ('Just (Apply ff a))
forall {k} (f :: k -> *) (a :: k). 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 :: 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 -> g a -> PMaybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). 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 :: 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 -> Rec g '[]
Rec g (ToList as)
forall {u} (a :: u -> *). Rec a '[]
RNil
    PJust g a
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 :: 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 -> r -> r
(PureProd Maybe as => r) -> r
forall a. a -> a
id
    PJust g a
_ -> r -> r
(PureProd Maybe as => r) -> r
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
_ = PMaybe g 'Nothing
Prod Maybe g 'Nothing
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 = g a -> PMaybe g ('Just a)
(forall (a :: k). g a) -> Prod Maybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust

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
_ = PMaybe g 'Nothing
Prod Maybe g 'Nothing
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 = g a -> PMaybe g ('Just a)
(forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust

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 = PMaybe (Dict c :. g) 'Nothing
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 g a
x) = Compose (Dict c) g a -> PMaybe (Dict c :. g) ('Just a)
forall {k} (f :: k -> *) (a :: k). 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 :: 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 = Sing 'IRight
SIRight ('Right a) a '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 :: forall (a :: IRight as a). Sing a -> Demote (IRight as a)
fromSing Sing a
SIRight as a a
SIRight = Demote (IRight as a)
IRight ('Right a) a
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 = Sing 'IRight -> SomeSing (IRight as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IRight
SIRight ('Right a) a 'IRight
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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
forall (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 Sing e
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 String
"PLeft" Int
d Sing e
e
    PRight (V.Compose (Dict f a
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 String
"PRight" Int
d f a
x
    where
      go :: a -> Sing t2 -> ShowS
go (a -> Demote Natural
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 (Text -> String)
-> (Sing (ShowsPrec a t2 a) -> Text)
-> Sing (ShowsPrec a t2 a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing (ShowsPrec a t2 a) -> Demote Symbol
Sing (ShowsPrec a t2 a) -> Text
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing (Sing (ShowsPrec a t2 a) -> String)
-> Sing (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 (t1 :: Natural) (t2 :: a) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
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 Elem (Either j) = IRight
  type Prod (Either j) = PEither

  singProd :: forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
singProd = \case
    SLeft Sing n
e -> Sing n -> PEither Sing ('Left n)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing n
e
    SRight Sing n
x -> Sing n -> PEither Sing ('Right n)
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 -> Sing e -> SEither ('Left e)
forall a b (n :: a). Sing n -> SEither ('Left n)
SLeft Sing e
e
    PRight Sing a
x -> Sing a -> SEither ('Right a)
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 -> Sing e -> PEither (IRight ('Left e) :*: g) ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
    PRight g a
x -> (:*:) (IRight ('Right a)) g a
-> PEither (IRight ('Right a) :*: g) ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). 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 {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 -> PEither h ('Left e) -> m (PEither h ('Left e))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
    PRight g a
x -> h a -> PEither h ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). 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 {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
_ -> Sing e -> PEither j ('Left 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 -> j a -> PEither j ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). 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 :: 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 -> PEither h ('Left e) -> m (PEither h ('Left e))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
    PRight g a
x -> h (Apply ff a) -> PEither h ('Right (Apply ff a))
forall {k} {j} (f :: k -> *) (a :: k). 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 :: 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 -> g a -> PEither g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). 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 :: forall {a} (g :: a -> *) (as :: Either j a).
Prod (Either j) g as -> Rec g (ToList as)
toRec = \case
    PLeft Sing e
_ -> Rec g '[]
Rec g (ToList as)
forall {u} (a :: u -> *). Rec a '[]
RNil
    PRight g a
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 :: 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 -> r -> r
(PureProd (Either j) as => r) -> r
forall a. a -> a
id
    PRight g a
_ -> r -> r
(PureProd (Either j) as => r) -> r
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
_ = Sing e -> PEither g ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
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 = g a -> PEither g ('Right a)
(forall (a :: k). g a) -> Prod (Either j) g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight

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
_ = Sing e -> PEither g ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
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 = g a -> PEither g ('Right a)
(forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight

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) = Sing e -> PEither (Dict c :. g) ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
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 g a
x) = Compose (Dict c) g a -> PEither (Dict c :. g) ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). 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 :: 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 = Sing 'NEHead
SNEIndex (a ':| as) a 'NEHead
forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) 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} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail Sing i
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 :: forall (a :: NEIndex as a). Sing a -> Demote (NEIndex as a)
fromSing = \case
    Sing a
SNEIndex as a a
SNEHead -> Demote (NEIndex as a)
NEIndex (a ':| as) a
forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead
    SNETail SIndex as a i
i -> Index as a -> NEIndex (b ':| as) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail (Index as a -> NEIndex (b ':| as) a)
-> Index as a -> NEIndex (b ':| 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
forall (a :: Index as a). Sing a -> Demote (Index as a)
fromSing Sing i
SIndex as a i
i
  toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)
toSing = \case
    Demote (NEIndex as a)
NEIndex as a
NEHead -> Sing 'NEHead -> SomeSing (NEIndex as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'NEHead
SNEIndex (a ':| as) a 'NEHead
forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
    NETail Index as a
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
$ Sing ('NETail a) -> SomeSing (NEIndex as a)
SNEIndex (b ':| as) a ('NETail a) -> SomeSing (NEIndex as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SNEIndex (b ':| as) a ('NETail a) -> SomeSing (NEIndex as a))
-> (SIndex as a a -> SNEIndex (b ':| as) a ('NETail a))
-> SIndex as a a
-> SomeSing (NEIndex as a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIndex as a a -> SNEIndex (b ':| as) a ('NETail a)
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 -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      SNETail SIndex as a i
_ -> 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 SIndex as a i
i -> \case
      Sing b
SNEIndex (b ':| as) a b
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 SIndex as a i
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)
forall (a :: Index as a) (b :: Index as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex as a i
j of
        Proved i :~: i
Refl -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
        Disproved 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 a :~: b
Refl -> Refuted (i :~: i)
v i :~: i
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 Elem NonEmpty = NEIndex
  type 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 Sing n1 -> Rec Sing n2 -> NERec Sing (n1 ':| n2)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| Sing n2 -> Prod [] Sing n2
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
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 Sing a -> Sing as -> SNonEmpty (a ':| as)
forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| Prod [] Sing as -> Sing as
forall {k} (as :: [k]). 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 :: 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) =
    (NEIndex (a ':| as) a
forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) 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 {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (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 (\(Index as a
i :*: g a
y) -> Index as a -> NEIndex (a ':| as) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) 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 {k} (g :: k -> *) (as :: [k]).
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 {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) =
    h a -> Rec h as -> NERec h (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) (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 a b. m (a -> b) -> m a -> m b
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 {k} (g :: k -> *) (h :: k -> *) (as :: [k]) (m :: * -> *).
Applicative m =>
(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 g a -> m (h a)
forall (a :: k). g a -> m (h a)
f Rec g as
Prod [] 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) = 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 {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
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
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 g a -> h a -> j a
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 :: 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) =
    h (Apply ff a)
-> Rec h (Fmap_6989586621679427133 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621679427133 ff as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) (h (Apply ff a)
 -> Rec h (Fmap_6989586621679427133 ff as)
 -> NERec h (Apply ff a ':| Fmap_6989586621679427133 ff as))
-> m (h (Apply ff a))
-> m (Rec h (Fmap_6989586621679427133 ff as)
      -> NERec h (Apply ff a ':| Fmap_6989586621679427133 ff as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a). g a -> m (h (ff @@ a))
f g a
x m (Rec h (Fmap_6989586621679427133 ff as)
   -> NERec h (Apply ff a ':| Fmap_6989586621679427133 ff as))
-> m (Rec h (Fmap_6989586621679427133 ff as))
-> m (NERec h (Apply ff a ':| Fmap_6989586621679427133 ff as))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
       (h :: k -> *) (as :: [a]).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
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 g a -> m (h (ff @@ a))
forall (a :: a). g a -> m (h (ff @@ a))
f Rec g as
Prod [] 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 -> (g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| 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 Index as a
i -> \g a -> f (g a)
f -> \case
      g a
x :&| Rec g as
xs -> (g a
x g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&|) (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 -> Lens' (Prod [] g as) (g a)
forall {k} (as :: [k]) (a :: k) (g :: k -> *).
Elem [] as a -> Lens' (Prod [] 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 Index as a
Elem [] as a
i g a -> f (g a)
f Rec g as
Prod [] 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 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 :: 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) = 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 :: 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 -> ((RecApplicative as, PureProd [] as) => r) -> r
Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r) -> r
forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList

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 = g a
forall (a :: k). g a
x g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (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
forall (g :: k -> *). (forall (a :: k). g a) -> Prod [] g as
pureProd g a
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 = g a
forall (a :: a). c a => g a
x g a -> Rec g as -> NERec g (a ':| as)
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
forall (f :: * -> *) (c :: a -> Constraint) (as :: f a)
       (g :: a -> *).
PureProdC f c as =>
(forall (a :: a). c a => g a) -> Prod f g as
pureProdC @_ @c g a
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) =
    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 {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
forall (f :: * -> *) (c :: * -> Constraint) (g :: a -> *)
       (as :: f a).
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 :: 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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    IS Index bs b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  IS Index bs a
i -> \case
    Index as b
IZ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
    IS 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 a :~: b
Refl -> a :~: a
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 :: 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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    NETail Index as b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  NETail Index as a
i -> \case
    NEIndex as b
NEHead -> Maybe (a :~: b)
forall a. Maybe a
Nothing
    NETail 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 a :~: b
Refl -> a :~: a
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 :: (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 = Sing 'ISnd
SISnd '(a, b) b '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 :: forall (a :: ISnd as a). Sing a -> Demote (ISnd as a)
fromSing Sing a
SISnd as a a
SISnd = Demote (ISnd as a)
ISnd '(a, a) a
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 = Sing 'ISnd -> SomeSing (ISnd as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'ISnd
SISnd '(a, a) a 'ISnd
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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 Elem ((,) j) = ISnd
  type Prod ((,) j) = PTup

  singProd :: forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
singProd (STuple2 Sing n1
w Sing n2
x) = Sing n1 -> Sing n2 -> PTup Sing '(n1, n2)
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) = Sing w -> Sing a -> STuple2 '(w, a)
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) = Sing w
-> (:*:) (ISnd '(w, a)) g a -> PTup (ISnd '(w, a) :*: g) '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, 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 {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) = Sing w -> h a -> PTup h '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, 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 {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) = Sing w -> j a -> PTup j '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, 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 :: 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) = Sing w -> h (Apply ff a) -> PTup h '(w, Apply ff a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, 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 :: 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) = Sing a -> g a -> PTup g '(a, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, 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 :: 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 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 :: 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 = r
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 = Sing w -> g a -> PTup g '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
forall {k} (a :: k). SingI a => Sing a
sing

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 = Sing w -> g a -> PTup g '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
forall {k} (a :: k). SingI a => Sing a
sing

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) = Sing w -> Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
Sing w
w (Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a))
-> Compose (Dict c) g a -> PTup (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 :: 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 = Sing 'IId
SIIdentity ('Identity x) x '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 :: forall (a :: IIdentity as a). Sing a -> Demote (IIdentity as a)
fromSing Sing a
SIIdentity as a a
SIId = Demote (IIdentity as a)
IIdentity ('Identity a) a
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 = Sing 'IId -> SomeSing (IIdentity as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IId
SIIdentity ('Identity a) a 'IId
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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) = Sing n -> PIdentity Sing ('Identity n)
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) = Sing a -> SIdentity ('Identity a)
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) = (:*:) (IIdentity ('Identity a)) g a
-> PIdentity (IIdentity ('Identity a) :*: g) ('Identity a)
forall {k} (f :: k -> *) (a :: k). 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 {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) = h a -> PIdentity h ('Identity a)
forall {k} (f :: k -> *) (a :: k). 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 {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) = j a -> PIdentity j ('Identity a)
forall {k} (f :: k -> *) (a :: k). 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 :: 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) = h (Apply ff a) -> PIdentity h ('Identity (Apply ff a))
forall {k} (f :: k -> *) (a :: k). 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 :: 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) = g a -> PIdentity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). 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 :: forall {a} (g :: a -> *) (as :: Identity a).
Prod Identity g as -> Rec g (ToList as)
toRec (PIdentity g a
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 :: 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 = r
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 = g a -> PIdentity g ('Identity a)
(forall (a :: k). g a) -> Prod Identity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity

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 = g a -> PIdentity g ('Identity a)
(forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity

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) = Compose (Dict c) g a -> PIdentity (Dict c :. g) ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (Compose (Dict c) g a -> PIdentity (Dict c :. g) ('Identity a))
-> Compose (Dict c) g a -> PIdentity (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 :: forall {k} (r :: k) (rs :: [k]) (i :: Nat).
(RElem r rs i, PureProd [] rs) =>
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
forall (f :: k -> *). (RecElemFCtx Rec f, r ~ r) => Rec f rs -> f r
rgetC Rec (Index rs) rs
Prod [] (Elem [] 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 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 -> 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 Index bs a
i -> \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)
Prod [] (Elem [] (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 :: 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 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} (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 -> 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 (f c -> Maybe (f c)
forall a. a -> Maybe a
Just f a
f c
x)
      Maybe (a :~: c)
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 :: 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 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 Sing a1
y -> case Sing a
x Sing a -> Sing a1 -> Decision (a :~: a1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
    Proved a :~: a1
Refl -> r -> r
(RElem a as (RIndex a as) => r) -> r
forall a. a -> a
id
    Disproved Refuted (a :~: a1)
_ -> \RElem a as (RIndex a as) => r
_ -> String -> r
forall a. String -> a
errorWithoutStackTrace String
"why :|"
  where
    x :: Sing a
x = Sing a
forall {k} (a :: k). SingI a => Sing a
sing