{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}

-- | Dual to 'Proarrow.Optic.Prod.ProdRes': combine over the /coproduct/ of two categories via
-- ':++:'. This lives in its own module (rather than next to 'Proarrow.Optic.Prod.ProdRes') only because
-- "Proarrow.Category.Instance.Coproduct" transitively imports "Proarrow.Optic" already (via
-- 'Proarrow.Profunctor.Corepresentable'), so 'Proarrow.Optic' can't import it back.
--
-- Unlike 'Proarrow.Optic.Prod.ProdRes', this doesn't let you combine two /different/ optics into one -- an
-- @(p ':++:' q) (L a) (L b)@ can only ever hold a @p@, never a @q@. Instead it lets any single
-- @w1@- or @w2@-flavored optic be /injected/ into a shared @'SumRes' w1 w2@ type, with the unused
-- side witnessed trivially by @'Id'@ (demanded via 'ClosedUnder').
module Proarrow.Optic.Sum where

import Prelude (type (~))

import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), (:++:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Optic (ClosedUnder, CompactFlavor, ExOptic (..), FLAVOR, Optic, Prostrong (..), ex2prof, withLegs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

-- | Unlike 'Proarrow.Optic.Prod.ProdRes', a 'SumRes' witness can be decomposed back: the trick is that
-- 'withSumL'\/'withSumR' only fix the /one/ endpoint anchored from outside (@s@ via @p@'s first
-- slot, @t@ via @q@'s second slot) -- the other endpoint (@a@, @b@) comes back /refined/ by the
-- continuation instead of being required upfront. That's what lets the ':.:' case recurse: the
-- existential "middle" object introduced there is exactly the next call's anchored endpoint, so
-- its tag is established by the previous step's own guarantee before it's ever needed as input.
type SumRes :: forall {j1} {k1} {j2} {k2}. FLAVOR j1 k1 -> FLAVOR j2 k2 -> FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2)
class SumRes w1 w2 (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2) (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) where
  withSumL
    :: p (L s) a
    -> q b (L t)
    -> (forall p1 q1 a' b'. (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') => p1 s a' -> q1 b' t -> r)
    -> r
  withSumR
    :: p (R s) a
    -> q b (R t)
    -> (forall p2 q2 a' b'. (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') => p2 s a' -> q2 b' t -> r)
    -> r

instance
  (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
  => SumRes w1 w2 (p1 :++: p2) (q1 :++: q2)
  where
  withSumL :: forall (s :: j1) (a :: COPRODUCT j1 j2) (b :: COPRODUCT j1 j2)
       (t :: j1) r.
(:++:) p1 p2 (L s) a
-> (:++:) q1 q2 b (L t)
-> (forall (p1 :: j1 +-> j1) (q1 :: j1 +-> j1) (a' :: j1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL (InjL p1 a1 b1
l1) (InjL q1 a1 b1
r1) forall (p1 :: j1 +-> j1) (q1 :: j1 +-> j1) (a' :: j1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k = p1 s b1 -> q1 a1 t -> r
forall (p1 :: j1 +-> j1) (q1 :: j1 +-> j1) (a' :: j1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k p1 s b1
p1 a1 b1
l1 q1 a1 t
q1 a1 b1
r1
  withSumR :: forall (s :: j2) (a :: COPRODUCT j1 j2) (b :: COPRODUCT j1 j2)
       (t :: j2) r.
(:++:) p1 p2 (R s) a
-> (:++:) q1 q2 b (R t)
-> (forall (p2 :: j2 +-> j2) (q2 :: j2 +-> j2) (a' :: j2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR (InjR p2 a1 b1
l2) (InjR q2 a1 b1
r2) forall (p2 :: j2 +-> j2) (q2 :: j2 +-> j2) (a' :: j2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k = p2 s b1 -> q2 a1 t -> r
forall (p2 :: j2 +-> j2) (q2 :: j2 +-> j2) (a' :: j2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k p2 s b1
p2 a1 b1
l2 q2 a1 t
q2 a1 b1
r2
instance
  (CategoryOf k1, CategoryOf k2, CategoryOf j1, CategoryOf j2, ClosedUnder w1, ClosedUnder w2)
  => SumRes w1 w2 (Id :: CAT (COPRODUCT k1 k2)) (Id :: CAT (COPRODUCT j1 j2))
  where
  withSumL :: forall (s :: k1) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2)
       (t :: j1) r.
Id (L s) a
-> Id b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL (Id (InjL a1 ~> b1
f)) (Id (InjL a1 ~> b1
g)) forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k = Id s b1 -> Id a1 t -> r
forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k ((s ~> b1) -> Id s b1
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id s ~> b1
a1 ~> b1
f) ((a1 ~> t) -> Id a1 t
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a1 ~> t
a1 ~> b1
g)
  withSumR :: forall (s :: k2) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2)
       (t :: j2) r.
Id (R s) a
-> Id b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR (Id (InjR a1 ~> b1
f)) (Id (InjR a1 ~> b1
g)) forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k = Id s b1 -> Id a1 t -> r
forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k ((s ~> b1) -> Id s b1
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id s ~> b1
a1 ~> b1
f) ((a1 ~> t) -> Id a1 t
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a1 ~> t
a1 ~> b1
g)
instance
  (SumRes w1 w2 f f', SumRes w1 w2 g g', ClosedUnder w1, ClosedUnder w2)
  => SumRes w1 w2 (f :.: g) (g' :.: f')
  where
  withSumL :: forall (s :: k1) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2)
       (t :: j1) r.
(:.:) f g (L s) a
-> (:.:) g' f' b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL (f (L s) b
f :.: g b a
g) (g' b b
g' :.: f' b (L t)
f') forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k =
    forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL @w1 @w2 f (L s) b
f f' b (L t)
f' \p1 s a'
p1 q1 b' t
q1 ->
      forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL @w1 @w2 g b a
g (L a') a
g g' b b
g' b (L b')
g' \p1 a' a'
p1' q1 b' b'
q1' ->
        (:.:) p1 p1 s a' -> (:.:) q1 q1 b' t -> r
forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1).
(w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
p1 s a' -> q1 b' t -> r
k (p1 s a'
p1 p1 s a' -> p1 a' a' -> (:.:) p1 p1 s a'
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p1 a' a'
p1') (q1 b' b'
q1' q1 b' b' -> q1 b' t -> (:.:) q1 q1 b' t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q1 b' t
q1)
  withSumR :: forall (s :: k2) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2)
       (t :: j2) r.
(:.:) f g (R s) a
-> (:.:) g' f' b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR (f (R s) b
f :.: g b a
g) (g' b b
g' :.: f' b (R t)
f') forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k =
    forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR @w1 @w2 f (R s) b
f f' b (R t)
f' \p2 s a'
p2 q2 b' t
q2 ->
      forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR @w1 @w2 g b a
g (R a') a
g g' b b
g' b (R b')
g' \p2 a' a'
p2' q2 b' b'
q2' ->
        (:.:) p2 p2 s a' -> (:.:) q2 q2 b' t -> r
forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2).
(w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
p2 s a' -> q2 b' t -> r
k (p2 s a'
p2 p2 s a' -> p2 a' a' -> (:.:) p2 p2 s a'
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p2 a' a'
p2') (q2 b' b'
q2' q2 b' b' -> q2 b' t -> (:.:) q2 q2 b' t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q2 b' t
q2)

instance
  forall j1 k1 j2 k2 (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
   . (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2)
  => CompactFlavor (SumRes w1 w2)

injLOptic
  :: forall {j1} {k1} {j2} {k2} (w2 :: FLAVOR j2 k2) (w1 :: FLAVOR j1 k1) s t a b
   . (CompactFlavor w1, w2 (Id :: CAT k2) (Id :: CAT j2), CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2)
  => Optic (Prostrong w1) s t a b -> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
injLOptic :: forall {j1} {k1} {j2} {k2} (w2 :: FLAVOR j2 k2)
       (w1 :: FLAVOR j1 k1) (s :: k1) (t :: j1) (a :: k1) (b :: j1).
(CompactFlavor w1, w2 Id Id, CategoryOf j1, CategoryOf k1,
 CategoryOf j2, CategoryOf k2) =>
Optic (Prostrong w1) s t a b
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
injLOptic =
  (forall (p :: k1 +-> k1) (q :: j1 +-> j1).
 (w1 p q, Profunctor p, Profunctor q) =>
 p s a
 -> q b t
 -> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b))
-> Optic (Prostrong w1) s t a b
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \ @p @q p s a
l q b t
r ->
    ExOptic (SumRes w1 w2) (L a) (L b) (L s) (L t)
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: COPRODUCT k1 k2)
       (t :: COPRODUCT j1 j2) (a :: COPRODUCT k1 k2)
       (b :: COPRODUCT j1 j2).
(SumRes w1 w2 p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic (SumRes w1 w2) a b) q s t
-> ExOptic (SumRes w1 w2) a b s t
ExProstrong @(p :++: (Id :: CAT k2)) @(q :++: (Id :: CAT j2)) (p s a -> (:++:) p Id (L s) (L a)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL p s a
l (:++:) p Id (L s) (L a)
-> ExOptic (SumRes w1 w2) (L a) (L b) (L a) (L b)
-> (:.:)
     (p :++: Id) (ExOptic (SumRes w1 w2) (L a) (L b)) (L s) (L b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (L a ~> L a)
-> (L b ~> L b) -> ExOptic (SumRes w1 w2) (L a) (L b) (L a) (L b)
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso L a ~> L a
(:++:) (~>) (~>) (L a) (L a)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COPRODUCT k1 k2). Ob a => (:++:) (~>) (~>) a a
id L b ~> L b
(:++:) (~>) (~>) (L b) (L b)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COPRODUCT j1 j2). Ob a => (:++:) (~>) (~>) a a
id (:.:) (p :++: Id) (ExOptic (SumRes w1 w2) (L a) (L b)) (L s) (L b)
-> (:++:) q Id (L b) (L t)
-> (:.:)
     ((p :++: Id) :.: ExOptic (SumRes w1 w2) (L a) (L b))
     (q :++: Id)
     (L s)
     (L t)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b t -> (:++:) q Id (L b) (L t)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL q b t
r)) ((Ob s, Ob a) =>
 Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b))
-> p s a
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
forall (a :: k1) (b :: k1) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p s a
l ((Ob b, Ob t) =>
 Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b))
-> q b t
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
forall (a :: j1) (b :: j1) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q b t
r

injROptic
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s t a b
   . (CompactFlavor w2, w1 (Id :: CAT k1) (Id :: CAT j1), CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2)
  => Optic (Prostrong w2) s t a b -> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
injROptic :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (s :: k2) (t :: j2) (a :: k2) (b :: j2).
(CompactFlavor w2, w1 Id Id, CategoryOf j1, CategoryOf k1,
 CategoryOf j2, CategoryOf k2) =>
Optic (Prostrong w2) s t a b
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
injROptic =
  (forall (p :: k2 +-> k2) (q :: j2 +-> j2).
 (w2 p q, Profunctor p, Profunctor q) =>
 p s a
 -> q b t
 -> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b))
-> Optic (Prostrong w2) s t a b
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \ @p @q p s a
l q b t
r ->
    ExOptic (SumRes w1 w2) (R a) (R b) (R s) (R t)
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: COPRODUCT k1 k2)
       (t :: COPRODUCT j1 j2) (a :: COPRODUCT k1 k2)
       (b :: COPRODUCT j1 j2).
(SumRes w1 w2 p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic (SumRes w1 w2) a b) q s t
-> ExOptic (SumRes w1 w2) a b s t
ExProstrong @((Id :: CAT k1) :++: p) @((Id :: CAT j1) :++: q) (p s a -> (:++:) Id p (R s) (R a)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR p s a
l (:++:) Id p (R s) (R a)
-> ExOptic (SumRes w1 w2) (R a) (R b) (R a) (R b)
-> (:.:)
     (Id :++: p) (ExOptic (SumRes w1 w2) (R a) (R b)) (R s) (R b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (R a ~> R a)
-> (R b ~> R b) -> ExOptic (SumRes w1 w2) (R a) (R b) (R a) (R b)
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso R a ~> R a
(:++:) (~>) (~>) (R a) (R a)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COPRODUCT k1 k2). Ob a => (:++:) (~>) (~>) a a
id R b ~> R b
(:++:) (~>) (~>) (R b) (R b)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COPRODUCT j1 j2). Ob a => (:++:) (~>) (~>) a a
id (:.:) (Id :++: p) (ExOptic (SumRes w1 w2) (R a) (R b)) (R s) (R b)
-> (:++:) Id q (R b) (R t)
-> (:.:)
     ((Id :++: p) :.: ExOptic (SumRes w1 w2) (R a) (R b))
     (Id :++: q)
     (R s)
     (R t)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b t -> (:++:) Id q (R b) (R t)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR q b t
r)) ((Ob s, Ob a) =>
 Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b))
-> p s a
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
forall (a :: k2) (b :: k2) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p s a
l ((Ob b, Ob t) =>
 Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b))
