Implement Quick Look impredicativity

This patch implements Quick Look impredicativity (#18126), sticking
very closely to the design in
    A quick look at impredicativity, Serrano et al, ICFP 2020

The main change is that a big chunk of GHC.Tc.Gen.Expr has been
extracted to two new modules
    GHC.Tc.Gen.App
    GHC.Tc.Gen.Head
which deal with typechecking n-ary applications, and the head of
such applications, respectively.  Both contain a good deal of
documentation.

Three other loosely-related changes are in this patch:

* I implemented (partly by accident) points (2,3)) of the accepted GHC
  proposal "Clean up printing of foralls", namely
  https://github.com/ghc-proposals/ghc-proposals/blob/
        master/proposals/0179-printing-foralls.rst
  (see #16320).

  In particular, see Note [TcRnExprMode] in GHC.Tc.Module
  - :type instantiates /inferred/, but not /specified/, quantifiers
  - :type +d instantiates /all/ quantifiers
  - :type +v is killed off

  That completes the implementation of the proposal,
  since point (1) was done in
    commit df08468113ab46832b7ac0a7311b608d1b418c4d
    Author: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
    Date:   Mon Feb 3 21:17:11 2020 +0100
    Always display inferred variables using braces

* HsRecFld (which the renamer introduces for record field selectors),
  is now preserved by the typechecker, rather than being rewritten
  back to HsVar.  This is more uniform, and turned out to be more
  convenient in the new scheme of things.

* The GHCi debugger uses a non-standard unification that allows the
  unification variables to unify with polytypes.  We used to hack
  this by using ImpredicativeTypes, but that doesn't work anymore
  so I introduces RuntimeUnkTv.  See Note [RuntimeUnkTv] in
  GHC.Runtime.Heap.Inspect

Updates haddock submodule.

WARNING: this patch won't validate on its own.  It was too
hard to fully disentangle it from the following patch, on
type errors and kind generalisation.

Changes to tests

* Fixes #9730 (test added)

* Fixes #7026 (test added)

* Fixes most of #8808, except function `g2'` which uses a
  section (which doesn't play with QL yet -- see #18126)
  Test added

* Fixes #1330. NB Church1.hs subsumes Church2.hs, which is now deleted

* Fixes #17332 (test added)

* Fixes #4295

* This patch makes typecheck/should_run/T7861 fail.
  But that turns out to be a pre-existing bug: #18467.
  So I have just made T7861 into expect_broken(18467)

3 files changed, 46 insertions, 53 deletions

diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index bdc0271e6f..516bf36563 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -3,6 +3,17 @@
 Version 9.2.1
 ==============
 
+Language
+~~~~~~~~
+
+* :extension:`ImpredicativeTypes`: Finally, polymorphic types have become first class!
+  GHC 9.2 includes a full implementation of the Quick Look approach to type inference for
+  impredicative types, as described in in the paper
+  `A quick look at impredicativity
+  <https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__
+ (Serrano et al, ICFP 2020).  More information here: :ref:`impredicative-polymorphism`.
+ This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/impredicative_types.rst b/docs/users_guide/exts/impredicative_types.rst
index 2380526fb6..01d6476923 100644
--- a/docs/users_guide/exts/impredicative_types.rst
+++ b/docs/users_guide/exts/impredicative_types.rst
@@ -25,33 +25,32 @@ instantiate ``id``\'s type with ``b := (forall s. ST s a) -> a``, and
 that is not allowed. Instantiating polymorphic type variables with
 polymorphic types is called *impredicative polymorphism*.
 
-GHC has extremely flaky support for *impredicative polymorphism*,
-enabled with :extension:`ImpredicativeTypes`. If it worked, this would mean
-that you *could* call a polymorphic function at a polymorphic type, and
-parameterise data structures over polymorphic types. For example: ::
-
-      f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
-      f (Just g) = Just (g [3], g "hello")
-      f Nothing  = Nothing
-
-Notice here that the ``Maybe`` type is parameterised by the
-*polymorphic* type ``(forall a. [a] -> [a])``. However *the extension
-should be considered highly experimental, and certainly un-supported*.
-You are welcome to try it, but please don't rely on it working
-consistently, or working the same in subsequent releases. See
-:ghc-wiki:`this wiki page <impredicative-polymorphism>` for more details.
-
-If you want impredicative polymorphism, the main workaround is to use a
-newtype wrapper. The ``id runST`` example can be written using this
-workaround like this: ::
-
-    runST :: (forall s. ST s a) -> a
-    id :: forall b. b -> b
-
-    newtype Wrap a = Wrap { unWrap :: (forall s. ST s a) -> a }
-
-    foo :: (forall s. ST s a) -> a
-    foo = unWrap (id (Wrap runST))
-          -- Here id is called at monomorphic type (Wrap a)
-
-
+GHC has robust support for *impredicative polymorphism*,
+enabled with :extension:`ImpredicativeTypes`, using the so-called Quick Look
+inference algorithm.  It is described in the paper
+`A quick look at impredicativity
+<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__
+(Serrano et al, ICFP 2020).
+
+Switching on :extension:`ImpredicativeTypes`
+
+- Switches on :extension: `RankNTypes`
+
+- Allows user-written types to have foralls under type constructors, not just under arrows.
+  For example ``f :: Maybe (forall a. [a] -> [a])`` is a legal type signature.
+
+- Allows polymorphic types in Visible Type Application
+  (when :extension: `TypeApplications` is enabled).  For example, you
+  can write ``reverse @(forall b. b->b) xs``.  Using VTA with a
+  polymorphic type argument is useful in cases when Quick Look cannot
+  infer the correct instantiation.
+
+- Switches on the Quick Look type inference algorithm, as described
+  in the paper.  This allows the compiler to infer impredicative instantiations of polymorphic
+  functions in many cases. For example, ``reverse xs`` will typecheck even if ``xs :: [forall a. a->a]``,
+  by instantiating ``reverse`` at type ``forall a. a->a``.
+
+For many years GHC has a special case for the function ``($)``, that allows it
+to typecheck an application like ``runST $ (do { ... })``, even though that
+instantiation may be impredicative.  This special case remains: even without
+:extension:`ImpredicativeTypes` GHC switches on Quick Look for applications of ``($)``.
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index d5a2083eab..92dc51e00f 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -2951,37 +2951,20 @@ commonly used commands.
 
 .. ghci-cmd:: :type; ⟨expression⟩
 
-    Infers and prints the type of ⟨expression⟩, including explicit
-    forall quantifiers for polymorphic types.
-    The type reported is the type that would be inferred
-    for a variable assigned to the expression, but without the
-    monomorphism restriction applied.
+    Infers and prints the type of ⟨expression⟩.  For polymorphic types
+    it instantiates the 'inferred' forall quantifiers (but not the
+    'specified' ones; see :ref:`inferred-vs-specified`), solves constraints, and re-generalises.
 
     .. code-block:: none
 
 	*X> :type length
 	length :: Foldable t => t a -> Int
 
-.. 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
-    are using :extension:`TypeApplications` and care about the distinction
-    between specified type variables (available for type application)
-    and inferred type variables (not available). This mode sometimes prints
-    constraints (such as ``Show Int``) that could readily be solved, but
-    solving these constraints may affect the type variables, so GHC refrains.
-
-    .. code-block:: none
-
-	*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
-    if possible. In this mode, if the inferred type is constrained by
+    Infers and prints the type of ⟨expression⟩, instantiating *all* the forall
+    quantifiers, solving constraints, defaulting, and generalising.
+    In this mode, if the inferred type is constrained by
     any interactive class (``Num``, ``Show``, ``Eq``, ``Ord``, ``Foldable``,
     or ``Traversable``), the constrained type variable(s) are defaulted
     according to the rules described under :extension:`ExtendedDefaultRules`.