content: {-# LANGUAGE
      DataKinds,
      PolyKinds,
      TypeFamilies,
      TypeOperators,
      UndecidableInstances #-}
  
  -- | Equality and ordering.
  --
  -- Note that equality doesn't really require a class,
  -- it can be defined uniformly as 'TyEq'.
  module Fcf.Class.Ord
    ( -- * Order
      Compare
    , type (<=)
    , type (>=)
    , type (<)
    , type (>)
  
      -- * Equality
    , TyEq
    ) where
  
  import qualified GHC.TypeLits as TL
  
  import Fcf.Core
  import Fcf.Class.Monoid (type (<>))  -- Semigroup Ordering
  import Fcf.Data.Bool (Not)
  import Fcf.Utils (TyEq)
  
  -- $setup
  -- >>> import Fcf.Core (Eval)
  
  -- | Type-level 'compare' for totally ordered data types.
  --
  -- === __Example__
  --
  -- >>> :kind! Eval (Compare "a" "b")
  -- Eval (Compare "a" "b") :: Ordering
  -- = LT
  --
  -- >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
  -- Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
  -- = EQ
  --
  -- >>> :kind! Eval (Compare '[1, 3] '[1, 2])
  -- Eval (Compare '[1, 3] '[1, 2]) :: Ordering
  -- = GT
  data Compare :: a -> a -> Exp Ordering
  
  -- (,)
  type instance Eval (Compare '(a1, a2) '(b1, b2)) = Eval (Compare a1 b1) <> Eval (Compare a2 b2)
  
  -- (,,)
  type instance Eval (Compare '(a1, a2, a3) '(b1, b2, b3))
    = Eval (Compare a1 b1) <> Eval (Compare a2 b2) <> Eval (Compare a3 b3)
  
  -- Either
  type instance Eval (Compare ('Left a) ('Left b)) = Eval (Compare a b)
  type instance Eval (Compare ('Right a) ('Right b)) = Eval (Compare a b)
  type instance Eval (Compare ('Left _a) ('Right _b)) = 'LT
  type instance Eval (Compare ('Right _a) ('Left _b)) = 'GT
  
  -- Maybe
  type instance Eval (Compare 'Nothing 'Nothing) = 'EQ
  type instance Eval (Compare ('Just a) ('Just b)) = Eval (Compare a b)
  type instance Eval (Compare 'Nothing ('Just _b)) = 'LT
  type instance Eval (Compare ('Just _a) 'Nothing) = 'GT
  
  -- List
  type instance Eval (Compare '[] '[]) = 'EQ
  type instance Eval (Compare (x ': xs) (y ': ys)) = Eval (Compare x y) <> Eval (Compare xs ys)
  type instance Eval (Compare '[] (_y ': _ys)) = 'LT
  type instance Eval (Compare (_x ': _xs) '[]) = 'GT
  
  -- Bool
  type instance Eval (Compare (a :: Bool) a) = 'EQ
  type instance Eval (Compare 'False 'True) = 'GT
  type instance Eval (Compare 'True 'False) = 'GT
  
  -- Ordering
  type instance Eval (Compare (a :: Ordering) a) = 'EQ
  type instance Eval (Compare 'LT 'EQ) = 'LT
  type instance Eval (Compare 'LT 'GT) = 'LT
  type instance Eval (Compare 'EQ 'GT) = 'LT
  type instance Eval (Compare 'EQ 'LT) = 'GT
  type instance Eval (Compare 'GT 'LT) = 'GT
  type instance Eval (Compare 'GT 'EQ) = 'GT
  
  -- Symbol
  type instance Eval (Compare a b) = TL.CmpSymbol a b
  
  -- Nat
  type instance Eval (Compare a b) = TL.CmpNat a b
  
  -- ()
  type instance Eval (Compare (a :: ()) b) = 'EQ
  
  -- * Derived operations
  
  -- Asymmetric comparison operators @Exp a -> a -> Bool@.
  type a ~== b = Eval (TyEq (Eval a) b)
  type a ~/= b = Eval (Not (a ~== b))
  
  -- | "Smaller than or equal to". Type-level version of @('<=')@.
  --
  -- === __Example__
  --
  -- >>> :kind! Eval ("b" <= "a")
  -- Eval ("b" <= "a") :: Bool
  -- = False
  data (<=) :: a -> a -> Exp Bool
  type instance Eval ((<=) a b) = Compare a b ~/= 'GT
  
  -- | "Greater than or equal to". Type-level version of @('>=')@.
  --
  -- === __Example__
  --
  -- >>> :kind! Eval ("b" >= "a")
  -- Eval ("b" >= "a") :: Bool
  -- = True
  data (>=) :: a -> a -> Exp Bool
  type instance Eval ((>=) a b) = Compare a b ~/= 'LT
  
  -- | "Smaller than". Type-level version of @('<')@.
  --
  -- === __Example__
  --
  -- >>> :kind! Eval ("a" < "b")
  -- Eval ("a" < "b") :: Bool
  -- = True
  data (<) :: a -> a -> Exp Bool
  type instance Eval ((<) a b) = Compare a b ~== 'LT
  
  -- | "Greater than". Type-level version of @('>')@.
  --
  -- === __Example__
  --
  -- >>> :kind! Eval ("b" > "a")
  -- Eval ("b" > "a") :: Bool
  -- = True
  data (>) :: a -> a -> Exp Bool
  type instance Eval ((>) a b) = Compare a b ~== 'GT
  