Further document :type +v's role in analyzing -XTypeApplications in GHCi

Summary:
The section on `-XTypeApplications` in the users' guide isn't terribly
clear on how to view the visibility of a function type signature's type
variables in GHCi properly (i.e., using the `:type +v` GHCi command). This
adds some more exposition that demonstrates how to use `:type +v` (and why you
don't want to use `:type`).

Fixes #13401.

Test Plan: Eyeball it

Reviewers: bgamari, austin, goldfire, crockeea

Reviewed By: goldfire, crockeea

Subscribers: rwbarton, thomie, crockeea

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

2 files changed, 56 insertions, 19 deletions

diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index 864ae80bd4..2d27c268b3 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -2559,23 +2559,23 @@ commonly used commands.
 
     Sets the string to be used as the prompt in GHCi. Inside ⟨prompt⟩,
     the next sequences are replaced:
-    
-    - ``%s`` by the names of the modules currently in scope.     
+
+    - ``%s`` by the names of the modules currently in scope.
     - ``%l`` by the line number (as referenced in compiler messages) of the
       current prompt.
     - ``%d`` by the date in "Weekday Month Date" format (e.g., "Tue May 26") .
     - ``%t`` by the current time in 24-hour HH:MM:SS format.
-    - ``%T`` by the current time in 12-hour HH:MM:SS format. 
-    - ``%@`` by the current time in 12-hour am/pm format. 
-    - ``%A`` by the current time in 24-hour HH:MM format. 
-    - ``%u`` by the username of the current user. 
+    - ``%T`` by the current time in 12-hour HH:MM:SS format.
+    - ``%@`` by the current time in 12-hour am/pm format.
+    - ``%A`` by the current time in 24-hour HH:MM format.
+    - ``%u`` by the username of the current user.
     - ``%w`` by the current working directory.
     - ``%o`` by the operating system.
-    - ``%a`` by the machine architecture. 
+    - ``%a`` by the machine architecture.
     - ``%N`` by the compiler name.
     - ``%V`` by the compiler version.
-    - ``%call(cmd [args])`` by the result of calling ``cmd args``.     
-    - ``%%`` by ``%``. 
+    - ``%call(cmd [args])`` by the result of calling ``cmd args``.
+    - ``%%`` by ``%``.
 
     If ⟨prompt⟩ starts with ``"`` then it is parsed as a Haskell String;
     otherwise it is treated as a literal string.
@@ -2590,11 +2590,11 @@ commonly used commands.
     .. index::
        single: GHCi prompt function; setting
 
-    Sets the function to be used for the prompt displaying in GHCi. The 
-    function should be of the type ``[String] -> Int -> IO String``. This 
+    Sets the function to be used for the prompt displaying in GHCi. The
+    function should be of the type ``[String] -> Int -> IO String``. This
     function is called each time the prompt is being made. The first argument
-    stands for the names of the modules currently in scope(the name of the 
-    "topmost" module  will begin with a ``*``; see  :ref:`ghci-scope` for 
+    stands for the names of the modules currently in scope(the name of the
+    "topmost" module  will begin with a ``*``; see  :ref:`ghci-scope` for
     more information). The second arguments is the line number (as referenced
     in compiler  messages) of the current prompt.
 
@@ -2724,7 +2724,7 @@ commonly used commands.
 	*X> :type length
 	length :: Foldable t => t a -> Int
 
-.. ghci-cmd:: :type +v ⟨expression⟩
+.. ghci-cmd:: :type +v; ⟨expression⟩
 
     Infers and prints the type of ⟨expression⟩, but without fiddling
     with type variables or class constraints. This is useful when you
@@ -2739,7 +2739,7 @@ commonly used commands.
 	*X> :set -fprint-explicit-foralls
 	*X> :type +v length
 	length :: forall (t :: * -> *). Foldable t => forall a. t a -> Int
-    
+
 .. ghci-cmd:: :type +d ⟨expression⟩
 
     Infers and prints the type of ⟨expression⟩, defaulting type variables
@@ -2755,7 +2755,7 @@ commonly used commands.
 
 	*X> :type +d length
 	length :: [a] -> Int
-	      
+
 .. ghci-cmd:: :type-at; ⟨module⟩ ⟨line⟩ ⟨col⟩ ⟨end-line⟩ ⟨end-col⟩ [⟨name⟩]
 
     Reports the inferred type at the given span/position in the module, e.g.:
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 43175ba729..c6f7f5ec3f 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9341,9 +9341,46 @@ Here are the details:
 
 - When printing types with :ghc-flag:`-fprint-explicit-foralls` enabled,
   type variables not available for visible type application are printed
-  in braces. Thus, if you write ``myLength = length`` without a type
-  signature, ``myLength``'s inferred type will be
-  ``forall {f} {a}. Foldable f => f a -> Int``.
+  in braces. We can observe this behavior in a GHCi session: ::
+
+    > :set -XTypeApplications -fprint-explicit-foralls
+    > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
+    > :type +v myLength1
+    myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
+    > let myLength2 = length
+    > :type +v myLength2
+    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+    > :type +v myLength2 @[]
+
+    <interactive>:1:1: error:
+        • Cannot apply expression of type ‘t0 a0 -> Int’
+          to a visible type argument ‘[]’
+        • In the expression: myLength2 @[]
+
+  Notice that since ``myLength1`` was defined with an explicit type signature,
+  :ghci-cmd:`:type +v` reports that all of its type variables are available
+  for type application. On the other hand, ``myLength2`` was not given a type
+  signature. As a result, all of its type variables are surrounded with braces,
+  and trying to use visible type application with ``myLength2`` fails.
+
+  Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
+  of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
+  that would be inferred for a variable assigned to the expression provided
+  (that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
+  ``myLength2``, this type will have no variables available to visible type
+  application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
+  type of the expression provided. To illustrate this: ::
+
+    > :type myLength1
+    myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
+    > :type myLength2
+    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+
+  Using :ghci-cmd:`:type` might lead one to conclude that none of the type
+  variables in ``myLength1``'s type signature are available for type
+  application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
+  if you want the most accurate information with respect to visible type
+  application properties.
 
 - Data constructors declared with GADT syntax follow different rules
   for the time being; it is expected that these will be brought in line