{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | The __tracer__: the write-only optic whose residual sits on the /source and target/ side,
--
-- > Tracer s t a b = exists m. (m ** s ~> a, b ~> m ** t)
--
-- witnessed by @'Corep'@\/@'Rep'@ @('ActionAt' 'Tensor' m)@ ('TracerFl' \/
-- 'withTracerP') -- a setter witness pair read the other way round, equivalently an 'ActFl'
-- @Tensor@ pair with the roles of the two witnesses swapped. Running it forwards closes a feedback loop through the
-- residual, so it distributes any 'Costrong' profunctor ('tracerP') and is a
-- 'Proarrow.Optic.Setter.Setter' exactly in a 'TracedMonoidal' category; run backwards
-- ('Proarrow.Optic.Setter.over' . 'Proarrow.Optic.re') it needs no trace at all. Build with
-- 'tracer', eliminate with 'tracerOf' (or 'Proarrow.Optic.Setter.over' at the hom) or recover the
-- legs with 'withTracer'; 'fromPTracer'\/'toPTracer' mediate with the profunctor-class-flavored
-- 'PTracer' (@'Optic' ('Costrong' 'Tensor')@).
module Proarrow.Optic.Tracer where

import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), Tensor, type (**))
import Proarrow.Category.Monoidal.Action (ActionAt)
import Proarrow.Category.Monoidal.Strength (Costrong (..), TracedMonoidal)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic (..)
  , FLAVOR
  , Flavor
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , convert
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.Setter (SetterFl (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..))

-- | The tracer flavor: a witness pair whose legs are @m ** s ~> a@ and @b ~> m ** t@ for an
-- existential residual @m@ -- the residual functor is applied to the source and target rather
-- than to the foci, i.e. an @'ActFl' 'Tensor'@ pair with the roles of the two witnesses swapped.
-- 'withTracerP' recovers the legs (the 'Proarrow.Optic.MonoidalLens.withMonLensP' of tracers), and
-- distributing a 'Costrong' profunctor ('tracerP') is derived from them. This is the @'Prostrong'@
-- counterpart of @'Costrong' 'Tensor'@ the way 'Proarrow.Optic.MonoidalLens.MonLensFl' is of
-- @'Proarrow.Category.Monoidal.Strength.Strong' 'Tensor'@.
--
-- Every tracer witness pair is a setter pair ('SetterFl' superclass, so 'Proarrow.Optic.Setter.over',
-- 'Proarrow.Optic.Setter.set', '(Proarrow.Optic.Setter.%~)' all work) and its flip is one too
-- (@'SetterFl' q p@, so @'Proarrow.Optic.Setter.over' . 'Proarrow.Optic.re'@ works without a trace, and
-- @'convert' t :: 'Optic' ('Prostrong' ('Flip' 'SetterFl')) s t a b@ -- the converse fails, since a
-- flipped setter need not have a trace, e.g. a flipped lens witness, so tracers are the subflavor of
-- flipped setters that can also run /forwards/);
-- 'TracedMonoidal' rides in the instance context of the tensor-action witness, not in the
-- method, so ordinary setters keep their honest constraints. 'Monoidal' sits on the method rather
-- than the class so that the identity witness needs only 'CategoryOf' and 'Proarrow.Optic.Iso.IsoFl'
-- can include this flavor.
type TracerFl :: forall {k}. FLAVOR k k
class (SetterFl p q, SetterFl q p) => TracerFl (p :: k +-> k) (q :: k +-> k) where
  -- | Recover the two legs, with the residual @m@ existential.
  withTracerP
    :: (Monoidal k) => p s a -> q b t -> (forall (m :: k). (Ob m) => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r) -> r

instance (CategoryOf k) => TracerFl (Id :: k +-> k) (Id :: k +-> k) where
  withTracerP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
