{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Preorder where

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

infixl 1 \\

type POS k = k -> k -> Constraint

data Dict a where
  Dict :: (a) => Dict a
newtype a :- b = Sub ((a) => Dict b)

(\\) :: (a) => ((c) => r) -> (a :- c) -> r
c => r
r \\ :: forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ Sub Dict c
a => Dict c
Dict = r
c => r
r

class (CPromonad ((<=) :: POS k)) => PreorderOf k where
  type (<=) :: POS k
  type COb (a :: k) :: Constraint
  type COb a = ()

type IsPosetOf k pos = (PreorderOf k, pos ~ (<=) @k, CPromonad pos)

class CProfunctor p where
  cdimap :: (c <= a, b <= d, p a b) :- p c d
  obs :: p a b :- (COb a, COb b)
class CProfunctor p => CPromonad p where
  cid :: (COb a) => () :- p a a
  ccomp :: forall a b c. (p b c, p a b) :- p a c

cdimapDefault :: forall p a b c d. (CPromonad p) => (p c a, p b d, p a b) :- p c d
cdimapDefault :: forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k)
       (d :: k).
CPromonad p =>
(p c a, p b d, p a b) :- p c d
cdimapDefault = ((p c a, p b d, p a b) => Dict (p c d))
-> (p c a, p b d, p a b) :- p c d
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict (p c d)
p c d => Dict (p c d)
forall (a :: Constraint). a => Dict a
Dict (p c d => Dict (p c d))
-> ((p b d, p c b) :- p c d) -> Dict (p c d)
forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
forall (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
ccomp @p @c @b @d (p c b => Dict (p c d))
-> ((p a b, p c a) :- p c b) -> Dict (p c d)
forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
forall (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
ccomp @p @c @a @b)