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)

2 files changed, 49 insertions, 43 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.
--}
diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs
index ea682702c6..7bcb1a364c 100644
--- a/compiler/GHC/Runtime/Heap/Inspect.hs
+++ b/compiler/GHC/Runtime/Heap/Inspect.hs
@@ -559,11 +559,52 @@ trIO = liftTcM . liftIO
 liftTcM :: TcM a -> TR a
 liftTcM = id
 
+-- When we make new unification variables in the GHCi debugger,
+-- we use RuntimeUnkTvs.   See Note [RuntimeUnkTv].
 newVar :: Kind -> TR TcType
-newVar = liftTcM . newFlexiTyVarTy
+newVar kind = liftTcM (do { tv <- newAnonMetaTyVar RuntimeUnkTv kind
+                          ; return (mkTyVarTy tv) })
 
 newOpenVar :: TR TcType
-newOpenVar = liftTcM newOpenFlexiTyVarTy
+newOpenVar = liftTcM (do { kind <- newOpenTypeKind
+                         ; newVar kind })
+
+{- Note [RuntimeUnkTv]
+~~~~~~~~~~~~~~~~~~~~~~
+In the GHCi debugger we use unification variables whose MetaInfo is
+RuntimeUnkTv.  The special property of a RuntimeUnkTv is that it can
+unify with a polytype (see GHC.Tc.Utils.Unify.metaTyVarUpdateOK).
+If we don't do this `: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
+unless we do something special.  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: allow RuntimeUnkTv to unify with a
+polytype (specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck).
+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.
+-}
+
 
 instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar])
 -- Instantiate fresh mutable type variables from some TyVars
@@ -578,6 +619,10 @@ type RttiInstantiation = [(TcTyVar, TyVar)]
    -- If the TcTyVar has not been refined by the runtime type
    -- elaboration, then we want to turn it back into the
    -- original RuntimeUnk
+   --
+   -- July 20: I'm not convinced that the little dance from
+   -- RuntimeUnkTv unification variables to RuntimeUnk skolems
+   -- is buying us anything.  ToDo: get rid of it.
 
 -- | Returns the instantiated type scheme ty', and the
 --   mapping from new (instantiated) -to- old (skolem) type variables
@@ -585,6 +630,7 @@ instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
 instScheme (tvs, ty)
   = do { (subst, tvs') <- instTyVars tvs
        ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
+       ; traceTR (text "instScheme" <+> (ppr tvs $$ ppr ty $$ ppr tvs'))
        ; return (substTy subst ty, rtti_inst) }
 
 applyRevSubst :: RttiInstantiation -> TR ()