{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..), (:=>) (..), reifyExp, eqIsSuperOrd, maybeLiftsSemigroup) where

import Data.Kind (Constraint)
import GHC.Exts (withDict)
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), Monoid (..), CopyDiscard)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.BinaryProduct qualified as P
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Category.Enriched.ThinCategory (ThinProfunctor (..))

newtype CONSTRAINT = CNSTRNT Constraint
type instance UN CNSTRNT (CNSTRNT a) = a

data (:-) a b where
  Entails :: {forall (a :: Constraint) (b :: Constraint).
('CNSTRNT a :- 'CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails :: forall r. (a) => ((b) => r) -> r} -> CNSTRNT a :- CNSTRNT b

-- | The category of type class constraints. An arrow from constraint a to constraint b
-- | means that a implies b, i.e. if a holds then b holds.
instance CategoryOf CONSTRAINT where
  type (~>) = (:-)
  type Ob a = (Is CNSTRNT a)

instance Promonad (:-) where
  id :: forall (a :: CONSTRAINT). Ob a => a :- a
id = (forall r. UN 'CNSTRNT a => (UN 'CNSTRNT a => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (UN 'CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \UN 'CNSTRNT a => r
r -> r
UN 'CNSTRNT a => r
r
  Entails forall r. a => (b => r) -> r
f . :: forall (b :: CONSTRAINT) (c :: CONSTRAINT) (a :: CONSTRAINT).
(b :- c) -> (a :- b) -> a :- c
. Entails forall r. a => (b => r) -> r
g = (forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \b => r
r -> (b => r) -> r
forall r. a => (b => r) -> r
g ((b => r) -> r
forall r. a => (b => r) -> r
f r
b => r
r)

instance Profunctor (:-) where
  dimap :: forall (c :: CONSTRAINT) (a :: CONSTRAINT) (b :: CONSTRAINT)
       (d :: CONSTRAINT).
(c ~> a) -> (b ~> d) -> (a :- b) -> c :- d
dimap = (c ~> a) -> (b ~> d) -> (a :- b) -> c :- d
(c :- a) -> (b :- d) -> (a :- b) -> c :- d
forall {k} (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 :: CONSTRAINT) (b :: CONSTRAINT) r.
((Ob a, Ob b) => r) -> (a :- b) -> r
\\ Entails{} = r
(Ob a, Ob b) => r
r

instance ThinProfunctor (:-) where
  type HasArrow (:-) a b = UN CNSTRNT a :=> UN CNSTRNT b
  arr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b, HasArrow (:-) a b) =>
a :- b
arr @(CNSTRNT a) @(CNSTRNT b) = (forall r. UN 'CNSTRNT a => (UN 'CNSTRNT b => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (UN 'CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \UN 'CNSTRNT b => r
r -> ('CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (UN 'CNSTRNT b))
-> forall r. UN 'CNSTRNT a => (UN 'CNSTRNT b => r) -> r
forall (a :: Constraint) (b :: Constraint).
('CNSTRNT a :- 'CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails (forall (b :: Constraint) (c :: Constraint).
(b :=> c) =>
'CNSTRNT b :- 'CNSTRNT c
entails @a @b) r
UN 'CNSTRNT b => r
r
  withArr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(a :- b) -> (HasArrow (:-) a b => r) -> r
withArr p :: a :- b
p@Entails{} = ('CNSTRNT a :- 'CNSTRNT b) -> ((a :=> b) => r) -> r
forall (b :: Constraint) (c :: Constraint) r.
('CNSTRNT b :- 'CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp a :- b
'CNSTRNT a :- 'CNSTRNT b
p

instance HasTerminalObject CONSTRAINT where
  type TerminalObject = CNSTRNT ()
  terminate :: forall (a :: CONSTRAINT). Ob a => a ~> TerminalObject
terminate = (forall r. UN 'CNSTRNT a => ((() :: Constraint) => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, r)
  withObProd :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a && b) ~> a
fst = (forall r.
 (UN 'CNSTRNT a, UN 'CNSTRNT b) =>
 (UN 'CNSTRNT a => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a, UN 'CNSTRNT b)
   :- 'CNSTRNT (UN 'CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \UN 'CNSTRNT a => r
r -> r
UN 'CNSTRNT a => r
r
  snd :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a && b) ~> b
snd = (forall r.
 (UN 'CNSTRNT a, UN 'CNSTRNT b) =>
 (UN 'CNSTRNT b => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a, UN 'CNSTRNT b)
   :- 'CNSTRNT (UN 'CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \UN 'CNSTRNT b => r
r -> r
UN 'CNSTRNT b => r
r
  Entails forall r. a => (b => r) -> r
f &&& :: forall (a :: CONSTRAINT) (x :: CONSTRAINT) (y :: CONSTRAINT).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Entails forall r. a => (b => r) -> r
g = (forall r. a => ((b, b) => r) -> r)
-> 'CNSTRNT a :- 'CNSTRNT (b, b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(b, b) => r
r -> (b => r) -> r
forall r. a => (b => r) -> r
f ((b => r) -> r
forall r. a => (b => r) -> r
g r
b => r
(b, b) => r
r)

instance MonoidalProfunctor (:-) where
  par0 :: Unit :- Unit
par0 = Unit :- Unit
'CNSTRNT (() :: Constraint) :- 'CNSTRNT (() :: Constraint)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: CONSTRAINT). Ob a => a :- a
id
  x1 :- x2
f par :: forall (x1 :: CONSTRAINT) (x2 :: CONSTRAINT) (y1 :: CONSTRAINT)
       (y2 :: CONSTRAINT).
(x1 :- x2) -> (y1 :- y2) -> (x1 ** y1) :- (x2 ** y2)
`par` y1 :- y2
g = x1 ~> x2
x1 :- x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: CONSTRAINT) (b :: CONSTRAINT) (x :: CONSTRAINT)
       (y :: CONSTRAINT).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** y1 ~> y2
y1 :- y2
g

-- | Products as monoidal structure.
instance Monoidal CONSTRAINT where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: CONSTRAINT). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && 'CNSTRNT (UN 'CNSTRNT a))
~> 'CNSTRNT (UN 'CNSTRNT a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
P.leftUnitorProd
  leftUnitorInv :: forall (a :: CONSTRAINT). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'CNSTRNT (UN 'CNSTRNT a)
~> (TerminalObject && 'CNSTRNT (UN 'CNSTRNT a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
P.leftUnitorProdInv
  rightUnitor :: forall (a :: CONSTRAINT). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('CNSTRNT (UN 'CNSTRNT a) && TerminalObject)
~> 'CNSTRNT (UN 'CNSTRNT a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
P.rightUnitorProd
  rightUnitorInv :: forall (a :: CONSTRAINT). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'CNSTRNT (UN 'CNSTRNT a)