Id s a
-> Id b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP (Id s ~> a
l) (Id b ~> t
r) forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
k = forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
k @Unit (s ~> a
l (s ~> a) -> ((Unit ** s) ~> s) -> (Unit ** s) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ** s) ~> s
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) (t ~> (Unit ** t)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv (t ~> (Unit ** t)) -> (b ~> t) -> b ~> (Unit ** t)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> t
r) ((Ob s, Ob a) => r) -> (s ~> a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ s ~> a
l ((Ob b, Ob t) => r) -> (b ~> t) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> t
r

instance
  forall k (f :: k +-> k) (f' :: k +-> k) (g :: k +-> k) (g' :: k +-> k)
   . (TracerFl f g, TracerFl f' g')
  => TracerFl (f :.: f') (g' :.: g)
  where
  withTracerP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
(:.:) f f' s a
-> (:.:) g' g b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP ((f :: f s b
f@f s b
Objs :: f s x) :.: f' b a
f') (g' b b
g' :.: (g :: g b t
g@g b t
Objs :: g y t)) forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
kk =
    f s b
-> g b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> b) -> (b ~> (m ** t)) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
f s a
-> g b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(TracerFl p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP f s b
f g b t
g \ @(mo :: k) (m ** s) ~> b
ho b ~> (m ** t)
io ->
      f' b a
-> g' b b
-> (forall (m :: k).
    Ob m =>
    ((m ** b) ~> a) -> (b ~> (m ** b)) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
f' s a
-> g' b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(TracerFl p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP f' b a
f' g' b b
g' \ @(mi :: k) (m ** b) ~> a
hi b ~> (m ** b)
ii ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @mi @mo
          ( forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
kk @(mi ** mo)
              ((m ** b) ~> a
hi ((m ** b) ~> a)
-> (((m ** m) ** s) ~> (m ** b)) -> ((m ** m) ** s) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @mi Obj m -> ((m ** s) ~> b) -> (m ** (m ** s)) ~> (m ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (m ** s) ~> b
ho) ((m ** (m ** s)) ~> (m ** b))
-> (((m ** m) ** s) ~> (m ** (m ** s)))
-> ((m ** m) ** s) ~> (m ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @mi @mo @s)
              (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @mi @mo @t ((m ** (m ** t)) ~> ((m ** m) ** t))
-> (b ~> (m ** (m ** t))) -> b ~> ((m ** m) ** t)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @mi Obj m -> (b ~> (m ** t)) -> (m ** b) ~> (m ** (m ** t))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** b ~> (m ** t)
io) ((m ** b) ~> (m ** (m ** t)))
-> (b ~> (m ** b)) -> b ~> (m ** (m ** t))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> (m ** b)
ii)
          )

-- | The tracer witness: the tensor-action pair read the other way round, @'Corep' ('ActionAt' 'Tensor' m)@
-- on the left and @'Rep' ('ActionAt' 'Tensor' m)@ on the right. Its 'overP' is the trace
-- of @m ** s ~> a ~> b ~> m ** t@ over @m@, so it needs the category to be 'TracedMonoidal'.
instance (TracedMonoidal k, Ob (m :: k)) => SetterFl (Corep (ActionAt Tensor m) :: k +-> k) (Rep (ActionAt Tensor m)) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Corep (ActionAt Tensor m) s a
-> Rep (ActionAt Tensor m) b t -> (a ~> b) -> s ~> t
overP (Corep (ActionAt Tensor m @ s) ~> a
l) (Rep b ~> (ActionAt Tensor m @ t)
r) a ~> b
f = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @_ @m (b ~> (ActionAt Tensor m @ t)
b ~> (m ** t)
r (b ~> (m ** t)) -> ((m ** s) ~> b) -> (m ** s) ~> (m ** t)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f (a ~> b) -> ((m ** s) ~> a) -> (m ** s) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ActionAt Tensor m @ s) ~> a
(m ** s) ~> a
l)

instance (TracedMonoidal k, Ob (m :: k)) => TracerFl (Corep (ActionAt Tensor m) :: k +-> k) (Rep (ActionAt Tensor m)) where
  withTracerP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
Corep (ActionAt Tensor m) s a
-> Rep (ActionAt Tensor m) b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP (Corep (ActionAt Tensor m @ s) ~> a
l) (Rep b ~> (ActionAt Tensor m @ t)
r) forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
k = forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
k @m (ActionAt Tensor m @ s) ~> a
(m ** s) ~> a
l b ~> (ActionAt Tensor m @ t)
b ~> (m ** t)
r

-- | Distribute any 'Costrong' profunctor through a tracer witness pair: 'dimap' the legs on and
-- 'coact' the residual away. At the hom this is 'overP'.
tracerP
  :: forall {k} p q (s :: k) a b t r
   . (TracerFl p q, Costrong Tensor r)
  => p s a -> q b t -> r a b -> r s t
tracerP :: forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) (r :: k +-> k).
(TracerFl p q, Costrong Tensor r) =>
p s a -> q b t -> r a b -> r s t
tracerP p s a
l q b t
r r a b
rab = p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r s t)
-> r s t
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(TracerFl p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP p s a
l q b t
r (\ @m (m ** s) ~> a
i b ~> (m ** t)
h -> forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @r @m (((m ** s) ~> a) -> (b ~> (m ** t)) -> r a b -> r (m ** s) (m ** t)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (m ** s) ~> a
i b ~> (m ** t)
h r a b
rab)) ((Ob s, Ob a) => r s t) -> p s a -> r s t
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 s a
l ((Ob b, Ob t) => r s t) -> q b t -> r s t
forall (a :: k) (b :: k) 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

type Tracer (s :: k) (t :: k) a b = Optic (Prostrong TracerFl) s t a b
type Tracer' s a = Tracer s s a a

-- | Build a tracer from its two legs and a chosen residual @m@: @m ** s ~> a@ decomposes the source
-- (given the residual), @b ~> m ** t@ rebuilds the target and produces the residual to feed back.
tracer
  :: forall {k} (m :: k) (s :: k) t a b
   . (TracedMonoidal k, Ob m, Ob s, Ob t, Ob a, Ob b)
  => ((m ** s) ~> a) -> (b ~> (m ** t)) -> Tracer s t a b
tracer :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k).
(TracedMonoidal k, Ob m, Ob s, Ob t, Ob a, Ob b) =>
((m ** s) ~> a) -> (b ~> (m ** t)) -> Tracer s t a b
tracer (m ** s) ~> a
l b ~> (m ** t)
r = 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 k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @TracerFl (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @s @(ActionAt Tensor m) (ActionAt Tensor m @ s) ~> a
(m ** s) ~> a
l) (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @t @(ActionAt Tensor m) b ~> (ActionAt Tensor m @ t)
b ~> (m ** t)
r)

