From eea96042f1e8682605ae68db10f2bcdd7dab923e Mon Sep 17 00:00:00 2001 From: Daniel Winograd-Cort Date: Sun, 21 Feb 2021 12:06:38 -0500 Subject: 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 + .../typecheck/should_compile/TcTypeNatSimple.hs | 7 +- .../typecheck/should_run/TcTypeNatSimpleRun.hs | 4 - .../typecheck/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 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 ( 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 -> Bool +type m ) 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] -- cgit v1.2.1