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

1 files changed, 53 insertions, 0 deletions

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