content: {-# Language CPP               #-}
  {-# Language DataKinds         #-}
  {-# Language RankNTypes        #-}
  {-# Language PatternSynonyms   #-}
  {-# Language TypeOperators     #-}
  {-# Language PolyKinds         #-}
  {-# Language GADTs             #-}
  {-# Language TypeFamilies      #-}
  {-# Language TypeApplications  #-}
  {-# Language FlexibleContexts  #-}
  {-# Language FlexibleInstances #-}
  {-# Language InstanceSigs      #-}
  
  module T15799 where
  import qualified GHC.TypeLits as TypeLits
  import GHC.TypeLits (Nat, KnownNat)
  import Data.Kind
  
  data Op obj = Op obj
  
  type family
   UnOp (op_a :: Op obj) :: obj where
   UnOp ('Op obj) = obj
  
  class
   Ríki (obj :: Type) where
   type (-->) :: Op obj -> obj -> Type
   type (<--) :: obj -> Op obj -> Type
  
   unop :: forall (a :: obj) (b :: obj). (a <-- 'Op b) -> ('Op b --> a)
  
  data (<=) :: Op Nat -> Nat -> Type where
    LessThan :: (KnownNat (UnOp op_a), KnownNat b, UnOp op_a TypeLits.<= b)
             => (op_a <= b)
  
  newtype (>=) :: Nat -> Op Nat -> Type where
    Y :: (a <= b) -> (b >= a)
  
  instance Ríki Nat where
   type (-->) = (<=)
   type (<--) = (>=)
  
   unop :: (a >= b) -> (b <= a)
   unop GreaterThan = LessThan
  
  pattern GreaterThan :: () => (KnownNat (UnOp b), KnownNat a, UnOp b <= a) => a >= b
  pattern GreaterThan = Y LessThan
  