-> q b t
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
forall (a :: j2) (b :: j2) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q b t
r

-- | The inverse of 'injLOptic': every 'SumRes' witness of an @(L s) (L t) (L a) (L b)@-shaped
-- optic actually comes from an underlying @w1@-flavored optic on @s t a b@.
withSumOpticL
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s t a b r
   . (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2, Ob a, Ob b)
  => Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
  -> (Optic (Prostrong w1) s t a b -> r)
  -> r
withSumOpticL :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (s :: k1) (t :: j1) (a :: k1) (b :: j1) r.
(CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2,
 ClosedUnder w1, ClosedUnder w2, Ob a, Ob b) =>
Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
-> (Optic (Prostrong w1) s t a b -> r) -> r
withSumOpticL = (forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
        (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2).
 (SumRes w1 w2 p q, Profunctor p, Profunctor q) =>
 p (L s) (L a)
 -> q (L b) (L t) -> (Optic (Prostrong w1) s t a b -> r) -> r)
-> Optic (Prostrong (SumRes w1 w2)) (L s) (L t) (L a) (L b)
-> (Optic (Prostrong w1) s t a b -> r)
-> r
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \p (L s) (L a)
l q (L b) (L t)
r -> forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k1)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r.
SumRes w1 w2 p q =>
p (L s) a
-> q b (L t)
-> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1)
           (b' :: j1).
    (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ L a', b ~ L b') =>
    p1 s a' -> q1 b' t -> r)
