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

8 files changed, 139 insertions, 36 deletions

diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 8bea770a08..d242ac08c6 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -1929,7 +1929,7 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
               mb_ctxt = Just (inHsDocContext ctxt)
 
         ; traceRn "rnConDecl" (ppr names $$ ppr free_tkvs $$ ppr explicit_forall )
-        ; rnImplicitBndrs (not explicit_forall) ctxt free_tkvs $ \ implicit_tkvs ->
+        ; rnImplicitBndrs (not explicit_forall) free_tkvs $ \ implicit_tkvs ->
           bindLHsTyVarBndrs ctxt mb_ctxt Nothing explicit_tkvs $ \ explicit_tkvs ->
     do  { (new_cxt, fvs1)    <- rnMbContext ctxt mcxt
         ; (new_args, fvs2)   <- rnConDeclDetails (unLoc (head new_names)) ctxt args
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 0aada39bd4..c4ab448e61 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -125,7 +125,7 @@ rn_hs_sig_wc_type always_bind_free_tvs ctxt
        ; (tv_rdrs, nwc_rdrs') <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
              bind_free_tvs = always_bind_free_tvs || not (isLHsForAllTy hs_ty)
-       ; rnImplicitBndrs bind_free_tvs ctxt tv_rdrs $ \ vars ->
+       ; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = ib_ty' }
              ib_ty'  = mk_implicit_bndrs vars hs_ty' fvs1
@@ -294,7 +294,7 @@ rnHsSigType :: HsDocContext -> LHsSigType GhcPs
 rnHsSigType ctx (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; vars <- extractFilteredRdrTyVarsDups hs_ty
-       ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) ctx vars $ \ vars ->
+       ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
     do { (body', fvs) <- rnLHsType ctx hs_ty
        ; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
 
@@ -303,14 +303,13 @@ rnImplicitBndrs :: Bool    -- True <=> bring into scope any free type variables
                            --  we do not want to bring 'b' into scope, hence False
                            -- But   f :: a -> b
                            --  we want to bring both 'a' and 'b' into scope
-                -> HsDocContext
                 -> FreeKiTyVarsWithDups
                                    -- Free vars of hs_ty (excluding wildcards)
                                    -- May have duplicates, which is
                                    -- checked here
                 -> ([Name] -> RnM (a, FreeVars))
                 -> RnM (a, FreeVars)
-rnImplicitBndrs bind_free_tvs doc
+rnImplicitBndrs bind_free_tvs
                 fvs_with_dups@(FKTV { fktv_kis = kvs_with_dups
                                     , fktv_tys = tvs_with_dups })
                 thing_inside
@@ -333,8 +332,6 @@ rnImplicitBndrs bind_free_tvs doc
        ; loc <- getSrcSpanM
        ; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
 
-       ; checkBadKindBndrs doc kvs
-
        ; traceRn "checkMixedVars2" $
            vcat [ text "kvs_with_dups" <+> ppr kvs_with_dups
                 , text "tvs_with_dups" <+> ppr tvs_with_dups ]
@@ -538,7 +535,14 @@ rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
                 , fvs1 `plusFV` fvs2) }
 
 rnHsTyKi env (HsTyVar _ ip (L loc rdr_name))
-  = do { name <- rnTyVar env rdr_name
+  = do { when (isRnKindLevel env && isRdrTyVar rdr_name) $
+         unlessXOptM LangExt.PolyKinds $ addErr $
+         withHsDocContext (rtke_ctxt env) $
+         vcat [ text "Unexpected kind variable" <+> quotes (ppr rdr_name)
+              , text "Perhaps you intended to use PolyKinds" ]
+           -- Any type variable at the kind level is illegal without the use
+           -- of PolyKinds (see #14710)
+       ; name <- rnTyVar env rdr_name
        ; return (HsTyVar noExt ip (L loc name), unitFV name) }
 
 rnHsTyKi env ty@(HsOpTy _ ty1 l_op ty2)
@@ -936,7 +940,6 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
                 , text "bndr_kv_occs"   <+> ppr bndr_kv_occs
                 , text "wubble" <+> ppr ((kv_occs \\ bndrs) \\ bndr_kv_occs)
                 ]
-       ; checkBadKindBndrs doc implicit_kvs
        ; checkMixedVars kv_occs bndrs
 
        ; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs
@@ -1041,6 +1044,34 @@ In implementation terms
   scope in the kind of 'a'.
 
 * Similarly in extract_hs_tv_bndrs
+
+Note [Variables used as both types and kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In (checkMixedVars kvs tvs), we bind the type variables tvs, and kvs is the
+set of free variables of the kinds in the scope of the binding. Here is one
+typical example:
+
+   forall a b. a -> (b::k) -> (c::a)
+
+Here, tvs will be {a,b}, and kvs {k,a}.
+Without -XTypeInType we want to complain that `a` is used both
+as a type and a kind.
+
+Specifically, check that there is no overlap between kvs and tvs
+See typecheck/should_fail/T11963 for examples.
+
+We must also make sure that kvs includes all of variables in the kinds of type
+variable bindings. For instance:
+
+   forall k (a :: k). Proxy a
+
+If we only look in the body of the `forall` type, we will mistakenly conclude
+that kvs is {}. But in fact, the type variable `k` is also used as a kind
+variable in (a :: k), later in the binding. (This mistake lead to #14710.)
+So tvs is {k,a} and kvs is {k}, so we must also reject this without the use
+of -XTypeInType.
+
+NB: we do this only at the binding site of 'tvs'.
 -}
 
 bindLHsTyVarBndrs :: HsDocContext
@@ -1515,15 +1546,6 @@ unexpectedTypeSigErr ty
   = hang (text "Illegal type signature:" <+> quotes (ppr ty))
        2 (text "Type signatures are only allowed in patterns with ScopedTypeVariables")
 
-checkBadKindBndrs :: HsDocContext -> [Located RdrName] -> RnM ()
-checkBadKindBndrs doc kvs
-  = unless (null kvs)             $
-    unlessXOptM LangExt.PolyKinds $
-    addErr (withHsDocContext doc  $
-            hang (text "Unexpected kind variable" <> plural kvs
-                  <+> pprQuotedList kvs)
-               2 (text "Perhaps you intended to use PolyKinds"))
-
 badKindSigErr :: HsDocContext -> LHsType GhcPs -> TcM ()
 badKindSigErr doc (L loc ty)
   = setSrcSpan loc $ addErr $
@@ -1866,16 +1888,22 @@ extract_hs_tv_bndrs tv_bndrs
   | otherwise
   = do { bndr_kvs <- extract_hs_tv_bndrs_kvs tv_bndrs
 
-       ; let tv_bndr_rdrs :: [Located RdrName]
+       ; let tv_bndr_rdrs, all_kv_occs :: [Located RdrName]
              tv_bndr_rdrs = map hsLTyVarLocName tv_bndrs
+             -- We must include both kind variables from the binding as well
+             -- as the body of the `forall` type.
+             -- See Note [Variables used as both types and kinds].
+             all_kv_occs = bndr_kvs ++ body_kvs
 
        ; traceRn "checkMixedVars1" $
-           vcat [ text "body_kvs"     <+> ppr body_kvs
+           vcat [ text "bndr_kvs"     <+> ppr bndr_kvs
+                , text "body_kvs"     <+> ppr body_kvs
+                , text "all_kv_occs"  <+> ppr all_kv_occs
                 , text "tv_bndr_rdrs" <+> ppr tv_bndr_rdrs ]
-       ; checkMixedVars body_kvs tv_bndr_rdrs
+       ; checkMixedVars all_kv_occs tv_bndr_rdrs
 
        ; return $
-         FKTV (filterOut (`elemRdr` tv_bndr_rdrs) (bndr_kvs ++ body_kvs)
+         FKTV (filterOut (`elemRdr` tv_bndr_rdrs) all_kv_occs
                     -- NB: delete all tv_bndr_rdrs from bndr_kvs as well
                     -- as body_kvs; see Note [Kind variable scoping]
                 ++ acc_kvs)
@@ -1907,19 +1935,9 @@ nubL = nubBy eqLocated
 elemRdr :: Located RdrName -> [Located RdrName] -> Bool
 elemRdr x = any (eqLocated x)
 
+-- Check for type variables that are also used as kinds without the use of
+-- -XTypeInType. See Note [Variables used as both types and kinds].
 checkMixedVars :: [Located RdrName] -> [Located RdrName] -> RnM ()
--- In (checkMixedVars kvs tvs) we are about to bind the type
--- variables tvs, and kvs is the set of free variables of the kinds
--- in the scope of the binding.  E.g.
---    forall a b. a -> (b::k) -> (c::a)
--- Here tv will be {a,b}, and kvs {k,a}.
--- Without -XTypeInType we want to complain that 'a' is used both
--- as a type and a kind.
---
--- Specifically, check that there is no overlap between kvs and tvs
--- See typecheck/should_fail/T11963 for examples
---
--- NB: we do this only at the binding site of 'tvs'.
 checkMixedVars kvs tvs
   = do { type_in_type <- xoptM LangExt.TypeInType
        ; unless type_in_type $
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
 ~~~~~~~~
 
diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs
index 4d5278978c..bccdab4221 100644
--- a/libraries/base/GHC/Base.hs
+++ b/libraries/base/GHC/Base.hs
@@ -84,6 +84,7 @@ Other Prelude modules are much easier with fewer complex dependencies.
            , ExistentialQuantification
            , RankNTypes
            , KindSignatures
+           , TypeInType
   #-}
 -- -Wno-orphans is needed for things like:
 -- Orphan rule: "x# -# x#" ALWAYS forall x# :: Int# -# x# x# = 0
diff --git a/testsuite/tests/polykinds/BadKindVar.stderr b/testsuite/tests/polykinds/BadKindVar.stderr
index 5989c62ea2..beeed2b3c8 100644
--- a/testsuite/tests/polykinds/BadKindVar.stderr
+++ b/testsuite/tests/polykinds/BadKindVar.stderr
@@ -1,4 +1,5 @@
 
-BadKindVar.hs:8:1: error:
-    Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds
+BadKindVar.hs:8:19: error:
+    Unexpected kind variable ‘k’
+    Perhaps you intended to use PolyKinds
     In the type signature for ‘f’
diff --git a/testsuite/tests/polykinds/T14710.hs b/testsuite/tests/polykinds/T14710.hs
new file mode 100644
index 0000000000..2fec10a7a1
--- /dev/null
+++ b/testsuite/tests/polykinds/T14710.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module T14710 where
+
+import Data.Proxy
+
+class C a b where
+  c1 :: Proxy (x :: a) -> b
+  c2 :: forall (x :: a). Proxy x -> b
+
+f :: forall a. a -> a
+f x = const x (const g1 g2)
+  where
+    g1 :: Proxy (x :: a)
+    g1 = Proxy
+
+    g2 :: forall (x :: a). Proxy x
+    g2 = Proxy
+
+h1 :: forall k a. Proxy (a :: k)
+h1 = Proxy
+
+h2 :: forall k (a :: k). Proxy a
+h2 = Proxy
diff --git a/testsuite/tests/polykinds/T14710.stderr b/testsuite/tests/polykinds/T14710.stderr
new file mode 100644
index 0000000000..8d8a9785a8
--- /dev/null
+++ b/testsuite/tests/polykinds/T14710.stderr
@@ -0,0 +1,38 @@
+
+T14710.hs:9:21: error:
+    Unexpected kind variable ‘a’
+    Perhaps you intended to use PolyKinds
+    In a class method signature for ‘c1’
+
+T14710.hs:10:22: error:
+    Unexpected kind variable ‘a’
+    Perhaps you intended to use PolyKinds
+    In a class method signature for ‘c2’
+
+T14710.hs:15:23: error:
+    Unexpected kind variable ‘a’
+    Perhaps you intended to use PolyKinds
+    In the type signature for ‘g1’
+
+T14710.hs:18:24: error:
+    Unexpected kind variable ‘a’
+    Perhaps you intended to use PolyKinds
+    In the type signature for ‘g2’
+
+T14710.hs:21:31: error:
+    Variable ‘k’ used as both a kind and a type
+    Did you intend to use TypeInType?
+
+T14710.hs:21:31: error:
+    Unexpected kind variable ‘k’
+    Perhaps you intended to use PolyKinds
+    In the type signature for ‘h1’
+
+T14710.hs:24:22: error:
+    Variable ‘k’ used as both a kind and a type
+    Did you intend to use TypeInType?
+
+T14710.hs:24:22: error:
+    Unexpected kind variable ‘k’
+    Perhaps you intended to use PolyKinds
+    In the type signature for ‘h2’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 1f547ece57..a405ce8e44 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -183,6 +183,7 @@ test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T14561', normal, compile_fail, [''])
 test('T14580', normal, compile_fail, [''])
 test('T14515', normal, compile, [''])
+test('T14710', normal, compile_fail, [''])
 test('T14723', normal, compile, [''])
 test('T14846', normal, compile_fail, [''])
 test('T14873', normal, compile, [''])