{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A third way to combine two flavors, alongside 'Proarrow.Optic.Prod.ProdRes' and
-- 'Proarrow.Optic.Sum.SumRes': via the Day convolution, which -- unlike those two -- keeps both
-- witnesses in the *same* ambient categories @j@\/@k@ (it needs 'Monoidal' structure there to
-- split objects across the two witnesses, rather than pairing\/summing two independent
-- categories).
module Proarrow.Optic.Day where

import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), type (**))
import Proarrow.Core (CAT, CategoryOf (..), Promonad (..), (\\), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (CompactFlavor, ExOptic (..), FLAVOR, Optic, Prostrong (..), ex2prof, withLegs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Day (Day, day)
import Proarrow.Profunctor.Instance.Identity (Id (..))

type DayRes :: FLAVOR j k -> FLAVOR j k -> FLAVOR j k
class DayRes w1 w2 (p :: k +-> k) (q :: j +-> j)
instance (w1 p1 q1, w2 p2 q2) => DayRes w1 w2 (Day p1 p2) (Day q1 q2)
instance (CategoryOf k, CategoryOf j) => DayRes w1 w2 (Id :: CAT k) (Id :: CAT j)
instance (DayRes w1 w2 f f', DayRes w1 w2 g g') => DayRes w1 w2 (f :.: g) (g' :.: f')

dayOptic
  :: forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) s1 t1 a1 b1 s2 t2 a2 b2
   . (Monoidal j, Monoidal k, CompactFlavor w1, CompactFlavor w2)
  => Optic (Prostrong w1) s1 t1 a1 b1
  -> Optic (Prostrong w2) s2 t2 a2 b2
  -> Optic (Prostrong (DayRes w1 w2)) (s1 ** s2) (t1 ** t2) (a1 ** a2) (b1 ** b2)
dayOptic :: forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (s1 :: k)
       (t1 :: j) (a1 :: k) (b1 :: j) (s2 :: k) (t2 :: j) (a2 :: k)
       (b2 :: j).
(Monoidal j, Monoidal k, CompactFlavor w1, CompactFlavor w2) =>
Optic (Prostrong w1) s1 t1 a1 b1
-> Optic (Prostrong w2) s2 t2 a2 b2
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
dayOptic Optic (Prostrong w1) s1 t1 a1 b1
o1 Optic (Prostrong w2) s2 t2 a2 b2
o2 =
  (forall (p :: k +-> k) (q :: j +-> j).
 (w1 p q, Profunctor p, Profunctor q) =>
 p s1 a1
 -> q b1 t1
 -> Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic (Prostrong w1) s1 t1 a1 b1
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
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
    ( \l1 :: p s1 a1
l1@p s1 a1
Objs r1 :: q b1 t1
r1@q b1 t1
Objs ->
        (forall (p :: k +-> k) (q :: j +-> j).
 (w2 p q, Profunctor p, Profunctor q) =>
 p s2 a2
 -> q b2 t2
 -> Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic (Prostrong w2) s2 t2 a2 b2
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
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
          ( \l2 :: p s2 a2
l2@p s2 a2
Objs r2 :: q b2 t2
r2@q b2 t2
Objs ->
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a1 @a2 ((Ob (a1 ** a2) =>
  Optic
    (Prostrong (DayRes w1 w2))
    (s1 ** s2)
    (t1 ** t2)
    (a1 ** a2)
    (b1 ** b2))
 -> Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> (Ob (a1 ** a2) =>
    Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall a b. (a -> b) -> a -> b
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @j @b1 @b2 ((Ob (b1 ** b2) =>
  Optic
    (Prostrong (DayRes w1 w2))
    (s1 ** s2)
    (t1 ** t2)
    (a1 ** a2)
    (b1 ** b2))
 -> Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> (Ob (b1 ** b2) =>
    Optic
      (Prostrong (DayRes w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall a b. (a -> b) -> a -> b
$
                  ExOptic (DayRes w1 w2) (a1 ** a2) (b1 ** b2) (s1 ** s2) (t1 ** t2)
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
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 ((:.:)
  (Day p p :.: ExOptic (DayRes w1 w2) (a1 ** a2) (b1 ** b2))
  (Day q q)
  (s1 ** s2)
  (t1 ** t2)
-> ExOptic
     (DayRes w1 w2) (a1 ** a2) (b1 ** b2) (s1 ** s2) (t1 ** t2)
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 (p s1 a1 -> p s2 a2 -> Day p p (s1 ** s2) (a1 ** a2)
forall j k (p :: j +-> k) (q :: j +-> k) (c :: k) (d :: j) (e :: k)
       (f :: j).
(Monoidal j, Monoidal k, Profunctor p, Profunctor q) =>
p c d -> q e f -> Day p q (c ** e) (d ** f)
day p s1 a1
l1 p s2 a2
l2 Day p p (s1 ** s2) (a1 ** a2)
-> ExOptic
     (DayRes w1 w2) (a1 ** a2) (b1 ** b2) (a1 ** a2) (b1 ** b2)
-> (:.:)
     (Day p p)
     (ExOptic (DayRes w1 w2) (a1 ** a2) (b1 ** b2))
     (s1 ** s2)
     (b1 ** b2)
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
:.: ((a1 ** a2) ~> (a1 ** a2))
-> ((b1 ** b2) ~> (b1 ** b2))
-> ExOptic
     (DayRes w1 w2) (a1 ** a2) (b1 ** b2) (a1 ** a2) (b1 ** b2)
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 (a1 ** a2) ~> (a1 ** a2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (b1 ** b2) ~> (b1 ** b2)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:)
  (Day p p)
  (ExOptic (DayRes w1 w2) (a1 ** a2) (b1 ** b2))
  (s1 ** s2)
  (b1 ** b2)
-> Day q q (b1 ** b2) (t1 ** t2)
-> (:.:)
     (Day p p :.: ExOptic (DayRes w1 w2) (a1 ** a2) (b1 ** b2))
     (Day q q)
     (s1 ** s2)
     (t1 ** t2)
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 b1 t1 -> q b2 t2 -> Day q q (b1 ** b2) (t1 ** t2)
forall j k (p :: j +-> k) (q :: j +-> k) (c :: k) (d :: j) (e :: k)
       (f :: j).
(Monoidal j, Monoidal k, Profunctor p, Profunctor q) =>
p c d -> q e f -> Day p q (c ** e) (d ** f)
day q b1 t1
r1 q b2 t2
r2)) ((Ob s1, Ob a1) =>
 Optic
   (Prostrong (DayRes w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> p s1 a1
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall (a :: k) (b :: k) 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 s1 a1
l1 ((Ob b1, Ob t1) =>
 Optic
   (Prostrong (DayRes w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> q b1 t1
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall (a :: j) (b :: j) 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 b1 t1
r1 ((Ob s2, Ob a2) =>
 Optic
   (Prostrong (DayRes w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> p s2 a2
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall (a :: k) (b :: k) 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 s2 a2
l2 ((Ob b2, Ob t2) =>
 Optic
   (Prostrong (DayRes w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> q b2 t2
-> Optic
     (Prostrong (DayRes w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall (a :: j) (b :: j) 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 b2 t2
r2
          )
          Optic (Prostrong w2) s2 t2 a2 b2
o2
    )
    Optic (Prostrong w1) s1 t1 a1 b1
o1