-> r
withSumL @w1 @w2 p (L s) (L a)
l q (L b) (L t)
r \p1 s a'
p1 q1 b' t
q1 Optic (Prostrong w1) s t a b -> r
k -> Optic (Prostrong w1) s t a b -> r
k (ExOptic w1 a b s t -> Optic (Prostrong w1) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (p1 :.: ExOptic w1 a b) q1 s t -> ExOptic w1 a b s t
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (p1 s a'
p1 p1 s a' -> ExOptic w1 a b a' b' -> (:.:) p1 (ExOptic w1 a b) s b'
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a' ~> a) -> (b ~> b') -> ExOptic w1 a b a' b'
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
a' ~> a
forall (a :: k1). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
b ~> b'
forall (a :: j1). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) p1 (ExOptic w1 a b) s b'
-> q1 b' t -> (:.:) (p1 :.: ExOptic w1 a b) q1 s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q1 b' t
q1)))

-- | The inverse of 'injROptic'.
withSumOpticR
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s t a b r
   . (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2, Ob a, Ob b)
  => Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
  -> (Optic (Prostrong w2) s t a b -> r)
  -> r
withSumOpticR :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (s :: k2) (t :: j2) (a :: k2) (b :: j2) r.
(CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2,
 ClosedUnder w1, ClosedUnder w2, Ob a, Ob b) =>
Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
-> (Optic (Prostrong w2) s t a b -> r) -> r
withSumOpticR = (forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
        (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2).
 (SumRes w1 w2 p q, Profunctor p, Profunctor q) =>
 p (R s) (R a)
 -> q (R b) (R t) -> (Optic (Prostrong w2) s t a b -> r) -> r)
