Visible dependent quantification

This implements GHC proposal 35
(https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst)
by adding the ability to write kinds with
visible dependent quantification (VDQ).

Most of the work for supporting VDQ was actually done _before_ this
patch. That is, GHC has been able to reason about kinds with VDQ for
some time, but it lacked the ability to let programmers directly
write these kinds in the source syntax. This patch is primarly about
exposing this ability, by:

* Changing `HsForAllTy` to add an additional field of type
  `ForallVisFlag` to distinguish between invisible `forall`s (i.e,
  with dots) and visible `forall`s (i.e., with arrows)
* Changing `Parser.y` accordingly

The rest of the patch mostly concerns adding validity checking to
ensure that VDQ is never used in the type of a term (as permitting
this would require full-spectrum dependent types). This is
accomplished by:

* Adding a `vdqAllowed` predicate to `TcValidity`.
* Introducing `splitLHsSigmaTyInvis`, a variant of `splitLHsSigmaTy`
  that only splits invisible `forall`s. This function is used in
  certain places (e.g., in instance declarations) to ensure that GHC
  doesn't try to split visible `forall`s (e.g., if it tried splitting
  `instance forall a -> Show (Blah a)`, then GHC would mistakenly
  allow that declaration!)

This also updates Template Haskell by introducing a new `ForallVisT`
constructor to `Type`.

Fixes #16326. Also fixes #15658 by documenting this feature in the
users' guide.

3 files changed, 60 insertions, 0 deletions

diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index cfe07deb81..cd865e257f 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -44,6 +44,16 @@ Language
     type T = Just (Nothing :: Maybe a)         -- no longer accepted
     type T = Just Nothing :: Maybe (Maybe a)   -- still accepted
 
+- GHC now parses visible, dependent quantifiers (as proposed in
+  `GHC proposal 35
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst>`__),
+  such as the following: ::
+
+    data Proxy :: forall k -> k -> Type
+
+  See the `section on explicit kind quantification
+  <#explicit-kind-quantification>`__ for more details.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 9ba8fa2daf..67be116ae4 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9170,6 +9170,8 @@ GHC reports an error, saying that the kind of ``a`` should be a kind variable
 restricted to be ``Type``. The function definition is then rejected for being
 more specific than its type signature.
 
+.. _explicit-kind-quantification:
+
 Explicit kind quantification
 ----------------------------
 
@@ -9253,6 +9255,53 @@ Closed type family instances are subject to the same rules: ::
   type family F :: Maybe (Maybe k) where
     F @k = 'Just ('Nothing :: Maybe k) -- accepted
 
+Kind variables can also be quantified in *visible* positions. Consider the
+following two examples: ::
+
+  data ProxyKInvis (a :: k)
+  data ProxyKVis k (a :: k)
+
+In the first example, the kind variable ``k`` is an *invisible* argument to
+``ProxyKInvis``. In other words, a user does not need to instantiate ``k``
+explicitly, as kind inference automatically determines what ``k`` should be.
+For instance, in ``ProxyKInvis True``, ``k`` is inferred to be ``Bool``.
+This is reflected in the kind of ``ProxyKInvis``: ::
+
+  ProxyKInvis :: forall k. k -> Type
+
+In the second example, ``k`` is a *visible* argument to ``ProxyKVis``. That is
+to say, ``k`` is an argument that users must provide explicitly when applying
+``ProxyKVis``. For example, ``ProxyKVis Bool True`` is a well formed type.
+
+What is the kind of ``ProxyKVis``? One might say
+``forall k. Type -> k -> Type``, but this isn't quite right, since this would
+allow incorrect things like ``ProxyKVis Bool Int``, which should be rejected
+due to the fact that ``Int`` is not of kind ``Bool``. The key observation is that
+the kind of the second argument *depend* on the first argument. GHC indicates
+this dependency in the syntax that it gives for the kind of ``ProxyKVis``: ::
+
+  ProxyKVis :: forall k -> k -> Type
+
+This kind is similar to the kind of ``ProxyKInvis``, but with a key difference:
+the type variables quantified by the ``forall`` are followed by an arrow
+(``->``), not a dot (``.``). This is a visible, dependent quantifier. It is
+visible in that it the user must pass in a type for ``k`` explicitly, and it is
+dependent in the sense that ``k`` appears later in the kind of ``ProxyKVis``.
+As a counterpart, the ``k`` binder in ``forall k. k -> Type`` can be thought
+of as an *invisible*, dependent quantifier.
+
+GHC permits writing kinds with this syntax, provided that the
+``ExplicitForAll`` and ``PolyKinds`` language extensions are enabled. Just
+like the invisible ``forall``, one can put explicit kind signatures on visibly
+bound kind variables, so the following is syntactically valid: ::
+
+  ProxyKVis :: forall (k :: Type) -> k -> Type
+
+Currently, the ability to write visible, dependent quantifiers is limited to
+kinds. Consequently, visible dependent quantifiers are rejected in any context
+that is unambiguously the type of a term. They are also rejected in the types
+of data constructors.
+
 Kind-indexed GADTs
 ------------------
 
diff --git a/docs/users_guide/index.rst b/docs/users_guide/index.rst
index c20aec7e56..c886722859 100644
--- a/docs/users_guide/index.rst
+++ b/docs/users_guide/index.rst
@@ -14,6 +14,7 @@ Contents:
    intro
    8.6.1-notes
    8.8.1-notes
+   8.10.1-notes
    ghci
    runghc
    usage