Make DataKinds the sole arbiter of kind-level literals (and friends)wip/T18831

Previously, the use of kind-level literals, promoted tuples,
and promoted lists required enabling both `DataKinds` and
`PolyKinds`. This made sense back in a `TypeInType` world, but not so
much now that `TypeInType`'s role has been superseded. Nowadays,
`PolyKinds` only controls kind polymorphism, so let's make `DataKinds`
the thing that controls the other aspects of `TypeInType`, which include
literals, promoted tuples and promoted lists.

There are some other things that overzealously required `PolyKinds`,
which this patch fixes as well:

* Previously, using constraints in kinds (e.g., `data T :: () -> Type`)
  required `PolyKinds`, despite the fact that this is orthogonal to kind
  polymorphism. This now requires `DataKinds` instead.
* Previously, using kind annotations in kinds
  (e.g., `data T :: (Type :: Type) -> Type`) required both `KindSignatures`
  and `PolyKinds`. This doesn't make much sense, so it only requires
  `KindSignatures` now.

Fixes #18831.

6 files changed, 54 insertions, 36 deletions

diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 9bd1fa64ac..77ece61c14 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -441,9 +441,9 @@ sites. This is less precise, but more accurate.
 rnHsType is here because we call it from loadInstDecl, and I didn't
 want a gratuitous knot.
 
-Note [QualTy in kinds]
+Note [HsQualTy in kinds]
 ~~~~~~~~~~~~~~~~~~~~~~
-I was wondering whether QualTy could occur only at TypeLevel.  But no,
+I was wondering whether HsQualTy could occur only at TypeLevel.  But no,
 we can have a qualified type in a kind too. Here is an example:
 
   type family F a where
@@ -466,9 +466,9 @@ suitable message:
       Expected kind: G Bool
         Actual kind: F Bool
 
-However: in a kind, the constraints in the QualTy must all be
+However: in a kind, the constraints in the HsQualTy must all be
 equalities; or at least, any kinds with a class constraint are
-uninhabited.
+uninhabited. See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
 -}
 
 data RnTyKiEnv
@@ -574,7 +574,9 @@ rnHsTyKi env ty@(HsForAllTy { hst_tele = tele, hst_body = tau })
                 , fvs) } }
 
 rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