-- | Distribute any 'Costrong' profunctor through a tracer (or any stronger optic). At the hom this
-- is 'Proarrow.Optic.Setter.over', computing the feedback loop through the residual.
--
-- Accepts any encoding (cf. 'Proarrow.Optic.Traversal.traverseOf'): a 'PTracer' works directly, as
-- does a '(Proarrow.Optic.%)'-composite.
tracerOf
  :: forall {k} c (s :: k) (t :: k) a b r
   . (Monoidal k, Costrong Tensor r, c (ExOptic TracerFl a b))
  => Optic c s t a b -> r a b -> r s t
tracerOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (r :: k -> k -> Type).
(Monoidal k, Costrong Tensor r, c (ExOptic TracerFl a b)) =>
Optic c s t a b -> r a b -> r s t
tracerOf Optic c s t a b
o r a b
rab = 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 k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @TracerFl Optic c s t a b
o \p s a
l q b t
r -> p s a -> q b t -> r a b -> r s t
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) (r :: k +-> k).
(TracerFl p q, Costrong Tensor r) =>
p s a -> q b t -> r a b -> r s t
tracerP p s a
l q b t
r r a b
rab

-- | The generic carrier absorbs the residual of a 'Costrong' action whenever the flavor contains the
-- tracer generator: one more tensor-action layer, composed onto the witnesses.
-- This is what lets profunctor-class-flavored tracers ('PTracer') eliminate through 'ExOptic' too.
instance
  ( Monoidal k
  , Ob (a :: k)
  , Ob b
  , Flavor w
  , forall (m :: k). (Ob m) => w (Corep (ActionAt Tensor m)) (Rep (ActionAt Tensor m))
  )
  => Costrong Tensor (ExOptic w a b :: k +-> k)
  where
  coact :: forall (a :: k) (x :: k) (y :: k).
