1 files changed, 77 insertions, 0 deletions
diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 38c6e0f441..6b4fc9cef7 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/docs/users_guide/exts/explicit_forall.rst
@@ -45,4 +45,81 @@ Notes:
 
   would warn about the unused type variable `a`.
 
+.. _forall-or-nothing:
+
+The ``forall``-or-nothing rule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In certain forms of types, type variables obey what is known as the
+"``forall``-or-nothing" rule: if a type has an outermost, explicit
+``forall``, then all of the type variables in the type must be explicitly
+quantified. These two examples illustrate how the rule works: ::
+
+  f  :: forall a b. a -> b -> b         -- OK, `a` and `b` are explicitly bound
+  g  :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound
+  h  :: forall a. a -> b -> b           -- Rejected, `b` is not in scope
+
+The type signatures for ``f``, ``g``, and ``h`` all begin with an outermost
+``forall``, so every type variable in these signatures must be explicitly
+bound by a ``forall``. Both ``f`` and ``g`` obey the ``forall``-or-nothing
+rule, since they explicitly quantify ``a`` and ``b``. On the other hand,
+``h`` does not explicitly quantify ``b``, so GHC will reject its type
+signature for being improperly scoped.
+
+In places where the ``forall``-or-nothing rule takes effect, if a type does
+*not* have an outermost ``forall``, then any type variables that are not
+explicitly bound by a ``forall`` become implicitly quantified. For example: ::
+
+  i :: a -> b -> b             -- `a` and `b` are implicitly quantified
+  j :: a -> forall b. b -> b   -- `a` is implicitly quantified
+  k :: (forall a. a -> b -> b) -- `b` is implicitly quantified
+
+GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that:
+
+- ``j``'s signature is accepted despite its mixture of implicit and explicit
+  quantification. As long as a ``forall`` is not an outermost one, it is fine
+  to use it among implicitly bound type variables.
+- ``k``'s signature is accepted because the outermost parentheses imply that
+  the ``forall`` is not an outermost ``forall``. The ``forall``-or-nothing
+  rule is one of the few places in GHC where the presence or absence of
+  parentheses can be semantically significant!
+
+The ``forall``-or-nothing rule takes effect in the following places:
+
+- Type signature declarations for functions, values, and class methods
+- Expression type annotations
+- Instance declarations
+- :ref:`class-default-signatures`
+- Type signatures in a :ref:`specialize-pragma` or
+  :ref:`specialize-instance-pragma`
+- :ref:`standalone-kind-signatures`
+- Type signatures for :ref:`gadt` constructors
+- Type signatures for :ref:`pattern-synonyms`
+- :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
+  :ref:`closed-type-families`, and :ref:`assoc-inst`
+- :ref:`rewrite-rules` in which the type variables are explicitly quantified
 
+Notes:
+
+- :ref:`pattern-type-sigs` are a notable example of a place where
+  types do *not* obey the ``forall``-or-nothing rule. For example, GHC will
+  accept the following: ::
+
+    f (g :: forall a. a -> b) x = g x :: b
+
+  Furthermore, :ref:`rewrite-rules` do not obey the ``forall``-or-nothing rule
+  when their type variables are not explicitly quantified: ::
+
+    {-# RULES "f" forall (g :: forall a. a -> b) x. f g x = g x :: b #-}
+
+- GADT constructors are extra particular about their ``forall``s. In addition
+  to adhering to the ``forall``-or-nothing rule, GADT constructors also forbid
+  nested ``forall``s. For example, GHC would reject the following GADT: ::
+
+    data T where
+      MkT :: (forall a. a -> b -> T)
+
+  Because of the lack of an outermost ``forall`` in the type of ``MkT``, the
+  ``b`` would be implicitly quantified. In effect, it would be as if one had
+  written ``MkT :: forall b. (forall a. a -> b -> T)``, which contains nested
+  ``forall``s. See :ref:`formal-gadt-syntax`.