-  = do { checkPolyKinds env ty  -- See Note [QualTy in kinds]
+  = do { data_kinds <- xoptM LangExt.DataKinds -- See Note [HsQualTy in kinds]
+       ; when (not data_kinds && isRnKindLevel env)
+              (addErr (dataKindsErr env ty))
        ; (ctxt', fvs1) <- rnTyKiContext env lctxt
        ; (tau',  fvs2) <- rnLHsTyKi env tau
        ; return (HsQualTy { hst_xqual = noExtField, hst_ctxt = ctxt'
@@ -636,9 +638,8 @@ rnHsTyKi env listTy@(HsListTy _ ty)
        ; (ty', fvs) <- rnLHsTyKi env ty
        ; return (HsListTy noExtField ty', fvs) }
 
-rnHsTyKi env t@(HsKindSig _ ty k)
-  = do { checkPolyKinds env t
-       ; kind_sigs_ok <- xoptM LangExt.KindSignatures
+rnHsTyKi env (HsKindSig _ ty k)
+  = do { kind_sigs_ok <- xoptM LangExt.KindSignatures
        ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
        ; (ty', lhs_fvs) <- rnLHsTyKi env ty
        ; (k', sig_fvs)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
@@ -665,7 +666,6 @@ rnHsTyKi env tyLit@(HsTyLit _ t)
   = do { data_kinds <- xoptM LangExt.DataKinds
        ; unless data_kinds (addErr (dataKindsErr env tyLit))
        ; when (negLit t) (addErr negLitErr)
-       ; checkPolyKinds env tyLit
        ; return (HsTyLit noExtField t, emptyFVs) }
   where
     negLit (HsStrTy _ _) = False
@@ -705,15 +705,13 @@ rnHsTyKi _ (XHsType (NHsCoreTy ty))
     -- but I don't think it matters
 
 rnHsTyKi env ty@(HsExplicitListTy _ ip tys)
-  = do { checkPolyKinds env ty
-       ; data_kinds <- xoptM LangExt.DataKinds
+  = do { data_kinds <- xoptM LangExt.DataKinds
        ; unless data_kinds (addErr (dataKindsErr env ty))
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsExplicitListTy noExtField ip tys', fvs) }
 
 rnHsTyKi env ty@(HsExplicitTupleTy _ tys)
-  = do { checkPolyKinds env ty
-       ; data_kinds <- xoptM LangExt.DataKinds
+  = do { data_kinds <- xoptM LangExt.DataKinds
        ; unless data_kinds (addErr (dataKindsErr env ty))
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsExplicitTupleTy noExtField tys', fvs) }
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst
index 7105b1adc8..86bd8832f5 100644
--- a/docs/users_guide/exts/data_kinds.rst
+++ b/docs/users_guide/exts/data_kinds.rst
@@ -134,6 +134,12 @@ promotion quote and the data constructor: ::
   type S = 'A'   -- ERROR: looks like a character
   type R = ' A'  -- OK: promoted `A'`
 
+Type-level literals
+-------------------
+
+:extension:`DataKinds` enables the use of numeric and string literals at the
+type level. For more information, see :ref:`type-level-literals`.
+
 .. _promoted-lists-and-tuples:
 
 Promoted list and tuple types
@@ -207,4 +213,27 @@ above code is valid.
 
 See also :ghc-ticket:`7347`.
 
+.. _constraints_in_kinds:
+
+Constraints in kinds
+--------------------
+
+Kinds can (with :extension:`DataKinds`) contain type constraints. However,
+only equality constraints are supported.
+
+Here is an example of a constrained kind: ::
+
+  type family IsTypeLit a where
+    IsTypeLit Nat    = 'True
+    IsTypeLit Symbol = 'True
+    IsTypeLit a      = 'False
+
+  data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
+    MkNat    :: T 42
+    MkSymbol :: T "Don't panic!"
 
+The declarations above are accepted. However, if we add ``MkOther :: T Int``,
+we get an error that the equality constraint is not satisfied; ``Int`` is
+not a type literal. Note that explicitly quantifying with ``forall a`` is
+necessary in order for ``T`` to typecheck
+(see :ref:`complete-kind-signatures`).
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst
index 39bd6e6f49..58800d47cb 100644
--- a/docs/users_guide/exts/poly_kinds.rst
+++ b/docs/users_guide/exts/poly_kinds.rst
@@ -787,29 +787,6 @@ distinction). GHC does not consider ``forall k. k -> Type`` and
 ``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
 ``Foo Proxy`` as ill-kinded.
 
-Constraints in kinds
---------------------
-
-As kinds and types are the same, kinds can (with :extension:`TypeInType`)
-contain type constraints. However, only equality constraints are supported.
-
-Here is an example of a constrained kind: ::
-
-  type family IsTypeLit a where
-    IsTypeLit Nat    = 'True
-    IsTypeLit Symbol = 'True
-    IsTypeLit a      = 'False
-
-  data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
-    MkNat    :: T 42
-    MkSymbol :: T "Don't panic!"
-
-The declarations above are accepted. However, if we add ``MkOther :: T Int``,
-we get an error that the equality constraint is not satisfied; ``Int`` is
-not a type literal. Note that explicitly quantifying with ``forall a`` is
-necessary in order for ``T`` to typecheck
-(see :ref:`complete-kind-signatures`).
-
 The kind ``Type``
 -----------------
 
diff --git a/testsuite/tests/th/T17688b.hs b/testsuite/tests/th/T17688b.hs
index f78cf0266a..f6252b79a4 100644
--- a/testsuite/tests/th/T17688b.hs
+++ b/testsuite/tests/th/T17688b.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
diff --git a/testsuite/tests/typecheck/should_compile/T18831.hs b/testsuite/tests/typecheck/should_compile/T18831.hs
new file mode 100644
index 0000000000..f717aa911a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18831.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+module T18831 where
+
+import Data.Kind
+import Data.Proxy
+
+data T1 :: Proxy 0 -> Type
+data T2 :: () => Type
+data T3 :: (Type :: Type) -> Type
+data T4 :: Proxy '[Type,Type] -> Type
+data T5 :: Proxy '(Type,Type) -> Type
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a74a84f461..ad682924e2 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -722,5 +722,6 @@ test('T18412', normal, compile, [''])
 test('T18470', normal, compile, [''])
 test('T18323', normal, compile, [''])
 test('T18585', normal, compile, [''])
+test('T18831', normal, compile, [''])
 test('T15942', normal, compile, [''])