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

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]

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)

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
+
 {-
 ************************************************************************
 *                                                                      *

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
 ~~~~~~
 

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 )
@@ -926,6 +927,23 @@ instance Data Integer where
   dataTypeOf _ = integerType
 
 
+------------------------------------------------------------------------------
+
+-- 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

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

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

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

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

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
@@ -259,16 +222,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'.
 --
@@ -282,17 +235,10 @@ 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

libraries/base/GHC/TypeNats.hs

+{-# 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
+