Fix #14710 with more validity checks during renaming

Summary:
#14710 revealed two unfortunate regressions related to kind
polymorphism that had crept in in recent GHC releases:

1. While GHC was able to catch illegal uses of kind polymorphism
   (i.e., if `PolyKinds` wasn't enabled) in limited situations, it
   wasn't able to catch kind polymorphism of the following form:

```lang=haskell
f :: forall a. a -> a
f x = const x g
  where
    g :: Proxy (x :: a)
    g = Proxy
```

Note that the variable `a` is being used as a kind variable in the
type signature of `g`, but GHC happily accepts it, even without
the use of `PolyKinds`.

2. If you have `PolyKinds` (but not `TypeInType`) enabled, then GHC
   incorrectly accepts the following definition:

```lang=haskell
f :: forall k (a :: k). Proxy a
f = Proxy
```

Even though `k` is explicitly bound and then later used as a kind
variable within the same telescope.

This patch fixes these two bugs as follows:

1. Whenever we rename any `HsTyVar`, we check if the following three
   criteria are met:

   (a) It's a type variable
   (b) It's used at the kind level
   (c) `PolyKinds` is not enabled

   If so, then we have found an illegal use of kind polymorphism, so
   throw an error.

   This check replaces the `checkBadKindBndrs` function, which could
   only catch illegal uses of kind polymorphism in very limited
   situations (when the bad kind variable happened to be implicitly
   quantified in the same type signature).

2. In `extract_hs_tv_bndrs`, we must error if `TypeInType` is not
   enabled and either of the following criteria are met:

   (a) An explicitly bound type variable is used in kind position
       in the body of a `forall` type.
   (b) An explicitly bound type variable is used in kind position
       in the kind of a bound type variable in a `forall` type.

   `extract_hs_tv_bndrs` was checking (a), but not (b). Easily fixed.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari, hvr

Reviewed By: simonpj

Subscribers: thomie, carter

GHC Trac Issues: #14710

Differential Revision: https://phabricator.haskell.org/D4554

1 files changed, 19 insertions, 0 deletions

diff --git a/docs/users_guide/8.6.1-notes.rst b/docs/users_guide/8.6.1-notes.rst
index 996fb17a28..25a4ac349b 100644
--- a/docs/users_guide/8.6.1-notes.rst
+++ b/docs/users_guide/8.6.1-notes.rst
@@ -70,6 +70,25 @@ Language
   See :ref:`Numeric underscores <numeric-underscores>`
   for the full details.
 
+- GHC is now more diligent about catching illegal uses of kind polymorphism.
+  For instance, this used to be accepted without :extension:`PolyKinds`: ::
+
+    class C a where
+      c :: Proxy (x :: a)
+
+  Despite the fact that ``a`` is used as a kind variable in the type signature
+  for ``c``. This is now an error unless :extension:`PolyKinds` is explicitly
+  enabled.
+
+  Moreover, GHC 8.4 would accept the following without the use of
+  :extension:`TypeInType` (or even :extension:`PolyKinds`!): ::
+
+    f :: forall k (a :: k). Proxy a
+    f = Proxy
+
+  Despite the fact that ``k`` is used as both a type and kind variable. This is
+  now an error unless :extension:`TypeInType` is explicitly enabled.
+
 Compiler
 ~~~~~~~~