{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Preorder.Constraint where

import Data.Kind (Constraint)

import Proarrow.Preorder (CProfunctor (..), CPromonad (..), Dict (..), POS, PreorderOf (..), type (:-) (..))

class ((a) => b) => a :=> b where
  entails :: a :- b
instance ((a) => b) => a :=> b where
  entails :: a :- b
entails = (a => Dict b) -> a :- b
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict b
a => Dict b
forall (a :: Constraint). a => Dict a
Dict

instance CProfunctor ((:=>) :: POS Constraint) where
  cdimap :: forall (c :: Constraint) (a :: Constraint) (b :: Constraint)
       (d :: Constraint).
(c <= a, b <= d, a :=> b) :- (c :=> d)
cdimap = ((c :=> a, b :=> d, a :=> b) => Dict (c :=> d))
-> (c :=> a, b :=> d, a :=> b) :- (c :=> d)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (c :=> d)
(c :=> a, b :=> d, a :=> b) => Dict (c :=> d)
forall (a :: Constraint). a => Dict a
Dict
  obs :: forall (a :: Constraint) (b :: Constraint).
(a :=> b) :- (COb a, COb b)
obs = ((a :=> b) => Dict (() :: Constraint, () :: Constraint))
-> (a :=> b) :- (() :: Constraint, () :: Constraint)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (() :: Constraint, () :: Constraint)
(a :=> b) => Dict (() :: Constraint, () :: Constraint)
forall (a :: Constraint). a => Dict a
Dict
instance CPromonad ((:=>) :: POS Constraint) where
  cid :: forall (a :: Constraint). COb a => (() :: Constraint) :- (a :=> a)
cid = ((() :: Constraint) => Dict (a :=> a))
-> (() :: Constraint) :- (a :=> a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (a :=> a)
(() :: Constraint) => Dict (a :=> a)
forall (a :: Constraint). a => Dict a
Dict
  ccomp :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
(b :=> c, a :=> b) :- (a :=> c)
ccomp = ((b :=> c, a :=> b) => Dict (a :=> c))
-> (b :=> c, a :=> b) :- (a :=> c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (a :=> c)
(b :=> c, a :=> b) => Dict (a :=> c)
forall (a :: Constraint). a => Dict a
Dict
instance PreorderOf Constraint where
  type (<=) = (:=>)