{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The encoding-agnostic core of the optics machinery: the 'Optic' type (a rank-2 profunctor
-- transformation @forall p. c p => p a b -> p s t@), optic flavors as witness-pair constraints
-- ('FLAVOR') with subtyping via flavor superclasses, carrier strength ('Prostrong'), and the existential
-- encoding 'ExOptic' with 'ex2prof'\/'prof2ex'\/'convert' mediating between the two. Also home to
-- the flavor-generic combinators 'iso', 're' and '(%)'. The concrete optic kinds live in the
-- @Proarrow.Optic.*@ submodules, and the user-facing vocabulary (with the full subtyping lattice
-- drawn out) is re-exported from "Proarrow.Optics".
module Proarrow.Optic where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..), UnOp (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), dimapDefault, (:~>), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

type data OPTIC (j :: Kind) (k :: Kind) (c :: j +-> k -> Constraint) = OPT k j
type family OptL (p :: OPTIC j k c) where
  OptL (OPT j k) = j
type family OptR (p :: OPTIC j k c) where
  OptR (OPT j k) = k
type Optic_ :: CAT (OPTIC j k c)
data Optic_ ab st where
  Optic
    :: (Ob a, Ob b, Ob s, Ob t)
    => {forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
Optic_ (OPT p q) (OPT s t)
-> forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t
unOptic :: forall p. (c p, Profunctor p) => p a b -> p s t} -> Optic_ (OPT a b :: OPTIC j k c) (OPT s t)

instance (CategoryOf j, CategoryOf k) => Profunctor (Optic_ :: CAT (OPTIC j k c)) where
  dimap :: forall (c :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c)
       (d :: OPTIC j k c).
