Unification of Nat and Naturals

This commit removes the separate kind 'Nat' and enables promotion
of type 'Natural' for using as type literal.
It partially solves #10776

Now the following code will be successfully typechecked:
    data C = MkC Natural
    type CC = MkC 1

Before this change we had to create the separate type for promotion
    data C = MkC Natural
    data CP = MkCP Nat
    type CC = MkCP 1

But CP is uninhabited in terms.

For backward compatibility type synonym `Nat` has been made:
    type Nat = Natural

The user's documentation and tests have been updated.
The haddock submodule also have been updated.

7 files changed, 28 insertions, 16 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index e1ad3ed3fe..81cd3caf22 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -91,7 +91,7 @@ import GHC.List ( splitAt, foldl', elem )
 import GHC.Word
 import GHC.Show
 import GHC.TypeLits ( KnownSymbol, symbolVal', AppendSymbol )
-import GHC.TypeNats ( KnownNat, natVal' )
+import GHC.TypeNats ( KnownNat, Nat, natVal' )
 import Unsafe.Coerce ( unsafeCoerce )
 
 import GHC.Fingerprint.Type
diff --git a/libraries/base/GHC/Event/PSQ.hs b/libraries/base/GHC/Event/PSQ.hs
index 25c5352880..9725734135 100644
--- a/libraries/base/GHC/Event/PSQ.hs
+++ b/libraries/base/GHC/Event/PSQ.hs
@@ -40,7 +40,7 @@ module GHC.Event.PSQ
     , atMost
     ) where
 
-import GHC.Base hiding (Nat, empty)
+import GHC.Base hiding (empty)
 import GHC.Event.Unique
 import GHC.Word (Word64)
 import GHC.Num (Num(..))
diff --git a/libraries/base/GHC/Generics.hs b/libraries/base/GHC/Generics.hs
index 9ea223bd9b..d4c8f73995 100644
--- a/libraries/base/GHC/Generics.hs
+++ b/libraries/base/GHC/Generics.hs
@@ -748,7 +748,7 @@ import GHC.Fingerprint.Type ( Fingerprint(..) )
 
 -- Needed for metadata
 import Data.Proxy   ( Proxy(..) )
-import GHC.TypeLits ( KnownSymbol, KnownNat, symbolVal, natVal )
+import GHC.TypeLits ( KnownSymbol, KnownNat, Nat, symbolVal, natVal )
 
 --------------------------------------------------------------------------------
 -- Representation types
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 0cf892f0a0..6cee76b2e3 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
-    Nat, Symbol  -- Both declared in GHC.Types in package ghc-prim
+    Natural, Nat, Symbol  -- Symbol is declared in GHC.Types in package ghc-prim
 
     -- * Linking type and value level
   , N.KnownNat, natVal, natVal'
@@ -54,7 +54,7 @@ module GHC.TypeLits
   ) where
 
 import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise)
-import GHC.Types( Nat, Symbol )
+import GHC.Types(Symbol)
 import GHC.Num(Integer, fromInteger)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
@@ -65,7 +65,7 @@ import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
 import Unsafe.Coerce(unsafeCoerce)
 
-import GHC.TypeNats (KnownNat)
+import GHC.TypeNats (Natural, Nat, KnownNat)
 import qualified GHC.TypeNats as N
 
 --------------------------------------------------------------------------------
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index d52a2890b0..a2dabb1fca 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -22,8 +22,8 @@ for working with type-level naturals should be defined in a separate library.
 
 module GHC.TypeNats
   ( -- * Nat Kind
-    Nat -- declared in GHC.Types in package ghc-prim
-
+    Natural -- declared in GHC.Num.Natural in package ghc-bignum
+  , Nat
     -- * Linking type and value level
   , KnownNat, natVal, natVal'
   , SomeNat(..)
@@ -37,8 +37,8 @@ module GHC.TypeNats
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
-import GHC.Types( Nat )
+import GHC.Base(Eq(..), Ord(..), otherwise)
+import GHC.Types
 import GHC.Num.Natural(Natural)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
@@ -48,6 +48,13 @@ import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
 import Unsafe.Coerce(unsafeCoerce)
 
+
+-- | A type synonym for 'Natural'.
+--
+-- Prevously, this was an opaque data type, but it was changed to a type synonym
+-- @since @base-4.15.0.0@.
+
+type Nat = Natural
 --------------------------------------------------------------------------------
 
 -- | This class gives the integer associated with a type-level natural.
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index e8ceab903b..79e47093cc 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -1,5 +1,13 @@
 # Changelog for [`base` package](http://hackage.haskell.org/package/base)
 
+## 4.16.0.0 *TBA*
+
+  * Make it possible to promote `Natural`s and remove the separate `Nat` kind.
+    For backwards compatibility, `Nat` is now a type synonym for `Natural`.
+    As a consequence, one must enable `TypeSynonymInstances`
+    in order to define instances for `Nat`. Also, different instances for `Nat` and `Natural`
+    won't typecheck anymore.
+
 ## 4.15.0.0 *TBA*
 
   * `openFile` now calls the `open` system call with an `interruptible` FFI
@@ -35,7 +43,7 @@
 
   * `catMaybes` is now implemented using `mapMaybe`, so that it is both a "good
     consumer" and "good producer" for list-fusion (#18574)
-   
+
 ## 4.14.0.0 *TBA*
   * Bundled with GHC 8.10.1
 
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 2883e3b04c..dc81a9b8d3 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -30,7 +30,7 @@ module GHC.Types (
         Ordering(..), IO(..),
         isTrue#,
         SPEC(..),
-        Nat, Symbol,
+        Symbol,
         Any,
         type (~~), Coercible,
         TYPE, RuntimeRep(..), Type, Constraint,
@@ -98,13 +98,10 @@ type family MultMul (a :: Multiplicity) (b :: Multiplicity) :: Multiplicity wher
 
 {- *********************************************************************
 *                                                                      *
-                  Nat and Symbol
+                  Symbol
 *                                                                      *
 ********************************************************************* -}
 
--- | (Kind) This is the kind of type-level natural numbers.
-data Nat
-
 -- | (Kind) This is the kind of type-level symbols.
 -- Declared here because class IP needs it
 data Symbol