Document ScopedTypeVariables' interaction with nested foralls

Summary:
This documents the status quo with regards to how
`ScopedTypeVariables` brings into scope type variables that are
quantified by nested `forall`s (that is to say, it doesn't). This
takes the prose in
https://ghc.haskell.org/trac/ghc/ticket/14288#comment:5
and enshrines it into the users' guide.

Test Plan: Read it

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14288

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

1 files changed, 21 insertions, 1 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 603dbc5eb9..201aa77f08 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9650,6 +9650,26 @@ This only happens if:
    the definition of "``g``", so "``x::a``" means "``x::forall a. a``"
    by Haskell's usual implicit quantification rules.
 
+-  The type variable is quantified by the single, syntactically visible,
+   outermost ``forall`` of the type signature. For example, GHC will reject
+   all of the following examples: ::
+
+         f1 :: forall a. forall b. a -> [b] -> [b]
+         f1 _ (x:xs) = xs ++ [ x :: b ]
+
+         f2 :: forall a. a -> forall b. [b] -> [b]
+         f2 _ (x:xs) = xs ++ [ x :: b ]
+
+         type Foo = forall b. [b] -> [b]
+
+         f3 :: Foo
+         f3 (x:xs) = xs ++ [ x :: b ]
+
+   In ``f1`` and ``f2``, the type variable ``b`` is not quantified by the
+   outermost ``forall``, so it is not in scope over the bodies of the
+   functions. Neither is ``b`` in scope over the body of ``f3``, as the
+   ``forall`` is tucked underneath the ``Foo`` type synonym.
+
 -  The signature gives a type for a function binding or a bare variable
    binding, not a pattern binding. For example: ::
 
@@ -12541,7 +12561,7 @@ optionally had by adding ``!`` in front of a variable.
 
    Turning patterns into irrefutable ones requires ``~(~p)`` or ``(~ ~p)`` when ``Strict`` is enabled.
 
-   
+
 
 -  **Let/where bindings**