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.

11 files changed, 58 insertions, 33 deletions

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