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.

8 files changed, 19 insertions, 27 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