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

-- | Dual to 'Proarrow.Optic.Prod.ProdFl': combine over the /coproduct/ of two categories via
-- ':++:'. It has its own module because "Proarrow.Category.Instance.Coproduct" already imports
-- "Proarrow.Optic" transitively.
--
-- It does not combine two different optics into one: an @(p ':++:' q) (L a) (L b)@ only ever holds
-- a @p@. It lets any @w1@- or @w2@-flavored optic be injected into a shared @'SumFl' w1 w2@, the
-- unused side witnessed by @'Id'@ (demanded via 'Flavor').
module Proarrow.Optic.Sum where

import Prelude (type (~))

import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), (:++:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (FLAVOR, Flavor, Optic, Prostrong (..), legs2prof, withLegs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

-- | Unlike 'Proarrow.Optic.Prod.ProdFl', a 'SumFl' witness can be decomposed back.
-- '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. So the ':.:' case can recurse: the existential
-- "middle" object introduced there is 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 SumFl :: forall {j1} {k1} {j2} {k2}. FLAVOR j1 k1 -> FLAVOR j2 k2 -> FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2)
class SumFl 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)
  => SumFl 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, Flavor w1, Flavor w2)
  => SumFl 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
  (SumFl w1 w2 f f', SumFl w1 w2 g g', Flavor w1, Flavor w2)
  => SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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.
SumFl 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)

injLOptic
  :: forall {j1} {k1} {j2} {k2} (w2 :: FLAVOR j2 k2) (w1 :: FLAVOR j1 k1) s t a b
   . (Flavor 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 (SumFl 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).
(Flavor w1, w2 Id Id, CategoryOf j1, CategoryOf k1, CategoryOf j2,
 CategoryOf k2) =>
Optic (Prostrong w1) s t a b
-> Optic (Prostrong (SumFl w1 w2)) (L s) (L t) (L a) (L b)
injLOptic Optic (Prostrong w1) s t a b
o =
  forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j1 k1) (c :: (k1 -> j1 -> Type) -> Constraint)
       (s :: k1) (t :: j1) (a :: k1) (b :: j1) r.
(CategoryOf j1, CategoryOf k1, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k1 +-> k1) (q :: j1 +-> j1).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @w1 Optic (Prostrong w1) s t a b
o \ @p @q l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs ->
    forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2))
       (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).
(CategoryOf (COPRODUCT j1 j2), CategoryOf (COPRODUCT k1 k2), w p q,
 Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(SumFl w1 w2)
      (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 :: CAT k2)) (L s) (L a))
      (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 :: (q :++: (Id :: CAT j2)) (L b) (L t))
injROptic
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s t a b
   . (Flavor 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 (SumFl 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).
(Flavor w2, w1 Id Id, CategoryOf j1, CategoryOf k1, CategoryOf j2,
 CategoryOf k2) =>
Optic (Prostrong w2) s t a b
-> Optic (Prostrong (SumFl w1 w2)) (R s) (R t) (R a) (R b)
injROptic Optic (Prostrong w2) s t a b
o =
  forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j2 k2) (c :: (k2 -> j2 -> Type) -> Constraint)
       (s :: k2) (t :: j2) (a :: k2) (b :: j2) r.
(CategoryOf j2, CategoryOf k2, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k2 +-> k2) (q :: j2 +-> j2).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @w2 Optic (Prostrong w2) s t a b
o \ @p @q l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs ->
    forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2))
       (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).
(CategoryOf (COPRODUCT j1 j2), CategoryOf (COPRODUCT k1 k2), w p q,
 Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(SumFl w1 w2)
      (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 :: CAT k1) :++: p) (R s) (R a))
      (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 :: ((Id :: CAT j1) :++: q) (R b) (R t))

-- | The inverse of 'injLOptic': every 'SumFl' 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, Flavor w1, Flavor w2, Ob a, Ob b)
  => Optic (Prostrong (SumFl 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,
 Flavor w1, Flavor w2, Ob a, Ob b) =>
Optic (Prostrong (SumFl w1 w2)) (L s) (L t) (L a) (L b)
-> (Optic (Prostrong w1) s t a b -> r) -> r
withSumOpticL Optic (Prostrong (SumFl w1 w2)) (L s) (L t) (L a) (L b)
o Optic (Prostrong w1) s t a b -> r
k = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2))
       (c :: (COPRODUCT k1 k2 -> COPRODUCT j1 j2 -> Type) -> Constraint)
       (s :: COPRODUCT k1 k2) (t :: COPRODUCT j1 j2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) r.
(CategoryOf (COPRODUCT j1 j2), CategoryOf (COPRODUCT k1 k2),
 Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
           (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @(SumFl w1 w2) Optic (Prostrong (SumFl w1 w2)) (L s) (L t) (L a) (L b)
o \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.
SumFl 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.
SumFl 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 (forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j1 k1) (p :: k1 +-> k1) (q :: j1 +-> j1)
       (s :: k1) (t :: j1) (a :: k1) (b :: j1).
(CategoryOf j1, CategoryOf k1, w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @w1 p1 s a
p1 s a'
p1 q1 b t
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, Flavor w1, Flavor w2, Ob a, Ob b)
  => Optic (Prostrong (SumFl 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,
 Flavor w1, Flavor w2, Ob a, Ob b) =>
Optic (Prostrong (SumFl w1 w2)) (R s) (R t) (R a) (R b)
-> (Optic (Prostrong w2) s t a b -> r) -> r
withSumOpticR Optic (Prostrong (SumFl w1 w2)) (R s) (R t) (R a) (R b)
o Optic (Prostrong w2) s t a b -> r
k = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR (COPRODUCT j1 j2) (COPRODUCT k1 k2))
       (c :: (COPRODUCT k1 k2 -> COPRODUCT j1 j2 -> Type) -> Constraint)
       (s :: COPRODUCT k1 k2) (t :: COPRODUCT j1 j2)
       (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) r.
(CategoryOf (COPRODUCT j1 j2), CategoryOf (COPRODUCT k1 k2),
 Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2)
           (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @(SumFl w1 w2) Optic (Prostrong (SumFl w1 w2)) (R s) (R t) (R a) (R b)
o \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.
SumFl 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.
SumFl 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 (forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j2 k2) (p :: k2 +-> k2) (q :: j2 +-> j2)
       (s :: k2) (t :: j2) (a :: k2) (b :: j2).
(CategoryOf j2, CategoryOf k2, w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @w2 p2 s a
p2 s a'
p2 q2 b t
q2 b' t
q2)