(c ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c d
dimap = (c ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c d
Optic_ c a -> Optic_ b d -> Optic_ a b -> Optic_ c d
forall {k :: Kind} (p :: CAT k) (c :: k) (a :: k) (b :: k)
       (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPTIC j k c) (b :: OPTIC j k c) (r :: Kind).
((Ob a, Ob b) => r) -> Optic_ a b -> r
\\ Optic{} = r
(Ob a, Ob b) => r
r
instance (CategoryOf j, CategoryOf k) => Promonad (Optic_ :: CAT (OPTIC j k c)) where
  id :: forall (a :: OPTIC j k c). Ob a => Optic_ a a
id = (forall (p :: j +-> k).
 (c p, Profunctor p) =>
 p (OptL a) (OptR a) -> p (OptL a) (OptR a))
-> Optic_ (OPT (OptL a) (OptR a)) (OPT (OptL a) (OptR a))
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic p (OptL a) (OptR a) -> p (OptL a) (OptR a)
forall (a :: Kind). Ob a => a -> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
forall (p :: j +-> k).
(c p, Profunctor p) =>
p (OptL a) (OptR a) -> p (OptL a) (OptR a)
id
  Optic forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
n . :: forall (b :: OPTIC j k c) (c :: OPTIC j k c) (a :: OPTIC j k c).
Optic_ b c -> Optic_ a b -> Optic_ a c
. Optic forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
m = (forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (p a b -> p s t
forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
n (p a b -> p s t) -> (p a b -> p a b) -> p a b -> p s t
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> p a b
p a b -> p s t
forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
m)

-- | Optics form a category: an object @'OPT' s t@ pairs the object @s@ an optic reads from
-- (contravariant) with the object @t@ it writes back (covariant), an arrow
-- @'OPT' a b '~>' 'OPT' s t@ is a @c@-flavored optic with focus @a@\/@b@ inside @s@\/@t@, and
-- composition is optic composition.
instance (CategoryOf j, CategoryOf k) => CategoryOf (OPTIC j k c) where
  type (~>) = Optic_
  type Ob opt = (opt ~ OPT (OptL opt) (OptR opt), Ob (OptL opt), Ob (OptR opt))

type Optic (c :: j +-> k -> Constraint) s t a b = Optic_ (OPT a b) (OPT s t :: OPTIC j k c)
type Optic' c s a = Optic c s s a a

class (c1 p, c2 p) => (c1 :&&: c2) p
instance (c1 p, c2 p) => (c1 :&&: c2) p

infixl 9 %

-- | Compose two optics, of any (possibly different) flavors or encodings. The composite's constraint
-- is the conjunction ':&&:', so the composite is automatically usable at exactly the meet of the two
-- flavors' capabilities: a lens composed with a prism previews, folds, traverses and sets, but
-- no longer views or reviews. Use 'convert' to name the composite at a single flavor for
-- storage, e.g. @'convert' (l % p) :: 'Proarrow.Optic.AffineTraversal.AffineTraversal' s t a b@.
(%) :: Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
Optic forall (p :: j +-> k). (c1 p, Profunctor p) => p a b -> p s t
n % :: forall {j :: Kind} {k :: Kind} (c1 :: (j +-> k) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j) (c2 :: (j +-> k) -> Constraint)
       (c :: k) (d :: j).
Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
% Optic forall (p :: j +-> k). (c2 p, Profunctor p) => p a b -> p s t
m = (forall (p :: j +-> k).
 ((:&&:) c1 c2 p, Profunctor p) =>
 p c d -> p s t)
-> Optic_ (OPT c d) (OPT s t)
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (p a b -> p s t
p a b -> p s t
forall (p :: j +-> k). (c1 p, Profunctor p) => p a b -> p s t
n (p a b -> p s t) -> (p c d -> p a b) -> p c d -> p s t
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p c d -> p a b
p a b -> p s t
forall (p :: j +-> k). (c2 p, Profunctor p) => p a b -> p s t
m)

-- | An iso in the profunctor-class-flavored encoding (the @P@-prefix convention: plain optic
-- names belong to the 'Prostrong'-flavored encoding, @P@-prefixed ones to the
-- profunctor-class-flavored one). Convert with 'Proarrow.Optic.Iso.fromPIso' and
-- 'Proarrow.Optic.Iso.toPIso'.
type PIso s t a b = Optic Profunctor s t a b

type PIso' s a = PIso s s a a

-- | Create an isomorphism from two arrows, at any optic constraint. Note that this doesn't
-- enforce that the arrows are actually inverses!
--
-- The same @iso@ builds a 'Proarrow.Optic.Iso.Iso', a 'PIso', a
-- 'Proarrow.Optic.Traversal.PTraversal', ... depending on the type it is used at; since @c@ is
-- only determined by the use site, bind the result with a type signature.
iso
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k)
  => (s ~> a) -> (b ~> t) -> Optic c s t a b
iso :: forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso s ~> a
sa b ~> t
bt = (forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic c s t a b
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic ((s ~> a) -> (b ~> t) -> p a b -> p s t
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (c :: k) (a :: k)
       (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> a
sa b ~> t
bt) ((Ob s, Ob a) => Optic c s t a b) -> (s ~> a) -> Optic c s t a b
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s ~> a
sa ((Ob b, Ob t) => Optic c s t a b) -> (b ~> t) -> Optic c s t a b
forall (a :: j) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> t
bt

type FLAVOR j k = (k +-> k) -> (j +-> j) -> Constraint

-- | A flavor: a class of witness pairs that is closed under composition and contains the identity
-- pair -- the monoidal structure of the residuals, with @(Id, Id)@ as unit and
-- @(f :.: g, g' :.: f')@ (note the reversal on the right) as tensor.
type Flavor :: forall {j} {k}. FLAVOR j k -> Constraint
class (forall f f' g g'. (w f f', w g g') => w (f :.: g) (g' :.: f'), w Id Id) => Flavor w where
  composeFlavor :: forall f f' g g' r. (w f f', w g g') => ((w (f :.: g) (g' :.: f')) => r) -> r

instance (forall f f' g g'. (w f f', w g g') => w (f :.: g) (g' :.: f'), w Id Id) => Flavor w where
  composeFlavor :: forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k)
       (g' :: j +-> j) (r :: Kind).
(w f f', w g g') =>
(w (f :.: g) (g' :.: f') => r) -> r
composeFlavor w (f :.: g) (g' :.: f') => r
r = r
w (f :.: g) (g' :.: f') => r
r

-- | @w p q@, as a class with a single instance instead of a bare constraint. The subtyping
-- quantified constraint is spelled @forall p q. v p q => Sub w p q@ rather than
-- @forall p q. v p q => w p q@ because GHC refuses to solve the head of a quantified constraint
-- from a superclass of its premise unless that superclass is strictly smaller than the head (its
-- safeguard against superclass loops in instance declarations), and @w p q@ is never smaller
-- than itself; behind the 'Sub' instance @w p q@ is an ordinary wanted, solved from the
-- superclasses of @v p q@ as usual. 'sub' hands @w p q@ back as an ordinary given (see 'Flavor').
--
-- Deliberately without @w p q@ as a superclass: with it, a quantified given @forall p q. w p q =>
-- Sub IsoFl p q@ would reach @'Profunctor' p@ through the flavor superclasses, which makes GHC
-- treat it as a potential match for every @Profunctor@ wanted in scope and reject the ordinary
-- instances as overlapping.
type Sub :: forall {j} {k}. FLAVOR j k -> FLAVOR j k
class Sub w p q where
  sub :: ((w p q) => r) -> r

instance (w p q) => Sub w p q where
  sub :: forall (r :: Kind). (w p q => r) -> r
sub w p q => r
r = r
w p q => r
r

-- | The carrier @p@ is @w@-strong: a Tambara module for the flavor @w@. 'proact' absorbs a
-- @w@-witness pair @(f, g)@ sandwiching @p@ back into @p@, which is exactly what lets an optic
-- built from that witness distribute the carrier. The name is the profunctor (\"pro\") version of
-- "Proarrow.Category.Monoidal.Strength"'s 'Proarrow.Category.Monoidal.Strength.Strong': its
-- @proact@ specializes to @act@ for certain 'Rep'/'Corep' pairs and to @coact@ for
-- certain 'Corep'/'Rep' ones.
type Prostrong :: forall {j} {k}. FLAVOR j k -> (j +-> k) -> Constraint
class (Profunctor p, CategoryOf j, CategoryOf k) => Prostrong w (p :: j +-> k) where
  proact :: (w f g, Profunctor f, Profunctor g) => f :.: p :.: g :~> p

-- | The existential encoding of an optic.
type ExOptic :: forall {j} {k}. FLAVOR j k -> k -> j -> j +-> k
data ExOptic w a b s t where
  ExOptic
    :: forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j) (s :: k) (t :: j) a b
     . (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> ExOptic w a b s t

instance (CategoryOf j, CategoryOf k) => Profunctor (ExOptic w a b :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> ExOptic w a b a b -> ExOptic w a b c d
dimap c ~> a
l b ~> d
r (ExOptic p a a
p q b b
q) = p c a -> q b d -> ExOptic w a b c d
forall {j :: Kind} {k :: Kind} {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
ExOptic ((c ~> a) -> p a a -> p c a
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (c :: k) (a :: k)
       (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a a
p) ((b ~> d) -> q b b -> q b d
forall (b :: j) (d :: j) (a :: j). (b ~> d) -> q a b -> q a d
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b :: j) (d :: j)
       (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r q b b
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> ExOptic w a b a b -> r
\\ ExOptic p a a
p q b b
q = r
(Ob a, Ob b) => r
(Ob a, Ob a) => r
r ((Ob a, Ob a) => r) -> p a a -> r
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> p a b -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a a
p ((Ob b, Ob b) => r) -> q b b -> r
forall (a :: j) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> q a b -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q b b
q

-- | The free @w@-strong profunctor is @v@-strong for every subflavor @v@ of @w@; this is what
-- lets 'convert' and 'withLegs' accept optics of any encoding (composites included). It is the one
-- bridge instance that replaces a per-carrier one for each flavor.
instance (CategoryOf j, CategoryOf k, forall p q. (v p q) => Sub w p q, Flavor w) => Prostrong v (ExOptic w a b :: j +-> k) where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(v f g, Profunctor f, Profunctor g) =>
((f :.: ExOptic w a b) :.: g) :~> ExOptic w a b
proact @f @g (f a b
f :.: ExOptic @p @q p b a
p q b b
q :.: g b b
g) = forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) (r :: Kind).
Sub w p q =>
(w p q => r) -> r
forall (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) (r :: Kind).
Sub w p q =>
(w p q => r) -> r
sub @w @f @g (forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (f :: k +-> k)
       (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j) (r :: Kind).
(Flavor w, w f f', w g g') =>
(w (f :.: g) (g' :.: f') => r) -> r
forall (w :: FLAVOR j k) (f :: k +-> k) (f' :: j +-> j)
       (g :: k +-> k) (g' :: j +-> j) (r :: Kind).
(Flavor w, w f f', w g g') =>
(w (f :.: g) (g' :.: f') => r) -> r
composeFlavor @w @f @g @p @q ((:.:) f p a a -> (:.:) q g b b -> ExOptic w a b a b
forall {j :: Kind} {k :: Kind} {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
ExOptic (f a b
f f a b -> p b a -> (:.:) f p a a
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b a
p) (q b b
q q b b -> g b b -> (:.:) q g b b
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: g b b
g)))

-- | Build a 'Prostrong'-flavored optic from a @w@-witness pair (the two legs @p s a@ and @q b t@)
-- by wrapping them around the carrier with one 'proact'. Every optic constructor
-- ('Proarrow.Optic.Lens.lens', 'Proarrow.Optic.Prism.prism', ...) is @legs2prof@ of its generating
-- witness pair; 'ex2prof' is the same on the packaged 'ExOptic'.
legs2prof
  :: forall {j} {k} (w :: FLAVOR j k) p q (s :: k) (t :: j) a b
   . (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 :: forall {j :: Kind} {k :: Kind} (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 p s a
p q b t
q = (forall (p :: j +-> k).
 (Prostrong w p, Profunctor p) =>
 p a b -> p s t)
-> Optic (Prostrong w) s t a b
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (\p a b
pab -> forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (p :: j +-> k)
       (f :: k +-> k) (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (p s a
p p s a -> p a b -> (:.:) p p s b
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
pab (:.:) p p s b -> q b t -> (:.:) (p :.: p) q s t
forall {j :: Kind} {k :: Kind} {i :: Kind} (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)) ((Ob s, Ob a) => Optic (Prostrong w) s t a b)
-> p s a -> Optic (Prostrong w) s t a b
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> p a b -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p s a
p ((Ob b, Ob t) => Optic (Prostrong w) s t a b)
-> q b t -> Optic (Prostrong w) s t a b
forall (a :: j) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> q a b -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q b t
q

ex2prof
  :: 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 :: Kind} {k :: Kind} {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 (ExOptic p s a
p q b t
q) = forall {j :: Kind} {k :: Kind} (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 @w p s a
p q b t
q

-- | Run an optic, in any encoding, at its own witness pair (the Pastro-Street move): a
-- 'Prostrong'-flavored optic discharges @c ('ExOptic' w a b)@ through the bridge instance above
-- (i.e. @forall p q. v p q => 'Sub' w p q@), a '(%)'-composite one conjunct at a time, and a profunctor-class-flavored
-- one through the carrier's own instances of its class.
prof2ex
  :: forall {j} {k} w c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b))
  => Optic c s t a b -> ExOptic w a b s t
prof2ex :: forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k)
       (c :: (k -> j -> Kind) -> Constraint) (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 -> ExOptic w a b s t
prof2ex (Optic forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
l) = forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t
l @(ExOptic w a b) (Id a a -> Id b b -> ExOptic w a b a b
forall {j :: Kind} {k :: Kind} {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
ExOptic ((a ~> a) -> Id a a
forall (k :: Kind) (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
a ~> a
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id) ((b ~> b) -> Id b b
forall (k :: Kind) (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
b ~> b
forall (a :: j). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id))

-- | 'prof2ex' in continuation-passing form: the generic eliminator.
withLegs
  :: forall {j} {k} w c (s :: k) (t :: j) a b r
   . (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b))
  => Optic c s t a b -> (forall p q. (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> r) -> r
withLegs :: forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k)
       (c :: (k -> j -> Kind) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) (r :: Kind).
(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 Optic c s t a b
o forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> r
k = case forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k)
       (c :: (k -> j -> Kind) -> Constraint) (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 -> ExOptic w a b s t
forall (w :: FLAVOR j k) (c :: (k -> j -> Kind) -> Constraint)
       (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 -> ExOptic w a b s t
prof2ex @w Optic c s t a b
o of ExOptic p s a
p q b t
q -> p s a -> q b t -> r
forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> r
k p s a
p q b t
q

-- | Convert an optic to a chosen flavor @w@, by running it at its existential encoding
-- @'ExOptic' w a b@ and wrapping the resulting witness pair back around the carrier: this works for
-- any input encoding. A 'Prostrong'-flavored optic converts along the subtyping lattice (via the
-- bridge instance of 'ExOptic'; an invalid conversion fails with @Could not deduce (w p q)@ for the
-- missing superclass), a ':&&:'-composite converts when both conjuncts do, and a
-- profunctor-class-flavored optic converts when @'ExOptic' w a b@ has an instance of its class -- which
-- it does for every class whose generating witnesses @w@ contains (cf. 'Proarrow.Optic.Iso.fromPIso',
-- 'Proarrow.Optic.MonoidalTraversal.fromPTraversal', 'Proarrow.Optic.Tracer.fromPTracer').
--
-- Consumers accept any sufficiently strong optic directly, so this is rarely needed to /use/ an
-- optic; but constructors and '%' return their exact type monomorphically, so it is the way to
-- /store/ an optic at a weaker type, e.g. @convert ('Proarrow.Optic.Lens.lens' f g) ::
-- 'Proarrow.Optic.Traversal.Traversal'' s a@.
convert
  :: forall {j} {k} c (w :: FLAVOR j k) (s :: k) (t :: j) a b
   . (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 :: forall {j :: Kind} {k :: Kind}
       (c :: (k -> j -> Kind) -> 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 Optic c s t a b
o = forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k)
       (c :: (k -> j -> Kind) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) (r :: Kind).
(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 -> Kind) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j) (r :: Kind).
(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 @w Optic c s t a b
o (forall {j :: Kind} {k :: Kind} (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 @w)

-- | The reversing carrier implementing 're': it stores a continuation @p b a -> p t s@, so
-- running an optic at @'Re' p _ _@ builds the optic turned around. Its 'Prostrong' instance
-- absorbs the witness pair mirrored, via 'Flip'.
data Re p s t a b where
  Re :: (Ob a, Ob b) => {forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
Re p s t a b -> p b a -> p t s
unRe :: p b a -> p t s} -> Re p s t a b

instance (Profunctor p) => Profunctor (Re p s t) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Re p s t a b -> Re p s t c d
dimap c ~> a
l b ~> d
r (Re p b a -> p t s
f) = (p d c -> p t s) -> Re p s t c d
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re (p b a -> p t s
f (p b a -> p t s) -> (p d c -> p b a) -> p d c -> p t s
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> d) -> (c ~> a) -> p d c -> p b a
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (c :: k) (a :: k)
       (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap b ~> d
r c ~> a
l) ((Ob c, Ob a) => Re p s t c d) -> (c ~> a) -> Re p s t c d
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => Re p s t c d) -> (b ~> d) -> Re p s t c d
forall (a :: j) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> Re p s t a b -> r
\\ Re{} = r
(Ob a, Ob b) => r
r

class
  (forall p a b. (coc p) => c (Re p a b)) =>
  ReversibleOptic (c :: j +-> k -> Constraint) (coc :: k +-> j -> Constraint)
    | c -> coc

instance ReversibleOptic Profunctor Profunctor
instance (ReversibleOptic l l', ReversibleOptic r r') => ReversibleOptic (l :&&: r) (l' :&&: r')
instance ReversibleOptic (Prostrong w) (Prostrong (Flip w))

re :: (Ob a, Ob b, ReversibleOptic c coc) => Optic c s t a b -> Optic coc b a t s
re :: forall {j :: Kind} {k :: Kind} (a :: j) (b :: k)
       (c :: (k +-> j) -> Constraint) (coc :: (j +-> k) -> Constraint)
       (s :: j) (t :: k).
(Ob a, Ob b, ReversibleOptic c coc) =>
Optic c s t a b -> Optic coc b a t s
re (Optic forall (p :: k +-> j). (c p, Profunctor p) => p a b -> p s t
l) = (forall (p :: j +-> k). (coc p, Profunctor p) => p t s -> p b a)
-> Optic_ (OPT t s) (OPT b a)
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (Re p a b s t -> p t s -> p b a
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
Re p s t a b -> p b a -> p t s
unRe (Re p a b a b -> Re p a b s t
forall (p :: k +-> j). (c p, Profunctor p) => p a b -> p s t
l ((p b a -> p b a) -> Re p a b a b
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re p b a -> p b a
p b a -> p b a
forall (a :: Kind). Ob a => a -> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id)))

class (w p q) => Flip w q p
instance (w p q) => Flip w q p

instance (CategoryOf j, CategoryOf k, Prostrong (Flip w) p) => Prostrong w (Re p s t :: k +-> j) where
  proact :: forall (f :: j +-> j) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Re p s t) :.: g) :~> Re p s t
proact (f :: f a b
f@f a b
Objs :.: Re p b b -> p t s
n :.: g :: g b b
g@g b b
Objs) = (p b a -> p t s) -> Re p s t a b
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re \p b a
p -> p b b -> p t s
n (forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (p :: j +-> k)
       (f :: k +-> k) (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @(Flip w) @p (g b b
g g b b -> p b a -> (:.:) g p b a
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b a
p (:.:) g p b a -> f a b -> (:.:) (g :.: p) f b b
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f a b
f))

class (c (Op q)) => OpConstraint c q
instance (c (Op q)) => OpConstraint c q

class (w (Op g) (Op f)) => OpFlavor w f g
instance (w (Op g) (Op f)) => OpFlavor w f g

instance (Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (OpFlavor w) (UnOp p :: j +-> k) where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(OpFlavor w f g, Profunctor f, Profunctor g) =>
((f :.: UnOp p) :.: g) :~> UnOp p
proact (f a b
f :.: UnOp p ('OP b) ('OP b)
p :.: g b b
g) = p ('OP b) ('OP a) -> UnOp p a b
forall {k :: Kind} {j :: Kind} (p :: OPPOSITE k +-> OPPOSITE j)
       (b :: j) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp (forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (p :: j +-> k)
       (f :: k +-> k) (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR (OPPOSITE k) (OPPOSITE j))
       (p :: OPPOSITE k +-> OPPOSITE j) (f :: OPPOSITE j +-> OPPOSITE j)
       (g :: OPPOSITE k +-> OPPOSITE k).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (g b b -> Op g ('OP b) ('OP b)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op g b b
g Op g ('OP b) ('OP b)
-> p ('OP b) ('OP b) -> (:.:) (Op g) p ('OP b) ('OP b)
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p ('OP b) ('OP b)
p (:.:) (Op g) p ('OP b) ('OP b)
-> Op f ('OP b) ('OP a)
-> (:.:) (Op g :.: p) (Op f) ('OP b) ('OP a)
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f a b -> Op f ('OP b) ('OP a)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op f a b
f))

instance (Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong w (Op (UnOp p :: j +-> k)) where
  proact :: forall (f :: OPPOSITE j +-> OPPOSITE j)
       (g :: OPPOSITE k +-> OPPOSITE k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Op (UnOp p)) :.: g) :~> Op (UnOp p)
proact (f :: f a b
f@f a b
Objs :.: Op (UnOp p ('OP a1) ('OP b1)
p) :.: g :: g b b
g@g b b
Objs) = UnOp p (UN 'OP b) (UN 'OP a)
-> Op (UnOp p) ('OP (UN 'OP a)) ('OP (UN 'OP b))
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (p ('OP (UN 'OP a)) ('OP (UN 'OP b)) -> UnOp p (UN 'OP b) (UN 'OP a)
forall {k :: Kind} {j :: Kind} (p :: OPPOSITE k +-> OPPOSITE j)
       (b :: j) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp (forall {j :: Kind} {k :: Kind} (w :: FLAVOR j k) (p :: j +-> k)
       (f :: k +-> k) (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR (OPPOSITE k) (OPPOSITE j))
       (p :: OPPOSITE k +-> OPPOSITE j) (f :: OPPOSITE j +-> OPPOSITE j)
       (g :: OPPOSITE k +-> OPPOSITE k).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (f a b
f ('OP (UN 'OP a)) b
f f ('OP (UN 'OP a)) b
-> p b ('OP b1) -> (:.:) f p ('OP (UN 'OP a)) ('OP b1)
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b ('OP b1)
p ('OP a1) ('OP b1)
p (:.:) f p ('OP (UN 'OP a)) ('OP b1)
-> g ('OP b1) ('OP (UN 'OP b))
-> (:.:) (f :.: p) g ('OP (UN 'OP a)) ('OP (UN 'OP b))
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: g b b
g ('OP b1) ('OP (UN 'OP b))
g)))

opOptic
  :: forall {j} {k} c (s :: j) (t :: k) a b
   . (forall p. (c p) => c (Op (UnOp p)), CategoryOf j, CategoryOf k)
  => Optic (OpConstraint c) s t a b -> Optic c (OP t) (OP s) (OP b) (OP a)
opOptic :: forall {j :: Kind} {k :: Kind}
       (c :: (OPPOSITE k -> OPPOSITE j -> Kind) -> Constraint) (s :: j)
       (t :: k) (a :: j) (b :: k).
(forall (p :: OPPOSITE k -> OPPOSITE j -> Kind).
 c p =>
 c (Op (UnOp p)),
 CategoryOf j, CategoryOf k) =>
Optic (OpConstraint c) s t a b
-> Optic c ('OP t) ('OP s) ('OP b) ('OP a)
opOptic (Optic forall (p :: k +-> j).
(OpConstraint c p, Profunctor p) =>
p a b -> p s t
n) = (forall (p :: OPPOSITE j +-> OPPOSITE k).
 (c p, Profunctor p) =>
 p ('OP b) ('OP a) -> p ('OP t) ('OP s))
-> Optic_ (OPT ('OP b) ('OP a)) (OPT ('OP t) ('OP s))
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (UnOp p s t -> p ('OP t) ('OP s)
forall {k1 :: Kind} {k2 :: Kind} (p :: OPPOSITE k1 +-> OPPOSITE k2)
       (b :: k2) (a :: k1).
UnOp p a b -> p ('OP b) ('OP a)
unUnOp (UnOp p s t -> p ('OP t) ('OP s))
-> (p ('OP b) ('OP a) -> UnOp p s t)
-> p ('OP b) ('OP a)
-> p ('OP t) ('OP s)
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UnOp p a b -> UnOp p s t
UnOp p a b -> UnOp p s t
forall (p :: k +-> j).
(OpConstraint c p, Profunctor p) =>
p a b -> p s t
n (UnOp p a b -> UnOp p s t)
-> (p ('OP b) ('OP a) -> UnOp p a b)
-> p ('OP b) ('OP a)
-> UnOp p s t
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p ('OP b) ('OP a) -> UnOp p a b
forall {k :: Kind} {j :: Kind} (p :: OPPOSITE k +-> OPPOSITE j)
       (b :: j) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp)

unOpOptic
  :: forall {k} c (s :: k) t a b
   . Optic c (OP t) (OP s) (OP b) (OP a) -> Optic (OpConstraint c) s t a b
unOpOptic :: forall {j :: Kind} {k :: Kind}
       (c :: (OPPOSITE k +-> OPPOSITE j) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
Optic c ('OP t) ('OP s) ('OP b) ('OP a)
-> Optic (OpConstraint c) s t a b
unOpOptic (Optic forall (p :: OPPOSITE k +-> OPPOSITE j).
(c p, Profunctor p) =>
p a b -> p s t
n) = (forall (p :: j +-> k).
 (OpConstraint c p, Profunctor p) =>
 p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall (k :: Kind) (p :: k) (j :: Kind) (q :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob p, Ob q, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p p q -> p s t)
-> Optic_ (OPT p q) (OPT s t)
Optic (Op p ('OP t) ('OP s) -> p s t
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp (Op p ('OP t) ('OP s) -> p s t)
-> (p a b -> Op p ('OP t) ('OP s)) -> p a b -> p s t
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Op p a b -> Op p s t
Op p ('OP b) ('OP a) -> Op p ('OP t) ('OP s)
forall (p :: OPPOSITE k +-> OPPOSITE j).
(c p, Profunctor p) =>
p a b -> p s t
n (Op p ('OP b) ('OP a) -> Op p ('OP t) ('OP s))
-> (p a b -> Op p ('OP b) ('OP a)) -> p a b -> Op p ('OP t) ('OP s)
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> Op p ('OP b) ('OP a)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op)