{-# HLINT ignore "Use id" #-}
{-# HLINT ignore "Avoid lambda" #-}
{-# HLINT ignore "Use const" #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

module Proarrow.Category.Instance.Constraint where

import Data.Kind (Constraint)
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 (..))
import Proarrow.Object (Obj)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.BinaryProduct qualified as P
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Preorder.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

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 ThinProfunctor (:-) where
  type HasArrow (:-) (CNSTRNT a) (CNSTRNT b) = a :=> b
  arr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b, HasArrow (:-) a b) =>
a :- b
arr = (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 a => UN 'CNSTRNT b) => r
r -> r
(UN 'CNSTRNT a => UN 'CNSTRNT b) => r
r
  withArr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(a :- b) -> (HasArrow (:-) a b => r) -> r
withArr (Entails forall r. ((a => b) => r) -> r
f) HasArrow (:-) a b => r
r = ((a => b) => r) -> r
forall r. ((a => b) => r) -> r
f r
HasArrow (:-) a b => r
(a => b) => r
r

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

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, 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, UN 'CNSTRNT b) => UN 'CNSTRNT a) => r
r -> r
((UN 'CNSTRNT a, UN 'CNSTRNT b) => 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 a, UN 'CNSTRNT b) => UN 'CNSTRNT b) => r
r -> r
((UN 'CNSTRNT a, UN 'CNSTRNT b) => 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 \(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 MonoidalProfunctor (:-) where
  par0 :: Unit :- Unit
par0 = Unit :- Unit
'CNSTRNT (() :: Constraint) :- 'CNSTRNT (() :: Constraint)
forall {k} (p :: PRO 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

instance Monoidal CONSTRAINT where
  type Unit = TerminalObject
  type a ** b = a && b
  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) (a' :: CONSTRAINT) (b :: CONSTRAINT)
       (b' :: CONSTRAINT).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Entails forall r. ((a => b) => r) -> r
f) (Entails forall r. ((a => b) => r) -> r
g) = (forall r. (((a, a) => (b, b)) => r) -> r)
-> 'CNSTRNT (a, a) :- 'CNSTRNT (b, b)
forall (a :: Constraint) (b :: Constraint).
(forall r. ((a => b) => r) -> r) -> 'CNSTRNT a :- 'CNSTRNT b
Entails \((a, 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) => r
((a, a) => (b, b)) => r
r)

instance Monoid (CNSTRNT ()) where
  mempty :: Unit ~> 'CNSTRNT (() :: Constraint)
mempty = Unit ~> 'CNSTRNT (() :: Constraint)
'CNSTRNT (() :: Constraint) :- 'CNSTRNT (() :: Constraint)
forall {k} (p :: PRO 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, () :: Constraint) => () :: Constraint) => r
r -> r
((() :: Constraint, () :: Constraint) => () :: 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 \(a => () :: Constraint) => r
r -> r
(a => () :: 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, a)) => r
r -> r
(a => (a, a)) => 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 (P.Ord a) :- CNSTRNT (P.Eq a)
-- eqIsSuperOrd = Entails \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 \(Semigroup a => Monoid (Maybe a)) => r
r -> r
(Semigroup a => Monoid (Maybe a)) => r
r