{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A third way to combine two flavors, alongside 'Proarrow.Optic.Prod.ProdFl' and
-- 'Proarrow.Optic.Sum.SumFl': via the Day convolution. Unlike those two, it keeps both witnesses
-- in the same ambient categories @j@\/@k@. It needs 'Monoidal' structure there to split objects
-- across the two witnesses, where the others pair\/sum two independent categories.
module Proarrow.Optic.Day where

import Prelude (($))

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

type DayFl :: FLAVOR j k -> FLAVOR j k -> FLAVOR j k
class DayFl w1 w2 (p :: k +-> k) (q :: j +-> j)
instance (w1 p1 q1, w2 p2 q2) => DayFl w1 w2 (Day p1 p2) (Day q1 q2)
instance (CategoryOf k, CategoryOf j) => DayFl w1 w2 (Id :: CAT k) (Id :: CAT j)
instance (DayFl w1 w2 f f', DayFl w1 w2 g g') => DayFl 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, Flavor w1, Flavor w2)
  => Optic (Prostrong w1) s1 t1 a1 b1
  -> Optic (Prostrong w2) s2 t2 a2 b2
  -> Optic (Prostrong (DayFl 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, Flavor w1, Flavor w2) =>
Optic (Prostrong w1) s1 t1 a1 b1
-> Optic (Prostrong w2) s2 t2 a2 b2
-> Optic
     (Prostrong (DayFl 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 {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 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
withLegs @w1 Optic (Prostrong w1) s1 t1 a1 b1
o1 \l1 :: p s1 a1
l1@p s1 a1
Objs r1 :: q b1 t1
r1@q b1 t1
Objs ->
    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 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
withLegs @w2 Optic (Prostrong w2) s2 t2 a2 b2
o2 \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 (DayFl w1 w2))
    (s1 ** s2)
    (t1 ** t2)
    (a1 ** a2)
    (b1 ** b2))
 -> Optic
      (Prostrong (DayFl w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> (Ob (a1 ** a2) =>
    Optic
      (Prostrong (DayFl w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic
     (Prostrong (DayFl 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 (DayFl w1 w2))
    (s1 ** s2)
    (t1 ** t2)
    (a1 ** a2)
    (b1 ** b2))
 -> Optic
      (Prostrong (DayFl w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> (Ob (b1 ** b2) =>
    Optic
      (Prostrong (DayFl w1 w2))
      (s1 ** s2)
      (t1 ** t2)
      (a1 ** a2)
      (b1 ** b2))
-> Optic
     (Prostrong (DayFl w1 w2))
     (s1 ** s2)
     (t1 ** t2)
     (a1 ** a2)
     (b1 ** b2)
forall a b. (a -> b) -> a -> b
$
          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 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
legs2prof @(DayFl w1 w2) (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) (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 (DayFl w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> p s1 a1
-> Optic
     (Prostrong (DayFl 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 (DayFl w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> q b1 t1
-> Optic
     (Prostrong (DayFl 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 (DayFl w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> p s2 a2
-> Optic
     (Prostrong (DayFl 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 (DayFl w1 w2))
   (s1 ** s2)
   (t1 ** t2)
   (a1 ** a2)
   (b1 ** b2))
-> q b2 t2
-> Optic
     (Prostrong (DayFl 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