{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use id" #-}
{-# HLINT ignore "Avoid lambda" #-}
{-# HLINT ignore "Use const" #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Instance.Constraint where

import Data.Kind (Constraint)

import Proarrow.Core (UN, Is, CategoryOf(..), Profunctor(..), Promonad(..), dimapDefault)
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..))
import Proarrow.Object.BinaryProduct qualified as P
import Prelude (Semigroup, Monoid, Maybe)
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal (..))
import Proarrow.Object.Exponential (Closed(..))
import Proarrow.Object (Obj)


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
getEntails :: forall r. ((a => b) => r) -> r } -> CNSTRNT a :- CNSTRNT b

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 => UN 'CNSTRNT a) => r
r -> r
(UN 'CNSTRNT a => 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 \(a => b) => r
r -> ((a => b) => r) -> r
forall r. ((a => b) => r) -> r
f (((a => b) => r) -> r
forall r. ((a => b) => r) -> r
g r
(a => b) => r
(a => 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 :: PRO 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 HasTerminalObject CONSTRAINT where
  type TerminalObject = CNSTRNT ()
  terminate' :: forall (a :: CONSTRAINT). Obj a -> a ~> TerminalObject
terminate' Entails{} = (forall r. ((b => () :: Constraint) => r) -> r)
-> 'CNSTRNT b :- 'CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \(b => () :: Constraint) => r
r -> r
(b => () :: Constraint) => r
r

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, r)
  fst' :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
Obj a -> Obj b -> (a && b) ~> a
fst' Entails{} Entails{} = (forall r. (((b, b) => b) => r) -> r)
-> 'CNSTRNT (b, b) :- 'CNSTRNT b
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \((b, b) => b) => r
r -> r
((b, b) => b) => r
r
  snd' :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
Obj a -> Obj b -> (a && b) ~> b
snd' Entails{} Entails{} = (forall r. (((b, b) => b) => r) -> r)
-> 'CNSTRNT (b, b) :- 'CNSTRNT b
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \((b, b) => b) => r
r -> r
((b, b) => 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 \(a => (b, b)) => r
r -> ((a => b) => r) -> r
forall r. ((a => b) => r) -> r
f (((a => b) => r) -> r
forall r. ((a => b) => r) -> r
g r
(a => (b, b)) => r
(a => b) => r
r)

instance Monoidal CONSTRAINT where
  type Unit = TerminalObject
  type a ** b = a && b
  a ~> b
f par :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT)
       (d :: CONSTRAINT).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g = a ~> b
f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d)
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)
*** c ~> d
g
  leftUnitor :: forall (a :: CONSTRAINT). Obj a -> (Unit ** a) ~> a
leftUnitor = (a ~> a) -> (Unit ** a) ~> a
(a ~> a) -> (TerminalObject && a) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (TerminalObject && a) ~> a
P.leftUnitorProd
  leftUnitorInv :: forall (a :: CONSTRAINT). Obj a -> a ~> (Unit ** a)
leftUnitorInv = (a ~> a) -> a ~> (Unit ** a)
(a ~> a) -> a ~> (TerminalObject && a)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (TerminalObject && a)
P.leftUnitorProdInv
  rightUnitor :: forall (a :: CONSTRAINT). Obj a -> (a ** Unit) ~> a
rightUnitor = (a ~> a) -> (a ** Unit) ~> a
(a ~> a) -> (a && TerminalObject) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (a && TerminalObject) ~> a
P.rightUnitorProd
  rightUnitorInv :: forall (a :: CONSTRAINT). Obj a -> a ~> (a ** Unit)
rightUnitorInv = (a ~> a) -> a ~> (a ** Unit)
(a ~> a) -> a ~> (a && TerminalObject)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (a && TerminalObject)
P.rightUnitorProdInv
  associator :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator = (a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c))
(a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c))
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c))
P.associatorProd
  associatorInv :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ~> a)
-> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c)
(a ~> a)
-> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c)
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c)
P.associatorProdInv

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

class (b => c) => b :=> c
instance (b => c) => b :=> c

instance Closed CONSTRAINT where
  type CNSTRNT a ~~> CNSTRNT b = CNSTRNT (a :=> b)
  (^^^) :: forall (a :: CONSTRAINT) b x y. (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
  Entails forall r. ((a => b) => r) -> r
f ^^^ :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (x :: CONSTRAINT)
       (y :: CONSTRAINT).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Entails forall r. ((a => b) => r) -> r
g = (forall r. (((b :=> a) => a :=> b) => r) -> r)
-> 'CNSTRNT (b :=> a) :- 'CNSTRNT (a :=> b)
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \((b :=> a) => a :=> b) => r
r -> ((a => b) => r) -> r
forall r. ((a => b) => r) -> r
f (((a => b) => r) -> r
forall r. ((a => b) => r) -> r
g r
(a => b) => r
((b :=> a) => a :=> b) => r
r)
  curry' :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Entails{} Entails{} (Entails forall r. ((a => b) => r) -> r
f) = (forall r. ((b => b :=> b) => r) -> r)
-> 'CNSTRNT b :- 'CNSTRNT (b :=> b)
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails ((b => b :=> b) => r) -> r
((a => b) => r) -> r
forall r. ((b => b :=> b) => r) -> r
forall r. ((a => b) => r) -> r
f
  uncurry' :: forall (a :: CONSTRAINT) b c. Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
  uncurry' :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Entails{} Entails{} (Entails forall r. ((a => b) => r) -> r
f) = (forall r. (((a, b) => b) => r) -> r)
-> 'CNSTRNT (a, b) :- 'CNSTRNT b
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails (forall (x :: Constraint) (y :: Constraint) (z :: Constraint) r.
(((x => y :=> z) => r) -> r) -> (((x, y) => z) => r) -> r
h @(UN CNSTRNT a) @(UN CNSTRNT b) @(UN CNSTRNT c) ((a => b) => r) -> r
((UN 'CNSTRNT a => UN 'CNSTRNT b :=> UN 'CNSTRNT c) => r) -> r
forall r. ((a => b) => r) -> r
f)
    where
      h :: (((x => y :=> z) => r) -> r) -> (((x, y) => z) => r) -> r
      h :: forall (x :: Constraint) (y :: Constraint) (z :: Constraint) r.
(((x => y :=> z) => r) -> r) -> (((x, y) => z) => r) -> r
h ((x => y :=> z) => r) -> r
g = ((x => y :=> z) => r) -> r
(((x, y) => z) => r) -> r
g

-- I am solving the constraint ‘Eq a’ in a way that might turn out to loop at runtime.
-- See § Undecidable instances and loopy superclasses.
-- eqIsSuperOrd :: CNSTRNT (Ord a) :- CNSTRNT (Eq a)
-- eqIsSuperOrd = Entails \r -> r

maybeLiftsSemigroup :: CNSTRNT (Semigroup a) :- CNSTRNT (Monoid (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 \(Semigroup a => Monoid (Maybe a)) => r
r -> r
(Semigroup a => Monoid (Maybe a)) => r
r