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

module Proarrow.Category.Instance.Free where

import Data.Char (toLower)
import Data.Kind (Constraint)
import Data.Typeable (Typeable, eqT, (:~:) (..))
import Prelude (Bool (..), Eq (..), Maybe (..), Show (..), (&&))
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , type (+->)
  )
import Proarrow.Profunctor.Initial (InitialProfunctor)
import Proarrow.Profunctor.Representable (Representable (..), withRepOb)

type family All (cs :: [Kind -> Constraint]) (k :: Kind) :: Constraint where
  All '[] k = ()
  All (c ': cs) k = (c k, All cs k)

class ((All cs k) => c k) => FromAll cs c k
instance ((All cs k) => c k) => FromAll cs c k

type Elem :: (Kind -> Constraint) -> [Kind -> Constraint] -> Constraint
class (forall k. FromAll cs c k) => c `Elem` cs
instance {-# OVERLAPPABLE #-} (c `Elem` cs) => c `Elem` (d ': cs)
instance c `Elem` (c ': cs)

newtype FREE (cs :: [Kind -> Constraint]) (p :: CAT j) = EMB j
type instance UN EMB (EMB a) = a

type Free :: CAT (FREE cs p)
data Free a b where
  Id :: (Ob a) => Free a a
  Emb :: (Ob a, Ob b, Typeable a, Typeable b) => p a b %1 -> Free (i :: FREE cs p) (EMB a) %1 -> Free i (EMB b)
  Str
    :: forall {j} {cs} {p :: CAT j} (c :: Kind -> Constraint) (a :: FREE cs p) b i
     . (HasStructure cs p c, Ob a, Ob b)
    => Struct c a b %1 -> Free i a %1 -> Free i b

emb :: (Ob a, Ob b, Typeable a, Typeable b, Ok cs p) => p a b %1 -> Free (EMB a :: FREE cs p) (EMB b)
emb :: forall {j :: Kind} (a :: j) (b :: j) (cs :: [Kind -> Constraint])
       (p :: CAT j).
(Ob a, Ob b, Typeable a, Typeable b, Ok cs p) =>
p a b %1 -> Free ('EMB a) ('EMB b)
emb p a b
p = p a b -> Free ('EMB a) ('EMB a) -> Free ('EMB a) ('EMB b)
forall {j :: Kind} (a :: j) (b :: j) (p :: j -> j -> Kind)
       (cs :: [Kind -> Constraint]) (i :: FREE cs p).
(Ob a, Ob b, Typeable a, Typeable b) =>
p a b -> Free i ('EMB a) -> Free i ('EMB b)
Emb p a b
p Free ('EMB a) ('EMB a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id

class (forall x y. Eq (p x y)) => Eq2 p
instance (forall x y. Eq (p x y)) => Eq2 p

class (forall x y. P.Show (p x y)) => Show2 p
instance (forall x y. P.Show (p x y)) => Show2 p

class (Typeable p, Typeable cs, Typeable j, All cs (FREE cs p)) => Ok cs (p :: CAT j)
instance (Typeable p, Typeable cs, Typeable j, All cs (FREE cs p)) => Ok cs (p :: CAT j)

class (Ok c p, Eq2 p) => WithEq (a :: FREE c (p :: CAT j))
instance (Ok c p, Eq2 p) => WithEq (a :: FREE c (p :: CAT j))

instance (WithEq a) => Eq (Free a b) where
  Free a b
Id == :: Free a b -> Free a b -> Bool
== Free a b
Id = Bool
True
  Emb @al p a b
p1 Free a ('EMB a)
g1 == Emb @ar p a b
p2 Free a ('EMB a)
g2 = case forall (a :: j) (b :: j).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k :: Kind} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @al @ar of Just a :~: a
Refl -> p a b
p1 p a b -> p a b -> Bool
forall (a :: Kind). Eq a => a -> a -> Bool
== p a b
p a b
p2 Bool -> Bool -> Bool
&& Free a ('EMB a)
g1 Free a ('EMB a) -> Free a ('EMB a) -> Bool
forall (a :: Kind). Eq a => a -> a -> Bool
== Free a ('EMB a)
Free a ('EMB a)
g2; Maybe (a :~: a)
Nothing -> Bool
False
  Str @strl @a1 Struct c a b
s1 Free a a
g1 == Str @strr @a2 Struct c a b
s2 Free a a
g2 = case (forall {k :: Kind} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: Kind -> Constraint) (b :: Kind -> Constraint).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @strl @strr, forall {k :: Kind} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: FREE cs p) (b :: FREE cs p).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2) of
    (Just c :~: c
Refl, Just a :~: a
Refl) -> Struct c a b
s1 Struct c a b -> Struct c a b -> Bool
forall (a :: Kind). Eq a => a -> a -> Bool
== Struct c a b
Struct c a b
s2 Bool -> Bool -> Bool
&& Free a a
g1 Free a a -> Free a a -> Bool
forall (a :: Kind). Eq a => a -> a -> Bool
== Free a a
Free a a
g2
    (Maybe (c :~: c), Maybe (a :~: a))
_ -> Bool
False
  Free a b
_ == Free a b
_ = Bool
False

class (Show2 p) => WithShow (a :: FREE c (p :: CAT j))
instance (Show2 p) => WithShow (a :: FREE c (p :: CAT j))

instance (WithShow a) => Show (Free a b) where
  showsPrec :: Int -> Free a b -> ShowS
showsPrec Int
_ Free a b
Id = String -> ShowS
P.showString String
"id"
  showsPrec Int
d (Emb p a b
p Free a ('EMB a)
g) = (Char -> Char) -> ShowS
forall (a :: Kind) (b :: Kind). (a -> b) -> [a] -> [b]
P.map Char -> Char
toLower ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> p a b -> Free a ('EMB a) -> ShowS
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d p a b
p Free a ('EMB a)
g
  showsPrec Int
d (Str Struct c a b
s Free a a
g) = (Char -> Char) -> ShowS
forall (a :: Kind) (b :: Kind). (a -> b) -> [a] -> [b]
P.map Char -> Char
toLower ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Struct c a b -> Free a a -> ShowS
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d Struct c a b
s Free a a
g

showPostComp :: (Show p, WithShow a) => P.Int -> p -> Free a b -> P.ShowS
showPostComp :: forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (p :: Kind) (a :: FREE cs p) (b :: FREE cs p).
(Show p, WithShow a) =>
Int -> p -> Free a b -> ShowS
showPostComp Int
d p
p Free a b
Id = Int -> p -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
d p
p
showPostComp Int
d p
p Free a b
g = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall (a :: Kind). Ord a => a -> a -> Bool
P.> Int
9) (Int -> p -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
10 p
p ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
P.showString String
" . " ShowS -> ShowS -> ShowS
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Free a b -> ShowS
forall (a :: Kind). Show a => Int -> a -> ShowS
P.showsPrec Int
10 Free a b
g)

type IsFreeOb :: forall {j} {cs :: [Kind -> Constraint]} {p :: CAT j}. FREE cs p -> Constraint
class IsFreeOb (a :: FREE cs (p :: CAT j)) where
  type Lower (f :: j +-> k) (a :: FREE cs p) :: k
  withLowerOb :: forall {k} (f :: j +-> k) r. (Representable f, All cs k) => ((Ob (Lower f (a :: FREE cs p))) => r) -> r
instance (Ob a, Typeable a) => IsFreeOb (EMB a) where
  type Lower f (EMB a) = f % a
  withLowerOb :: forall {k :: Kind} (f :: j +-> k) (r :: Kind).
(Representable f, All cs k) =>
(Ob (Lower f ('EMB a)) => r) -> r
withLowerOb @f = forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @f @a

class ((Ok cs p, Eq2 p) => Eq2 str, (Ok cs p) => Typeable str, (Show2 p) => Show2 str) => CanEqShow (str :: CAT (FREE cs p))
instance ((Ok cs p, Eq2 p) => Eq2 str, (Ok cs p) => Typeable str, (Show2 p) => Show2 str) => CanEqShow (str :: CAT (FREE cs p))

class
  (Typeable c, CanEqShow (Struct c :: CAT (FREE cs p)), c `Elem` cs) =>
  HasStructure cs (p :: CAT j) (c :: Kind -> Constraint)
  where
  data Struct c :: CAT (FREE cs p)
  foldStructure
    :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p)
     . (All cs k, Representable f)
    => (forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y)
    -> Struct c a b
    -> Lower f a ~> Lower f b

fold
  :: forall {j} {k} {p :: CAT j} (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p)
   . (All cs k, Representable f)
  => (forall x y. p x y -> (f % x) ~> (f % y))
  -> a ~> b
  -> Lower f a ~> Lower f b
fold :: forall {j :: Kind} {k :: Kind} {p :: CAT j}
       (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y)
pn = (a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go
  where
    go :: forall (x :: FREE cs p) y. x ~> y -> Lower f x ~> Lower f y
    go :: forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> y
Free x y
Id = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @x @f Lower f x ~> Lower f x
Ob (Lower f x) => Lower f x ~> Lower f x
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
    go (Emb p a b
p Free x ('EMB a)
g) = p a b -> (f % a) ~> (f % b)
forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y)
pn p a b
p ((f % a) ~> (f % b))
-> (Lower f x ~> (f % a)) -> Lower f x ~> (f % b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> 'EMB a) -> Lower f x ~> Lower f ('EMB a)
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> 'EMB a
Free x ('EMB a)
g
    go (Str Struct c a y
s Free x a
g) = forall (j :: Kind) (cs :: [Kind -> Constraint]) (p :: CAT j)
       (c :: Kind -> Constraint) {k :: Kind} (f :: j +-> k)
       (a :: FREE cs p) (b :: FREE cs p).
(HasStructure cs p c, All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct c a b -> Lower f a ~> Lower f b
foldStructure @_ @_ @_ @_ @f (x ~> y) -> Lower f x ~> Lower f y
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go Struct c a y
s (Lower f a ~> Lower f y)
-> (Lower f x ~> Lower f a) -> Lower f x ~> Lower f y
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> a) -> Lower f x ~> Lower f a
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go x ~> a
Free x a
g

retract
  :: forall {j} {k} cs (f :: j +-> k) a b
   . (All cs k, Representable f) => (a :: FREE cs InitialProfunctor) ~> b -> Lower f a ~> Lower f b
retract :: forall {j :: Kind} {k :: Kind} (cs :: [Kind -> Constraint])
       (f :: j +-> k) (a :: FREE cs InitialProfunctor)
       (b :: FREE cs InitialProfunctor).
(All cs k, Representable f) =>
(a ~> b) -> Lower f a ~> Lower f b
retract = forall (cs :: [Kind -> Constraint]) (f :: j +-> k)
       (a :: FREE cs InitialProfunctor) (b :: FREE cs InitialProfunctor).
(All cs k, Representable f) =>
(forall (x :: j) (y :: j).
 InitialProfunctor x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
forall {j :: Kind} {k :: Kind} {p :: CAT j}
       (cs :: [Kind -> Constraint]) (f :: j +-> k) (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: j) (y :: j). p x y -> (f % x) ~> (f % y))
-> (a ~> b) -> Lower f a ~> Lower f b
fold @cs @f (\case {})

instance (Ok cs p) => CategoryOf (FREE cs p) where
  type (~>) = Free
  type Ob a = (IsFreeOb a, Typeable a)

instance (Ok cs p) => Promonad (Free :: CAT (FREE cs p)) where
  id :: forall (a :: FREE cs p). Ob a => Free a a
id = Free a a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  Free b c
Id . :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g = Free a b
Free a c
g
  Free b c
f . Free a b
Id = Free b c
Free a c
f
  Emb p a b
p Free b ('EMB a)
f . Free a b
g = p a b -> Free a ('EMB a) -> Free a ('EMB b)
forall {j :: Kind} (a :: j) (b :: j) (p :: j -> j -> Kind)
       (cs :: [Kind -> Constraint]) (i :: FREE cs p).
(Ob a, Ob b, Typeable a, Typeable b) =>
p a b -> Free i ('EMB a) -> Free i ('EMB b)
Emb p a b
p (Free b ('EMB a)
f Free b ('EMB a) -> Free a b -> Free a ('EMB a)
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)
  Str Struct c a c
s Free b a
f . Free a b
g = Struct c a c -> Free a a -> Free a c
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct c a c
s (Free b a
f Free b a -> Free a b -> Free a a
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)

instance (Ok cs p) => Profunctor (Free :: CAT (FREE cs p)) where
  dimap :: forall (c :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p)
       (d :: FREE cs p).
(c ~> a) -> (b ~> d) -> Free a b -> Free c d
dimap = (c ~> a) -> (b ~> d) -> Free a b -> Free c d
Free c a -> Free b d -> Free a b -> Free c d
forall {k :: Kind} (p :: k +-> 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 :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a b
Id = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Emb p a b
_ Free a ('EMB a)
f = r
(Ob a, Ob b) => r
(Ob a, Ob ('EMB a)) => r
r ((Ob a, Ob ('EMB a)) => r) -> Free a ('EMB a) -> 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
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a ('EMB a)
f
  (Ob a, Ob b) => r
r \\ Str Struct c a b
_ Free a a
f = r
(Ob a, Ob b) => r
(Ob a, Ob a) => r
r ((Ob a, Ob a) => r) -> Free a a -> 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
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free a a
f

data family UnitF :: k
instance (Monoidal `Elem` cs) => IsFreeOb (UnitF :: FREE cs p) where
  type Lower f UnitF = Unit
  withLowerOb :: forall {k :: Kind} (f :: j +-> k) (r :: Kind).
(Representable f, All cs k) =>
(Ob (Lower f UnitF) => r) -> r
withLowerOb Ob (Lower f UnitF) => r
r = r
Ob (Lower f UnitF) => r
r
data family (**!) (a :: k) (b :: k) :: k
instance (Ob (a :: FREE cs p), Ob b, Monoidal `Elem` cs) => IsFreeOb (a **! b) where
  type Lower f (a **! b) = Lower f a ** Lower f b
  withLowerOb :: forall {k :: Kind} (f :: j +-> k) (r :: Kind).
(Representable f, All cs k) =>
(Ob (Lower f (a **! b)) => r) -> r
withLowerOb @f Ob (Lower f (a **! b)) => r
r = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Lower f a) @(Lower f b) r
Ob (Lower f a ** Lower f b) => r
Ob (Lower f (a **! b)) => r
r))
instance (Monoidal `Elem` cs) => HasStructure cs p Monoidal where
  data Struct Monoidal i o where
    Par0 :: Struct Monoidal UnitF UnitF
    Par :: a ~> b -> c ~> d -> Struct Monoidal (a **! c) (b **! d)
    LeftUnitor :: (Ob a) => Struct Monoidal (UnitF **! a) a
    LeftUnitorInv :: (Ob a) => Struct Monoidal a (UnitF **! a)
    RightUnitor :: (Ob a) => Struct Monoidal (a **! UnitF) a
    RightUnitorInv :: (Ob a) => Struct Monoidal a (a **! UnitF)
    Associator :: (Ob a, Ob b, Ob c) => Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
    AssociatorInv :: (Ob a, Ob b, Ob c) => Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
  foldStructure :: forall {k :: Kind} (f :: j +-> k) (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct Monoidal a b -> Lower f a ~> Lower f b
foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ Struct Monoidal a b
R:StructjcspMonoidalio j cs p a b
Par0 = Unit ~> Unit
Lower f a ~> Lower f b
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
MonoidalProfunctor p =>
p Unit Unit
par0
  foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (Par a ~> b
f c ~> d
g) = (a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go a ~> b
f (Lower f a ~> Lower f b)
-> (Lower f c ~> Lower f d)
-> (Lower f a ** Lower f c) ~> (Lower f b ** Lower f d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (c ~> d) -> Lower f c ~> Lower f d
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go c ~> d
g
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (LeftUnitor @a) = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (Unit ** Lower f b) ~> Lower f b
Ob (Lower f b) => (Unit ** Lower f b) ~> Lower f b
forall (a :: k). Ob a => (Unit ** a) ~> a
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (LeftUnitorInv @a) = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f Lower f a ~> (Unit ** Lower f a)
Ob (Lower f a) => Lower f a ~> (Unit ** Lower f a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (RightUnitor @a) = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (Lower f b ** Unit) ~> Lower f b
Ob (Lower f b) => (Lower f b ** Unit) ~> Lower f b
forall (a :: k). Ob a => (a ** Unit) ~> a
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (RightUnitorInv @a) = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f Lower f a ~> (Lower f a ** Unit)
Ob (Lower f a) => Lower f a ~> (Lower f a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Associator @a @b @c') = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @c' @f (forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @(Lower f a) @(Lower f b) @(Lower f c'))))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (AssociatorInv @a @b @c') = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @c' @f (forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @(Lower f a) @(Lower f b) @(Lower f c'))))
deriving instance (WithEq a) => Eq (Struct Monoidal a b)
deriving instance (WithShow a) => Show (Struct Monoidal a b)
instance (Ok cs p, Monoidal `Elem` cs) => MonoidalProfunctor (Free :: CAT (FREE cs p)) where
  par0 :: Free Unit Unit
par0 = Struct Monoidal UnitF UnitF -> Free UnitF UnitF -> Free UnitF UnitF
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal UnitF UnitF
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}.
Struct Monoidal UnitF UnitF
Par0 Free UnitF UnitF
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  Free x1 x2
f par :: forall (x1 :: FREE cs p) (x2 :: FREE cs p) (y1 :: FREE cs p)
       (y2 :: FREE cs p).
Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2)
`par` Free y1 y2
g = Struct Monoidal (x1 **! y1) (x2 **! y2)
-> Free (x1 **! y1) (x1 **! y1) -> Free (x1 **! y1) (x2 **! y2)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str ((x1 ~> x2) -> (y1 ~> y2) -> Struct Monoidal (x1 **! y1) (x2 **! y2)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p)
       (d :: FREE cs p).
(a ~> b) -> (c ~> d) -> Struct Monoidal (a **! c) (b **! d)
Par x1 ~> x2
Free x1 x2
f y1 ~> y2
Free y1 y2
g) Free (x1 **! y1) (x1 **! y1)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id ((Ob x1, Ob x2) => Free (x1 **! y1) (x2 **! y2))
-> Free x1 x2 -> Free (x1 **! y1) (x2 **! y2)
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
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free x1 x2
f ((Ob y1, Ob y2) => Free (x1 **! y1) (x2 **! y2))
-> Free y1 y2 -> Free (x1 **! y1) (x2 **! y2)
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
forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free y1 y2
g
instance (Ok cs p, Monoidal `Elem` cs) => Monoidal (FREE cs p) where
  type Unit = UnitF
  type a ** b = a **! b
  withOb2 :: forall (a :: FREE cs p) (b :: FREE cs p) (r :: Kind).
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: FREE cs p). Ob a => (Unit ** a) ~> a
leftUnitor = Struct Monoidal (UnitF **! a) a
-> Free (UnitF **! a) (UnitF **! a) -> Free (UnitF **! a) a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal (UnitF **! a) a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (UnitF **! a) a
LeftUnitor Free (UnitF **! a) (UnitF **! a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  leftUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> (Unit ** a)
leftUnitorInv = Struct Monoidal a (UnitF **! a) -> Free a a -> Free a (UnitF **! a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal a (UnitF **! a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (UnitF **! a)
LeftUnitorInv Free a a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  rightUnitor :: forall (a :: FREE cs p). Ob a => (a ** Unit) ~> a
rightUnitor = Struct Monoidal (a **! UnitF) a
-> Free (a **! UnitF) (a **! UnitF) -> Free (a **! UnitF) a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal (a **! UnitF) a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (a **! UnitF) a
RightUnitor Free (a **! UnitF) (a **! UnitF)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  rightUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> (a ** Unit)
rightUnitorInv = Struct Monoidal a (a **! UnitF) -> Free a a -> Free a (a **! UnitF)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal a (a **! UnitF)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (a **! UnitF)
RightUnitorInv Free a a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  associator :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
-> Free ((a **! b) **! c) ((a **! b) **! c)
-> Free ((a **! b) **! c) (a **! (b **! c))
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
Associator Free ((a **! b) **! c) ((a **! b) **! c)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  associatorInv :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
-> Free (a **! (b **! c)) (a **! (b **! c))
-> Free (a **! (b **! c)) ((a **! b) **! c)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
AssociatorInv Free (a **! (b **! c)) (a **! (b **! c))
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id

instance (SymMonoidal `Elem` cs) => HasStructure cs p SymMonoidal where
  data Struct SymMonoidal i o where
    Swap :: (Ob a, Ob b) => Struct SymMonoidal (a **! b) (b **! a)
  foldStructure :: forall {k :: Kind} (f :: j +-> k) (a :: FREE cs p)
       (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct SymMonoidal a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Swap @a @b) = forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k :: Kind} (f :: j +-> k) (r :: Kind).
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(Lower f a) @(Lower f b)))
deriving instance (WithEq a) => Eq (Struct SymMonoidal a b)
deriving instance (WithShow a) => Show (Struct SymMonoidal a b)
instance (Ok cs p, SymMonoidal `Elem` cs, Monoidal `Elem` cs) => SymMonoidal (FREE cs p) where
  swap :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = Struct SymMonoidal (a **! b) (b **! a)
-> Free (a **! b) (a **! b) -> Free (a **! b) (b **! a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: Kind -> Constraint) (b :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p a, Ob b, Ob b) =>
Struct a b b -> Free i b -> Free i b
Str Struct SymMonoidal (a **! b) (b **! a)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct SymMonoidal (a **! b) (b **! a)
Swap Free (a **! b) (a **! b)
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id