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.

29 files changed, 129 insertions, 78 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index baae7a1019..881753f6f2 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -1872,7 +1872,7 @@ uIntTyConKey    = mkPreludeTyConUnique 162
 uWordTyConKey   = mkPreludeTyConUnique 163
 
 -- Type-level naturals
-typeNatKindConNameKey, typeSymbolKindConNameKey,
+typeSymbolKindConNameKey,
   typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
   typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
   , typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey
@@ -1880,7 +1880,6 @@ typeNatKindConNameKey, typeSymbolKindConNameKey,
   , typeNatModTyFamNameKey
   , typeNatLogTyFamNameKey
   :: Unique
-typeNatKindConNameKey     = mkPreludeTyConUnique 164
 typeSymbolKindConNameKey  = mkPreludeTyConUnique 165
 typeNatAddTyFamNameKey    = mkPreludeTyConUnique 166
 typeNatMulTyFamNameKey    = mkPreludeTyConUnique 167
diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
index b254bc233d..abc8e90bcb 100644
--- a/compiler/GHC/Builtin/Types.hs
+++ b/compiler/GHC/Builtin/Types.hs
@@ -96,7 +96,7 @@ module GHC.Builtin.Types (
         mkSumTy, sumTyCon, sumDataCon,
 
         -- * Kinds
-        typeNatKindCon, typeNatKind, typeSymbolKindCon, typeSymbolKind,
+        typeSymbolKindCon, typeSymbolKind,
         isLiftedTypeKindTyConName, liftedTypeKind,
         typeToTypeKind, constraintKind,
         liftedTypeKindTyCon, constraintKindTyCon,  constraintKindTyConName,
@@ -256,7 +256,6 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
                 , heqTyCon
                 , eqTyCon
                 , coercibleTyCon
-                , typeNatKindCon
                 , typeSymbolKindCon
                 , runtimeRepTyCon
                 , vecCountTyCon
@@ -477,8 +476,7 @@ makeRecoveryTyCon tc
         -- at (promoted) use-sites of MkT.
 
 -- Kinds
-typeNatKindConName, typeSymbolKindConName :: Name
-typeNatKindConName    = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Nat")    typeNatKindConNameKey    typeNatKindCon
+typeSymbolKindConName :: Name
 typeSymbolKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Symbol") typeSymbolKindConNameKey typeSymbolKindCon
 
 constraintKindTyConName :: Name
@@ -679,14 +677,11 @@ pcSpecialDataCon dc_name arg_tys tycon rri
 ************************************************************************
 -}
 
-typeNatKindCon, typeSymbolKindCon :: TyCon
--- data Nat
+typeSymbolKindCon :: TyCon
 -- data Symbol
-typeNatKindCon    = pcTyCon typeNatKindConName    Nothing [] []
 typeSymbolKindCon = pcTyCon typeSymbolKindConName Nothing [] []
 
-typeNatKind, typeSymbolKind :: Kind
-typeNatKind    = mkTyConTy typeNatKindCon
+typeSymbolKind :: Kind
 typeSymbolKind = mkTyConTy typeSymbolKindCon
 
 constraintKindTyCon :: TyCon
