Warn about implicit kind variables with -Wcompat

According to an accepted proposal
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/002
4-no-kind-vars.rst

    With -Wcompat, warn if a kind variable is brought into scope
    implicitly in a type with an explicit forall. This applies to type
    signatures and to other contexts that allow a forall with the
    forall-or-nothing rule in effect (for example, class instances).

Test Plan: Validate

Reviewers: goldfire, hvr, bgamari, RyanGlScott

Reviewed By: goldfire

Subscribers: RyanGlScott, rwbarton, thomie, carter

GHC Trac Issues: #15264

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

8 files changed, 108 insertions, 4 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 437afc33a7..485eb72942 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -807,6 +807,7 @@ data WarningFlag =
    | Opt_WarnMissingExportList
    | Opt_WarnInaccessibleCode
    | Opt_WarnStarIsType                   -- Since 8.6
+   | Opt_WarnImplicitKindVars             -- Since 8.6
    deriving (Eq, Show, Enum)
 
 data Language = Haskell98 | Haskell2010
@@ -3784,6 +3785,7 @@ wWarningFlagsDeps = [
   flagSpec "hi-shadowing"                Opt_WarnHiShadows,
   flagSpec "inaccessible-code"           Opt_WarnInaccessibleCode,
   flagSpec "implicit-prelude"            Opt_WarnImplicitPrelude,
+  flagSpec "implicit-kind-vars"          Opt_WarnImplicitKindVars,
   flagSpec "incomplete-patterns"         Opt_WarnIncompletePatterns,
   flagSpec "incomplete-record-updates"   Opt_WarnIncompletePatternsRecUpd,
   flagSpec "incomplete-uni-patterns"     Opt_WarnIncompleteUniPatterns,
@@ -4593,6 +4595,7 @@ minusWcompatOpts
     = [ Opt_WarnMissingMonadFailInstances
       , Opt_WarnSemigroup
       , Opt_WarnNonCanonicalMonoidInstances
+      , Opt_WarnImplicitKindVars
       ]
 
 enableUnusedBinds :: DynP ()
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 3d60a9f6c3..ca4986f050 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -334,6 +334,11 @@ rnImplicitBndrs bind_free_tvs
 
        ; traceRn "rnImplicitBndrs" (vcat [ ppr kvs, ppr tvs, ppr real_tvs ])
 
+       ; whenWOptM Opt_WarnImplicitKindVars $
+         unless (bind_free_tvs || null kvs) $
+         addWarnAt (Reason Opt_WarnImplicitKindVars) (getLoc (head kvs)) $
+         implicit_kind_vars_msg kvs
+
        ; loc <- getSrcSpanM
        ; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
 
@@ -343,6 +348,16 @@ rnImplicitBndrs bind_free_tvs
 
        ; bindLocalNamesFV vars $
          thing_inside vars }
+  where
+    implicit_kind_vars_msg kvs =
+      vcat [ text "An explicit" <+> quotes (text "forall") <+>
+             text "was used, but the following kind variables" <+>
+             text "are not quantified:" <+>
+             hsep (punctuate comma (map (quotes . ppr) kvs))
+           , text "Despite this fact, GHC will introduce them into scope," <+>
+             text "but it will stop doing so in the future."
+           , text "Suggested fix: add" <+>
+             quotes (text "forall" <+> hsep (map ppr kvs) <> char '.') ]
 
 rnLHsInstType :: SDoc -> LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars)
 -- Rename the type in an instance.
diff --git a/docs/users_guide/8.6.1-notes.rst b/docs/users_guide/8.6.1-notes.rst
index 4bc01c904e..5b13909401 100644
--- a/docs/users_guide/8.6.1-notes.rst
+++ b/docs/users_guide/8.6.1-notes.rst
@@ -152,6 +152,12 @@ Compiler
   :ghc-flag:`-fexternal-dynamic-refs`. If you don't know why you might
   need this, you don't need it.
 
