Add cmpNat, cmpSymbol, and cmpChar

Add Data.Type.Ord
Add and update tests
Metric Increase:
    MultiLayerModules

15 files changed, 317 insertions, 137 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 2dc6e47493..6f9aec86cb 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -555,7 +555,8 @@ gHC_PRIM, gHC_PRIM_PANIC, gHC_PRIM_EXCEPTION,
     tYPEABLE, tYPEABLE_INTERNAL, gENERICS,
     rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, mONAD_ZIP, mONAD_FAIL,
     aRROW, cONTROL_APPLICATIVE, gHC_DESUGAR, rANDOM, gHC_EXTS,
-    cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_TYPENATS, dATA_TYPE_EQUALITY,
+    cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_TYPELITS_INTERNAL,
+    gHC_TYPENATS, gHC_TYPENATS_INTERNAL, dATA_TYPE_EQUALITY,
     dATA_COERCE, dEBUG_TRACE, uNSAFE_COERCE :: Module
 
 gHC_PRIM        = mkPrimModule (fsLit "GHC.Prim")   -- Primitive types and values
@@ -618,7 +619,9 @@ gHC_EXTS        = mkBaseModule (fsLit "GHC.Exts")
 cONTROL_EXCEPTION_BASE = mkBaseModule (fsLit "Control.Exception.Base")
 gHC_GENERICS    = mkBaseModule (fsLit "GHC.Generics")
 gHC_TYPELITS    = mkBaseModule (fsLit "GHC.TypeLits")
+gHC_TYPELITS_INTERNAL = mkBaseModule (fsLit "GHC.TypeLits.Internal")
 gHC_TYPENATS    = mkBaseModule (fsLit "GHC.TypeNats")
+gHC_TYPENATS_INTERNAL = mkBaseModule (fsLit "GHC.TypeNats.Internal")
 dATA_TYPE_EQUALITY = mkBaseModule (fsLit "Data.Type.Equality")
 dATA_COERCE     = mkBaseModule (fsLit "Data.Coerce")
 dEBUG_TRACE     = mkBaseModule (fsLit "Debug.Trace")
@@ -1991,7 +1994,7 @@ uWordTyConKey   = mkPreludeTyConUnique 163
 -- Type-level naturals
 typeSymbolKindConNameKey, typeCharKindConNameKey,
   typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
-  typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
+  typeNatSubTyFamNameKey
   , typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey, typeCharCmpTyFamNameKey
   , typeLeqCharTyFamNameKey
   , typeNatDivTyFamNameKey
@@ -2004,7 +2007,6 @@ typeCharKindConNameKey    = mkPreludeTyConUnique 166
 typeNatAddTyFamNameKey    = mkPreludeTyConUnique 167
 typeNatMulTyFamNameKey    = mkPreludeTyConUnique 168
 typeNatExpTyFamNameKey    = mkPreludeTyConUnique 169
-typeNatLeqTyFamNameKey    = mkPreludeTyConUnique 170
 typeNatSubTyFamNameKey    = mkPreludeTyConUnique 171
 typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 172
 typeNatCmpTyFamNameKey    = mkPreludeTyConUnique 173
diff --git a/compiler/GHC/Builtin/Types/Literals.hs b/compiler/GHC/Builtin/Types/Literals.hs
index 59fd758293..6b21a68bd3 100644
--- a/compiler/GHC/Builtin/Types/Literals.hs
+++ b/compiler/GHC/Builtin/Types/Literals.hs
@@ -11,7 +11,6 @@ module GHC.Builtin.Types.Literals
   , typeNatAddTyCon
   , typeNatMulTyCon
   , typeNatExpTyCon
-  , typeNatLeqTyCon
   , typeNatSubTyCon
   , typeNatDivTyCon
   , typeNatModTyCon
@@ -40,11 +39,12 @@ import GHC.Builtin.Types
 import GHC.Builtin.Types.Prim  ( mkTemplateAnonTyConBinders )
 import GHC.Builtin.Names
                   ( gHC_TYPELITS
+                  , gHC_TYPELITS_INTERNAL
                   , gHC_TYPENATS
+                  , gHC_TYPENATS_INTERNAL
                   , typeNatAddTyFamNameKey
                   , typeNatMulTyFamNameKey
                   , typeNatExpTyFamNameKey
-                  , typeNatLeqTyFamNameKey
                   , typeNatSubTyFamNameKey
                   , typeNatDivTyFamNameKey
                   , typeNatModTyFamNameKey
@@ -57,7 +57,6 @@ import GHC.Builtin.Names
                   , typeUnconsSymbolTyFamNameKey
                   )
 import GHC.Data.FastString
-import Data.Maybe ( isJust )
 import Control.Monad ( guard )
 import Data.List  ( isPrefixOf, isSuffixOf )
 
@@ -146,7 +145,6 @@ typeNatTyCons =
   [ typeNatAddTyCon
   , typeNatMulTyCon
   , typeNatExpTyCon
-  , typeNatLeqTyCon
   , typeNatSubTyCon
   , typeNatDivTyCon
   , typeNatModTyCon
@@ -236,24 +234,7 @@ typeNatLogTyCon = mkTypeNatFunTyCon1 name
   name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Log2")
             typeNatLogTyFamNameKey typeNatLogTyCon
 
-typeNatLeqTyCon :: TyCon
-typeNatLeqTyCon =
-  mkFamilyTyCon name
-    (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
-    boolTy
-    Nothing
-    (BuiltInSynFamTyCon ops)
-    Nothing
-    NotInjective
 
-  where
-  name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "<=?")
-                typeNatLeqTyFamNameKey typeNatLeqTyCon
-  ops = BuiltInSynFamily
-    { sfMatchFam      = matchFamLeq
-    , sfInteractTop   = interactTopLeq
-    , sfInteractInert = interactInertLeq
-    }
 
 typeNatCmpTyCon :: TyCon
 typeNatCmpTyCon =
@@ -266,7 +247,7 @@ typeNatCmpTyCon =
     NotInjective
 
   where
-  name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "CmpNat")
+  name = mkWiredInTyConName UserSyntax gHC_TYPENATS_INTERNAL (fsLit "CmpNat")
                 typeNatCmpTyFamNameKey typeNatCmpTyCon
   ops = BuiltInSynFamily
     { sfMatchFam      = matchFamCmpNat
@@ -285,7 +266,7 @@ typeSymbolCmpTyCon =
     NotInjective
 
   where
-  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol")
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS_INTERNAL (fsLit "CmpSymbol")
                 typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
   ops = BuiltInSynFamily
     { sfMatchFam      = matchFamCmpSymbol
@@ -383,7 +364,6 @@ Built-in rules axioms
 axAddDef
   , axMulDef
   , axExpDef
-  , axLeqDef
   , axCmpNatDef
   , axCmpSymbolDef
   , axAppendSymbolDef
@@ -398,10 +378,8 @@ axAddDef
   , axExp1L
   , axExp0R
   , axExp1R
-  , axLeqRefl
   , axCmpNatRefl
   , axCmpSymbolRefl
-  , axLeq0L
   , axSubDef
   , axSub0R
   , axAppendSymbol0R
@@ -422,9 +400,6 @@ axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon isNumLitTy isNumLitTy $
 axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon isNumLitTy isNumLitTy $
               \x y -> Just $ num (x ^ y)
 
-axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon isNumLitTy isNumLitTy $
-              \x y -> Just $ bool (x <= y)
-
 axCmpNatDef   = mkBinAxiom "CmpNatDef" typeNatCmpTyCon isNumLitTy isNumLitTy
               $ \x y -> Just $ ordering (compare x y)
 
@@ -489,12 +464,10 @@ axMod1      = mkAxiom1 "Mod1"     $ \(Pair s _) -> (tMod s (num 1) === num 0)
 axExp1L     = mkAxiom1 "Exp1L"    $ \(Pair s _) -> (num 1 .^. s) === num 1
 axExp0R     = mkAxiom1 "Exp0R"    $ \(Pair s _) -> (s .^. num 0) === num 1
 axExp1R     = mkAxiom1 "Exp1R"    $ \(Pair s t) -> (s .^. num 1) === t
-axLeqRefl   = mkAxiom1 "LeqRefl"  $ \(Pair s _) -> (s <== s) === bool True
 axCmpNatRefl    = mkAxiom1 "CmpNatRefl"
                 $ \(Pair s _) -> (cmpNat s s) === ordering EQ
 axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
                 $ \(Pair s _) -> (cmpSymbol s s) === ordering EQ
-axLeq0L     = mkAxiom1 "Leq0L"    $ \(Pair s _) -> (num 0 <== s) === bool True
 axAppendSymbol0R  = mkAxiom1 "Concat0R"
             $ \(Pair s t) -> (mkStrLitTy nilFS `appendSymbol` s) === t
 axAppendSymbol0L  = mkAxiom1 "Concat0L"
@@ -508,7 +481,6 @@ typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x))
   [ axAddDef
   , axMulDef
   , axExpDef
-  , axLeqDef
   , axCmpNatDef
   , axCmpSymbolDef
   , axCmpCharDef
@@ -524,11 +496,9 @@ typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x))
   , axExp1L
   , axExp0R
   , axExp1R
-  , axLeqRefl
   , axCmpNatRefl
   , axCmpSymbolRefl
   , axCmpCharRefl
-  , axLeq0L
   , axSubDef
   , axSub0R
   , axAppendSymbol0R
@@ -564,9 +534,6 @@ tMod s t = mkTyConApp typeNatModTyCon [s,t]
 (.^.) :: Type -> Type -> Type
 s .^. t = mkTyConApp typeNatExpTyCon [s,t]
 
-(<==) :: Type -> Type -> Type
-s <== t = mkTyConApp typeNatLeqTyCon [s,t]
-
 cmpNat :: Type -> Type -> Type
 cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
 
@@ -582,24 +549,12 @@ x === y = Pair x y
 num :: Integer -> Type
 num = mkNumLitTy
 
-bool :: Bool -> Type
-bool b = if b then mkTyConApp promotedTrueDataCon []
-              else mkTyConApp promotedFalseDataCon []
-
 charSymbolPair :: Type -> Type -> Type
 charSymbolPair = mkPromotedPairTy charTy typeSymbolKind
 
 charSymbolPairKind :: Kind
 charSymbolPairKind = mkTyConApp pairTyCon [charTy, typeSymbolKind]
 
-isBoolLitTy :: Type -> Maybe Bool
-isBoolLitTy tc =
-  do (tc,[]) <- splitTyConApp_maybe tc
-     case () of
-       _ | tc == promotedFalseDataCon -> return False
-         | tc == promotedTrueDataCon  -> return True
-         | otherwise                   -> Nothing
-
 orderingKind :: Kind
 orderingKind = mkTyConApp orderingTyCon []
 
@@ -734,15 +689,6 @@ matchFamLog [s]
   where mbX = isNumLitTy s
 matchFamLog _ = Nothing
 
-matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
-matchFamLeq [s,t]
-  | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
-  | Just x <- mbX, Just y <- mbY =
-    Just (axLeqDef, [s,t], bool (x <= y))
-  | tcEqType s t  = Just (axLeqRefl, [s], bool True)
-  where mbX = isNumLitTy s
-        mbY = isNumLitTy t
-matchFamLeq _ = Nothing
 
 matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamCmpNat [s,t]
@@ -883,13 +829,6 @@ interactTopLog :: [Xi] -> Xi -> [Pair Type]
 interactTopLog _ _ = []   -- I can't think of anything...
 
 
-interactTopLeq :: [Xi] -> Xi -> [Pair Type]
-interactTopLeq [s,t] r
-  | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]                     -- (s <= 0) => (s ~ 0)
-  where
-  mbY = isNumLitTy t
-  mbZ = isBoolLitTy r
-interactTopLeq _ _ = []
 
 interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
 interactTopCmpNat [s,t] r
@@ -993,18 +932,6 @@ interactInertLog :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertLog _ _ _ _ = []
 
 
-interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
-interactInertLeq [x1,y1] z1 [x2,y2] z2
-  | bothTrue && tcEqType x1 y2 && tcEqType y1 x2 = [ x1 === y1 ]
-  | bothTrue && tcEqType y1 x2                 = [ (x1 <== y2) === bool True ]
-  | bothTrue && tcEqType y2 x1                 = [ (x2 <== y1) === bool True ]
-  where bothTrue = isJust $ do True <- isBoolLitTy z1
-                               True <- isBoolLitTy z2
-                               return ()
-
-interactInertLeq _ _ _ _ = []
-
-
 interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertAppendSymbol [x1,y1] z1 [x2,y2] z2
   | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
@@ -1110,7 +1037,7 @@ typeCharCmpTyCon =
     Nothing
     NotInjective
   where
-  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpChar")
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS_INTERNAL (fsLit "CmpChar")
                   typeCharCmpTyFamNameKey typeCharCmpTyCon
   ops = BuiltInSynFamily
       { sfMatchFam      = matchFamCmpChar
diff --git a/libraries/base/Data/Type/Ord.hs b/libraries/base/Data/Type/Ord.hs
new file mode 100644
index 0000000000..d882a82a61
--- /dev/null
+++ b/libraries/base/Data/Type/Ord.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Ord
+-- License     :  BSD-style (see the LICENSE file in the distribution)
+--
+-- Maintainer  :  libraries@haskell.org
+-- Stability   :  experimental
+-- Portability :  not portable
+--
+-- Basic operations on type-level Orderings.
+--
+-- @since 4.16.0.0
+-----------------------------------------------------------------------------
+
+module Data.Type.Ord (
+  Compare, OrderingI(..)
+  , type (<=), type (<=?)
+  , type (>=), type (>=?)
+  , type (>), type (>?)
+  , type (<), type (<?)
+  , Max, Min
+  , OrdCond
+  ) where
+
+import GHC.Show(Show(..))
+import GHC.TypeLits.Internal
+import GHC.TypeNats.Internal
+import Data.Bool
+import Data.Char(Char)
+import Data.Eq
+import Data.Ord
+
+-- | 'Compare' branches on the kind of its arguments to either compare by
+-- 'Symbol' or 'Nat'.
+-- @since 4.16.0.0
+type Compare :: k -> k -> Ordering
+type family Compare a b
+
+type instance Compare (a :: Natural) b = CmpNat    a b
+type instance Compare (a :: Symbol)  b = CmpSymbol a b
+type instance Compare (a :: Char)    b = CmpChar   a b
+
+-- | Ordering data type for type literals that provides proof of their ordering.
+-- @since 4.16.0.0
+data OrderingI a b where
+  LTI :: Compare a b ~ 'LT => OrderingI a b
+  EQI :: Compare a a ~ 'EQ => OrderingI a a
+  GTI :: Compare a b ~ 'GT => OrderingI a b
+
+deriving instance Show (OrderingI a b)
+deriving instance Eq   (OrderingI a b)
+
+
+infix 4 <=?, <=, >=?, >=, <?, <, >?, >
+
+-- | Comparison (<=) of comparable types, as a constraint.
+-- @since 4.16.0.0
+type x <= y = (x <=? y) ~ 'True
+
+-- | Comparison (>=) of comparable types, as a constraint.
+-- @since 4.16.0.0
+type x >= y = (x >=? y) ~ 'True
+
+-- | Comparison (<) of comparable types, as a constraint.
+-- @since 4.16.0.0
+type x < y = (x >? y) ~ 'True
+
+-- | Comparison (>) of comparable types, as a constraint.
+-- @since 4.16.0.0
+type x > y = (x >? y) ~ 'True
+
+
+-- | Comparison (<=) of comparable types, as a function.
+-- @since 4.16.0.0
+type (<=?) :: k -> k -> Bool
+type m <=? n = OrdCond (Compare m n) 'True 'True 'False
+
+-- | Comparison (>=) of comparable types, as a function.
+-- @since 4.16.0.0
+type (>=?) :: k -> k -> Bool
+type m >=? n = OrdCond (Compare m n) 'False 'True 'True
+
+-- | Comparison (<) of comparable types, as a function.
+-- @since 4.16.0.0
+type (<?) :: k -> k -> Bool
+type m <? n = OrdCond (Compare m n) 'True 'False 'False
+
+-- | Comparison (>) of comparable types, as a function.
+-- @since 4.16.0.0
+type (>?) :: k -> k -> Bool
+type m >? n = OrdCond (Compare m n) 'False 'False 'True
+
+
+-- | Maximum between two comparable types.
+-- @since 4.16.0.0
+type Max :: k -> k -> k
+type Max m n = OrdCond (Compare m n) n n m
+
+-- | Minimum between two comparable types.
+-- @since 4.16.0.0
+type Min :: k -> k -> k
+type Min m n = OrdCond (Compare m n) m m n
+
+
+-- | A case statement on `Ordering`.
+-- `Ordering c l e g` is `l` when `c ~ LT`, `e` when `c ~ EQ`, and `g` when
+-- `c ~ GT`.
+-- @since 4.16.0.0
+type OrdCond :: Ordering -> k -> k -> k -> k
+type family OrdCond o lt eq gt where
+  OrdCond 'LT lt eq gt = lt
+  OrdCond 'EQ lt eq gt = eq
+  OrdCond 'GT lt eq gt = gt
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 206fd385ea..b0daf341c8 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -31,7 +31,7 @@ working with type-level data will be defined in a separate library.
 
 module GHC.TypeLits
   ( -- * Kinds
-    Natural, Nat, Symbol  -- Symbol is declared in GHC.Types in package ghc-prim
+    N.Natural, N.Nat, Symbol  -- Symbol is declared in GHC.Types in package ghc-prim
 
     -- * Linking type and value level
   , N.KnownNat, natVal, natVal'
@@ -40,6 +40,8 @@ module GHC.TypeLits
   , N.SomeNat(..), SomeSymbol(..), SomeChar(..)
   , someNatVal, someSymbolVal, someCharVal
   , N.sameNat, sameSymbol, sameChar
+  , OrderingI(..)
+  , N.cmpNat, cmpSymbol, cmpChar
 
 
     -- * Functions on type literals
@@ -65,9 +67,10 @@ import GHC.Prim(magicDict, Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
+import Data.Type.Ord(OrderingI(..))
 import Unsafe.Coerce(unsafeCoerce)
 
-import GHC.TypeNats (Natural, Nat, KnownNat)
+import GHC.TypeLits.Internal(CmpSymbol, CmpChar)
 import qualified GHC.TypeNats as N
 
 --------------------------------------------------------------------------------
@@ -80,7 +83,7 @@ class KnownSymbol (n :: Symbol) where
   symbolSing :: SSymbol n
 
 -- | @since 4.7.0.0
-natVal :: forall n proxy. KnownNat n => proxy n -> Integer
+natVal :: forall n proxy. N.KnownNat n => proxy n -> Integer
 natVal p = toInteger (N.natVal p)
 
 -- | @since 4.7.0.0
@@ -89,7 +92,7 @@ symbolVal _ = case symbolSing :: SSymbol n of
                 SSymbol x -> x
 
 -- | @since 4.8.0.0
-natVal' :: forall n. KnownNat n => Proxy# n -> Integer
+natVal' :: forall n. N.KnownNat n => Proxy# n -> Integer
 natVal' p = toInteger (N.natVal' p)
 
 -- | @since 4.8.0.0
@@ -171,11 +174,6 @@ instance Read SomeChar where
 
 --------------------------------------------------------------------------------
 
--- | Comparison of type-level symbols, as a function.
---
--- @since 4.7.0.0
-type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
-
 -- | Concatenation of type-level symbols.
 --
 -- @since 4.10.0.0
@@ -231,11 +229,6 @@ type family TypeError (a :: ErrorMessage) :: b where
 
 -- Char-related type families
 
--- | Comparison of type-level characters.
---
--- @since 4.16.0.0
-type family CmpChar (a :: Char) (b :: Char) :: Ordering
-
 -- | Extending a type-level symbol with a type-level character
 --
 -- @since 4.16.0.0
@@ -270,6 +263,33 @@ sameChar x y
   | charVal x == charVal y  = Just (unsafeCoerce Refl)
   | otherwise                = Nothing
 
+-- | Like 'sameSymbol', but if the symbols aren't equal, this additionally
+-- provides proof of LT or GT.
+-- @since 4.16.0.0
+cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b)
+          => proxy1 a -> proxy2 b -> OrderingI a b
+cmpSymbol x y = case compare (symbolVal x) (symbolVal y) of
+  EQ -> case unsafeCoerce (Refl, Refl) :: (CmpSymbol a b :~: 'EQ, a :~: b) of
+    (Refl, Refl) -> EQI
+  LT -> case unsafeCoerce Refl :: (CmpSymbol a b :~: 'LT) of
+    Refl -> LTI
+  GT -> case unsafeCoerce Refl :: (CmpSymbol a b :~: 'GT) of
+    Refl -> GTI
+
+-- | Like 'sameChar', but if the Chars aren't equal, this additionally
+-- provides proof of LT or GT.
+-- @since 4.16.0.0
+cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b)
+        => proxy1 a -> proxy2 b -> OrderingI a b
+cmpChar x y = case compare (charVal x) (charVal y) of
+  EQ -> case unsafeCoerce (Refl, Refl) :: (CmpChar a b :~: 'EQ, a :~: b) of
+    (Refl, Refl) -> EQI
+  LT -> case unsafeCoerce Refl :: (CmpChar a b :~: 'LT) of
+    Refl -> LTI
+  GT -> case unsafeCoerce Refl :: (CmpChar a b :~: 'GT) of
+    Refl -> GTI
+
+
 --------------------------------------------------------------------------------
 -- PRIVATE:
 
diff --git a/libraries/base/GHC/TypeLits/Internal.hs b/libraries/base/GHC/TypeLits/Internal.hs
new file mode 100644
index 0000000000..052394065e
--- /dev/null
+++ b/libraries/base/GHC/TypeLits/Internal.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+{-|
+This module exports the Type Literal kinds as well as the comparison type
+families for those kinds.  It is needed to prevent module cycles while still
+allowing these identifiers to be improted in 'Data.Type.Ord'.
+
+@since 4.16.0.0
+-}
+
+module GHC.TypeLits.Internal
+  ( Symbol
+  , CmpSymbol, CmpChar
+  ) where
+
+import GHC.Base(Ordering)
+import GHC.Types(Symbol, Char)
+
+-- | Comparison of type-level symbols, as a function.
+--
+-- @since 4.7.0.0
+type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
+
+-- Char-related type families
+
+-- | Comparison of type-level characters.
+--
+-- @since 4.16.0.0
+type family CmpChar (a :: Char) (b :: Char) :: Ordering
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index a2dabb1fca..f9733d55a3 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -33,6 +33,7 @@ module GHC.TypeNats
     -- * Functions on type literals
   , type (<=), type (<=?), type (+), type (*), type (^), type (-)
   , CmpNat
+  , cmpNat
   , Div, Mod, Log2
 
   ) where
@@ -46,8 +47,10 @@ import GHC.Prim(magicDict, Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
+import Data.Type.Ord(OrderingI(..), type (<=), type (<=?))
 import Unsafe.Coerce(unsafeCoerce)
 
+import GHC.TypeNats.Internal(CmpNat)
 
 -- | A type synonym for 'Natural'.
 --
@@ -163,27 +166,10 @@ instance Read SomeNat where
 
 --------------------------------------------------------------------------------
 
-infix  4 <=?, <=
 infixl 6 +, -
 infixl 7 *, `Div`, `Mod`
 infixr 8 ^
 
--- | Comparison of type-level naturals, as a constraint.
---
--- @since 4.7.0.0
-type x <= y = (x <=? y) ~ 'True
-
--- | Comparison of type-level naturals, as a function.
---
--- @since 4.7.0.0
-type family CmpNat    (m :: Nat)    (n :: Nat)    :: Ordering
-
-{- | Comparison of type-level naturals, as a function.
-NOTE: The functionality for this function should be subsumed
-by 'CmpNat', so this might go away in the future.
-Please let us know, if you encounter discrepancies between the two. -}
-type family (m :: Nat) <=? (n :: Nat) :: Bool
-
 -- | Addition of type-level naturals.
 --
 -- @since 4.7.0.0
@@ -234,6 +220,21 @@ sameNat x y
   | natVal x == natVal y = Just (unsafeCoerce Refl)
   | otherwise            = Nothing
 
+-- | Like 'sameNat', but if the numbers aren't equal, this additionally
+-- provides proof of LT or GT.
+-- @since 4.16.0.0
+cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b)
+       => proxy1 a -> proxy2 b -> OrderingI a b
+cmpNat x y = case compare (natVal x) (natVal y) of
+  EQ -> case unsafeCoerce (Refl, Refl) :: (CmpNat a b :~: 'EQ, a :~: b) of
+    (Refl, Refl) -> EQI
+  LT -> case unsafeCoerce Refl :: (CmpNat a b :~: 'LT) of
+    Refl -> LTI
+  GT -> case unsafeCoerce Refl :: (CmpNat a b :~: 'GT) of
+    Refl -> GTI
+
+
+
 --------------------------------------------------------------------------------
 -- PRIVATE:
 
diff --git a/libraries/base/GHC/TypeNats/Internal.hs b/libraries/base/GHC/TypeNats/Internal.hs
new file mode 100644
index 0000000000..7ae787310f
--- /dev/null
+++ b/libraries/base/GHC/TypeNats/Internal.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+{-|
+This module exports the Type Nat kind as well as the comparison type
+family for that kinds.  It is needed to prevent module cycles while still
+allowing these identifiers to be improted in 'Data.Type.Ord'.
+
+@since 4.16.0.0
+-}
+
+module GHC.TypeNats.Internal
+  ( Natural
+  , CmpNat
+  ) where
+
+import GHC.Base(Ordering)
+import GHC.Num.Natural(Natural)
+
+-- | Comparison of type-level naturals, as a function.
+--
+-- @since 4.7.0.0
+type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal
index ac5cb24814..530e0503c0 100644
--- a/libraries/base/base.cabal
+++ b/libraries/base/base.cabal
@@ -159,6 +159,7 @@ Library
         Data.Type.Bool
         Data.Type.Coercion
         Data.Type.Equality
+        Data.Type.Ord
         Data.Typeable
         Data.Unique
         Data.Version
@@ -277,7 +278,9 @@ Library
         GHC.Storable
         GHC.TopHandler
         GHC.TypeLits
+        GHC.TypeLits.Internal
         GHC.TypeNats
+        GHC.TypeNats.Internal
         GHC.Unicode
         GHC.Weak
         GHC.Word
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index d4e869f073..8ca20e265d 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -1,11 +1,6 @@
 type GHC.TypeLits.AppendSymbol :: GHC.Types.Symbol
                                   -> GHC.Types.Symbol -> GHC.Types.Symbol
 type family GHC.TypeLits.AppendSymbol a b
-type GHC.TypeLits.CmpChar :: Char -> Char -> Ordering
-type family GHC.TypeLits.CmpChar a b
-type GHC.TypeLits.CmpSymbol :: GHC.Types.Symbol
-                               -> GHC.Types.Symbol -> Ordering
-type family GHC.TypeLits.CmpSymbol a b
 type GHC.TypeLits.ConsSymbol :: Char
                                 -> GHC.Types.Symbol -> GHC.Types.Symbol
 type family GHC.TypeLits.ConsSymbol a b
@@ -46,6 +41,12 @@ type family GHC.TypeLits.UnconsSymbol a
 GHC.TypeLits.charVal :: GHC.TypeLits.KnownChar n => proxy n -> Char
 GHC.TypeLits.charVal' ::
   GHC.TypeLits.KnownChar n => GHC.Prim.Proxy# n -> Char
+GHC.TypeLits.cmpChar ::
+  (GHC.TypeLits.KnownChar a, GHC.TypeLits.KnownChar b) =>
+  proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
+GHC.TypeLits.cmpSymbol ::
+  (GHC.TypeLits.KnownSymbol a, GHC.TypeLits.KnownSymbol b) =>
+  proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
 GHC.TypeLits.natVal ::
   GHC.TypeNats.KnownNat n => proxy n -> Integer
 GHC.TypeLits.natVal' ::
@@ -72,16 +73,22 @@ type family (GHC.TypeNats.+) a b
 type (GHC.TypeNats.-) :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family (GHC.TypeNats.-) a b
-type (GHC.TypeNats.<=) :: GHC.Num.Natural.Natural
-                          -> GHC.Num.Natural.Natural -> Constraint
-type (GHC.TypeNats.<=) x y =
-  (x GHC.TypeNats.<=? y) ~ 'True :: Constraint
-type (GHC.TypeNats.<=?) :: GHC.Num.Natural.Natural
-                           -> GHC.Num.Natural.Natural -> Bool
-type family (GHC.TypeNats.<=?) a b
-type GHC.TypeNats.CmpNat :: GHC.Num.Natural.Natural
-                            -> GHC.Num.Natural.Natural -> Ordering
-type family GHC.TypeNats.CmpNat a b
+type (Data.Type.Ord.<=) :: forall {k}. k -> k -> Constraint
+type (Data.Type.Ord.<=) x y =
+  (x Data.Type.Ord.<=? y) ~ 'True :: Constraint
+type (Data.Type.Ord.<=?) :: forall k. k -> k -> Bool
+type (Data.Type.Ord.<=?) m n =
+  Data.Type.Ord.OrdCond
+    (Data.Type.Ord.Compare m n) 'True 'True 'False
+  :: Bool
+type GHC.TypeLits.Internal.CmpChar :: Char -> Char -> Ordering
+type family GHC.TypeLits.Internal.CmpChar a b
+type GHC.TypeNats.Internal.CmpNat :: GHC.Num.Natural.Natural
+                                     -> GHC.Num.Natural.Natural -> Ordering
+type family GHC.TypeNats.Internal.CmpNat a b
+type GHC.TypeLits.Internal.CmpSymbol :: GHC.Types.Symbol
+                                        -> GHC.Types.Symbol -> Ordering
+type family GHC.TypeLits.Internal.CmpSymbol a b
 type GHC.TypeNats.Div :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family GHC.TypeNats.Div a b
@@ -101,6 +108,18 @@ type GHC.Num.Natural.Natural :: *
 data GHC.Num.Natural.Natural
   = GHC.Num.Natural.NS GHC.Prim.Word#
   | GHC.Num.Natural.NB GHC.Prim.ByteArray#
+type role Data.Type.Ord.OrderingI nominal nominal
+type Data.Type.Ord.OrderingI :: forall {k}. k -> k -> *
+data Data.Type.Ord.OrderingI a b where
+  Data.Type.Ord.LTI :: forall {k} (a :: k) (b :: k).
+                       (Data.Type.Ord.Compare a b ~ 'LT) =>
+                       Data.Type.Ord.OrderingI a b
+  Data.Type.Ord.EQI :: forall {k} (a :: k).
+                       (Data.Type.Ord.Compare a a ~ 'EQ) =>
+                       Data.Type.Ord.OrderingI a a
+  Data.Type.Ord.GTI :: forall {k} (a :: k) (b :: k).
+                       (Data.Type.Ord.Compare a b ~ 'GT) =>
+                       Data.Type.Ord.OrderingI a b
 type GHC.TypeNats.SomeNat :: *
 data GHC.TypeNats.SomeNat
   = forall (n :: GHC.TypeNats.Nat).
@@ -111,6 +130,9 @@ data GHC.Types.Symbol
 type (GHC.TypeNats.^) :: GHC.Num.Natural.Natural
                          -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family (GHC.TypeNats.^) a b
+GHC.TypeNats.cmpNat ::
+  (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
+  proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
 GHC.TypeNats.sameNat ::
   (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
   proxy1 a -> proxy2 b -> Maybe (a Data.Type.Equality.:~: b)
diff --git a/testsuite/tests/lib/base/DataTypeOrd.hs b/testsuite/tests/lib/base/DataTypeOrd.hs
new file mode 100644
index 0000000000..1f190d3efe
--- /dev/null
+++ b/testsuite/tests/lib/base/DataTypeOrd.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main where
+
+import Data.Type.Ord
+import GHC.TypeLits
+
+data Prox t = Prox
+
+main :: IO ()
+main = do
+  print $ cmpSymbol (Prox @"foo") (Prox @"qux")
+  print $ cmpSymbol (Prox @"foo") (Prox @"foo")
+  print $ cmpSymbol (Prox @"foo") (Prox @"bar")
+  print $ cmpNat (Prox @1) (Prox @3)
+  print $ cmpNat (Prox @5) (Prox @5)
+  print $ cmpNat (Prox @7) (Prox @2)
diff --git a/testsuite/tests/lib/base/DataTypeOrd.stdout b/testsuite/tests/lib/base/DataTypeOrd.stdout
new file mode 100644
index 0000000000..c14e6794f3
--- /dev/null
+++ b/testsuite/tests/lib/base/DataTypeOrd.stdout
@@ -0,0 +1,6 @@
+LTI
+EQI
+GTI
+LTI
+EQI
+GTI
diff --git a/testsuite/tests/lib/base/all.T b/testsuite/tests/lib/base/all.T
index 695b60b51c..6bf890c148 100644
--- a/testsuite/tests/lib/base/all.T
+++ b/testsuite/tests/lib/base/all.T
@@ -1,3 +1,4 @@
+test('DataTypeOrd', normal, compile_and_run, [''])
 test('T16586', normal, compile_and_run, ['-O2'])
 # Event-manager not supported on Windows
 test('T16916', when(opsys('mingw32'), skip), compile_and_run, ['-O2 -threaded -with-rtsopts="-I0" -rtsopts'])
diff --git a/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
index d0077edbdb..18db425413 100644
--- a/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
+++ b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, ExplicitForAll #-}
 module TcTypeNatSimple where
 import GHC.TypeLits as L
 import Data.Proxy
@@ -47,12 +47,9 @@ e13 = id
 e14 :: Proxy (2 <=? 1) -> Proxy False
 e14 = id
 
-e15 :: Proxy (x <=? x) -> Proxy True
+e15 :: forall (x :: Nat). Proxy (x <=? x) -> Proxy True
 e15 = id
 
-e16 :: Proxy (0 <=? x) -> Proxy True
-e16 = id
-
 e17 :: Proxy (3 - 2) -> Proxy 1
 e17 = id
 
diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
index c12d53cde6..7365569036 100644
--- a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
+++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
@@ -24,9 +24,6 @@ troot _ _ = Proxy
 tlog :: Proxy (x ^ y) -> Proxy x -> Proxy y
 tlog _ _ = Proxy
 
-tleq :: ((x <=? y) ~ True) => Proxy y -> Proxy x
-tleq _ = Proxy
-
 main :: IO ()
 main = print [ sh (tsub  (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
              , let (p, q) = tsub2 (Proxy :: Proxy 0)
@@ -36,7 +33,6 @@ main = print [ sh (tsub  (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
                in (sh p, sh q) == ("1", "1")
              , sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
              , sh (tlog  (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
-             , sh (tleq  (Proxy :: Proxy 0))                    == "0"
              ]
   where
   sh x = show (natVal x)
diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
index 74c592960e..895c94bb19 100644
--- a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
+++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
@@ -1 +1 @@
-[True,True,True,True,True,True,True]
+[True,True,True,True,True,True]