-> Optic (Prostrong (SumRes w1 w2)) (R s) (R t) (R a) (R b)
-> (Optic (Prostrong w2) s t a b -> r)
-> r
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \p (R s) (R a)
l q (R b) (R t)
r -> forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
       (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) (s :: k2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r.
SumRes w1 w2 p q =>
p (R s) a
-> q b (R t)
-> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2)
           (b' :: j2).
    (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ R a', b ~ R b') =>
    p2 s a' -> q2 b' t -> r)
-> r
withSumR @w1 @w2 p (R s) (R a)
l q (R b) (R t)
r \p2 s a'
p2 q2 b' t
q2 Optic (Prostrong w2) s t a b -> r
k -> Optic (Prostrong w2) s t a b -> r
k (ExOptic w2 a b s t -> Optic (Prostrong w2) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (p2 :.: ExOptic w2 a b) q2 s t -> ExOptic w2 a b s t
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (p2 s a'
p2 p2 s a' -> ExOptic w2 a b a' b' -> (:.:) p2 (ExOptic w2 a b) s b'
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a' ~> a) -> (b ~> b') -> ExOptic w2 a b a' b'
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
a' ~> a
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
b ~> b'
forall (a :: j2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) p2 (ExOptic w2 a b) s b'
-> q2 b' t -> (:.:) (p2 :.: ExOptic w2 a b) q2 s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q2 b' t
q2)))