diff options
author | Oleg Grenrus <oleg.grenrus@iki.fi> | 2017-02-01 22:49:17 -0500 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2017-02-01 23:37:47 -0500 |
commit | 1fcede43d2b30f33b7505e25eb6b1f321be0407f (patch) | |
tree | 9c206c94aa567b0a8d53cc65156666c26030d955 | |
parent | f5b275a239d2554c4da0b7621211642bf3b10650 (diff) | |
download | haskell-1fcede43d2b30f33b7505e25eb6b1f321be0407f.tar.gz |
Introduce GHC.TypeNats module, change KnownNat evidence to be Natural
Reviewers: dfeuer, austin, hvr, bgamari
Reviewed By: bgamari
Subscribers: thomie
Differential Revision: https://phabricator.haskell.org/D3024
GHC Trac Issues: #13181
-rw-r--r-- | compiler/coreSyn/MkCore.hs | 11 | ||||
-rw-r--r-- | compiler/deSugar/DsBinds.hs | 2 | ||||
-rw-r--r-- | compiler/prelude/PrelNames.hs | 27 | ||||
-rw-r--r-- | docs/users_guide/8.2.1-notes.rst | 4 | ||||
-rw-r--r-- | libraries/base/Data/Data.hs | 18 | ||||
-rw-r--r-- | libraries/base/Data/Typeable/Internal.hs | 3 | ||||
-rw-r--r-- | libraries/base/GHC/Exception.hs | 4 | ||||
-rw-r--r-- | libraries/base/GHC/Exception.hs-boot | 4 | ||||
-rw-r--r-- | libraries/base/GHC/Natural.hs | 79 | ||||
-rw-r--r-- | libraries/base/GHC/TypeLits.hs | 78 | ||||
-rw-r--r-- | libraries/base/GHC/TypeNats.hs | 160 | ||||
-rw-r--r-- | libraries/base/base.cabal | 1 | ||||
-rw-r--r-- | libraries/base/changelog.md | 4 | ||||
-rw-r--r-- | testsuite/tests/annotations/should_fail/annfail10.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/ghci/scripts/T9181.stdout | 26 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T12921.stderr | 2 |
16 files changed, 302 insertions, 125 deletions
diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index 7d2420245a..7ba9445f7c 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -12,7 +12,7 @@ module MkCore ( -- * Constructing boxed literals mkWordExpr, mkWordExprWord, mkIntExpr, mkIntExprInt, - mkIntegerExpr, + mkIntegerExpr, mkNaturalExpr, mkFloatExpr, mkDoubleExpr, mkCharExpr, mkStringExpr, mkStringExprFS, mkStringExprFSWith, @@ -250,6 +250,15 @@ mkIntegerExpr :: MonadThings m => Integer -> m CoreExpr -- Result :: Integer mkIntegerExpr i = do t <- lookupTyCon integerTyConName return (Lit (mkLitInteger i (mkTyConTy t))) +-- | Create a 'CoreExpr' which will evaluate to the given @Natural@ +-- +-- TODO: should we add LitNatural to Core? +mkNaturalExpr :: MonadThings m => Integer -> m CoreExpr -- Result :: Natural +mkNaturalExpr i = do iExpr <- mkIntegerExpr i + fiExpr <- lookupId naturalFromIntegerName + return (mkCoreApps (Var fiExpr) [iExpr]) + + -- | Create a 'CoreExpr' which will evaluate to the given @Float@ mkFloatExpr :: Float -> CoreExpr mkFloatExpr f = mkCoreConApps floatDataCon [mkFloatLitFloat f] diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index c3704e382e..443a21e4fa 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -1151,7 +1151,7 @@ dsEvTerm :: EvTerm -> DsM CoreExpr dsEvTerm (EvId v) = return (Var v) dsEvTerm (EvCallStack cs) = dsEvCallStack cs dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev -dsEvTerm (EvLit (EvNum n)) = mkIntegerExpr n +dsEvTerm (EvLit (EvNum n)) = mkNaturalExpr n dsEvTerm (EvLit (EvStr s)) = mkStringExprFS s dsEvTerm (EvCast tm co) diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs index 4d28ba39d7..6fe1485f7d 100644 --- a/compiler/prelude/PrelNames.hs +++ b/compiler/prelude/PrelNames.hs @@ -330,6 +330,10 @@ basicKnownKeyNames andIntegerName, orIntegerName, xorIntegerName, complementIntegerName, shiftLIntegerName, shiftRIntegerName, bitIntegerName, + -- Natural + naturalTyConName, + naturalFromIntegerName, + -- Float/Double rationalToFloatName, rationalToDoubleName, @@ -440,7 +444,7 @@ pRELUDE = mkBaseModule_ pRELUDE_NAME gHC_PRIM, gHC_TYPES, gHC_GENERICS, gHC_MAGIC, gHC_CLASSES, gHC_BASE, gHC_ENUM, gHC_GHCI, gHC_CSTRING, - gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER_TYPE, gHC_LIST, + gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER_TYPE, gHC_NATURAL, gHC_LIST, gHC_TUPLE, dATA_TUPLE, dATA_EITHER, dATA_STRING, dATA_FOLDABLE, dATA_TRAVERSABLE, dATA_MONOID, dATA_SEMIGROUP, gHC_CONC, gHC_IO, gHC_IO_Exception, @@ -449,7 +453,7 @@ gHC_PRIM, gHC_TYPES, gHC_GENERICS, gHC_MAGIC, 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, dATA_TYPE_EQUALITY, + cONTROL_EXCEPTION_BASE, gHC_TYPELITS, gHC_TYPENATS, dATA_TYPE_EQUALITY, dATA_COERCE :: Module gHC_PRIM = mkPrimModule (fsLit "GHC.Prim") -- Primitive types and values @@ -465,6 +469,7 @@ gHC_SHOW = mkBaseModule (fsLit "GHC.Show") gHC_READ = mkBaseModule (fsLit "GHC.Read") gHC_NUM = mkBaseModule (fsLit "GHC.Num") gHC_INTEGER_TYPE= mkIntegerModule (fsLit "GHC.Integer.Type") +gHC_NATURAL = mkBaseModule (fsLit "GHC.Natural") gHC_LIST = mkBaseModule (fsLit "GHC.List") gHC_TUPLE = mkPrimModule (fsLit "GHC.Tuple") dATA_TUPLE = mkBaseModule (fsLit "Data.Tuple") @@ -506,6 +511,7 @@ 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_TYPENATS = mkBaseModule (fsLit "GHC.TypeNats") dATA_TYPE_EQUALITY = mkBaseModule (fsLit "Data.Type.Equality") dATA_COERCE = mkBaseModule (fsLit "Data.Coerce") @@ -1127,6 +1133,13 @@ shiftLIntegerName = varQual gHC_INTEGER_TYPE (fsLit "shiftLInteger") shi shiftRIntegerName = varQual gHC_INTEGER_TYPE (fsLit "shiftRInteger") shiftRIntegerIdKey bitIntegerName = varQual gHC_INTEGER_TYPE (fsLit "bitInteger") bitIntegerIdKey +-- GHC.Natural types +naturalTyConName :: Name +naturalTyConName = tcQual gHC_NATURAL (fsLit "Natural") naturalTyConKey + +naturalFromIntegerName :: Name +naturalFromIntegerName = varQual gHC_NATURAL (fsLit "naturalFromInteger") naturalFromIntegerIdKey + -- GHC.Real types and classes rationalTyConName, ratioTyConName, ratioDataConName, realClassName, integralClassName, realFracClassName, fractionalClassName, @@ -1355,7 +1368,7 @@ isStringClassName = clsQual dATA_STRING (fsLit "IsString") isStringClassKey -- Type-level naturals knownNatClassName :: Name -knownNatClassName = clsQual gHC_TYPELITS (fsLit "KnownNat") knownNatClassNameKey +knownNatClassName = clsQual gHC_TYPENATS (fsLit "KnownNat") knownNatClassNameKey knownSymbolClassName :: Name knownSymbolClassName = clsQual gHC_TYPELITS (fsLit "KnownSymbol") knownSymbolClassNameKey @@ -1553,7 +1566,8 @@ addrPrimTyConKey, arrayPrimTyConKey, arrayArrayPrimTyConKey, boolTyConKey, doubleTyConKey, floatPrimTyConKey, floatTyConKey, funTyConKey, intPrimTyConKey, intTyConKey, int8TyConKey, int16TyConKey, int32PrimTyConKey, int32TyConKey, int64PrimTyConKey, int64TyConKey, - integerTyConKey, listTyConKey, foreignObjPrimTyConKey, maybeTyConKey, + integerTyConKey, naturalTyConKey, + listTyConKey, foreignObjPrimTyConKey, maybeTyConKey, weakPrimTyConKey, mutableArrayPrimTyConKey, mutableArrayArrayPrimTyConKey, mutableByteArrayPrimTyConKey, orderingTyConKey, mVarPrimTyConKey, ratioTyConKey, rationalTyConKey, realWorldTyConKey, stablePtrPrimTyConKey, @@ -1579,6 +1593,7 @@ int32TyConKey = mkPreludeTyConUnique 19 int64PrimTyConKey = mkPreludeTyConUnique 20 int64TyConKey = mkPreludeTyConUnique 21 integerTyConKey = mkPreludeTyConUnique 22 +naturalTyConKey = mkPreludeTyConUnique 23 listTyConKey = mkPreludeTyConUnique 24 foreignObjPrimTyConKey = mkPreludeTyConUnique 25 @@ -2235,6 +2250,10 @@ fromStaticPtrClassOpKey = mkPreludeMiscIdUnique 519 makeStaticKey :: Unique makeStaticKey = mkPreludeMiscIdUnique 520 +-- Natural +naturalFromIntegerIdKey :: Unique +naturalFromIntegerIdKey = mkPreludeMiscIdUnique 521 + {- ************************************************************************ * * diff --git a/docs/users_guide/8.2.1-notes.rst b/docs/users_guide/8.2.1-notes.rst index 3b04975d87..f81c3995e0 100644 --- a/docs/users_guide/8.2.1-notes.rst +++ b/docs/users_guide/8.2.1-notes.rst @@ -291,6 +291,10 @@ See ``changelog.md`` in the ``base`` package for full release notes. - Add ``type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol`` to ``GHC.TypeLits`` +- Add ``GHC.TypeNats`` module with ``Natural``-based ``KnownNat``. The ``Nat`` + operations in ``GHC.TypeLits`` are a thin compatibility layer on top. + Note: the ``KnownNat`` evidence is changed from an ``Integer`` to a ``Natural``. + binary ~~~~~~ diff --git a/libraries/base/Data/Data.hs b/libraries/base/Data/Data.hs index e43ec74e3f..12f9378a9a 100644 --- a/libraries/base/Data/Data.hs +++ b/libraries/base/Data/Data.hs @@ -126,6 +126,7 @@ import Data.Version( Version(..) ) import GHC.Base hiding (Any, IntRep, FloatRep) import GHC.List import GHC.Num +import GHC.Natural import GHC.Read import GHC.Show import Text.Read( reads ) @@ -928,6 +929,23 @@ instance Data Integer where ------------------------------------------------------------------------------ +-- This follows the same style as the other integral 'Data' instances +-- defined in "Data.Data" +naturalType :: DataType +naturalType = mkIntType "Numeric.Natural.Natural" + +-- | @since 4.8.0.0 +instance Data Natural where + toConstr x = mkIntegralConstr naturalType x + gunfold _ z c = case constrRep c of + (IntConstr x) -> z (fromIntegral x) + _ -> errorWithoutStackTrace $ "Data.Data.gunfold: Constructor " ++ show c + ++ " is not of type Natural" + dataTypeOf _ = naturalType + + +------------------------------------------------------------------------------ + int8Type :: DataType int8Type = mkIntType "Data.Int.Int8" diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs index 0054b7a64a..7746bfbe6c 100644 --- a/libraries/base/Data/Typeable/Internal.hs +++ b/libraries/base/Data/Typeable/Internal.hs @@ -67,7 +67,8 @@ import GHC.Types (TYPE) import GHC.Word import GHC.Show import Data.Proxy -import GHC.TypeLits( KnownNat, KnownSymbol, natVal', symbolVal' ) +import GHC.TypeLits ( KnownSymbol, symbolVal' ) +import GHC.TypeNats ( KnownNat, natVal' ) import GHC.Fingerprint.Type import {-# SOURCE #-} GHC.Fingerprint diff --git a/libraries/base/GHC/Exception.hs b/libraries/base/GHC/Exception.hs index d2b5e209cc..be2ee3f4c9 100644 --- a/libraries/base/GHC/Exception.hs +++ b/libraries/base/GHC/Exception.hs @@ -26,6 +26,7 @@ module GHC.Exception , throw , SomeException(..), ErrorCall(..,ErrorCall), ArithException(..) , divZeroException, overflowException, ratioZeroDenomException + , underflowException , errorCallException, errorCallWithCallStackException -- re-export CallStack and SrcLoc from GHC.Types , CallStack, fromCallSiteList, getCallStack, prettyCallStack @@ -238,10 +239,11 @@ data ArithException | RatioZeroDenominator -- ^ @since 4.6.0.0 deriving (Eq, Ord) -divZeroException, overflowException, ratioZeroDenomException :: SomeException +divZeroException, overflowException, ratioZeroDenomException, underflowException :: SomeException divZeroException = toException DivideByZero overflowException = toException Overflow ratioZeroDenomException = toException RatioZeroDenominator +underflowException = toException Underflow -- | @since 4.0.0.0 instance Exception ArithException diff --git a/libraries/base/GHC/Exception.hs-boot b/libraries/base/GHC/Exception.hs-boot index f89fed1aa2..d539dd4962 100644 --- a/libraries/base/GHC/Exception.hs-boot +++ b/libraries/base/GHC/Exception.hs-boot @@ -26,13 +26,15 @@ to get a visibly-bottom value. module GHC.Exception ( SomeException, errorCallException, errorCallWithCallStackException, - divZeroException, overflowException, ratioZeroDenomException + divZeroException, overflowException, ratioZeroDenomException, + underflowException ) where import GHC.Types ( Char ) import GHC.Stack.Types ( CallStack ) data SomeException divZeroException, overflowException, ratioZeroDenomException :: SomeException +underflowException :: SomeException errorCallException :: [Char] -> SomeException errorCallWithCallStackException :: [Char] -> CallStack -> SomeException diff --git a/libraries/base/GHC/Natural.hs b/libraries/base/GHC/Natural.hs index 953b2a4c26..9bca0a2079 100644 --- a/libraries/base/GHC/Natural.hs +++ b/libraries/base/GHC/Natural.hs @@ -36,6 +36,7 @@ module GHC.Natural Natural(..) , isValidNatural -- * Conversions + , naturalFromInteger , wordToNatural , naturalToWordMaybe -- * Checked subtraction @@ -54,7 +55,7 @@ module GHC.Natural import GHC.Arr import GHC.Base -import GHC.Exception +import {-# SOURCE #-} GHC.Exception (underflowException) #if HAVE_GMP_BIGNAT import GHC.Integer.GMP.Internals import Data.Word @@ -68,12 +69,26 @@ import GHC.Enum import GHC.List import Data.Bits -import Data.Data default () +------------------------------------------------------------------------------- +-- Arithmetic underflow +------------------------------------------------------------------------------- + +-- We put them here because they are needed relatively early +-- in the libraries before the Exception type has been defined yet. + +{-# NOINLINE underflowError #-} +underflowError :: a +underflowError = raise# underflowException + +------------------------------------------------------------------------------- +-- Natural type +------------------------------------------------------------------------------- + #if HAVE_GMP_BIGNAT --- TODO: if saturated arithmetic is to used, replace 'throw Underflow' by '0' +-- TODO: if saturated arithmetic is to used, replace 'underflowError' by '0' -- | Type representing arbitrary-precision non-negative integers. -- @@ -162,9 +177,7 @@ instance Read Natural where -- | @since 4.8.0.0 instance Num Natural where - fromInteger (S# i#) | I# i# >= 0 = NatS# (int2Word# i#) - fromInteger (Jp# bn) = bigNatToNatural bn - fromInteger _ = throw Underflow + fromInteger = naturalFromInteger (+) = plusNatural (*) = timesNatural @@ -176,7 +189,14 @@ instance Num Natural where signum _ = NatS# 1## negate (NatS# 0##) = NatS# 0## - negate _ = throw Underflow + negate _ = underflowError + +-- | @since 4.10.0.0 +naturalFromInteger :: Integer -> Natural +naturalFromInteger (S# i#) | I# i# >= 0 = NatS# (int2Word# i#) +naturalFromInteger (Jp# bn) = bigNatToNatural bn +naturalFromInteger _ = underflowError +{-# INLINE naturalFromInteger #-} -- | @since 4.8.0.0 instance Real Natural where @@ -262,7 +282,7 @@ instance Integral Natural where div = quot mod = rem - quotRem _ (NatS# 0##) = throw DivideByZero + quotRem _ (NatS# 0##) = divZeroError quotRem n (NatS# 1##) = (n,NatS# 0##) quotRem n@(NatS# _) (NatJ# _) = (NatS# 0##, n) quotRem (NatS# n) (NatS# d) = case quotRem (W# n) (W# d) of @@ -272,14 +292,14 @@ instance Integral Natural where quotRem (NatJ# n) (NatJ# d) = case quotRemBigNat n d of (# q,r #) -> (bigNatToNatural q, bigNatToNatural r) - quot _ (NatS# 0##) = throw DivideByZero + quot _ (NatS# 0##) = divZeroError quot n (NatS# 1##) = n quot (NatS# _) (NatJ# _) = NatS# 0## quot (NatS# n) (NatS# d) = wordToNatural (quot (W# n) (W# d)) quot (NatJ# n) (NatS# d) = bigNatToNatural (quotBigNatWord n d) quot (NatJ# n) (NatJ# d) = bigNatToNatural (quotBigNat n d) - rem _ (NatS# 0##) = throw DivideByZero + rem _ (NatS# 0##) = divZeroError rem _ (NatS# 1##) = NatS# 0## rem n@(NatS# _) (NatJ# _) = n rem (NatS# n) (NatS# d) = wordToNatural (rem (W# n) (W# d)) @@ -379,8 +399,8 @@ minusNatural :: Natural -> Natural -> Natural minusNatural x (NatS# 0##) = x minusNatural (NatS# x) (NatS# y) = case subWordC# x y of (# l, 0# #) -> NatS# l - _ -> throw Underflow -minusNatural (NatS# _) (NatJ# _) = throw Underflow + _ -> divZeroError -- underflowException +minusNatural (NatS# _) (NatJ# _) = divZeroError -- underflowException minusNatural (NatJ# x) (NatS# y) = bigNatToNatural $ minusBigNatWord x y minusNatural (NatJ# x) (NatJ# y) @@ -409,7 +429,7 @@ minusNaturalMaybe (NatJ# x) (NatJ# y) bigNatToNatural :: BigNat -> Natural bigNatToNatural bn | isTrue# (sizeofBigNat# bn ==# 1#) = NatS# (bigNatToWord bn) - | isTrue# (isNullBigNat# bn) = throw Underflow + | isTrue# (isNullBigNat# bn) = underflowError | otherwise = NatJ# bn naturalToBigNat :: Natural -> BigNat @@ -419,7 +439,7 @@ naturalToBigNat (NatJ# bn) = bn -- | Convert 'Int' to 'Natural'. -- Throws 'Underflow' when passed a negative 'Int'. intToNatural :: Int -> Natural -intToNatural i | i<0 = throw Underflow +intToNatural i | i<0 = underflowError intToNatural (I# i#) = NatS# (int2Word# i#) naturalToWord :: Natural -> Word @@ -467,7 +487,7 @@ instance Num Natural where {-# INLINE (+) #-} Natural n * Natural m = Natural (n * m) {-# INLINE (*) #-} - Natural n - Natural m | result < 0 = throw Underflow + Natural n - Natural m | result < 0 = underflowError | otherwise = Natural result where result = n - m {-# INLINE (-) #-} @@ -475,11 +495,16 @@ instance Num Natural where {-# INLINE abs #-} signum (Natural n) = Natural (signum n) {-# INLINE signum #-} - fromInteger n - | n >= 0 = Natural n - | otherwise = throw Underflow + fromInteger = naturalFromInteger {-# INLINE fromInteger #-} +-- | @since 4.10.0.0 +naturalFromInteger :: Integer -> Natural +naturalFromInteger n + | n >= 0 = Natural n + | otherwise = underflowError +{-# INLINE naturalFromInteger #-} + -- | 'Natural' subtraction. Returns 'Nothing's for non-positive results. -- -- @since 4.8.0.0 @@ -603,27 +628,13 @@ naturalToWordMaybe (Natural i) maxw = toInteger (maxBound :: Word) #endif --- This follows the same style as the other integral 'Data' instances --- defined in "Data.Data" -naturalType :: DataType -naturalType = mkIntType "Numeric.Natural.Natural" - --- | @since 4.8.0.0 -instance Data Natural where - toConstr x = mkIntegralConstr naturalType x - gunfold _ z c = case constrRep c of - (IntConstr x) -> z (fromIntegral x) - _ -> errorWithoutStackTrace $ "Data.Data.gunfold: Constructor " ++ show c - ++ " is not of type Natural" - dataTypeOf _ = naturalType - -- | \"@'powModNatural' /b/ /e/ /m/@\" computes base @/b/@ raised to -- exponent @/e/@ modulo @/m/@. -- -- @since 4.8.0.0 powModNatural :: Natural -> Natural -> Natural -> Natural #if HAVE_GMP_BIGNAT -powModNatural _ _ (NatS# 0##) = throw DivideByZero +powModNatural _ _ (NatS# 0##) = divZeroError powModNatural _ _ (NatS# 1##) = NatS# 0## powModNatural _ (NatS# 0##) _ = NatS# 1## powModNatural (NatS# 0##) _ _ = NatS# 0## @@ -635,7 +646,7 @@ powModNatural b e (NatJ# m) = bigNatToNatural (powModBigNat (naturalToBigNat b) (naturalToBigNat e) m) #else -- Portable reference fallback implementation -powModNatural _ _ 0 = throw DivideByZero +powModNatural _ _ 0 = divZeroError powModNatural _ _ 1 = 0 powModNatural _ 0 _ = 1 powModNatural 0 _ _ = 0 diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs index 41cf523ab8..3981f14b4d 100644 --- a/libraries/base/GHC/TypeLits.hs +++ b/libraries/base/GHC/TypeLits.hs @@ -26,11 +26,11 @@ module GHC.TypeLits Nat, Symbol -- Both declared in GHC.Types in package ghc-prim -- * Linking type and value level - , KnownNat, natVal, natVal' + , N.KnownNat, natVal, natVal' , KnownSymbol, symbolVal, symbolVal' - , SomeNat(..), SomeSymbol(..) + , N.SomeNat(..), SomeSymbol(..) , someNatVal, someSymbolVal - , sameNat, sameSymbol + , N.sameNat, sameSymbol -- * Functions on type literals @@ -46,24 +46,21 @@ module GHC.TypeLits import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise) import GHC.Types( Nat, Symbol ) -import GHC.Num(Integer) +import GHC.Num(Integer, fromInteger) import GHC.Base(String) import GHC.Show(Show(..)) import GHC.Read(Read(..)) +import GHC.Real(toInteger) import GHC.Prim(magicDict, Proxy#) import Data.Maybe(Maybe(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality(type (==), (:~:)(Refl)) import Unsafe.Coerce(unsafeCoerce) --------------------------------------------------------------------------------- +import GHC.TypeNats (KnownNat) +import qualified GHC.TypeNats as N --- | This class gives the integer associated with a type-level natural. --- There are instances of the class for every concrete literal: 0, 1, 2, etc. --- --- @since 4.7.0.0 -class KnownNat (n :: Nat) where - natSing :: SNat n +-------------------------------------------------------------------------------- -- | This class gives the string associated with a type-level symbol. -- There are instances of the class for every concrete literal: "hello", etc. @@ -74,8 +71,7 @@ class KnownSymbol (n :: Symbol) where -- | @since 4.7.0.0 natVal :: forall n proxy. KnownNat n => proxy n -> Integer -natVal _ = case natSing :: SNat n of - SNat x -> x +natVal p = toInteger (N.natVal p) -- | @since 4.7.0.0 symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String @@ -84,8 +80,7 @@ symbolVal _ = case symbolSing :: SSymbol n of -- | @since 4.8.0.0 natVal' :: forall n. KnownNat n => Proxy# n -> Integer -natVal' _ = case natSing :: SNat n of - SNat x -> x +natVal' p = toInteger (N.natVal' p) -- | @since 4.8.0.0 symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String @@ -93,11 +88,6 @@ symbolVal' _ = case symbolSing :: SSymbol n of SSymbol x -> x - --- | This type represents unknown type-level natural numbers. -data SomeNat = forall n. KnownNat n => SomeNat (Proxy n) - -- ^ @since 4.7.0.0 - -- | This type represents unknown type-level symbols. data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n) -- ^ @since 4.7.0.0 @@ -105,9 +95,9 @@ data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n) -- | Convert an integer into an unknown type-level natural. -- -- @since 4.7.0.0 -someNatVal :: Integer -> Maybe SomeNat +someNatVal :: Integer -> Maybe N.SomeNat someNatVal n - | n >= 0 = Just (withSNat SomeNat (SNat n) Proxy) + | n >= 0 = Just (N.someNatVal (fromInteger n)) | otherwise = Nothing -- | Convert a string into an unknown type-level symbol. @@ -116,28 +106,6 @@ someNatVal n someSymbolVal :: String -> SomeSymbol someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy - - --- | @since 4.7.0.0 -instance Eq SomeNat where - SomeNat x == SomeNat y = natVal x == natVal y - --- | @since 4.7.0.0 -instance Ord SomeNat where - compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y) - --- | @since 4.7.0.0 -instance Show SomeNat where - showsPrec p (SomeNat x) = showsPrec p (natVal x) - --- | @since 4.7.0.0 -instance Read SomeNat where - readsPrec p xs = do (a,ys) <- readsPrec p xs - case someNatVal a of - Nothing -> [] - Just n -> [(n,ys)] - - -- | @since 4.7.0.0 instance Eq SomeSymbol where SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y @@ -154,11 +122,6 @@ instance Show SomeSymbol where instance Read SomeSymbol where readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ] -type family EqNat (a :: Nat) (b :: Nat) where - EqNat a a = 'True - EqNat a b = 'False -type instance a == b = EqNat a b - type family EqSymbol (a :: Symbol) (b :: Symbol) where EqSymbol a a = 'True EqSymbol a b = 'False @@ -260,16 +223,6 @@ type family TypeError (a :: ErrorMessage) :: b where -------------------------------------------------------------------------------- -- | We either get evidence that this function was instantiated with the --- same type-level numbers, or 'Nothing'. --- --- @since 4.7.0.0 -sameNat :: (KnownNat a, KnownNat b) => - Proxy a -> Proxy b -> Maybe (a :~: b) -sameNat x y - | natVal x == natVal y = Just (unsafeCoerce Refl) - | otherwise = Nothing - --- | We either get evidence that this function was instantiated with the -- same type-level symbols, or 'Nothing'. -- -- @since 4.7.0.0 @@ -282,18 +235,11 @@ sameSymbol x y -------------------------------------------------------------------------------- -- PRIVATE: -newtype SNat (n :: Nat) = SNat Integer newtype SSymbol (s :: Symbol) = SSymbol String -data WrapN a b = WrapN (KnownNat a => Proxy a -> b) data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b) -- See Note [magicDictId magic] in "basicType/MkId.hs" -withSNat :: (KnownNat a => Proxy a -> b) - -> SNat a -> Proxy a -> b -withSNat f x y = magicDict (WrapN f) x y - --- See Note [magicDictId magic] in "basicType/MkId.hs" withSSymbol :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b withSSymbol f x y = magicDict (WrapS f) x y diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs new file mode 100644 index 0000000000..cb75367ac8 --- /dev/null +++ b/libraries/base/GHC/TypeNats.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==) +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} + +{-| This module is an internal GHC module. It declares the constants used +in the implementation of type-level natural numbers. The programmer interface +for working with type-level naturals should be defined in a separate library. + +@since 4.10.0.0 +-} + +module GHC.TypeNats + ( -- * Nat Kind + Nat -- declared in GHC.Types in package ghc-prim + + -- * Linking type and value level + , KnownNat, natVal, natVal' + , SomeNat(..) + , someNatVal + , sameNat + + -- * Functions on type literals + , type (<=), type (<=?), type (+), type (*), type (^), type (-) + , CmpNat + + ) where + +import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise) +import GHC.Types( Nat ) +import GHC.Natural(Natural) +import GHC.Show(Show(..)) +import GHC.Read(Read(..)) +import GHC.Prim(magicDict, Proxy#) +import Data.Maybe(Maybe(..)) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality(type (==), (:~:)(Refl)) +import Unsafe.Coerce(unsafeCoerce) + +-------------------------------------------------------------------------------- + +-- | This class gives the integer associated with a type-level natural. +-- There are instances of the class for every concrete literal: 0, 1, 2, etc. +-- +-- @since 4.7.0.0 +class KnownNat (n :: Nat) where + natSing :: SNat n + +-- | @since 4.10.0.0 +natVal :: forall n proxy. KnownNat n => proxy n -> Natural +natVal _ = case natSing :: SNat n of + SNat x -> x + +-- | @since 4.10.0.0 +natVal' :: forall n. KnownNat n => Proxy# n -> Natural +natVal' _ = case natSing :: SNat n of + SNat x -> x + +-- | This type represents unknown type-level natural numbers. +-- +-- @since 4.10.0.0 +data SomeNat = forall n. KnownNat n => SomeNat (Proxy n) + +-- | Convert an integer into an unknown type-level natural. +-- +-- @since 4.10.0.0 +someNatVal :: Natural -> SomeNat +someNatVal n = withSNat SomeNat (SNat n) Proxy + +-- | @since 4.7.0.0 +instance Eq SomeNat where + SomeNat x == SomeNat y = natVal x == natVal y + +-- | @since 4.7.0.0 +instance Ord SomeNat where + compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y) + +-- | @since 4.7.0.0 +instance Show SomeNat where + showsPrec p (SomeNat x) = showsPrec p (natVal x) + +-- | @since 4.7.0.0 +instance Read SomeNat where + readsPrec p xs = do (a,ys) <- readsPrec p xs + [(someNatVal a, ys)] + +type family EqNat (a :: Nat) (b :: Nat) where + EqNat a a = 'True + EqNat a b = 'False +type instance a == b = EqNat a b + +-------------------------------------------------------------------------------- + +infix 4 <=?, <= +infixl 6 +, - +infixl 7 * +infixr 8 ^ + +-- | Comparison of type-level naturals, as a constraint. +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. +type family (m :: Nat) + (n :: Nat) :: Nat + +-- | Multiplication of type-level naturals. +type family (m :: Nat) * (n :: Nat) :: Nat + +-- | Exponentiation of type-level naturals. +type family (m :: Nat) ^ (n :: Nat) :: Nat + +-- | Subtraction of type-level naturals. +-- +-- @since 4.7.0.0 +type family (m :: Nat) - (n :: Nat) :: Nat + +-------------------------------------------------------------------------------- + +-- | We either get evidence that this function was instantiated with the +-- same type-level numbers, or 'Nothing'. +-- +-- @since 4.7.0.0 +sameNat :: (KnownNat a, KnownNat b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameNat x y + | natVal x == natVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-------------------------------------------------------------------------------- +-- PRIVATE: + +newtype SNat (n :: Nat) = SNat Natural + +data WrapN a b = WrapN (KnownNat a => Proxy a -> b) + +-- See Note [magicDictId magic] in "basicType/MkId.hs" +withSNat :: (KnownNat a => Proxy a -> b) + -> SNat a -> Proxy a -> b +withSNat f x y = magicDict (WrapN f) x y diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal index a4f0c7d990..691dc83909 100644 --- a/libraries/base/base.cabal +++ b/libraries/base/base.cabal @@ -277,6 +277,7 @@ Library GHC.Storable GHC.TopHandler GHC.TypeLits + GHC.TypeNats GHC.Unicode GHC.Weak GHC.Word diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md index afb9e9f664..ab9158d244 100644 --- a/libraries/base/changelog.md +++ b/libraries/base/changelog.md @@ -43,6 +43,10 @@ * Add `type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol` to `GHC.TypeLits` (#12162) + * Add `GHC.TypeNats` module with `Natural`-based `KnownNat`. The `Nat` + operations in `GHC.TypeLits` are a thin compatibility layer on top. + Note: the `KnownNat` evidence is changed from an `Integer` to a `Natural`. + * The type of `asProxyTypeOf` in `Data.Proxy` has been generalized (#12805) ## 4.9.0.0 *May 2016* diff --git a/testsuite/tests/annotations/should_fail/annfail10.stderr b/testsuite/tests/annotations/should_fail/annfail10.stderr index 6a52a9c8d8..0dea31a872 100644 --- a/testsuite/tests/annotations/should_fail/annfail10.stderr +++ b/testsuite/tests/annotations/should_fail/annfail10.stderr @@ -10,7 +10,7 @@ annfail10.hs:9:1: error: instance Data.Data.Data Ordering -- Defined in ‘Data.Data’ instance Data.Data.Data Integer -- Defined in ‘Data.Data’ ...plus 15 others - ...plus 40 instances involving out-of-scope types + ...plus 41 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the annotation: {-# ANN f 1 #-} @@ -23,6 +23,6 @@ annfail10.hs:9:11: error: instance Num Double -- Defined in ‘GHC.Float’ instance Num Float -- Defined in ‘GHC.Float’ ...plus two others - ...plus 14 instances involving out-of-scope types + ...plus 15 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the annotation: {-# ANN f 1 #-} diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout index 2e149d31d2..3894125696 100644 --- a/testsuite/tests/ghci/scripts/T9181.stdout +++ b/testsuite/tests/ghci/scripts/T9181.stdout @@ -28,15 +28,9 @@ data GHC.TypeLits.ErrorMessage where -> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage (GHC.TypeLits.:$$:) :: GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage -> GHC.TypeLits.ErrorMessage -class GHC.TypeLits.KnownNat (n :: GHC.Types.Nat) where - GHC.TypeLits.natSing :: GHC.TypeLits.SNat n - {-# MINIMAL natSing #-} class GHC.TypeLits.KnownSymbol (n :: GHC.Types.Symbol) where GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n {-# MINIMAL symbolSing #-} -data GHC.TypeLits.SomeNat where - GHC.TypeLits.SomeNat :: GHC.TypeLits.KnownNat n => - (Data.Proxy.Proxy n) -> GHC.TypeLits.SomeNat data GHC.TypeLits.SomeSymbol where GHC.TypeLits.SomeSymbol :: GHC.TypeLits.KnownSymbol n => (Data.Proxy.Proxy n) -> GHC.TypeLits.SomeSymbol @@ -46,22 +40,28 @@ type family (GHC.TypeLits.^) (a :: GHC.Types.Nat) (b :: GHC.Types.Nat) :: GHC.Types.Nat GHC.TypeLits.natVal :: - GHC.TypeLits.KnownNat n => proxy n -> Integer + GHC.TypeNats.KnownNat n => proxy n -> Integer GHC.TypeLits.natVal' :: - GHC.TypeLits.KnownNat n => GHC.Prim.Proxy# n -> Integer -GHC.TypeLits.sameNat :: - (GHC.TypeLits.KnownNat a, GHC.TypeLits.KnownNat b) => - Data.Proxy.Proxy a - -> Data.Proxy.Proxy b -> Maybe (a Data.Type.Equality.:~: b) + GHC.TypeNats.KnownNat n => GHC.Prim.Proxy# n -> Integer GHC.TypeLits.sameSymbol :: (GHC.TypeLits.KnownSymbol a, GHC.TypeLits.KnownSymbol b) => Data.Proxy.Proxy a -> Data.Proxy.Proxy b -> Maybe (a Data.Type.Equality.:~: b) -GHC.TypeLits.someNatVal :: Integer -> Maybe GHC.TypeLits.SomeNat +GHC.TypeLits.someNatVal :: Integer -> Maybe GHC.TypeNats.SomeNat GHC.TypeLits.someSymbolVal :: String -> GHC.TypeLits.SomeSymbol GHC.TypeLits.symbolVal :: GHC.TypeLits.KnownSymbol n => proxy n -> String GHC.TypeLits.symbolVal' :: GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String +class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where + GHC.TypeNats.natSing :: GHC.TypeNats.SNat n + {-# MINIMAL natSing #-} data GHC.Types.Nat +data GHC.TypeNats.SomeNat where + GHC.TypeNats.SomeNat :: GHC.TypeNats.KnownNat n => + (Data.Proxy.Proxy n) -> GHC.TypeNats.SomeNat data GHC.Types.Symbol +GHC.TypeNats.sameNat :: + (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) => + Data.Proxy.Proxy a + -> Data.Proxy.Proxy b -> Maybe (a Data.Type.Equality.:~: b) diff --git a/testsuite/tests/typecheck/should_fail/T12921.stderr b/testsuite/tests/typecheck/should_fail/T12921.stderr index 8d84c2e84b..a3ac8a2cc0 100644 --- a/testsuite/tests/typecheck/should_fail/T12921.stderr +++ b/testsuite/tests/typecheck/should_fail/T12921.stderr @@ -10,7 +10,7 @@ T12921.hs:4:1: error: instance Data.Data.Data Ordering -- Defined in ‘Data.Data’ instance Data.Data.Data Integer -- Defined in ‘Data.Data’ ...plus 15 others - ...plus 40 instances involving out-of-scope types + ...plus 41 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the annotation: {-# ANN module "HLint: ignore Reduce duplication" #-} |