{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Enriched where

import Data.Kind (Constraint, Type)
import Prelude (($), type (~))

import Proarrow.Category.Bicategory (Bicategory (I, O), Monad (..))
import Proarrow.Category.Bicategory.MonoidalAsBi (Mon2 (..), MonK (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Promonad (..), UN)
import Proarrow.Object.BinaryProduct ()
-- import Proarrow.Preorder (PreorderOf(..), CPromonad(..), (\\), POS)
-- import Proarrow.Category.Instance.PreorderAsCategory (POCATK(..), PoAsCat (..))

type family V (vk :: k -> Type) :: CAT k
type family Arr (v :: CAT k) (a :: vk exta) (b :: vk extb) :: v exta extb
type (a :: vk exta) %~> (b :: vk extb) = Arr (V vk) a b

class (Bicategory (V vk)) => ECategory (vk :: k -> Type) where
  type EOb (a :: vk exta) :: Constraint
  eid :: (EOb (a :: vk exta)) => I ~> a %~> a
  ecomp
    :: (EOb (a :: vk exta), EOb (b :: vk extb), EOb (c :: vk extc))
    => ((b :: vk extb) %~> c) `O` (a %~> b) ~> a %~> c

type CATK :: Kind -> () -> Kind
data CATK k ext where
  CK :: k -> CATK k i
type instance UN CK (CK a) = a

type instance V (CATK k) = MonK Type
type instance Arr (MonK Type) (CK a) (CK b) = MK (a ~> b)

-- | A regular category as a Type-enriched category
instance (CategoryOf k) => ECategory (CATK k) where
  type EOb (a :: CATK k exta) = (Is CK a, Ob (UN CK a))
  eid :: forall (exta :: ()) (a :: CATK k exta). EOb a => I ~> (a %~> a)
eid = (() ~> (UN 'CK a ~> UN 'CK a))
-> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((() ~> (UN 'CK a ~> UN 'CK a))
 -> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a)))
-> (() ~> (UN 'CK a ~> UN 'CK a))
-> Mon2 ('MK ()) ('MK (UN 'CK a ~> UN 'CK a))
forall a b. (a -> b) -> a -> b
$ \() -> UN 'CK a ~> UN 'CK a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  ecomp :: forall (exta :: ()) (a :: CATK k exta) (extb :: ())
       (b :: CATK k extb) (extc :: ()) (c :: CATK k extc).
(EOb a, EOb b, EOb c) =>
O (b %~> c) (a %~> b) ~> (a %~> c)
ecomp = ((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
 ~> (UN 'CK a ~> UN 'CK c))
-> Mon2
     ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
     ('MK (UN 'CK a ~> UN 'CK c))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 (((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
  ~> (UN 'CK a ~> UN 'CK c))
 -> Mon2
      ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
      ('MK (UN 'CK a ~> UN 'CK c)))
-> ((UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b)
    ~> (UN 'CK a ~> UN 'CK c))
-> Mon2
     ('MK (UN 'CK b ~> UN 'CK c, UN 'CK a ~> UN 'CK b))
     ('MK (UN 'CK a ~> UN 'CK c))
forall a b. (a -> b) -> a -> b
$ \(UN 'CK b ~> UN 'CK c
f, UN 'CK a ~> UN 'CK b
g) -> UN 'CK b ~> UN 'CK c
f (UN 'CK b ~> UN 'CK c)
-> (UN 'CK a ~> UN 'CK b) -> UN 'CK a ~> UN 'CK c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN 'CK a ~> UN 'CK b
g

-- type POSK :: Kind -> () -> Kind
-- data POSK k ext where
--   PK :: k -> POSK k i
-- type instance UN PK (PK a) = a

-- type instance V (POSK k) = MonK (POCATK Constraint)
-- type instance Arr (MonK (POCATK Constraint)) a b = MK (PC (UN PK a <= UN PK b))

-- -- | A poset as a Constraint-enriched category
-- instance (PreorderOf k) => ECategory (POSK k) where
--   type EOb (a :: POSK k exta) = (Is PK a, COb (UN PK a))
--   eid @_ @a = Mon2 $ PoAsCat \\ (cid @((<=) :: POS k) @(UN PK a))
--   ecomp @_ @a @_ @b @_ @c = Mon2 $ _ -- PoAsCat \\ (ccomp @((<=) :: POS k) @(UN PK a) @(UN PK b) @(UN PK c))


type MONADK :: forall {k} {kk} {a}. kk (a :: k) a -> k -> Type
data MONADK t ext where
  MDK :: () -> MONADK (t :: kk a a) exta

type instance V (MONADK (t :: kk a a)) = kk
type instance Arr kk (m :: MONADK (t :: kk a a) a) (n :: MONADK t a) = t

-- | A monad in a bicategory as a one object enriched category
instance (Monad t) => ECategory (MONADK (t :: kk a a)) where
  type EOb (m :: MONADK (t :: kk a a) exta) = (Is MDK m, exta ~ a)
  eid :: forall (exta :: k) (a :: MONADK t exta). EOb a => I ~> (a %~> a)
eid = I ~> t
I ~> Arr (V (MONADK t)) a a
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  ecomp :: forall (exta :: k) (a :: MONADK t exta) (extb :: k)
       (b :: MONADK t extb) (extc :: k) (c :: MONADK t extc).
(EOb a, EOb b, EOb c) =>
O (b %~> c) (a %~> b) ~> (a %~> c)
ecomp = O t t ~> t
O (Arr (V (MONADK t)) b c) (Arr (V (MONADK t)) a b)
~> Arr (V (MONADK t)) a c
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu