Add cmpNat, cmpSymbol, and cmpChar

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

7 files changed, 68 insertions, 25 deletions

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]