From eea96042f1e8682605ae68db10f2bcdd7dab923e Mon Sep 17 00:00:00 2001
From: Daniel Winograd-Cort <dwincort@gmail.com>
Date: Sun, 21 Feb 2021 12:06:38 -0500
Subject: [PATCH] Add cmpNat, cmpSymbol, and cmpChar Add Data.Type.Ord Add and
update tests Metric Increase: MultiLayerModules
---
compiler/GHC/Builtin/Names.hs | 8 +-
compiler/GHC/Builtin/Types/Literals.hs | 83 +-----------
libraries/base/Data/Type/Ord.hs | 125 ++++++++++++++++++
libraries/base/GHC/TypeLits.hs | 48 +++++--
libraries/base/GHC/TypeLits/Internal.hs | 33 +++++
libraries/base/GHC/TypeNats.hs | 35 ++---
libraries/base/GHC/TypeNats/Internal.hs | 26 ++++
libraries/base/base.cabal | 3 +
testsuite/tests/ghci/scripts/T9181.stdout | 52 +++++---
testsuite/tests/lib/base/DataTypeOrd.hs | 21 +++
testsuite/tests/lib/base/DataTypeOrd.stdout | 6 +
testsuite/tests/lib/base/all.T | 1 +
.../should_compile/TcTypeNatSimple.hs | 7 +-
.../should_run/TcTypeNatSimpleRun.hs | 4 -
.../should_run/TcTypeNatSimpleRun.stdout | 2 +-
15 files changed, 317 insertions(+), 137 deletions(-)
create mode 100644 libraries/base/Data/Type/Ord.hs
create mode 100644 libraries/base/GHC/TypeLits/Internal.hs
create mode 100644 libraries/base/GHC/TypeNats/Internal.hs
create mode 100644 testsuite/tests/lib/base/DataTypeOrd.hs
create mode 100644 testsuite/tests/lib/base/DataTypeOrd.stdout
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 2dc6e47493d1..6f9aec86cb0b 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 59fd75829364..6b21a68bd31e 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 000000000000..d882a82a6146
--- /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 206fd385ea83..b0daf341c835 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 000000000000..052394065e8c
--- /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 a2dabb1fcaf9..f9733d55a3af 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 000000000000..7ae787310fa1
--- /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 ac5cb2481456..530e0503c0df 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 d4e869f07309..8ca20e265df9 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 000000000000..1f190d3efe1e
--- /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 000000000000..c14e6794f3ee
--- /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 695b60b51cee..6bf890c1481e 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 d0077edbdb39..18db42541312 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 c12d53cde67c..736556903682 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 74c592960ea4..895c94bb19e5 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]
--
GitLab