~> ('CNSTRNT (UN 'CNSTRNT a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
P.rightUnitorProdInv
  associator :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
(('CNSTRNT (UN 'CNSTRNT a) && 'CNSTRNT (UN 'CNSTRNT b))
 && 'CNSTRNT (UN 'CNSTRNT c))
~> ('CNSTRNT (UN 'CNSTRNT a)
    && ('CNSTRNT (UN 'CNSTRNT b) && 'CNSTRNT (UN 'CNSTRNT c)))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
P.associatorProd
  associatorInv :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
('CNSTRNT (UN 'CNSTRNT a)
 && ('CNSTRNT (UN 'CNSTRNT b) && 'CNSTRNT (UN 'CNSTRNT c)))
~> (('CNSTRNT (UN 'CNSTRNT a) && 'CNSTRNT (UN 'CNSTRNT b))
    && 'CNSTRNT (UN 'CNSTRNT c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
P.associatorProdInv

instance SymMonoidal CONSTRAINT where
  swap :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (forall r.
 (UN 'CNSTRNT a, UN 'CNSTRNT b) =>
 ((UN 'CNSTRNT b, UN 'CNSTRNT a) => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a, UN 'CNSTRNT b)
   :- 'CNSTRNT (UN 'CNSTRNT b, UN 'CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(UN 'CNSTRNT b, UN 'CNSTRNT a) => r
r -> r
(UN 'CNSTRNT b, UN 'CNSTRNT a) => r
r

instance Monoid (CNSTRNT ()) where
  mempty :: Unit ~> 'CNSTRNT (() :: Constraint)
mempty = Unit ~> 'CNSTRNT (() :: Constraint)
'CNSTRNT (() :: Constraint) :- 'CNSTRNT (() :: Constraint)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: CONSTRAINT). Ob a => a :- a
id
  mappend :: ('CNSTRNT (() :: Constraint) ** 'CNSTRNT (() :: Constraint))
~> 'CNSTRNT (() :: Constraint)
mappend = (forall r.
 (() :: Constraint, () :: Constraint) =>
 ((() :: Constraint) => r) -> r)
-> 'CNSTRNT (() :: Constraint, () :: Constraint)
   :- 'CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r

instance Comonoid (CNSTRNT a) where
  counit :: 'CNSTRNT a ~> Unit
counit = (forall r. a => ((() :: Constraint) => r) -> r)
-> 'CNSTRNT a :- 'CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r
  comult :: 'CNSTRNT a ~> ('CNSTRNT a ** 'CNSTRNT a)
comult = (forall r. a => ((a, a) => r) -> r)
-> 'CNSTRNT a :- 'CNSTRNT (a, a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(a, a) => r
r -> r
(a, a) => r
r
instance CopyDiscard CONSTRAINT

class b :=> c where
  entails :: CNSTRNT b :- CNSTRNT c
instance (b => c) => (b :=> c) where
  entails :: 'CNSTRNT b :- 'CNSTRNT c
entails = (forall r. b => (c => r) -> r) -> 'CNSTRNT b :- 'CNSTRNT c
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \c => r
r -> r
c => r
r

reifyExp :: forall b c r. CNSTRNT b :- CNSTRNT c -> ((b :=> c) => r) -> r
reifyExp :: forall (b :: Constraint) (c :: Constraint) r.
('CNSTRNT b :- 'CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(b :=> c)

instance Closed CONSTRAINT where
  type a ~~> b = CNSTRNT (UN CNSTRNT a :=> UN CNSTRNT b)
  withObExp :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(CNSTRNT b) (Entails @_ @c forall r. a => (b => r) -> r
f) = (forall r. UN 'CNSTRNT a => ((UN 'CNSTRNT b :=> b) => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (UN 'CNSTRNT b :=> b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(UN 'CNSTRNT b :=> b) => r
r -> ('CNSTRNT (UN 'CNSTRNT b) :- 'CNSTRNT b)
-> ((UN 'CNSTRNT b :=> b) => r) -> r
forall (b :: Constraint) (c :: Constraint) r.
('CNSTRNT b :- 'CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp (forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails @b @c (b => r) -> r
forall r. a => (b => r) -> r
forall {r}. UN 'CNSTRNT b => (b => r) -> r
f) r
(UN 'CNSTRNT b :=> b) => r
r
  apply :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(CNSTRNT a) @(CNSTRNT b) = (forall r.
 (UN 'CNSTRNT a :=> UN 'CNSTRNT b, UN 'CNSTRNT a) =>
 (UN 'CNSTRNT b => r) -> r)
-> 'CNSTRNT (UN 'CNSTRNT a :=> UN 'CNSTRNT b, UN 'CNSTRNT a)
   :- 'CNSTRNT (UN 'CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \UN 'CNSTRNT b => r
r -> ('CNSTRNT (UN 'CNSTRNT a) :- 'CNSTRNT (UN 'CNSTRNT b))
-> forall r. UN 'CNSTRNT a => (UN 'CNSTRNT b => r) -> r
forall (a :: Constraint) (b :: Constraint).
('CNSTRNT a :- 'CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails (forall (b :: Constraint) (c :: Constraint).
(b :=> c) =>
'CNSTRNT b :- 'CNSTRNT c
entails @a @b) r
UN 'CNSTRNT b => r
r

eqIsSuperOrd :: CNSTRNT (P.Ord a) :- CNSTRNT (P.Eq a)
eqIsSuperOrd :: forall a. 'CNSTRNT (Ord a) :- 'CNSTRNT (Eq a)
eqIsSuperOrd = (forall r. Ord a => (Eq a => r) -> r)
-> 'CNSTRNT (Ord a) :- 'CNSTRNT (Eq a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \Eq a => r
r -> r
Eq a => r
r

maybeLiftsSemigroup :: CNSTRNT (P.Semigroup a) :- CNSTRNT (Monoid (P.Maybe a))
maybeLiftsSemigroup :: forall a. 'CNSTRNT (Semigroup a) :- 'CNSTRNT (Monoid (Maybe a))
maybeLiftsSemigroup = (forall r. Semigroup a => (Monoid (Maybe a) => r) -> r)
-> 'CNSTRNT (Semigroup a) :- 'CNSTRNT (Monoid (Maybe a))
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \Monoid (Maybe a) => r
r -> r
Monoid (Maybe a) => r
r