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)

1 files changed, 1 insertions, 41 deletions

diff --git a/compiler/GHC/Runtime/Eval.hs b/compiler/GHC/Runtime/Eval.hs
index 0891da5808..aad557579b 100644
--- a/compiler/GHC/Runtime/Eval.hs
+++ b/compiler/GHC/Runtime/Eval.hs
@@ -81,7 +81,6 @@ import GHC.ByteCode.Types
 import GHC.Runtime.Linker as Linker
 import GHC.Driver.Session
 import GHC.Driver.Ppr
-import GHC.LanguageExtensions
 import GHC.Types.Unique
 import GHC.Types.Unique.Supply
 import GHC.Utils.Monad
@@ -1283,10 +1282,7 @@ obtainTermFromVal hsc_env _bound _force _ty _x = withInterp hsc_env $ \case
 obtainTermFromId :: HscEnv -> Int -> Bool -> Id -> IO Term
 obtainTermFromId hsc_env bound force id =  do
   hv <- Linker.getHValue hsc_env (varName id)
-  cvObtainTerm (updEnv hsc_env) bound force (idType id) hv
- where updEnv env = env {hsc_dflags =                             -- #14828
-            xopt_set (hsc_dflags env) ImpredicativeTypes}
-         -- See Note [Setting ImpredicativeTypes for :print command]
+  cvObtainTerm hsc_env bound force (idType id) hv
 
 -- Uses RTTI to reconstruct the type of an Id, making it less polymorphic
 reconstructType :: HscEnv -> Int -> Id -> IO (Maybe Type)
@@ -1296,39 +1292,3 @@ reconstructType hsc_env bound id = do
 
 mkRuntimeUnkTyVar :: Name -> Kind -> TyVar
 mkRuntimeUnkTyVar name kind = mkTcTyVar name kind RuntimeUnk
-
-
-{-
-Note [Setting ImpredicativeTypes for :print command]
-
-If ImpredicativeTypes is not enabled, then `:print <term>` will fail if the
-type of <term> has nested `forall`s or `=>`s.
-This is because the GHCi debugger's internals will attempt to unify a
-metavariable with the type of <term> and then display the result, but if the
-type has nested `forall`s or `=>`s, then unification will fail.
-As a result, `:print` will bail out and the unhelpful result will be
-`<term> = (_t1::t1)` (where `t1` is a metavariable).
-
-Beware: <term> can have nested `forall`s even if its definition doesn't use
-RankNTypes! Here is an example from #14828:
-
-  class Functor f where
-    fmap :: (a -> b) -> f a -> f b
-
-Somewhat surprisingly, `:print fmap` considers the type of fmap to have
-nested foralls. This is because the GHCi debugger sees the type
-`fmap :: forall f. Functor f => forall a b. (a -> b) -> f a -> f b`.
-We could envision deeply instantiating this type to get the type
-`forall f a b. Functor f => (a -> b) -> f a -> f b`,
-but this trick wouldn't work for higher-rank types.
-
-Instead, we adopt a simpler fix: enable `ImpredicativeTypes` when using
-`:print` and friends in the GHCi debugger. This allows metavariables
-to unify with types that have nested (or higher-rank) `forall`s/`=>`s,
-which makes `:print fmap` display as
-`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected.
-
-Although ImpredicativeTypes is a somewhat unpredictable from a type inference
-perspective, there is no danger in using it in the GHCi debugger, since all
-of the terms that the GHCi debugger deals with have already been typechecked.
--}