(Ob a, Ob x, Ob y) =>
ExOptic w a b (Act Tensor a x) (Act Tensor a y)
-> ExOptic w a b x y
coact @m @x @y (ExOptic @p @q p (Act Tensor a x) a
l q b (Act Tensor a y)
r) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @m @x ((Ob (a ** x) => ExOptic w a b x y) -> ExOptic w a b x y)
-> (Ob (a ** x) => ExOptic w a b x y) -> ExOptic w a b x y
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 @k @m @y ((Ob (a ** y) => ExOptic w a b x y) -> ExOptic w a b x y)
-> (Ob (a ** y) => ExOptic w a b x y) -> ExOptic w a b x y
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).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(Corep (ActionAt Tensor m) :.: p) @(q :.: Rep (ActionAt Tensor m)) (Corep (ActionAt Tensor a) x (Corep (ActionAt Tensor a) %% x)
Corep (ActionAt Tensor a) x (a ** x)
forall (a :: k).
Ob a =>
Corep (ActionAt Tensor a) a (Corep (ActionAt Tensor a) %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv Corep (ActionAt Tensor a) x (a ** x)
-> p (a ** x) a -> (:.:) (Corep (ActionAt Tensor a)) p x 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
:.: p (Act Tensor a x) a
p (a ** x) a
l) (q b (Act Tensor a y)
q b (a ** y)
r q b (a ** y)
-> Rep (ActionAt Tensor a) (a ** y) y
-> (:.:) q (Rep (ActionAt Tensor a)) b y
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
:.: Rep (ActionAt Tensor a) (Rep (ActionAt Tensor a) % y) y
Rep (ActionAt Tensor a) (a ** y) y
forall (a :: k).
Ob a =>
Rep (ActionAt Tensor a) (Rep (ActionAt Tensor a) % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv)

-- | Eliminate any optic that is at least an iso and at most a tracer to its two legs, recovering
-- the existential residual @m@, in either encoding: run it at its witness pair ('ExOptic' 'TracerFl',
-- via 'withLegs') and read the legs off with 'withTracerP'.
withTracer
  :: forall {k} c (s :: k) (t :: k) a b r
   . (Monoidal k, (Ob a, Ob b) => c (ExOptic TracerFl a b))
  => Optic c s t a b -> (forall (m :: k). (Ob m) => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r) -> r
withTracer :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(Monoidal k, (Ob a, Ob b) => c (ExOptic TracerFl a b)) =>
Optic c s t a b
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracer Optic c s t a b
o forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> 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 k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @TracerFl Optic c s t a b
o \ @p @q p s a
p q b t
q -> forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(TracerFl p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(TracerFl p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ((m ** s) ~> a) -> (b ~> (m ** t)) -> r)
-> r
withTracerP @p @q p s a
p q b t
q \ @m (m ** s) ~> a
h b ~> (m ** t)
i -> forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r
k @m (m ** s) ~> a
h b ~> (m ** t)
i

-- | A tracer in the profunctor-class-flavored encoding (cf. 'Proarrow.Optic.PIso'). Equivalent to
-- 'Tracer' via 'toPTracer' and 'fromPTracer'.
type PTracer s t a b = Optic (Costrong Tensor) s t a b

-- | Instantiate a profunctor-class tracer at the generic carrier @'ExOptic' 'TracerFl' a b@, which is
-- 'Costrong' by the instance above (the Pastro-Street move).
fromPTracer :: forall {k} (s :: k) (t :: k) a b. (TracedMonoidal k) => PTracer s t a b -> Tracer s t a b
fromPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
TracedMonoidal k =>
PTracer s t a b -> Tracer s t a b
fromPTracer = Optic (Costrong Tensor) s t a b
-> Optic (Prostrong TracerFl) s t a b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert

-- | Eliminate a 'Tracer' to its profunctor-class form: run 'tracerP' at the caller's profunctor.
toPTracer :: forall {k} (s :: k) (t :: k) a b. (CategoryOf k) => Tracer s t a b -> PTracer s t a b
toPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
CategoryOf k =>
Tracer s t a b -> PTracer s t a b
toPTracer Tracer 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 k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @TracerFl Tracer s t a b
o \l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs -> (forall (p :: k +-> k).
 (Costrong Tensor p, Profunctor p) =>
 p a b -> p s t)
-> PTracer s t a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (p s a -> q b t -> p a b -> p s t
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) (r :: k +-> k).
(TracerFl p q, Costrong Tensor r) =>
p s a -> q b t -> r a b -> r s t
tracerP p s a
l q b t
r)