module Proarrow.Object
  ( Obj
  , pattern Obj
  , pattern Objs
  , obj
  , src
  , tgt
  , Ob'
  , VacuusOb
  ) where

import Data.Kind (Type)

import Proarrow.Core (CategoryOf (..), Obj, obj, src, tgt, (\\), Profunctor)

class (Ob a, CategoryOf k) => Ob' (a :: k)
instance (Ob a, CategoryOf k) => Ob' (a :: k)
type VacuusOb k = forall a. Ob' (a :: k)

type ObjDict :: forall {k}. k -> Type
data ObjDict a where
  ObjDict :: (Ob a) => ObjDict a

objDict :: (Profunctor p) => p a a' -> (ObjDict a, ObjDict a')
objDict :: forall {k} {k} (p :: k +-> k) (a :: k) (a' :: k).
Profunctor p =>
p a a' -> (ObjDict a, ObjDict a')
objDict p a a'
a = (ObjDict a
(Ob a, Ob a') => ObjDict a
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a) -> p a a' -> ObjDict a
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 a a'
a, ObjDict a'
(Ob a, Ob a') => ObjDict a'
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a') -> p a a' -> ObjDict a'
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 a a'
a)

pattern Obj :: (CategoryOf k) => (Ob (a :: k)) => Obj a
pattern $bObj :: forall k (a :: k). (CategoryOf k, Ob a) => Obj a
$mObj :: forall {r} {k} {a :: k}.
CategoryOf k =>
Obj a -> (Ob a => r) -> ((# #) -> r) -> r
Obj <- (objDict -> (ObjDict, ObjDict))
  where
    Obj = Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
obj

{-# COMPLETE Obj #-}

pattern Objs :: (Profunctor p) => (Ob a, Ob b) => p a b
pattern $mObjs :: forall {r} {j} {k} {p :: j +-> k} {a :: k} {b :: j}.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> ((# #) -> r) -> r
Objs <- (objDict -> (ObjDict, ObjDict))

{-# COMPLETE Objs #-}