+- :ghc-flag:`-Wcompat` now includes :ghc-flag:`-Wimplicit-kind-vars` to
+  provide early detection of breakage that will be caused by implementation of
+  `GHC proposal #24
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__
+  in a future release.
+
 Plugins
 ~~~~~~~
 
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 87ddcdabf7..7dc4a3b048 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -109,6 +109,7 @@ The following flags are simple ways to select standard "packages" of warnings:
         * :ghc-flag:`-Wmissing-monadfail-instances`
         * :ghc-flag:`-Wsemigroup`
         * :ghc-flag:`-Wnoncanonical-monoid-instances`
+        * :ghc-flag:`-Wimplicit-kind-vars`
 
 .. ghc-flag:: -Wno-compat
     :shortdesc: Disables all warnings enabled by :ghc-flag:`-Wcompat`.
@@ -768,6 +769,58 @@ of ``-W(no-)*``.
 
     This warning is off by default.
 
+.. ghc-flag:: -Wimplicit-kind-vars
+    :shortdesc: warn when kind variables are brought into scope implicitly despite
+        the "forall-or-nothing" rule
+    :type: dynamic
+    :reverse: -Wno-implicit-kind-vars
+    :category:
+
+    :since: 8.6
+
+    `GHC proposal #24
+    <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__
+    prescribes to treat kind variables and type variables identically in
+    ``forall``, removing the legacy distinction between them.
+
+    Consider the following examples: ::
+
+        f :: Proxy a -> Proxy b -> ()
+        g :: forall a b. Proxy a -> Proxy b -> ()
+
+    ``f`` does not use an explicit ``forall``, so type variables ``a`` and ``b``
+    are brought into scope implicitly. ``g`` quantifies both ``a`` and ``b``
+    explicitly. Both ``f`` and ``g`` work today and will continue to work in the
+    future because they adhere to the "forall-or-nothing" rule: either all type
+    variables in a function definition are introduced explicitly or implicitly,
+    there is no middle ground.
+
+    A violation of the "forall-or-nothing" rule looks like this: ::
+
+        m :: forall a. Proxy a -> Proxy b -> ()
+
+    ``m`` does not introduce one of the variables, ``b``, and thus is rejected.
+
+    However, consider the following example: ::
+
+        n :: forall a. Proxy (a :: k) -> ()
+
+    While ``n`` uses ``k`` without introducing it and thus violates the rule, it
+    is currently accepted. This is because ``k`` in ``n`` is considered a kind
+    variable, as it occurs in a kind signature. In reality, the line between
+    type variables and kind variables is blurry, as the following example
+    demonstrates: ::
+
+        kindOf :: forall a. Proxy (a :: k) -> Proxy k
+
+    In ``kindOf``, the ``k`` variable is used both in a kind position and a type
+    position. Currently, ``kindOf`` happens to be accepted as well.
+
+    In a future release of GHC, both ``n`` and ``kindOf`` will be rejected per
+    the "forall-or-nothing" rule. This warning, being part of the
+    :ghc-flag:`-Wcompat` option group, allows to detect this before the actual
+    breaking change takes place.
+
 .. ghc-flag:: -Wincomplete-patterns
     :shortdesc: warn when a pattern match could fail
     :type: dynamic
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 09290485e4..0d4fc825cf 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -476,7 +476,7 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
       Refl -> IsCon con kinds
 
 -- | Use a 'TypeRep' as 'Typeable' evidence.
-withTypeable :: forall (a :: k) (r :: TYPE rep). ()
+withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
              => TypeRep a -> (Typeable a => r) -> r
 withTypeable rep k = unsafeCoerce k' rep
   where k' :: Gift a r
@@ -631,7 +631,7 @@ unkindedTypeRep :: SomeKindedTypeRep k -> SomeTypeRep
 unkindedTypeRep (SomeKindedTypeRep x) = SomeTypeRep x
 
 data SomeKindedTypeRep k where
-    SomeKindedTypeRep :: forall (a :: k). TypeRep a
+    SomeKindedTypeRep :: forall k (a :: k). TypeRep a
                       -> SomeKindedTypeRep k
 
 kApp :: SomeKindedTypeRep (k -> k')
@@ -640,7 +640,7 @@ kApp :: SomeKindedTypeRep (k -> k')
 kApp (SomeKindedTypeRep f) (SomeKindedTypeRep a) =
     SomeKindedTypeRep (mkTrApp f a)
 
-kindedTypeRep :: forall (a :: k). Typeable a => SomeKindedTypeRep k
+kindedTypeRep :: forall k (a :: k). Typeable a => SomeKindedTypeRep k
 kindedTypeRep = SomeKindedTypeRep (typeRep @a)
 
 buildList :: forall k. Typeable k
@@ -980,7 +980,8 @@ tcNat :: TyCon
 tcNat = typeRepTyCon (typeRep @Nat)
 
 -- | An internal function, to make representations for type literals.
-typeLitTypeRep :: forall (a :: k). (Typeable k) => String -> TyCon -> TypeRep a
+typeLitTypeRep :: forall k (a :: k). (Typeable k) =>
+                  String -> TyCon -> TypeRep a
 typeLitTypeRep nm kind_tycon = mkTrCon (mkTypeLitTyCon nm kind_tycon) []
 
 -- | For compiler use.
diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_compile/T15264.hs
new file mode 100644
index 0000000000..a03cf4346e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds #-}
+{-# OPTIONS -Wcompat #-}
+
+module T15264 where
+
+import Data.Proxy
+
+bad1 :: forall (a :: k). Proxy a -> ()
+bad1 _ = ()
+
+bad2 :: forall (a :: k1) (b :: k2). Proxy a -> ()
+bad2 _ = ()
+
+good :: forall k (a :: k). Proxy a -> ()
+good _ = ()
diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr
new file mode 100644
index 0000000000..222d686513
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.stderr
@@ -0,0 +1,10 @@
+
+T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k.’
+
+T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k1 k2.’
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 40ba2110f9..2865351ff5 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -48,4 +48,5 @@ test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
 test('T14991', normal, compile, [''])
+test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
\ No newline at end of file