diff --git a/compiler/GHC/Builtin/Types.hs-boot b/compiler/GHC/Builtin/Types.hs-boot
index 95bed63a40..000df212c3 100644
--- a/compiler/GHC/Builtin/Types.hs-boot
+++ b/compiler/GHC/Builtin/Types.hs-boot
@@ -8,7 +8,7 @@ import GHC.Types.Basic (Arity, TupleSort, Boxity, ConTag)
 import {-# SOURCE #-} GHC.Types.Name (Name)
 
 listTyCon :: TyCon
-typeNatKind, typeSymbolKind :: Type
+typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
 
 coercibleTyCon, heqTyCon :: TyCon
diff --git a/compiler/GHC/Builtin/Types/Literals.hs b/compiler/GHC/Builtin/Types/Literals.hs
index cbb9f9e847..0f609eaad8 100644
--- a/compiler/GHC/Builtin/Types/Literals.hs
+++ b/compiler/GHC/Builtin/Types/Literals.hs
@@ -236,7 +236,7 @@ typeNatLogTyCon = mkTypeNatFunTyCon1 name
 typeNatLeqTyCon :: TyCon
 typeNatLeqTyCon =
   mkFamilyTyCon name
-    (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
+    (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
     boolTy
     Nothing
     (BuiltInSynFamTyCon ops)
@@ -255,7 +255,7 @@ typeNatLeqTyCon =
 typeNatCmpTyCon :: TyCon
 typeNatCmpTyCon =
   mkFamilyTyCon name
-    (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
+    (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
     orderingKind
     Nothing
     (BuiltInSynFamTyCon ops)
@@ -301,14 +301,12 @@ typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
   name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol")
                 typeSymbolAppendFamNameKey typeSymbolAppendTyCon
 
-
-
 -- Make a unary built-in constructor of kind: Nat -> Nat
 mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon1 op tcb =
   mkFamilyTyCon op
-    (mkTemplateAnonTyConBinders [ typeNatKind ])
-    typeNatKind
+    (mkTemplateAnonTyConBinders [ naturalTy ])
+    naturalTy
     Nothing
     (BuiltInSynFamTyCon tcb)
     Nothing
@@ -319,8 +317,8 @@ mkTypeNatFunTyCon1 op tcb =
 mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon2 op tcb =
   mkFamilyTyCon op
-    (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
-    typeNatKind
+    (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
+    naturalTy
     Nothing
     (BuiltInSynFamTyCon tcb)
     Nothing
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 6e612f6e1f..49dd3f97b9 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -253,7 +253,7 @@ import GHC.Types.Unique.Set
 import GHC.Core.TyCon
 import GHC.Builtin.Types.Prim
 import {-# SOURCE #-} GHC.Builtin.Types
-                                 ( listTyCon, typeNatKind
+                                 ( naturalTy, listTyCon
                                  , typeSymbolKind, liftedTypeKind
                                  , constraintKind
                                  , unrestrictedFunTyCon
@@ -2599,7 +2599,7 @@ tcReturnsConstraintKind _                       = False
 
 --------------------------
 typeLiteralKind :: TyLit -> Kind
-typeLiteralKind (NumTyLit {}) = typeNatKind
+typeLiteralKind (NumTyLit {}) = naturalTy
 typeLiteralKind (StrTyLit {}) = typeSymbolKind
 
 -- | Returns True if a type is levity polymorphic. Should be the same
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index f1140afae1..5072fa1fc4 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -53,7 +53,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.Multiplicity
-import GHC.Builtin.Types ( typeNatKind, typeSymbolKind )
+import GHC.Builtin.Types ( naturalTy, typeSymbolKind )
 import GHC.Types.Id
 import GHC.Types.Id.Make(proxyHashId)
 import GHC.Types.Name
@@ -1306,7 +1306,7 @@ ds_ev_typeable ty (EvTypeableTyLit ev)
     -- tr_fun is the Name of
     --       typeNatTypeRep    :: KnownNat    a => Proxy# a -> TypeRep a
     -- of    typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep a
-    tr_fun | ty_kind `eqType` typeNatKind    = typeNatTypeRepName
+    tr_fun | ty_kind `eqType` naturalTy      = typeNatTypeRepName
            | ty_kind `eqType` typeSymbolKind = typeSymbolTypeRepName
            | otherwise = panic "dsEvTypeable: unknown type lit kind"
 
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 324bdca5bf..d0b841b41b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1192,8 +1192,8 @@ tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
 
 --------- Literals
 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
-  = do { checkWiredInTyCon typeNatKindCon
-       ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
+  = do { checkWiredInTyCon naturalTyCon
+       ; checkExpectedKind rn_ty (mkNumLitTy n) naturalTy exp_kind }
 
 tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
   = do { checkWiredInTyCon typeSymbolKindCon
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 10270e3726..639a9e6cf1 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -418,7 +418,7 @@ matchTypeable clas [k,t]  -- clas = Typeable
   | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
 
   -- Now cases that do work
-  | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
+  | k `eqType` naturalTy                   = doTyLit knownNatClassName         t
   | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
   | tcIsConstraintKind t                   = doTyConApp clas t constraintKindTyCon []
   | Just (mult,arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t mult arg ret
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index f8e9853e8f..673fc9f169 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -28,8 +28,24 @@ Compiler
   since the argument was already forced in the first equation. For more
   details see :ghc-flag:`-Wredundant-bang-patterns`.
 
+- Type checker plugins which work with the natural numbers now
+  should use ``naturalTy`` kind instead of ``typeNatKind``, which has been removed.
+
 ``ghc-prim`` library
 ~~~~~~~~~~~~~~~~~~~~
 
 - ``Void#`` is now a type synonym for the unboxed tuple ``(# #)``.
   Code using ``Void#`` now has to enable :extension:`UnboxedTuples`.
+
+``base`` library
+~~~~~~~~~~~~~~~~
+
+- It's possible now to promote the ``Natural`` type: :: 
+    
+    data Coordinate = Mk2D Natural Natural
+    type MyCoordinate = Mk2D 1 10
+    
+  The separate kind ``Nat`` is removed and now it is just a type synonym for
+  ``Natural``. As a consequence, one must enable ``TypeSynonymInstances``
+  in order to define instances for ``Nat``.
+
diff --git a/docs/users_guide/exts/type_literals.rst b/docs/users_guide/exts/type_literals.rst
index cbf4d89023..202577668d 100644
--- a/docs/users_guide/exts/type_literals.rst
+++ b/docs/users_guide/exts/type_literals.rst
@@ -5,7 +5,7 @@ Type-Level Literals
 
 GHC supports numeric and string literals at the type level, giving
 convenient access to a large number of predefined type-level constants.
-Numeric literals are of kind ``Nat``, while string literals are of kind
+Numeric literals are of kind ``Natural``, while string literals are of kind
 ``Symbol``. This feature is enabled by the :extension:`DataKinds` language
 extension.
 
@@ -23,11 +23,17 @@ safe interface to a low-level function: ::
     import Data.Word
     import Foreign
 
-    newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)
+    newtype ArrPtr (n :: Natural) a = ArrPtr (Ptr a)
 
     clearPage :: ArrPtr 4096 Word8 -> IO ()
     clearPage (ArrPtr p) = ...
 
+Also type-level naturals could be promoted from the ``Natural`` data type
+using `DataKinds`, for example: ::
+
+    data Point = MkPoint Natural Natural
+    type MyCoordinates = MkPoint 95 101
+
 Here is an example of using type-level string literals to simulate
 simple record operations: ::
 
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
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index c523624fe2..170e17b995 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -39,47 +39,53 @@ GHC.TypeLits.symbolVal ::
   GHC.TypeLits.KnownSymbol n => proxy n -> String
 GHC.TypeLits.symbolVal' ::
   GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String
-type (GHC.TypeNats.*) :: GHC.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+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.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+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.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+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.Types.Nat
-                          -> GHC.Types.Nat -> Constraint
+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.Types.Nat -> GHC.Types.Nat -> Bool
+type (GHC.TypeNats.<=?) :: GHC.Num.Natural.Natural
+                           -> GHC.Num.Natural.Natural -> Bool
 type family (GHC.TypeNats.<=?) a b
-type GHC.TypeNats.CmpNat :: GHC.Types.Nat
-                            -> GHC.Types.Nat -> Ordering
+type GHC.TypeNats.CmpNat :: GHC.Num.Natural.Natural
+                            -> GHC.Num.Natural.Natural -> Ordering
 type family GHC.TypeNats.CmpNat a b
-type GHC.TypeNats.Div :: GHC.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+type GHC.TypeNats.Div :: GHC.Num.Natural.Natural
+                         -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family GHC.TypeNats.Div a b
-type GHC.TypeNats.KnownNat :: GHC.Types.Nat -> Constraint
+type GHC.TypeNats.KnownNat :: GHC.TypeNats.Nat -> Constraint
 class GHC.TypeNats.KnownNat n where
   GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
   {-# MINIMAL natSing #-}
-type GHC.TypeNats.Log2 :: GHC.Types.Nat -> GHC.Types.Nat
+type GHC.TypeNats.Log2 :: GHC.Num.Natural.Natural
+                          -> GHC.Num.Natural.Natural
 type family GHC.TypeNats.Log2 a
-type GHC.TypeNats.Mod :: GHC.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+type GHC.TypeNats.Mod :: GHC.Num.Natural.Natural
+                         -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family GHC.TypeNats.Mod a b
-type GHC.Types.Nat :: *
-data GHC.Types.Nat
+type GHC.TypeNats.Nat :: *
+type GHC.TypeNats.Nat = GHC.Num.Natural.Natural
+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 GHC.TypeNats.SomeNat :: *
 data GHC.TypeNats.SomeNat
-  = forall (n :: GHC.Types.Nat).
+  = forall (n :: GHC.TypeNats.Nat).
     GHC.TypeNats.KnownNat n =>
     GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
 type GHC.Types.Symbol :: *
 data GHC.Types.Symbol
-type (GHC.TypeNats.^) :: GHC.Types.Nat
-                         -> GHC.Types.Nat -> GHC.Types.Nat
+type (GHC.TypeNats.^) :: GHC.Num.Natural.Natural
+                         -> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
 type family (GHC.TypeNats.^) a b
 GHC.TypeNats.sameNat ::
   (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
diff --git a/testsuite/tests/indexed-types/should_compile/T13398b.hs b/testsuite/tests/indexed-types/should_compile/T13398b.hs
index 703a81763a..e02a536ff1 100644
--- a/testsuite/tests/indexed-types/should_compile/T13398b.hs
+++ b/testsuite/tests/indexed-types/should_compile/T13398b.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 module T13398b where
 
 import GHC.TypeLits
diff --git a/testsuite/tests/indexed-types/should_compile/T15322a.stderr b/testsuite/tests/indexed-types/should_compile/T15322a.stderr
index 37a9070e27..d3f938eccc 100644
--- a/testsuite/tests/indexed-types/should_compile/T15322a.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15322a.stderr
@@ -4,7 +4,7 @@ T15322a.hs:12:7: error:
         arising from a use of ‘typeRep’
       from the context: KnownNat n
         bound by the type signature for:
-                   f :: forall (n :: GHC.Types.Nat).
+                   f :: forall (n :: GHC.TypeNats.Nat).
                         KnownNat n =>
                         Proxy n -> TypeRep (n + 1)
         at T15322a.hs:11:1-56
diff --git a/testsuite/tests/th/T15360b.stderr b/testsuite/tests/th/T15360b.stderr
index 7bfacf202e..f39226dda8 100644
--- a/testsuite/tests/th/T15360b.stderr
+++ b/testsuite/tests/th/T15360b.stderr
@@ -5,7 +5,7 @@ T15360b.hs:10:13: error:
       In the type signature: x :: Proxy (Type Double)
 
 T15360b.hs:13:13: error:
-    • Expected kind ‘* -> k2’, but ‘1’ has kind ‘GHC.Types.Nat’
+    • Expected kind ‘* -> k2’, but ‘1’ has kind ‘GHC.Num.Natural.Natural’
     • In the first argument of ‘Proxy’, namely ‘(1 Int)’
       In the type signature: y :: Proxy (1 Int)
 
diff --git a/testsuite/tests/typecheck/should_compile/T10776.hs b/testsuite/tests/typecheck/should_compile/T10776.hs
new file mode 100644
index 0000000000..ae724dcd7b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10776.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, TypeOperators #-}
+
+module T10776 where
+
+import GHC.TypeLits (Nat, Natural, Symbol, KnownNat)
+import Data.Type.Equality ((:~:)(..))
+import Data.Proxy
+
+nat_is_natural :: Nat :~: Natural
+nat_is_natural = Refl
+
+data NatPair = TN Natural Natural
+
+type X = TN 1 101
+
+type family SecondNat (a :: NatPair) :: Nat where
+    SecondNat ('TN _ a) = a
diff --git a/testsuite/tests/typecheck/should_fail/T15799.stderr b/testsuite/tests/typecheck/should_fail/T15799.stderr
index 4e6d7b4dfd..6823cadb8c 100644
--- a/testsuite/tests/typecheck/should_fail/T15799.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15799.stderr
@@ -1,4 +1,5 @@
 
 T15799.hs:46:62: error:
+    Couldn't match kind ‘TypeLits.Natural’ with ‘Op Nat’
     • Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’
     • In the first argument of ‘(<=)’, namely ‘UnOp b’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
index c868a1321e..fe78140a80 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
@@ -1,5 +1,5 @@
 
 UnliftedNewtypesFamilyKindFail1.hs:11:31: error:
-    • Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+    • Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
     • In the kind ‘5’
       In the data family declaration for ‘DF’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
index 57c4a3c2e9..05f3a935eb 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
@@ -1,10 +1,10 @@
 UnliftedNewtypesFamilyKindFail2.hs:12:20:
-     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
      In the first argument of ‘F’, namely ‘5’
       In the newtype instance declaration for ‘F’
 
 UnliftedNewtypesFamilyKindFail2.hs:12:31:
-     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
      In the first argument of ‘F’, namely ‘5’
       In the type ‘(F 5)’
       In the definition of data constructor ‘MkF’
diff --git a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
index 7769b78eb9..1303db844c 100644
--- a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
+++ b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
@@ -12,4 +12,4 @@ good: *
 good: Int -> Int
 good: 5
 good: "hello world"
-good: 'Just Nat 5
+good: 'Just Natural 5
diff --git a/testsuite/tests/typecheck/should_run/TypeOf.stdout b/testsuite/tests/typecheck/should_run/TypeOf.stdout
index 912fe39a84..40d2cb5f8f 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeOf.stdout
@@ -12,13 +12,13 @@ Int -> Int
 Proxy Constraint (Eq Int)
 Proxy * (Int,Int)
 Proxy Symbol "hello world"
-Proxy Nat 1
-Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
+Proxy Natural 1
+Proxy [Natural] (': Natural 1 (': Natural 2 (': Natural 3 ('[] Natural))))
 Proxy Ordering 'EQ
 Proxy (RuntimeRep -> *) TYPE
 Proxy * *
 Proxy * *
 Proxy * *
 Proxy RuntimeRep 'LiftedRep
-Proxy (Nat,Symbol) ('(,) Nat Symbol 1 "hello")
+Proxy (Natural,Symbol) ('(,) Natural Symbol 1 "hello")
 Proxy (* -> * -> Constraint) ((~~) * *)
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.stdout b/testsuite/tests/typecheck/should_run/TypeRep.stdout
index 46cb8e4ce7..a0c03e09d8 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeRep.stdout
@@ -17,8 +17,8 @@ Int#
 Proxy Constraint (Eq Int)
 Proxy * (Int,Int)
 Proxy Symbol "hello world"
-Proxy Nat 1
-Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
+Proxy Natural 1
+Proxy [Natural] (': Natural 1 (': Natural 2 (': Natural 3 ('[] Natural))))
 Proxy Ordering 'EQ
 Proxy (RuntimeRep -> *) TYPE
 Proxy * *
diff --git a/utils/haddock b/utils/haddock
-Subproject 6f16399e0320d0ef5e6c3dd0329ce7ed3715b6b
+Subproject f7d9e0bb987ca31c3b15cbe63198dafbeee3a39