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)

31 files changed, 2776 insertions, 1801 deletions

diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 251fae2c48..11a102f91b 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -40,6 +40,7 @@ import GHC.Hs.Binds
 -- others:
 import GHC.Tc.Types.Evidence
 import GHC.Core
+import GHC.Types.Id( Id )
 import GHC.Types.Name
 import GHC.Types.Name.Set
 import GHC.Types.Basic
@@ -251,8 +252,8 @@ data HsExpr p
                              -- Turned from HsVar to HsUnboundVar by the
                              --   renamer, when it finds an out-of-scope
                              --   variable or hole.
-                             -- Turned into HsVar by type checker, to support
-                             --   deferred type errors.
+                             -- The (XUnboundVar p) field becomes Id
+                             --   after typechecking
 
   | HsConLikeOut (XConLikeOut p)
                  ConLike     -- ^ After typechecker only; must be different
@@ -260,7 +261,9 @@ data HsExpr p
 
   | HsRecFld  (XRecFld p)
               (AmbiguousFieldOcc p) -- ^ Variable pointing to record selector
-                                    -- Not in use after typechecking
+              -- The parser produces HsVars
+              -- The renamer renames record-field selectors to HsRecFld
+              -- The typechecker preserves HsRecFld
 
   | HsOverLabel (XOverLabel p)
                 (Maybe (IdP p)) FastString
@@ -592,7 +595,6 @@ deriving instance (Data (hs_syn GhcTc), Typeable hs_syn) => Data (HsWrap hs_syn)
 -- ---------------------------------------------------------------------
 
 type instance XVar           (GhcPass _) = NoExtField
-type instance XUnboundVar    (GhcPass _) = NoExtField
 type instance XConLikeOut    (GhcPass _) = NoExtField
 type instance XRecFld        (GhcPass _) = NoExtField
 type instance XOverLabel     (GhcPass _) = NoExtField
@@ -603,6 +605,10 @@ type instance XLam           (GhcPass _) = NoExtField
 type instance XLamCase       (GhcPass _) = NoExtField
 type instance XApp           (GhcPass _) = NoExtField
 
+type instance XUnboundVar    GhcPs = NoExtField
+type instance XUnboundVar    GhcRn = NoExtField
+type instance XUnboundVar    GhcTc = Id
+
 type instance XAppTypeE      GhcPs = NoExtField
 type instance XAppTypeE      GhcRn = NoExtField
 type instance XAppTypeE      GhcTc = Type
@@ -1049,14 +1055,15 @@ ppr_lexpr e = ppr_expr (unLoc e)
 
 ppr_expr :: forall p. (OutputableBndrId p)
          => HsExpr (GhcPass p) -> SDoc
-ppr_expr (HsVar _ (L _ v))  = pprPrefixOcc v
-ppr_expr (HsUnboundVar _ uv)= pprPrefixOcc uv
-ppr_expr (HsConLikeOut _ c) = pprPrefixOcc c
-ppr_expr (HsIPVar _ v)      = ppr v
-ppr_expr (HsOverLabel _ _ l)= char '#' <> ppr l
-ppr_expr (HsLit _ lit)      = ppr lit
-ppr_expr (HsOverLit _ lit)  = ppr lit
-ppr_expr (HsPar _ e)        = parens (ppr_lexpr e)
+ppr_expr (HsVar _ (L _ v))   = pprPrefixOcc v
+ppr_expr (HsUnboundVar _ uv) = pprPrefixOcc uv
+ppr_expr (HsConLikeOut _ c)  = pprPrefixOcc c
+ppr_expr (HsRecFld _ f)      = pprPrefixOcc f
+ppr_expr (HsIPVar _ v)       = ppr v
+ppr_expr (HsOverLabel _ _ l) = char '#' <> ppr l
+ppr_expr (HsLit _ lit)       = ppr lit
+ppr_expr (HsOverLit _ lit)   = ppr lit
+ppr_expr (HsPar _ e)         = parens (ppr_lexpr e)
 
 ppr_expr (HsPragE _ prag e) = sep [ppr prag, ppr_lexpr e]
 
@@ -1212,7 +1219,6 @@ ppr_expr (HsBinTick _ tickIdTrue tickIdFalse exp)
           text ">(",
           ppr exp, text ")"]
 
-ppr_expr (HsRecFld _ f) = ppr f
 ppr_expr (XExpr x) = case ghcPass @p of
 #if __GLASGOW_HASKELL__ < 811
   GhcPs -> ppr x
@@ -1377,7 +1383,6 @@ isAtomicHsExpr (HsOverLit {})    = True
 isAtomicHsExpr (HsIPVar {})      = True
 isAtomicHsExpr (HsOverLabel {})  = True
 isAtomicHsExpr (HsUnboundVar {}) = True
-isAtomicHsExpr (HsPar _ e)       = isAtomicHsExpr (unLoc e)
 isAtomicHsExpr (HsRecFld{})      = True
 isAtomicHsExpr (XExpr x)
   | GhcTc <- ghcPass @p          = case x of
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index b1507f0adc..8ce29a72d3 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -478,7 +478,7 @@ data HsRecField' id arg = HsRecField {
 --
 --     hsRecFieldLbl = Unambiguous "x" $sel:x:MkS  :: AmbiguousFieldOcc Id
 --
--- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Expr.
+-- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Head.
 
 hsRecFields :: HsRecFields p arg -> [XCFieldOcc p]
 hsRecFields rbinds = map (unLoc . hsRecFieldSel . unLoc) (rec_flds rbinds)
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 65210d1044..c2da3857d4 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -348,7 +348,7 @@ data HsForAllTelescope pass
     { hsf_xvis      :: XHsForAllVis pass
     , hsf_vis_bndrs :: [LHsTyVarBndr () pass]
     }
-  | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@),
+  | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c. {...}@),
                   --   where each binder has a 'Specificity'.
     { hsf_xinvis       :: XHsForAllInvis pass
     , hsf_invis_bndrs  :: [LHsTyVarBndr Specificity pass]
@@ -1712,7 +1712,7 @@ mkFieldOcc rdr = FieldOcc noExtField rdr
 -- occurrences).
 --
 -- See Note [HsRecField and HsRecUpdField] in "GHC.Hs.Pat" and
--- Note [Disambiguating record fields] in "GHC.Tc.Gen.Expr".
+-- Note [Disambiguating record fields] in "GHC.Tc.Gen.Head".
 -- See Note [Located RdrNames] in "GHC.Hs.Expr"
 data AmbiguousFieldOcc pass
   = Unambiguous (XUnambiguous pass) (Located RdrName)
diff --git a/compiler/GHC/HsToCore/Coverage.hs b/compiler/GHC/HsToCore/Coverage.hs
index 59c0bfb4ed..ae8c5a3b83 100644
--- a/compiler/GHC/HsToCore/Coverage.hs
+++ b/compiler/GHC/HsToCore/Coverage.hs
@@ -505,23 +505,25 @@ addBinTickLHsExpr boxLabel (L pos e0)
 -- in the addTickLHsExpr family of functions.)
 
 addTickHsExpr :: HsExpr GhcTc -> TM (HsExpr GhcTc)
-addTickHsExpr e@(HsVar _ (L _ id)) = do freeVar id; return e
-addTickHsExpr (HsUnboundVar {})    = panic "addTickHsExpr.HsUnboundVar"
+addTickHsExpr e@(HsVar _ (L _ id))  = do freeVar id; return e
+addTickHsExpr e@(HsUnboundVar id _) = do freeVar id; return e
+addTickHsExpr e@(HsRecFld _ (Ambiguous id _))   = do freeVar id; return e
+addTickHsExpr e@(HsRecFld _ (Unambiguous id _)) = do freeVar id; return e
 addTickHsExpr e@(HsConLikeOut _ con)
   | Just id <- conLikeWrapId_maybe con = do freeVar id; return e
-addTickHsExpr e@(HsIPVar {})       = return e
-addTickHsExpr e@(HsOverLit {})     = return e
-addTickHsExpr e@(HsOverLabel{})    = return e
-addTickHsExpr e@(HsLit {})         = return e
-addTickHsExpr (HsLam x matchgroup) = liftM (HsLam x)
-                                           (addTickMatchGroup True matchgroup)
-addTickHsExpr (HsLamCase x mgs)    = liftM (HsLamCase x)
-                                           (addTickMatchGroup True mgs)
-addTickHsExpr (HsApp x e1 e2)      = liftM2 (HsApp x) (addTickLHsExprNever e1)
-                                                      (addTickLHsExpr      e2)
-addTickHsExpr (HsAppType x e ty)   = liftM3 HsAppType (return x)
-                                                      (addTickLHsExprNever e)
-                                                      (return ty)
+addTickHsExpr e@(HsIPVar {})     = return e
+addTickHsExpr e@(HsOverLit {})   = return e
+addTickHsExpr e@(HsOverLabel{})  = return e
+addTickHsExpr e@(HsLit {})       = return e
+addTickHsExpr (HsLam x mg)       = liftM (HsLam x)
+                                         (addTickMatchGroup True mg)
+addTickHsExpr (HsLamCase x mgs)  = liftM (HsLamCase x)
+                                         (addTickMatchGroup True mgs)
+addTickHsExpr (HsApp x e1 e2)    = liftM2 (HsApp x) (addTickLHsExprNever e1)
+                                                    (addTickLHsExpr      e2)
+addTickHsExpr (HsAppType x e ty) = liftM3 HsAppType (return x)
+                                                    (addTickLHsExprNever e)
+                                                    (return ty)
 
 addTickHsExpr (OpApp fix e1 e2 e3) =
         liftM4 OpApp
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index be61777722..783e8b098b 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -261,10 +261,14 @@ dsLExprNoLP (L loc e)
        ; return e' }
 
 dsExpr :: HsExpr GhcTc -> DsM CoreExpr
+dsExpr (HsVar    _ (L _ id))           = dsHsVar id
+dsExpr (HsRecFld _ (Unambiguous id _)) = dsHsVar id
+dsExpr (HsRecFld _ (Ambiguous   id _)) = dsHsVar id
+dsExpr (HsUnboundVar id _)             = dsHsVar id
+
 dsExpr (HsPar _ e)            = dsLExpr e
 dsExpr (ExprWithTySig _ e _)  = dsLExpr e
-dsExpr (HsVar _ (L _ var))    = dsHsVar var
-dsExpr (HsUnboundVar {})      = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them
+
 dsExpr (HsConLikeOut _ con)   = dsConLike con
 dsExpr (HsIPVar {})           = panic "dsExpr: HsIPVar"
 dsExpr (HsOverLabel{})        = panic "dsExpr: HsOverLabel"
@@ -806,7 +810,6 @@ dsExpr (HsBinTick _ ixT ixF e) = do
 -- HsSyn constructs that just shouldn't be here:
 dsExpr (HsBracket     {})  = panic "dsExpr:HsBracket"
 dsExpr (HsDo          {})  = panic "dsExpr:HsDo"
-dsExpr (HsRecFld      {})  = panic "dsExpr:HsRecFld"
 
 ds_prag_expr :: HsPragE GhcTc -> LHsExpr GhcTc -> DsM CoreExpr
 ds_prag_expr (HsPragSCC _ _ cc) expr = do
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index b123450b60..ffc9c0a742 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -785,6 +785,7 @@ class ( IsPass p
       , Data (HsTupArg (GhcPass p))
       , Data (IPBind (GhcPass p))
       , ToHie (Context (Located (IdGhcP p)))
+      , ToHie (Context (Located (XUnboundVar (GhcPass p))))
       , ToHie (RFContext (Located (AmbiguousFieldOcc (GhcPass p))))
       , ToHie (RFContext (Located (FieldOcc (GhcPass p))))
       , ToHie (TScoped (LHsWcType (GhcPass (NoGhcTcPass p))))
@@ -799,6 +800,9 @@ instance HiePass 'Renamed where
 instance HiePass 'Typechecked where
   hiePass = HieTc
 
+instance ToHie (Context (Located NoExtField)) where
+  toHie _ = pure []
+
 instance HiePass p => ToHie (BindContext (Located (HsBind (GhcPass p)))) where
   toHie (BC context scope b@(L span bind)) =
     concatM $ getTypeNode b : case bind of
@@ -1042,8 +1046,8 @@ instance HiePass p => ToHie (Located (HsExpr (GhcPass p))) where
         [ toHie $ C Use (L mspan var)
              -- Patch up var location since typechecker removes it
         ]
-      HsUnboundVar _ _ ->
-        []
+      HsUnboundVar var _ ->
+        [ toHie $ C Use (L mspan var) ]
       HsConLikeOut _ con ->
         [ toHie $ C Use $ L mspan $ conLikeName con
         ]
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index ecf31c01ea..9014c9f159 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -1634,7 +1634,7 @@ patSynErr item l e explanation =
         explanation
      ; return (L l hsHoleExpr) }
 
-hsHoleExpr :: HsExpr (GhcPass id)
+hsHoleExpr :: HsExpr GhcPs
 hsHoleExpr = HsUnboundVar noExtField (mkVarOcc "_")
 
 -- | See Note [Ambiguous syntactic categories] and Note [PatBuilder]
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index f0cd54358f..72058a2512 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -749,7 +749,7 @@ rnHsRecUpdFields flds
       = do { let lbl = rdrNameAmbiguousFieldOcc f
            ; sel <- setSrcSpan loc $
                       -- Defer renaming of overloaded fields to the typechecker
-                      -- See Note [Disambiguating record fields] in GHC.Tc.Gen.Expr
+                      -- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
                       if overload_ok
                           then do { mb <- lookupGlobalOccRn_overloaded
                                             overload_ok lbl
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 ()
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 3585c9ad70..400d4afbe7 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -1691,19 +1691,14 @@ a polytype.  E.g.
                  @(T x      -> forall b. b -> b)
                 op
 
-The use of type applications is crucial here. If we had tried using only
-explicit type signatures, like so:
+The use of type applications is crucial here. We have to instantiate
+both type args of (coerce :: Coercible a b => a -> b) to polytypes,
+and we can only do that with VTA or Quick Look. Here VTA seems more
+appropriate for machine generated code: it's simple and robust.
 
-   instance C <rep-ty> => C (T x) where
-     op :: T x -> forall b. b -> b
-     op = coerce (op :: <rep-ty> -> forall b. b -> b)
-
-Then GHC will attempt to deeply skolemize the two type signatures, which will
-wreak havoc with the Coercible solver. Therefore, we instead use type
-applications, which do not deeply skolemize and thus avoid this issue.
-The downside is that we currently require -XImpredicativeTypes to permit this
-polymorphic type instantiation, so we have to switch that flag on locally in
-GHC.Tc.Deriv.genInst. See #8503 for more discussion.
+However, to allow VTA with polytypes we must switch on
+-XImpredicativeTypes locally in GHC.Tc.Deriv.genInst.
+See #8503 for more discussion.
 
 Note [Newtype-deriving trickiness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1807,9 +1802,8 @@ break this example (from the T15290d test case):
     c = coerce @(Int -> forall b. b -> Int)
                c
 
-That is because the instance signature deeply skolemizes the forall-bound
-`b`, which wreaks havoc with the `Coercible` solver. An additional visible type
-argument of @(Int -> forall b. b -> Age) is enough to prevent this.
+That is because we still need to instantiate the second argument of
+coerce with a polytype, and we can only do that with VTA or QuickLook.
 
 Be aware that the use of an instance signature doesn't /solve/ this
 problem; it just makes it less likely to occur. For example, if a class has
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
new file mode 100644
index 0000000000..79749c70c7
--- /dev/null
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -0,0 +1,1083 @@
+{-
+%
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+-}
+
+{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
+
+module GHC.Tc.Gen.App
+       ( tcApp
+       , tcInferSigma
+       , tcValArg
+       , tcExprPrag ) where
+
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC )
+
+import GHC.Tc.Gen.Head
+import GHC.Hs
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Unify
+import GHC.Tc.Utils.Instantiate
+import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
+import GHC.Tc.Gen.HsType
+import GHC.Tc.Utils.TcMType
+import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcType as TcType
+import GHC.Core.TyCon
+import GHC.Core.TyCo.Rep
+import GHC.Core.TyCo.Ppr
+import GHC.Core.TyCo.Subst (substTyWithInScope)
+import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
+import GHC.Core.Type
+import GHC.Tc.Types.Evidence
+import GHC.Types.Var.Set
+import GHC.Builtin.PrimOps( tagToEnumKey )
+import GHC.Builtin.Names
+import GHC.Driver.Session
+import GHC.Types.SrcLoc
+import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
+import GHC.Data.Maybe
+import GHC.Utils.Misc
+import GHC.Utils.Outputable as Outputable
+import GHC.Utils.Panic
+import qualified GHC.LanguageExtensions as LangExt
+
+import Control.Monad
+import Data.Function
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+{- *********************************************************************
+*                                                                      *
+                 Quick Look overview
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Quick Look]
+~~~~~~~~~~~~~~~~~~~~
+The implementation of Quick Look closely follows the QL paper
+   A quick look at impredicativity, Serrano et al, ICFP 2020
+   https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/
+
+All the moving parts are in this module, GHC.Tc.Gen.App, so named
+because it deal with n-ary application.  The main workhorse is tcApp.
+
+Some notes relative to the paper
+
+* The "instantiation variables" of the paper are ordinary unification
+  variables.  We keep track of which variables are instantiation variables
+  by keeping a set Delta of instantiation variables.
+
+* When we learn what an instantiation variable must be, we simply unify
+  it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2)
+  of the paper.  This may fill in a (mutable) instantiation variable with
+  a polytype.
+
+* When QL is done, we don't need to turn the un-filled-in
+  instantiation variables into unification variables -- they already
+  are!
+
+  Moreover, all filled-in occurrences of instantiation variables
+  have been zonked away (see "Crucial step" in tcValArgs), and
+  so the rest of the type checker never sees a meta-type variable
+  filled in with a polytype.  For the rest of the typechecker,
+  a meta type variable stands (only) for a monotype.
+
+* We cleverly avoid the quadratic cost of QL, alluded to in the paper.
+  See Note [Quick Look at value arguments]
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+              tcInferSigma
+*                                                                      *
+********************************************************************* -}
+
+tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
+-- Used only to implement :type; see GHC.Tc.Module.tcRnExpr
+-- True  <=> instantiate -- return a rho-type
+-- False <=> don't instantiate -- return a sigma-type
+tcInferSigma inst (L loc rn_expr)
+  | (rn_fun, rn_args, _) <- splitHsApps rn_expr
+  = addExprCtxt rn_expr $
+    setSrcSpan loc      $
+    do { do_ql <- wantQuickLook rn_fun
+       ; (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args Nothing
+       ; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst rn_fun fun_sigma rn_args
+       ; _tc_args <- tcValArgs do_ql tc_fun inst_args
+       ; return app_res_sigma }
+
+{- *********************************************************************
+*                                                                      *
+              Typechecking n-ary applications
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Application chains and heads]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Quick Look treats application chains specially.  What is an
+"application chain"?  See Fig 2, of the QL paper: "A quick look at
+impredicativity" (ICFP'20). Here's the syntax:
+
+app :: head
+     | app expr            -- HsApp: ordinary application
+     | app @type           -- HsTypeApp: VTA
+     | expr `head` expr    -- OpApp: infix applications
+     | ( app )             -- HsPar: parens
+     | {-# PRAGMA #-} app  -- HsPragE: pragmas
+
+head ::= f             -- HsVar:    variables
+      |  fld           -- HsRecFld: record field selectors
+      |  (expr :: ty)  -- ExprWithTySig: expr with user type sig
+      |  other_expr    -- Other expressions
+
+When tcExpr sees something that starts an application chain (namely,
+any of the constructors in 'app' or 'head'), it invokes tcApp to
+typecheck it: see Note [tcApp: typechecking applications].  However,
+for HsPar and HsPragE, there is no tcWrapResult (which would
+instantiate types, bypassing Quick Look), so nothing is gained by
+using the application chain route, and we can just recurse to tcExpr.
+
+A "head" has three special cases (for which we can infer a polytype
+using tcInferAppHead_maybe); otherwise is just any old expression (for
+which we can infer a rho-type (via tcInfer).
+
+There is no special treatment for HsUnboundVar, HsOverLit etc, because
+we can't get a polytype from them.
+
+Left and right sections (e.g. (x +) and (+ x)) are not yet supported.
+Probably left sections (x +) would be esay to add, since x is the
+first arg of (+); but right sections are not so easy.  For symmetry
+reasons I've left both unchanged, in GHC.Tc.Gen.Expr.
+
+It may not be immediately obvious why ExprWithTySig (e::ty) should be
+dealt with by tcApp, even when it is not applied to anything. Consider
+   f :: [forall a. a->a] -> Int
+   ...(f (undefined :: forall b. b))...
+Clearly this should work!  But it will /only/ work because if we
+instantiate that (forall b. b) impredicatively!  And that only happens
+in tcApp.
+
+Note [tcApp: typechecking applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tcApp implements the APP-Downarrow/Uparrow rule of
+Fig 3, plus the modification in Fig 5, of the QL paper:
+"A quick look at impredicativity" (ICFP'20).
+
+It treats application chains (f e1 @ty e2) specially:
+
+* So we can report errors like "in the third arument of a call of f"
+
+* So we can do Visible Type Application (VTA), for which we must not
+  eagerly instantiate the function part of the application.
+
+* So that we can do Quick Look impredicativity.
+
+tcApp works like this:
+
+1. Use splitHsApps, which peels off
+     HsApp, HsTypeApp, HsPrag, HsPar
+   returning the function in the corner and the arguments
+
+   splitHsApps can deal with infix as well as prefix application,
+   and returns a Rebuilder to re-assemble the the application after
+   typechecking.
+
+   The "list of arguments" is [HsExprArg], described in Note [HsExprArg].
+   in GHC.Tc.Gen.Head
+
+2. Use tcInferAppHead to infer the type of the fuction,
+     as an (uninstantiated) TcSigmaType
+   There are special cases for
+     HsVar, HsRecFld, and ExprWithTySig
+   Otherwise, delegate back to tcExpr, which
+     infers an (instantiated) TcRhoType
+
+3. Use tcInstFun to instantiate the function, Quick-Looking as we go.
+   This implements the |-inst judgement in Fig 4, plus the
+   modification in Fig 5, of the QL paper:
+   "A quick look at impredicativity" (ICFP'20).
+
+   In tcInstFun we take a quick look at value arguments, using
+   quickLookArg.  See Note [Quick Look at value arguments].
+
+4. Use quickLookResultType to take a quick look at the result type,
+   when in checking mode.  This is the shaded part of APP-Downarrow
+   in Fig 5.
+
+5. Use tcValArgs to typecheck the value arguments
+
+6. After a gruesome special case for tagToEnum, rebuild the result.
+
+
+Some cases that /won't/ work:
+
+1. Consider this (which uses visible type application):
+
+    (let { f :: forall a. a -> a; f x = x } in f) @Int
+
+   Since 'let' is not among the special cases for tcInferAppHead,
+   we'll delegate back to tcExpr, which will instantiate f's type
+   and the type application to @Int will fail.  Too bad!
+
+-}
+
+tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
+-- See Note [tcApp: typechecking applications]
+tcApp rn_expr exp_res_ty
+  | (rn_fun, rn_args, rebuild) <- splitHsApps rn_expr
+  = do { (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args
+                                    (checkingExpType_maybe exp_res_ty)
+
+       -- Instantiate
+       ; do_ql <- wantQuickLook rn_fun
+       ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True rn_fun fun_sigma rn_args
+
+       -- Quick look at result
+       ; quickLookResultType do_ql delta app_res_rho exp_res_ty
+
+       ; whenDOptM Opt_D_dump_tc_trace $
+         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
+            ; traceTc "tcApp" (vcat [ text "rn_fun"       <+> ppr rn_fun
+                               , text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
+                               , text "do_ql:  "     <+> ppr do_ql
+                               , text "fun_sigma:  " <+> ppr fun_sigma
+                               , text "delta:      " <+> ppr delta
+                               , text "app_res_rho:" <+> ppr app_res_rho
+                               , text "exp_res_ty:"  <+> ppr exp_res_ty
+                               , text "rn_expr:"     <+> ppr rn_expr ]) }
+
+       -- Typecheck the value arguments
+       ; tc_args <- tcValArgs do_ql tc_fun inst_args
+
+       -- Special case for tagToEnum#
+       ; if isTagToEnum rn_fun
+         then tcTagToEnum rn_expr tc_fun tc_args app_res_rho exp_res_ty
+         else
+
+    do { -- Reconstruct
+       ; let tc_expr = rebuild tc_fun tc_args
+
+       -- Wrap the result
+       -- NB: app_res_ty may be a polytype, via zonkQuickLook
+       ; addFunResCtxt tc_fun tc_args app_res_rho exp_res_ty $
+         tcWrapResult rn_expr tc_expr app_res_rho exp_res_ty } }
+
+--------------------
+-- zonkArg is used *only* during debug-tracing, to make it easier to
+-- see what is going on.  For that reason, it is not a full zonk: add
+-- more if you need it.
+zonkArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
+zonkArg eva@(EValArg { eva_arg_ty = Scaled m ty })
+  = do { ty' <- zonkTcType ty
+       ; return (eva { eva_arg_ty = Scaled m ty' }) }
+zonkArg arg = return arg
+
+
+wantQuickLook :: HsExpr GhcRn -> TcM Bool
+-- GHC switches on impredicativity all the time for ($)
+wantQuickLook (HsVar _ f) | unLoc f `hasKey` dollarIdKey = return True
+wantQuickLook _                                          = xoptM LangExt.ImpredicativeTypes
+
+
+----------------
+tcValArgs :: Bool                    -- Quick-look on?
+          -> HsExpr GhcTc            -- The function (for error messages)
+          -> [HsExprArg 'TcpInst]    -- Actual argument
+          -> TcM [HsExprArg 'TcpTc]  -- Resulting argument
+tcValArgs quick_look fun args
+  = go 1 args
+  where
+    go _ [] = return []
+    go n (arg:args) = do { (n',arg') <- tc_arg n arg
+                         ; args'     <- go n' args
+                         ; return (arg' : args') }
+
+    tc_arg :: Int -> HsExprArg 'TcpInst -> TcM (Int, HsExprArg 'TcpTc)
+    tc_arg n (EPar l)              = return (n,   EPar l)
+    tc_arg n (EPrag l p)           = return (n,   EPrag l (tcExprPrag p))
+    tc_arg n (EWrap wrap)          = return (n,   EWrap wrap)
+    tc_arg n (ETypeArg l hs_ty ty) = return (n+1, ETypeArg l hs_ty ty)
+
+    tc_arg n eva@(EValArg { eva_arg = arg, eva_arg_ty = Scaled mult arg_ty })
+      = do { -- Crucial step: expose QL results before checking arg_ty
+             -- So far as the paper is concerned, this step applies
+             -- the poly-substitution Theta, learned by QL, so that we
+             -- "see" the polymorphism in that argument type. E.g.
+             --    (:) e ids, where ids :: [forall a. a->a]
+             --                     (:) :: forall p. p->[p]->[p]
+             -- Then Theta = [p :-> forall a. a->a], and we want
+             -- to check 'e' with expected type (forall a. a->a)
+             arg_ty <- if quick_look then zonkTcType arg_ty
+                                     else return arg_ty
+
+             -- Now check the argument
+           ; arg' <- addErrCtxt (funAppCtxt fun (eValArgExpr arg) n) $
+                     tcScalingUsage mult $
+                     do { traceTc "tcEValArg" $
+                          vcat [ ppr n <+> text "of" <+> ppr fun
+                               , text "arg type:" <+> ppr arg_ty
+                               , text "arg:" <+> ppr arg ]
+                        ; tcEValArg arg arg_ty }
+
+           ; return (n+1, eva { eva_arg = ValArg arg'
+                              , eva_arg_ty = Scaled mult arg_ty }) }
+
+tcEValArg :: EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
+-- Typecheck one value argument of a function call
+tcEValArg (ValArg arg) exp_arg_sigma
+  = tcCheckPolyExprNC arg exp_arg_sigma
+
+tcEValArg (ValArgQL { va_expr = L loc _, va_fun = fun, va_args = args
+                    , va_ty = app_res_rho, va_rebuild = rebuild }) exp_arg_sigma
+  = setSrcSpan loc $
+    do { traceTc "tcEValArg {" (vcat [ ppr fun <+> ppr args ])
+       ; tc_args <- tcValArgs True fun args
+       ; co <- unifyType Nothing app_res_rho exp_arg_sigma
+       ; traceTc "tcEValArg }" empty
+       ; return (L loc $ mkHsWrapCo co $ rebuild fun tc_args) }
+
+----------------
+tcValArg :: HsExpr GhcRn          -- The function (for error messages)
+         -> LHsExpr GhcRn         -- Actual argument
+         -> Scaled TcSigmaType    -- expected arg type
+         -> Int                   -- # of argument
+         -> TcM (LHsExpr GhcTc)   -- Resulting argument
+-- tcValArg is called only from Gen.Expr, dealing with left and right sections
+tcValArg fun arg (Scaled mult arg_ty) arg_no
+   = addErrCtxt (funAppCtxt fun arg arg_no) $
+     tcScalingUsage mult $
+     do { traceTc "tcValArg" $
+          vcat [ ppr arg_no <+> text "of" <+> ppr fun
+               , text "arg type:" <+> ppr arg_ty
+               , text "arg:" <+> ppr arg ]
+        ; tcCheckPolyExprNC arg arg_ty }
+
+
+{- *********************************************************************
+*                                                                      *
+              Instantiating the call
+*                                                                      *
+********************************************************************* -}
+
+type Delta = TcTyVarSet   -- Set of instantiation variables,
+                          --   written \kappa in the QL paper
+                          -- Just a set of ordinary unification variables,
+                          --   but ones that QL may fill in with polytypes
+
+tcInstFun :: Bool   -- True  <=> Do quick-look
+          -> Bool   -- False <=> Instantiate only /inferred/ variables at the end
+                    --           so may return a sigma-typex
+                    -- True  <=> Instantiate all type variables at the end:
+                    --           return a rho-type
+                    -- The /only/ call site that passes in False is the one
+                    --    in tcInferSigma, which is used only to implement :type
+                    -- Otherwise we do eager instantiation; in Fig 5 of the paper
+                    --    |-inst returns a rho-type
+          -> HsExpr GhcRn -> TcSigmaType -> [HsExprArg 'TcpRn]
+          -> TcM ( Delta
+                 , [HsExprArg 'TcpInst]
+                 , TcSigmaType )
+-- This function implements the |-inst judgement in Fig 4, plus the
+-- modification in Fig 5, of the QL paper:
+-- "A quick look at impredicativity" (ICFP'20).
+tcInstFun do_ql inst_final rn_fun fun_sigma rn_args
+  = do { traceTc "tcInstFun" (ppr rn_fun $$ ppr rn_args $$ text "do_ql" <+> ppr do_ql)
+       ; go emptyVarSet [] [] fun_sigma rn_args }
+  where
+    fun_orig = exprCtOrigin rn_fun
+    herald = sep [ text "The function" <+> quotes (ppr rn_fun)
+                 , text "is applied to"]
+
+    -- Count value args only when complaining about a function
+    -- applied to too many value args
+    -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
+    n_val_args = count isHsValArg rn_args
+
+    fun_is_out_of_scope  -- See Note [VTA for out-of-scope functions]
+      = case rn_fun of
+          HsUnboundVar {} -> True
+          _               -> False
+
+    inst_all :: ArgFlag -> Bool
+    inst_all (Invisible {}) = True
+    inst_all Required       = False
+
+    inst_inferred :: ArgFlag -> Bool
+    inst_inferred (Invisible InferredSpec)  = True
+    inst_inferred (Invisible SpecifiedSpec) = False
+    inst_inferred Required                  = False
+
+    inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
+    inst_fun [] | inst_final  = inst_all
+                | otherwise   = inst_inferred
+    inst_fun (EValArg {} : _) = inst_all
+    inst_fun _                = inst_inferred
+
+    -----------
+    go, go1 :: Delta
+            -> [HsExprArg 'TcpInst]  -- Accumulator, reversed
+            -> [Scaled TcSigmaType]  -- Value args to which applied so far
+            -> TcSigmaType -> [HsExprArg 'TcpRn]
+            -> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
+
+    -- go: If fun_ty=kappa, look it up in Theta
+    go delta acc so_far fun_ty args
+      | Just kappa <- tcGetTyVar_maybe fun_ty
+      , kappa `elemVarSet` delta
+      = do { cts <- readMetaTyVar kappa
+           ; case cts of
+                Indirect fun_ty' -> go  delta acc so_far fun_ty' args
+                Flexi            -> go1 delta acc so_far fun_ty  args }
+     | otherwise
+     = go1 delta acc so_far fun_ty args
+
+    -- go1: fun_ty is not filled-in instantiation variable
+    --      ('go' dealt with that case)
+
+    -- Rule IALL from Fig 4 of the QL paper
+    go1 delta acc so_far fun_ty args
+      | (tvs,   body1) <- tcSplitSomeForAllTys (inst_fun args) fun_ty
+      , (theta, body2) <- tcSplitPhiTy body1
+      , not (null tvs && null theta)
+      = do { (inst_tvs, wrap, fun_rho) <- setSrcSpanFromArgs rn_args $
+                                          instantiateSigma fun_orig tvs theta body2
+                 -- setSrcSpanFromArgs: important for the class constraints
+                 -- that may be emitted from instantiating fun_sigma
+           ; go (delta `extendVarSetList` inst_tvs)
+                (addArgWrap wrap acc) so_far fun_rho args }
+                -- Going around again means we deal easily with
+                -- nested  forall a. Eq a => forall b. Show b => blah
+
+    -- Rule IRESULT from Fig 4 of the QL paper
+    go1 delta acc _ fun_ty []
+       = do { traceTc "tcInstFun:ret" (ppr fun_ty)
+            ; return (delta, reverse acc, fun_ty) }
+
+    go1 delta acc so_far fun_ty (EPar sp : args)
+      = go1 delta (EPar sp : acc) so_far fun_ty args
+
+    go1 delta acc so_far fun_ty (EPrag sp prag : args)
+      = go1 delta (EPrag sp prag : acc) so_far fun_ty args
+
+    -- Rule ITYARG from Fig 4 of the QL paper
+    go1 delta acc so_far fun_ty ( ETypeArg { eva_loc = loc, eva_hs_ty = hs_ty }
+                                : rest_args )
+      | fun_is_out_of_scope   -- See Note [VTA for out-of-scope functions]
+      = go delta acc so_far fun_ty rest_args
+
+      | otherwise
+      = do { (ty_arg, inst_ty) <- tcVTA fun_ty hs_ty
+           ; let arg' = ETypeArg { eva_loc = loc, eva_hs_ty = hs_ty, eva_ty = ty_arg }
+           ; go delta (arg' : acc) so_far inst_ty rest_args }
+
+    -- Rule IVAR from Fig 4 of the QL paper:
+    go1 delta acc so_far fun_ty args@(EValArg {} : _)
+      | Just kappa <- tcGetTyVar_maybe fun_ty
+      , kappa `elemVarSet` delta
+      = -- Function type was of form   f :: forall a b. t1 -> t2 -> b
+        -- with 'b', one of the quantified type variables, in the corner
+        -- but the call applies it to three or more value args.
+        -- Suppose b is instantiated by kappa.  Then we want to make fresh
+        -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2
+        --
+        -- In principle what is happening here is not unlike matchActualFunTysRho
+        -- but there are many small differences:
+        --   - We know that the function type in unfilled meta-tyvar
+        --     matchActualFunTysRho is much more general, has a loop, etc.
+        --   - We must be sure to actually update the variable right now,
+        --     not defer in any way, because this is a QL instantiation variable.
+        --   - We need the freshly allocated unification variables, to extend
+        --     delta with.
+        -- It's easier just to do the job directly here.
+        do { arg_nus <- replicateM (countLeadingValArgs args) newOpenFlexiTyVar
+           ; res_nu  <- newOpenFlexiTyVar
+           ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
+           ; let delta'  = delta `extendVarSetList` (res_nu:arg_nus)
+                 arg_tys = mkTyVarTys arg_nus
+                 res_ty  = mkTyVarTy res_nu
+                 fun_ty' = mkVisFunTysMany arg_tys res_ty
+                 co_wrap = mkWpCastN (mkTcGReflLeftCo Nominal fun_ty' kind_co)
+                 acc'    = addArgWrap co_wrap acc
+                 -- Suppose kappa :: kk
+                 -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
+                 --      co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'
+           ; writeMetaTyVar kappa (mkCastTy fun_ty' kind_co)
+                 -- kappa is uninstantiated ('go' already checked that)
+           ; go delta' acc' so_far fun_ty' args }
+
+    -- Rule IARG from Fig 4 of the QL paper:
+    go1 delta acc so_far fun_ty
+        (eva@(EValArg { eva_arg = ValArg arg })  : rest_args)
+      = do { (wrap, arg_ty, res_ty) <- matchActualFunTySigma herald
+                                          (Just (ppr rn_fun))
+                                          (n_val_args, so_far) fun_ty
+          ; let arg_no = 1 + count isVisibleArg acc
+                -- We could cache this in a pair with acc; but
+                -- it's only evaluated if there's a type error
+          ; (delta', arg') <- if do_ql
+                              then addErrCtxt (funAppCtxt rn_fun arg arg_no) $
+                                   -- Context needed for constraints
+                                   -- generated by calls in arg
+                                   quickLookArg delta arg arg_ty
+                              else return (delta, ValArg arg)
+          ; let acc' = eva { eva_arg = arg', eva_arg_ty = arg_ty }
+                       : addArgWrap wrap acc
+          ; go delta' acc' (arg_ty:so_far) res_ty rest_args }
+
+
+
+{- *********************************************************************
+*                                                                      *
+              Visible type application
+*                                                                      *
+********************************************************************* -}
+
+tcVTA :: TcType            -- Function type
+      -> LHsWcType GhcRn   -- Argument type
+      -> TcM (TcType, TcType)
+-- Deal with a visible type application
+-- The function type has already had its Inferred binders instantiated
+tcVTA fun_ty hs_ty
+  | Just (tvb, inner_ty) <- tcSplitForAllTy_maybe fun_ty
+  , binderArgFlag tvb == Specified
+    -- It really can't be Inferred, because we've just
+    -- instantiated those. But, oddly, it might just be Required.
+    -- See Note [Required quantifiers in the type of a term]
+  = do { let tv   = binderVar tvb
+             kind = tyVarKind tv
+       ; ty_arg <- tcHsTypeApp hs_ty kind
+
+       ; inner_ty <- zonkTcType inner_ty
+             -- See Note [Visible type application zonk]
+
+       ; let in_scope  = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
+             insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
+                         -- NB: tv and ty_arg have the same kind, so this
+                         --     substitution is kind-respecting
+       ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
+                             , debugPprType ty_arg
+                             , debugPprType (tcTypeKind ty_arg)
+                             , debugPprType inner_ty
+                             , debugPprType insted_ty ])
+       ; return (ty_arg, insted_ty) }
+
+  | otherwise
+  = do { (_, fun_ty) <- zonkTidyTcType emptyTidyEnv fun_ty
+       ; failWith $
+         text "Cannot apply expression of type" <+> quotes (ppr fun_ty) $$
+         text "to a visible type argument" <+> quotes (ppr hs_ty) }
+
+{- Note [Required quantifiers in the type of a term]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#15859)
+
+  data A k :: k -> Type      -- A      :: forall k -> k -> Type
+  type KindOf (a :: k) = k   -- KindOf :: forall k. k -> Type
+  a = (undefind :: KindOf A) @Int
+
+With ImpredicativeTypes (thin ice, I know), we instantiate
+KindOf at type (forall k -> k -> Type), so
+  KindOf A = forall k -> k -> Type
+whose first argument is Required
+
+We want to reject this type application to Int, but in earlier
+GHCs we had an ASSERT that Required could not occur here.
+
+The ice is thin; c.f. Note [No Required TyCoBinder in terms]
+in GHC.Core.TyCo.Rep.
+
+Note [VTA for out-of-scope functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose 'wurble' is not in scope, and we have
+   (wurble @Int @Bool True 'x')
+
+Then the renamer will make (HsUnboundVar "wurble) for 'wurble',
+and the typechecker will typecheck it with tcUnboundId, giving it
+a type 'alpha', and emitting a deferred Hole constraint, to
+be reported later.
+
+But then comes the visible type application. If we do nothing, we'll
+generate an immediate failure (in tc_app_err), saying that a function
+of type 'alpha' can't be applied to Bool.  That's insane!  And indeed
+users complain bitterly (#13834, #17150.)
+
+The right error is the Hole, which has /already/ been emitted by
+tcUnboundId.  It later reports 'wurble' as out of scope, and tries to
+give its type.
+
+Fortunately in tcInstFun we still have access to the function, so we
+can check if it is a HsUnboundVar.  We use this info to simply skip
+over any visible type arguments.  We've already inferred the type of
+the function (in tcInferAppHead), so we'll /already/ have emitted a
+Hole constraint; failing preserves that constraint.
+
+We do /not/ want to fail altogether in this case (via failM) becuase
+that may abandon an entire instance decl, which (in the presence of
+-fdefer-type-errors) leads to leading to #17792.
+
+Downside; the typechecked term has lost its visible type arguments; we
+don't even kind-check them.  But let's jump that bridge if we come to
+it.  Meanwhile, let's not crash!
+
+
+Note [Visible type application zonk]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
+
+* tcHsTypeApp only guarantees that
+    - ty_arg is zonked
+    - kind(zonk(tv)) = kind(ty_arg)
+  (checkExpectedKind zonks as it goes).
+
+So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
+and inner_ty.  Otherwise we can build an ill-kinded type.  An example was
+#14158, where we had:
+   id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
+and we had the visible type application
+  id @(->)
+
+* We instantiated k := kappa, yielding
+    forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
+* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
+* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
+  Here q1 :: RuntimeRep
+* Now we substitute
+     cat  :->  (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
+  but we must first zonk the inner_ty to get
+      forall (a :: TYPE q1). cat a a
+  so that the result of substitution is well-kinded
+  Failing to do so led to #14158.
+
+-}
+
+{- *********************************************************************
+*                                                                      *
+              Quick Look
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Quick Look at value arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The function quickLookArg implements the "QL argument" judgement of
+the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
+rather directly.
+
+Wrinkles:
+
+* We avoid zonking, so quickLookArg thereby sees the argument type /before/
+  the QL substitution Theta is applied to it. So we achieve argument-order
+  independence for free (see 5.7 in the paper).
+
+* When we quick-look at an argument, we save the work done, by returning
+  an EValArg with a ValArgQL inside it.  (It started life with a ValArg
+  inside.)  The ValArgQL remembers all the work that QL did (notably,
+  decomposing the argument and instantiating) so that tcValArgs does
+  not need to repeat it.  Rather neat, and remarkably easy.
+-}
+
+----------------
+quickLookArg :: Delta
+             -> LHsExpr GhcRn       -- Argument
+             -> Scaled TcSigmaType  -- Type expected by the function
+             -> TcM (Delta, EValArg 'TcpInst)
+-- See Note [Quick Look at value arguments]
+--
+-- The returned Delta is a superset of the one passed in
+-- with added instantiation variables from
+--   (a) the call itself
+--   (b) the arguments of the call
+quickLookArg delta larg (Scaled _ arg_ty)
+  | isEmptyVarSet delta  = skipQuickLook delta larg
+  | otherwise            = go arg_ty
+  where
+    guarded         = isGuardedTy arg_ty
+      -- NB: guardedness is computed based on the original,
+      -- unzonked arg_ty, so we deliberately do not exploit
+      -- guardedness that emerges a result of QL on earlier args
+
+    go arg_ty | not (isRhoTy arg_ty)
+              = skipQuickLook delta larg
+
+              -- This top-level zonk step, which is the reason
+              -- we need a local 'go' loop, is subtle
+              -- See Section 9 of the QL paper
+              | Just kappa <- tcGetTyVar_maybe arg_ty
+              , kappa `elemVarSet` delta
+              = do { info <- readMetaTyVar kappa
+                   ; case info of
+                       Indirect arg_ty' -> go arg_ty'
+                       Flexi            -> quickLookArg1 guarded delta larg arg_ty }
+
+              | otherwise
+              = quickLookArg1 guarded delta larg arg_ty
+
+isGuardedTy :: TcType -> Bool
+isGuardedTy ty
+  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
+  | Just {} <- tcSplitAppTy_maybe ty        = True
+  | otherwise                               = False
+
+quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
+              -> TcM (Delta, EValArg 'TcpInst)
+quickLookArg1 guarded delta larg@(L loc arg) arg_ty
+  = setSrcSpan loc $
+    do { let (rn_fun,rn_args,rebuild) = splitHsApps arg
+       ; mb_fun_ty <- tcInferAppHead_maybe rn_fun rn_args (Just arg_ty)
+       ; traceTc "quickLookArg 1" $
+         vcat [ text "arg:" <+> ppr arg
+              , text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
+              , text "args:" <+> ppr rn_args ]
+
+       ; case mb_fun_ty of {
+           Nothing     -> -- fun is too complicated
+                          skipQuickLook delta larg ;
+           Just (fun', fun_sigma) ->
+
+    do { let no_free_kappas = findNoQuantVars fun_sigma rn_args
+       ; traceTc "quickLookArg 2" $
+         vcat [ text "no_free_kappas:" <+> ppr no_free_kappas
+              , text "guarded:" <+> ppr guarded ]
+       ; if not (guarded || no_free_kappas)
+         then skipQuickLook delta larg
+         else
+    do { do_ql <- wantQuickLook rn_fun
+       ; (delta_app, inst_args, app_res_rho)
+             <- tcInstFun do_ql True rn_fun fun_sigma rn_args
+       ; traceTc "quickLookArg" $
+         vcat [ text "arg:" <+> ppr arg
+              , text "delta:" <+> ppr delta
+              , text "delta_app:" <+> ppr delta_app
+              , text "arg_ty:" <+> ppr arg_ty
+              , text "app_res_rho:" <+> ppr app_res_rho ]
+
+       -- Do quick-look unification
+       -- NB: arg_ty may not be zonked, but that's ok
+       ; let delta' = delta `unionVarSet` delta_app
+       ; qlUnify delta' arg_ty app_res_rho
+
+       ; let ql_arg = ValArgQL { va_expr = larg, va_fun = fun'
+                               , va_args = inst_args
+                               , va_ty = app_res_rho
+                               , va_rebuild = rebuild }
+       ; return (delta', ql_arg) } } } }
+
+skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
+skipQuickLook delta larg = return (delta, ValArg larg)
+
+----------------
+quickLookResultType :: Bool -> Delta -> TcRhoType -> ExpRhoType -> TcM ()
+-- This function implements the shaded bit of rule APP-Downarrow in
+-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
+
+quickLookResultType do_ql delta app_res_rho exp_res_ty
+  | do_ql
+  , not (isEmptyVarSet delta)  -- Optimisation only
+  , Just exp_rho <- checkingExpType_maybe exp_res_ty
+                               -- In checking mode only
+  = qlUnify delta app_res_rho exp_rho
+  | otherwise
+  = return ()
+
+---------------------
+qlUnify :: Delta -> TcType -> TcType -> TcM ()
+-- Unify ty1 with ty2, unifying only variables in delta
+qlUnify delta ty1 ty2
+  = do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2)
+       ; go (emptyVarSet,emptyVarSet) ty1 ty2 }
+  where
+    go :: (TyVarSet, TcTyVarSet)
+       -> TcType -> TcType
+       -> TcM ()
+    -- The TyVarSets give the variables bound by enclosing foralls
+    -- for the corresponding type. Don't unify with these.
+    go bvs (TyVarTy tv) ty2
+      | tv `elemVarSet` delta = go_kappa bvs tv ty2
+
+    go (bvs1, bvs2) ty1 (TyVarTy tv)
+      | tv `elemVarSet` delta = go_kappa (bvs2,bvs1) tv ty1
+
+    go bvs (CastTy ty1 _) ty2 = go bvs ty1 ty2
+    go bvs ty1 (CastTy ty2 _) = go bvs ty1 ty2
+
+    go _ (TyConApp tc1 []) (TyConApp tc2 [])
+      | tc1 == tc2 -- See GHC.Tc.Utils.Unify
+      = return ()  -- Note [Expanding synonyms during unification]
+
+    -- Now, and only now, expand synonyms
+    go bvs rho1 rho2
+      | Just rho1 <- tcView rho1 = go bvs rho1 rho2
+      | Just rho2 <- tcView rho2 = go bvs rho1 rho2
+
+    go bvs (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+      | tc1 == tc2
+      , not (isTypeFamilyTyCon tc1)
+      , tys1 `equalLength` tys2
+      = zipWithM_ (go bvs) tys1 tys2
+
+    -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
+    -- and         (c1 => res1) ~   (c2 => res2)
+    -- But for the latter we only learn instantiation info from t1~t2
+    -- We look at the multiplicity too, although the chances of getting
+    -- impredicative instantiation info from there seems...remote.
+    go bvs (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
+           (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
+      | af1 == af2
+      = do { when (af1 == VisArg) $
+             do { go bvs arg1 arg2; go bvs mult1 mult2 }
+           ; go bvs res1 res2 }
+
+    -- ToDo: c.f. Tc.Utils.unify.uType,
+    -- which does not split FunTy here
+    -- Also NB tcRepSplitAppTy here, which does not split (c => t)
+    go bvs (AppTy t1a t1b) ty2
+      | Just (t2a, t2b) <- tcRepSplitAppTy_maybe ty2
+      = do { go bvs t1a t2a; go bvs t1b t2b }
+
+    go bvs ty1 (AppTy t2a t2b)
+      | Just (t1a, t1b) <- tcRepSplitAppTy_maybe ty1
+      = do { go bvs t1a t2a; go bvs t1b t2b }
+
+    go (bvs1, bvs2) (ForAllTy bv1 ty1) (ForAllTy bv2 ty2)
+      = go (bvs1',bvs2') ty1 ty2
+      where
+       bvs1' = bvs1 `extendVarSet` binderVar bv1
+       bvs2' = bvs2 `extendVarSet` binderVar bv2
+
+    go _ _ _ = return ()
+
+
+    ----------------
+    go_kappa bvs kappa ty2
+      = ASSERT2( isMetaTyVar kappa, ppr kappa )
+        do { info <- readMetaTyVar kappa
+           ; case info of
+               Indirect ty1 -> go bvs ty1 ty2
+               Flexi        -> do { ty2 <- zonkTcType ty2
+                                  ; go_flexi bvs kappa ty2 } }
+
+    ----------------
+    go_flexi (_,bvs2) kappa ty2  -- ty2 is zonked
+      | -- See Note [Actual unification in qlUnify]
+        let ty2_tvs = shallowTyCoVarsOfType ty2
+      , not (ty2_tvs `intersectsVarSet` bvs2)
+          -- Can't instantiate a delta-varto a forall-bound variable
+      , Just ty2 <- occCheckExpand [kappa] ty2
+          -- Passes the occurs check
+      = do { let ty2_kind   = typeKind ty2
+                 kappa_kind = tyVarKind kappa
+           ; co <- unifyKind (Just (ppr ty2)) ty2_kind kappa_kind
+                   -- unifyKind: see Note [Actual unification in qlUnify]
+
+           ; traceTc "qlUnify:update" $
+             vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
+                       2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
+                 , text "co:" <+> ppr co ]
+           ; writeMetaTyVar kappa (mkCastTy ty2 co) }
+
+      | otherwise
+      = return ()   -- Occurs-check or forall-bound varialbe
+
+
+{- Note [Actual unification in qlUnify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
+That is the entire point of qlUnify!   Wrinkles:
+
+* We must not unify with anything bound by an enclosing forall; e.g.
+    (forall a. kappa -> Int) ~ forall a. a -> Int)
+  That's tracked by the 'bvs' arg of 'go'.
+
+* We must not make an occurs-check; we use occCheckExpand for that.
+
+* metaTyVarUpdateOK also checks for various other things, including
+  - foralls, and predicate types (which we want to allow here)
+  - type families (relates to a very specific and exotic performance
+    question, that is unlikely to bite here)
+  - blocking coercion holes
+  After some thought we believe that none of these are relevant
+  here
+
+* What if kappa and ty have different kinds?  We solve that problem by
+  calling unifyKind, producing a coercion perhaps emitting some deferred
+  equality constraints.  That is /different/ from the approach we use in
+  the main constraint solver for herterogeneous equalities; see Note
+  [Equalities with incompatible kinds] in Solver.Canonical
+
+  Why different? Because:
+  - We can't use qlUnify to solve the kind constraint because qlUnify
+    won't unify ordinary (non-instantiation) unification variables.
+    (It would have to worry about lots of things like untouchability
+    if it did.)
+  - qlUnify can't give up if the kinds look un-equal because that would
+    mean that it might succeed some times (when the eager unifier
+    has already unified those kinds) but not others -- order
+    dependence.
+  - We can't use the ordinary unifier/constraint solver instead,
+    because it doesn't unify polykinds, and has all kinds of other
+    magic.  qlUnify is very focused.
+
+  TL;DR Calling unifyKind seems like the lesser evil.
+  -}
+
+{- *********************************************************************
+*                                                                      *
+              Guardedness
+*                                                                      *
+********************************************************************* -}
+
+findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
+-- True <=> there are no free quantified variables
+--          in the result of the call
+-- E.g. in the call (f e1 e2), if
+--   f :: forall a b. a -> b -> Int   return True
+--   f :: forall a b. a -> b -> b     return False (b is free)
+findNoQuantVars fun_ty args
+  = go emptyVarSet fun_ty args
+  where
+    need_instantiation []               = True
+    need_instantiation (EValArg {} : _) = True
+    need_instantiation _                = False
+
+    go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
+    go bvs fun_ty args
+      | need_instantiation args
+      , (tvs, theta, rho) <- tcSplitSigmaTy fun_ty
+      , not (null tvs && null theta)
+      = go (bvs `extendVarSetList` tvs) rho args
+
+    go bvs fun_ty [] =  tyCoVarsOfType fun_ty `disjointVarSet` bvs
+
+    go bvs fun_ty (EPar {}  : args) = go bvs fun_ty args
+    go bvs fun_ty (EPrag {} : args) = go bvs fun_ty args
+
+    go bvs fun_ty args@(ETypeArg {} : rest_args)
+      | (tvs,  body1) <- tcSplitSomeForAllTys (== Inferred) fun_ty
+      , (theta, body2) <- tcSplitPhiTy body1
+      , not (null tvs && null theta)
+      = go (bvs `extendVarSetList` tvs) body2 args
+      | Just (_tv, res_ty) <- tcSplitForAllTy_maybe fun_ty
+      = go bvs res_ty rest_args
+      | otherwise
+      = False  -- E.g. head ids @Int
+
+    go bvs fun_ty (EValArg {} : rest_args)
+      | Just (_, res_ty) <- tcSplitFunTy_maybe fun_ty
+      = go bvs res_ty rest_args
+      | otherwise
+      = False  -- E.g. head id 'x'
+
+
+{- *********************************************************************
+*                                                                      *
+                 tagToEnum#
+*                                                                      *
+********************************************************************* -}
+
+{- Note [tagToEnum#]
+~~~~~~~~~~~~~~~~~~~~
+Nasty check to ensure that tagToEnum# is applied to a type that is an
+enumeration TyCon.  Unification may refine the type later, but this
+check won't see that, alas.  It's crude, because it relies on our
+knowing *now* that the type is ok, which in turn relies on the
+eager-unification part of the type checker pushing enough information
+here.  In theory the Right Thing to do is to have a new form of
+constraint but I definitely cannot face that!  And it works ok as-is.
+
+Here's are two cases that should fail
+        f :: forall a. a
+        f = tagToEnum# 0        -- Can't do tagToEnum# at a type variable
+
+        g :: Int
+        g = tagToEnum# 0        -- Int is not an enumeration
+
+When data type families are involved it's a bit more complicated.
+     data family F a
+     data instance F [Int] = A | B | C
+Then we want to generate something like
+     tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
+Usually that coercion is hidden inside the wrappers for
+constructors of F [Int] but here we have to do it explicitly.
+
+It's all grotesquely complicated.
+-}
+
+isTagToEnum :: HsExpr GhcRn -> Bool
+isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
+isTagToEnum _ = False
+
+tcTagToEnum :: HsExpr GhcRn -> HsExpr GhcTc -> [HsExprArg 'TcpTc]
+            -> TcRhoType -> ExpRhoType
+            -> TcM (HsExpr GhcTc)
+-- tagToEnum# :: forall a. Int# -> a
+-- See Note [tagToEnum#]   Urgh!
+tcTagToEnum expr fun args app_res_ty res_ty
+  | null val_args
+  = failWithTc (text "tagToEnum# must appear applied to one argument")
+
+  | otherwise
+  = do { res_ty <- readExpType res_ty
+       ; ty'    <- zonkTcType res_ty
+
+       -- Check that the type is algebraic
+       ; case tcSplitTyConApp_maybe ty' of {
+           Nothing -> do { addErrTc (mk_error ty' doc1)
+                         ; vanilla_result } ;
+           Just (tc, tc_args) ->
+
+    do { -- Look through any type family
+       ; fam_envs <- tcGetFamInstEnvs
+       ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
+           Nothing -> do { check_enumeration ty' tc
+                         ; vanilla_result } ;
+           Just (rep_tc, rep_args, coi) ->
+
+    do { -- coi :: tc tc_args ~R rep_tc rep_args
+         check_enumeration ty' rep_tc
+       ; let rep_ty  = mkTyConApp rep_tc rep_args
+             fun'    = mkHsWrap (WpTyApp rep_ty) fun
+             expr'   = rebuildPrefixApps fun' val_args
+             df_wrap = mkWpCastR (mkTcSymCo coi)
+       ; return (mkHsWrap df_wrap expr') }}}}}
+
+  where
+    val_args = dropWhile (not . isHsValArg) args
+
+    vanilla_result
+      = do { let expr' = rebuildPrefixApps fun args
+           ; tcWrapResult expr expr' app_res_ty res_ty }
+
+    check_enumeration ty' tc
+      | isEnumerationTyCon tc = return ()
+      | otherwise             = addErrTc (mk_error ty' doc2)
+
+    doc1 = vcat [ text "Specify the type by giving a type signature"
+                , text "e.g. (tagToEnum# x) :: Bool" ]
+    doc2 = text "Result type must be an enumeration type"
+
+    mk_error :: TcType -> SDoc -> SDoc
+    mk_error ty what
+      = hang (text "Bad call to tagToEnum#"
+               <+> text "at type" <+> ppr ty)
+           2 what
+
+
+{- *********************************************************************
+*                                                                      *
+             Pragmas on expressions
+*                                                                      *
+********************************************************************* -}
+
+tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
+tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
+
+
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 1cbdcc005b..82d405f0bb 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -15,10 +15,11 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where
 import GHC.Prelude
 
 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp
-                                       , tcCheckId, tcCheckPolyExpr )
+                                       , tcCheckPolyExpr )
 
 import GHC.Hs
 import GHC.Tc.Gen.Match
+import GHC.Tc.Gen.Head( tcCheckId )
 import GHC.Tc.Utils.Zonk( hsLPatType )
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.TcMType
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 9870c36ff5..9d40225a55 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -14,9 +14,9 @@
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 
 module GHC.Tc.Gen.Expr
-       ( tcCheckPolyExpr,
+       ( tcCheckPolyExpr, tcCheckPolyExprNC,
          tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC,
-         tcInferSigma, tcInferRho, tcInferRhoNC,
+         tcInferRho, tcInferRhoNC,
          tcExpr,
          tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
          tcCheckId,
@@ -28,7 +28,6 @@ module GHC.Tc.Gen.Expr
 import GHC.Prelude
 
 import {-# SOURCE #-}   GHC.Tc.Gen.Splice( tcSpliceExpr, tcTypedBracket, tcUntypedBracket )
-import GHC.Builtin.Names.TH( liftStringName, liftName )
 
 import GHC.Hs
 import GHC.Tc.Utils.Zonk
@@ -38,18 +37,16 @@ import GHC.Types.Basic
 import GHC.Core.Multiplicity
 import GHC.Core.UsageEnv
 import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Gen.Bind        ( chooseInferredQuantifiers, tcLocalBinds )
-import GHC.Tc.Gen.Sig         ( tcUserTypeSig, tcInstSig )
-import GHC.Tc.Solver          ( simplifyInfer, InferMode(..) )
-import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst, tcLookupDataFamInst_maybe )
+import GHC.Tc.Gen.App
+import GHC.Tc.Gen.Head
+import GHC.Tc.Gen.Bind        ( tcLocalBinds )
+import GHC.Tc.Instance.Family ( tcGetFamInstEnvs )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
 import GHC.Rename.Env         ( addUsedGRE )
-import GHC.Rename.Utils       ( addNameClashErrRn, unknownSubordinateErr )
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.Arrow
 import GHC.Tc.Gen.Match
 import GHC.Tc.Gen.HsType
-import GHC.Tc.TyCl.PatSyn     ( tcPatSynBuilderOcc, nonBidirectionalErr )
 import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Origin
@@ -64,19 +61,14 @@ import GHC.Types.Name.Env
 import GHC.Types.Name.Set
 import GHC.Types.Name.Reader
 import GHC.Core.TyCon
-import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.Ppr
-import GHC.Core.TyCo.Subst (substTyWithInScope)
 import GHC.Core.Type
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
 import GHC.Builtin.Types
-import GHC.Builtin.PrimOps( tagToEnumKey )
 import GHC.Builtin.Names
 import GHC.Driver.Session
 import GHC.Types.SrcLoc
 import GHC.Utils.Misc
-import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
 import GHC.Data.List.SetOps
 import GHC.Data.Maybe
 import GHC.Utils.Outputable as Outputable
@@ -84,7 +76,7 @@ import GHC.Utils.Panic
 import GHC.Data.FastString
 import Control.Monad
 import GHC.Core.Class(classTyCon)
-import GHC.Types.Unique.Set
+import GHC.Types.Unique.Set ( UniqSet, mkUniqSet, elementOfUniqSet, nonDetEltsUniqSet )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.Function
@@ -118,7 +110,7 @@ tcPolyExpr, tcPolyExprNC
   -> TcM (LHsExpr GhcTc)
 
 tcPolyExpr expr res_ty
-  = addExprCtxt expr $
+  = addLExprCtxt expr $
     do { traceTc "tcPolyExpr" (ppr res_ty)
        ; tcPolyExprNC expr res_ty }
 
@@ -134,21 +126,11 @@ tcPolyExprNC (L loc expr) res_ty
         set_loc_and_ctxt l e m = do
           inGenCode <- inGeneratedCode
           if inGenCode && not (isGeneratedSrcSpan l)
-            then setSrcSpan l $ addExprCtxt (L l e) m
+            then setSrcSpan l $
+                 addExprCtxt e m
             else setSrcSpan l m
 
 ---------------
-tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)
--- Used by tcRnExpr to implement GHCi :type
--- It goes against the principle of eager instantiation,
--- so we expect very very few calls to this function
--- Most clients will want tcInferRho
-tcInferSigma le@(L loc expr)
-  = addExprCtxt le $ setSrcSpan loc $
-    do { (fun, args, ty) <- tcInferApp expr
-       ; return (L loc (applyHsArgs fun args), ty) }
-
----------------
 tcCheckMonoExpr, tcCheckMonoExprNC
     :: LHsExpr GhcRn     -- Expression to type check
     -> TcRhoType         -- Expected type
@@ -164,7 +146,7 @@ tcMonoExpr, tcMonoExprNC
     -> TcM (LHsExpr GhcTc)
 
 tcMonoExpr expr res_ty
-  = addExprCtxt expr $
+  = addLExprCtxt expr $
     tcMonoExprNC expr res_ty
 
 tcMonoExprNC (L loc expr) res_ty
@@ -175,7 +157,8 @@ tcMonoExprNC (L loc expr) res_ty
 ---------------
 tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
 -- Infer a *rho*-type. The return type is always instantiated.
-tcInferRho le = addExprCtxt le (tcInferRhoNC le)
+tcInferRho le = addLExprCtxt le $
+                tcInferRhoNC le
 
 tcInferRhoNC (L loc expr)
   = setSrcSpan loc $
@@ -189,36 +172,45 @@ tcInferRhoNC (L loc expr)
 *                                                                      *
 ********************************************************************* -}
 
-tcLExpr, tcLExprNC
-    :: LHsExpr GhcRn     -- Expression to type check
-    -> ExpRhoType        -- Expected type
-                         -- Definitely no foralls at the top
-    -> TcM (LHsExpr GhcTc)
-
-tcLExpr expr res_ty
-  = setSrcSpan (getLoc expr) $ addExprCtxt expr (tcLExprNC expr res_ty)
-
-tcLExprNC (L loc expr) res_ty
-  = setSrcSpan loc $
-    do  { expr' <- tcExpr expr res_ty
-        ; return (L loc expr') }
-
 tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-tcExpr (HsVar _ (L _ name))   res_ty = tcCheckId name res_ty
-tcExpr e@(HsUnboundVar _ uv)  res_ty = tcUnboundId e uv res_ty
 
-tcExpr e@(HsApp {})     res_ty = tcApp e res_ty
-tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty
+-- Use tcApp to typecheck appplications, which are treated specially
+-- by Quick Look.  Specifically:
+--   - HsApp:     value applications
+--   - HsTypeApp: type applications
+--   - HsVar:     lone variables, to ensure that they can get an
+--                impredicative instantiation (via Quick Look
+--                driven by res_ty (in checking mode).
+--   - ExprWithTySig: (e :: type)
+-- See Note [Application chains and heads] in GHC.Tc.Gen.App
+tcExpr e@(HsVar {})         res_ty = tcApp e res_ty
+tcExpr e@(HsApp {})         res_ty = tcApp e res_ty
+tcExpr e@(HsAppType {})     res_ty = tcApp e res_ty
+tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty
+tcExpr e@(HsRecFld {})      res_ty = tcApp e res_ty
+
+-- Typecheck an occurrence of an unbound Id
+--
+-- Some of these started life as a true expression hole "_".
+-- Others might simply be variables that accidentally have no binding site
+tcExpr e@(HsUnboundVar _ occ) res_ty
+  = do { ty <- newOpenFlexiTyVarTy  -- Allow Int# etc (#12531)
+       ; name <- newSysName occ
+       ; let ev = mkLocalId name Many ty
+       ; emitNewExprHole occ ev ty
+       ; tcWrapResultO (UnboundOccurrenceOf occ) e
+                       (HsUnboundVar ev occ) ty res_ty }
 
 tcExpr e@(HsLit x lit) res_ty
   = do { let lit_ty = hsLitType lit
        ; tcWrapResult e (HsLit x (convertLit lit)) lit_ty res_ty }
 
-tcExpr (HsPar x expr) res_ty = do { expr' <- tcLExprNC expr res_ty
-                                  ; return (HsPar x expr') }
+tcExpr (HsPar x expr) res_ty
+  = do { expr' <- tcMonoExprNC expr res_ty
+       ; return (HsPar x expr') }
 
 tcExpr (HsPragE x prag expr) res_ty
-  = do { expr' <- tcLExpr expr res_ty
+  = do { expr' <- tcMonoExpr expr res_ty
        ; return (HsPragE x (tcExprPrag prag) expr') }
 
 tcExpr (HsOverLit x lit) res_ty
@@ -229,7 +221,7 @@ tcExpr (NegApp x expr neg_expr) res_ty
   = do  { (expr', neg_expr')
             <- tcSyntaxOp NegateOrigin neg_expr [SynAny] res_ty $
                \[arg_ty] [arg_mult] ->
-               tcScalingUsage arg_mult $ tcLExpr expr (mkCheckExpType arg_ty)
+               tcScalingUsage arg_mult $ tcCheckMonoExpr expr arg_ty
         ; return (NegApp x expr' neg_expr') }
 
 tcExpr e@(HsIPVar _ x) res_ty
@@ -297,10 +289,6 @@ tcExpr e@(HsLamCase x matches) res_ty
               , text "requires"]
     match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
 
-tcExpr e@(ExprWithTySig _ expr hs_ty) res_ty
-  = do { (expr', poly_ty) <- tcExprWithSig expr hs_ty
-       ; tcWrapResult e expr' poly_ty res_ty }
-
 {-
 Note [Type-checking overloaded labels]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -345,102 +333,10 @@ With PostfixOperators we don't actually require the function to take
 two arguments at all.  For example, (x `not`) means (not x); you get
 postfix operators!  Not Haskell 98, but it's less work and kind of
 useful.
-
-Note [Typing rule for ($)]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-People write
-   runST $ blah
-so much, where
-   runST :: (forall s. ST s a) -> a
-that I have finally given in and written a special type-checking
-rule just for saturated applications of ($).
-  * Infer the type of the first argument
-  * Decompose it; should be of form (arg2_ty -> res_ty),
-       where arg2_ty might be a polytype
-  * Use arg2_ty to typecheck arg2
 -}
 
-tcExpr expr@(OpApp fix arg1 op arg2) res_ty
-  | (L loc (HsVar _ (L lv op_name))) <- op
-  , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
-  = do { traceTc "Application rule" (ppr op)
-       ; (arg1', arg1_ty) <- addErrCtxt (funAppCtxt op arg1 1) $
-                             tcInferRhoNC arg1
-
-       ; let doc   = text "The first argument of ($) takes"
-             orig1 = lexprCtOrigin arg1
-       ; (wrap_arg1, [arg2_sigma], op_res_ty) <-
-           matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty
-
-       ; mult_wrap <- tcSubMult AppOrigin Many (scaledMult arg2_sigma)
-         -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
-         --
-         -- When ($) becomes multiplicity-polymorphic, then the above check will
-         -- need to go. But in the meantime, it would produce ill-typed
-         -- desugared code to accept linear functions to the left of a ($).
-
-         -- We have (arg1 $ arg2)
-         -- So: arg1_ty = arg2_ty -> op_res_ty
-         -- where arg2_sigma maybe polymorphic; that's the point
-
-       ; arg2' <- tcArg nl_op arg2 arg2_sigma 2
-
-       -- Make sure that the argument type has kind '*'
-       --   ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b
-       -- Eg we do not want to allow  (D#  $  4.0#)   #5570
-       --    (which gives a seg fault)
-       ; _ <- unifyKind (Just (XHsType $ NHsCoreTy (scaledThing arg2_sigma)))
-                        (tcTypeKind (scaledThing arg2_sigma)) liftedTypeKind
-           -- Ignore the evidence. arg2_sigma must have type * or #,
-           -- because we know (arg2_sigma -> op_res_ty) is well-kinded
-           -- (because otherwise matchActualFunTysRho would fail)
-           -- So this 'unifyKind' will either succeed with Refl, or will
-           -- produce an insoluble constraint * ~ #, which we'll report later.
-
-       -- NB: unlike the argument type, the *result* type, op_res_ty can
-       -- have any kind (#8739), so we don't need to check anything for that
-
-       ; op_id  <- tcLookupId op_name
-       ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep op_res_ty
-                                               , scaledThing arg2_sigma
-                                               , op_res_ty])
-                                   (HsVar noExtField (L lv op_id)))
-             -- arg1' :: arg1_ty
-             -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
-             -- op' :: (a2_ty -> op_res_ty) -> a2_ty -> op_res_ty
-
-             expr' = OpApp fix (mkLHsWrap (wrap_arg1 <.> mult_wrap) arg1') op' arg2'
-
-       ; tcWrapResult expr expr' op_res_ty res_ty }
-
-  | L loc (HsRecFld _ (Ambiguous _ lbl)) <- op
-  , Just sig_ty <- obviousSig (unLoc arg1)
-    -- See Note [Disambiguating record fields]
-  = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
-       ; sel_name <- disambiguateSelector lbl sig_tc_ty
-       ; let op' = L loc (HsRecFld noExtField (Unambiguous sel_name lbl))
-       ; tcExpr (OpApp fix arg1 op' arg2) res_ty
-       }
-
-  | otherwise
-  = do { traceTc "Non Application rule" (ppr op)
-       ; (op', op_ty) <- tcInferRhoNC op
-
-       ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
-                  <- matchActualFunTysRho (mk_op_msg op) fn_orig
-                                          (Just (unLoc op)) 2 op_ty
-         -- You might think we should use tcInferApp here, but there is
-         -- too much impedance-matching, because tcApp may return wrappers as
-         -- well as type-checked arguments.
-
-       ; arg1' <- tcArg nl_op arg1 arg1_ty 1
-       ; arg2' <- tcArg nl_op arg2 arg2_ty 2
-
-       ; let expr' = OpApp fix arg1' (mkLHsWrap wrap_fun op') arg2'
-       ; tcWrapResult expr expr' op_res_ty res_ty }
-  where
-    fn_orig = exprCtOrigin nl_op
-    nl_op   = unLoc op
+tcExpr expr@(OpApp {}) res_ty
+  = tcApp expr res_ty
 
 -- Right sections, equivalent to \ x -> x `op` expr, or
 --      \ x -> op x expr
@@ -449,8 +345,8 @@ tcExpr expr@(SectionR x op arg2) res_ty
   = do { (op', op_ty) <- tcInferRhoNC op
        ; (wrap_fun, [Scaled arg1_mult arg1_ty, arg2_ty], op_res_ty)
                   <- matchActualFunTysRho (mk_op_msg op) fn_orig
-                                          (Just (unLoc op)) 2 op_ty
-       ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2
+                                          (Just (ppr op)) 2 op_ty
+       ; arg2' <- tcValArg (unLoc op) arg2 arg2_ty 2
        ; let expr'      = SectionR x (mkLHsWrap wrap_fun op') arg2'
              act_res_ty = mkVisFunTy arg1_mult arg1_ty op_res_ty
        ; tcWrapResultMono expr expr' act_res_ty res_ty }
@@ -469,8 +365,8 @@ tcExpr expr@(SectionL x arg1 op) res_ty
 
        ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty)
            <- matchActualFunTysRho (mk_op_msg op) fn_orig
-                                   (Just (unLoc op)) n_reqd_args op_ty
-       ; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1
+                                   (Just (ppr op)) n_reqd_args op_ty
+       ; arg1' <- tcValArg (unLoc op) arg1 arg1_ty 1
        ; let expr'      = SectionL x arg1' (mkLHsWrap wrap_fn op')
              act_res_ty = mkVisFunTys arg_tys op_res_ty
        ; tcWrapResultMono expr expr' act_res_ty res_ty }
@@ -510,7 +406,7 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty
        ; let expr'       = ExplicitTuple x tup_args1 boxity
              missing_tys = [Scaled mult ty | (L _ (Missing (Scaled mult _)), ty) <- zip tup_args1 arg_tys]
 
-             -- See Note [Linear fields generalization]
+             -- See Note [Linear fields generalization] in GHC.Tc.Gen.App
              act_res_ty
                  = mkVisFunTys missing_tys (mkTupleTy1 boxity arg_tys)
                    -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
@@ -565,7 +461,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty
 
 tcExpr (HsLet x (L l binds) expr) res_ty
   = do  { (binds', expr') <- tcLocalBinds binds $
-                             tcLExpr expr res_ty
+                             tcMonoExpr expr res_ty
         ; return (HsLet x (L l binds') expr') }
 
 tcExpr (HsCase x scrut matches) res_ty
@@ -598,9 +494,9 @@ tcExpr (HsCase x scrut matches) res_ty
                       mc_body = tcBody }
 
 tcExpr (HsIf x pred b1 b2) res_ty
-  = do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
-       ; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty
-       ; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty
+  = do { pred'    <- tcCheckMonoExpr pred boolTy
+       ; (u1,b1') <- tcCollectingUsage $ tcMonoExpr b1 res_ty
+       ; (u2,b2') <- tcCollectingUsage $ tcMonoExpr b2 res_ty
        ; tcEmitBindingUsage (supUE u1 u2)
        ; return (HsIf x pred' b1' b2') }
 
@@ -858,7 +754,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
             --
             -- This should definitely *not* typecheck.
 
-        -- STEP -1  See Note [Disambiguating record fields]
+        -- STEP -1  See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
         -- After this we know that rbinds is unambiguous
         ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty
         ; let upd_flds = map (unLoc . hsRecFieldLbl . unLoc) rbinds
@@ -929,7 +825,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
         -- Check that we're not dealing with a unidirectional pattern
         -- synonym
         ; unless (isJust $ conLikeWrapId_maybe con1)
-                  (nonBidirectionalErr (conLikeName con1))
+                 (nonBidirectionalErr (conLikeName con1))
 
         -- STEP 3    Note [Criteria for update]
         -- Check that each updated field is polymorphic; that is, its type
@@ -972,7 +868,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
               scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
               con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
 
-        ; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty
+        ; co_scrut <- unifyType (Just (ppr record_expr)) record_rho scrut_ty
                 -- NB: normal unification is OK here (as opposed to subsumption),
                 -- because for this to work out, both record_rho and scrut_ty have
                 -- to be normal datatypes -- no contravariant stuff can go on
@@ -1012,8 +908,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
 
         ; tcWrapResult expr expr' rec_res_ty res_ty }
 
-tcExpr e@(HsRecFld _ f) res_ty
-    = tcCheckRecSelId e f res_ty
 
 {-
 ************************************************************************
@@ -1069,37 +963,11 @@ tcExpr (XExpr (HsExpanded a b)) t
 ************************************************************************
 -}
 
-tcExpr other _ = pprPanic "tcLExpr" (ppr other)
+tcExpr other _ = pprPanic "tcExpr" (ppr other)
   -- Include ArrForm, ArrApp, which shouldn't appear at all
   -- Also HsTcBracketOut, HsQuasiQuoteE
 
 
-{- *********************************************************************
-*                                                                      *
-             Pragmas on expressions
-*                                                                      *
-********************************************************************* -}
-
-tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
-tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-
-
-{- *********************************************************************
-*                                                                      *
-             Expression with type signature e::ty
-*                                                                      *
-********************************************************************* -}
-
-tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
-              -> TcM (HsExpr GhcTc, TcSigmaType)
-tcExprWithSig expr hs_ty
-  = do { sig_info <- checkNoErrs $  -- Avoid error cascade
-                     tcUserTypeSig loc hs_ty Nothing
-       ; (expr', poly_ty) <- tcExprSig expr sig_info
-       ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
-  where
-    loc = getLoc (hsSigWcType hs_ty)
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1160,400 +1028,13 @@ arithSeqEltType (Just fl) res_ty
               \ [elt_ty] [elt_mult] -> return (elt_mult, elt_ty)
        ; return (idHsWrapper, elt_mult, elt_ty, Just fl') }
 
-{-
-************************************************************************
-*                                                                      *
-                Applications
-*                                                                      *
-************************************************************************
--}
-
-{- Note [Typechecking applications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We typecheck application chains (f e1 @ty e2) specially:
-
-* So we can report errors like "in the third arument of a call of f"
-
-* So we can do Visible Type Application (VTA), for which we must not
-  eagerly instantiate the function part of the application.
-
-* So that we can do Quick Look impredicativity.
-
-The idea is:
-
-* Use collectHsArgs, which peels off
-     HsApp, HsTypeApp, HsPrag, HsPar
-  returning the function in the corner and the arguments
-
-* Use tcInferAppHead to infer the type of the fuction,
-    as an (uninstantiated) TcSigmaType
-  There are special cases for
-     HsVar, HsREcFld, and ExprWithTySig
-  Otherwise, delegate back to tcExpr, which
-    infers an (instantiated) TcRhoType
-
-Some cases that /won't/ work:
-
-1. Consider this (which uses visible type application):
-
-    (let { f :: forall a. a -> a; f x = x } in f) @Int
-
-   Since 'let' is not among the special cases for tcInferAppHead,
-   we'll delegate back to tcExpr, which will instantiate f's type
-   and the type application to @Int will fail.  Too bad!
-
--}
-
--- HsExprArg is a very local type, used only within this module.
--- It's really a zipper for an application chain
--- It's a GHC-specific type, so using TTG only where necessary
-data HsExprArg id
-  = HsEValArg  SrcSpan        -- Of the function
-               (LHsExpr (GhcPass id))
-  | HsETypeArg SrcSpan        -- Of the function
-               (LHsWcType (NoGhcTc (GhcPass id)))
-               !(XExprTypeArg id)
-  | HsEPrag    SrcSpan
-               (HsPragE (GhcPass id))
-  | HsEPar     SrcSpan         -- Of the nested expr
-  | HsEWrap    !(XArgWrap id)  -- Wrapper, after typechecking only
-
--- The outer location is the location of the application itself
-type LHsExprArgIn  = HsExprArg 'Renamed
-type LHsExprArgOut = HsExprArg 'Typechecked
-
-instance OutputableBndrId id => Outputable (HsExprArg id) where
-  ppr (HsEValArg _ tm)       = ppr tm
-  ppr (HsEPrag _ p)          = text "HsPrag" <+> ppr p
-  ppr (HsETypeArg _ hs_ty _) = char '@' <> ppr hs_ty
-  ppr (HsEPar _)             = text "HsEPar"
-  ppr (HsEWrap w)             = case ghcPass @id of
-                                    GhcTc -> text "HsEWrap" <+> ppr w
-#if __GLASGOW_HASKELL__ <= 900
-                                    _     -> empty
-#endif
-
-type family XExprTypeArg id where
-  XExprTypeArg 'Parsed      = NoExtField
-  XExprTypeArg 'Renamed     = NoExtField
-  XExprTypeArg 'Typechecked = Type
-
-type family XArgWrap id where
-  XArgWrap 'Parsed      = NoExtCon
-  XArgWrap 'Renamed     = NoExtCon
-  XArgWrap 'Typechecked = HsWrapper
-
-addArgWrap :: HsWrapper -> [LHsExprArgOut] -> [LHsExprArgOut]
-addArgWrap wrap args
- | isIdHsWrapper wrap = args
- | otherwise          = HsEWrap wrap : args
-
-collectHsArgs :: HsExpr GhcRn -> (HsExpr GhcRn, [LHsExprArgIn])
-collectHsArgs e = go e []
-  where
-    go (HsPar _     (L l fun))       args = go fun (HsEPar l : args)
-    go (HsPragE _ p (L l fun))       args = go fun (HsEPrag l p : args)
-    go (HsApp _     (L l fun) arg)   args = go fun (HsEValArg l arg : args)
-    go (HsAppType _ (L l fun) hs_ty) args = go fun (HsETypeArg l hs_ty noExtField : args)
-    go e                             args = (e,args)
-
-applyHsArgs :: HsExpr GhcTc -> [LHsExprArgOut]-> HsExpr GhcTc
-applyHsArgs fun args
-  = go fun args
-  where
-    go fun [] = fun
-    go fun (HsEWrap wrap : args)          = go (mkHsWrap wrap fun) args
-    go fun (HsEValArg l arg : args)       = go (HsApp noExtField (L l fun) arg) args
-    go fun (HsETypeArg l hs_ty ty : args) = go (HsAppType ty (L l fun) hs_ty) args
-    go fun (HsEPar l : args)              = go (HsPar noExtField (L l fun)) args
-    go fun (HsEPrag l p : args)           = go (HsPragE noExtField p (L l fun)) args
-
-isHsValArg :: HsExprArg id -> Bool
-isHsValArg (HsEValArg {}) = True
-isHsValArg _              = False
-
-isArgPar :: HsExprArg id -> Bool
-isArgPar (HsEPar {}) = True
-isArgPar _           = False
-
-getFunLoc :: [HsExprArg 'Renamed] -> Maybe SrcSpan
-getFunLoc []    = Nothing
-getFunLoc (a:_) = Just $ case a of
-                           HsEValArg l _    -> l
-                           HsETypeArg l _ _ -> l
-                           HsEPrag l _      -> l
-                           HsEPar l         -> l
-
----------------------------
-tcApp :: HsExpr GhcRn  -- either HsApp or HsAppType
-       -> ExpRhoType -> TcM (HsExpr GhcTc)
--- See Note [Typechecking applications]
-tcApp expr res_ty
-  = do { (fun, args, app_res_ty) <- tcInferApp expr
-       ; if isTagToEnum fun
-         then tcTagToEnum expr fun args app_res_ty res_ty
-              -- Done here because we have res_ty,
-              -- whereas tcInferApp does not
-         else
-
-    -- The wildly common case
-    do { let expr' = applyHsArgs fun args
-       ; addFunResCtxt True fun app_res_ty res_ty $
-         tcWrapResult expr expr' app_res_ty res_ty } }
-
----------------------------
-tcInferApp :: HsExpr GhcRn
-           -> TcM ( HsExpr GhcTc    -- Function
-                  , [LHsExprArgOut]  -- Arguments
-                  , TcSigmaType)     -- Inferred type: a sigma-type!
--- Also used by Module.tcRnExpr to implement GHCi :type
-tcInferApp expr
-  | -- Gruesome special case for ambiguous record selectors
-    HsRecFld _ fld_lbl        <- fun
-  , Ambiguous _ lbl           <- fld_lbl  -- Still ambiguous
-  , HsEValArg _ (L _ arg) : _ <- filterOut isArgPar args -- A value arg is first
-  , Just sig_ty               <- obviousSig arg  -- A type sig on the arg disambiguates
-  = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
-       ; sel_name  <- disambiguateSelector lbl sig_tc_ty
-       ; (tc_fun, fun_ty) <- tcInferRecSelId (Unambiguous sel_name lbl)
-       ; tcInferApp_finish fun tc_fun fun_ty args }
-
-  | otherwise  -- The wildly common case
-  = do { (tc_fun, fun_ty) <- set_fun_loc (tcInferAppHead fun)
-       ; tcInferApp_finish fun tc_fun fun_ty args }
-  where
-    (fun, args) = collectHsArgs expr
-    set_fun_loc thing_inside
-      = case getFunLoc args of
-          Nothing  -> thing_inside  -- Don't set the location twice
-          Just loc -> setSrcSpan loc thing_inside
-
-tcInferApp_finish
-    :: HsExpr GhcRn                 -- Renamed function
-    -> HsExpr GhcTc -> TcSigmaType  -- Function and its type
-    -> [LHsExprArgIn]               -- Arguments
-    -> TcM (HsExpr GhcTc, [LHsExprArgOut], TcSigmaType)
-tcInferApp_finish rn_fun tc_fun fun_sigma rn_args
-  = do { (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args
-       ; return (tc_fun, tc_args, actual_res_ty) }
-
-mk_op_msg :: LHsExpr GhcRn -> SDoc
-mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
-
-----------------
-tcInferAppHead :: HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType)
--- Infer type of the head of an application, returning a /SigmaType/
---   i.e. the 'f' in (f e1 ... en)
--- We get back a SigmaType because we have special cases for
---   * A bare identifier (just look it up)
---     This case also covers a record selectro HsRecFld
---   * An expression with a type signature (e :: ty)
---
--- Note that [] and (,,) are both HsVar:
---   see Note [Empty lists] and [ExplicitTuple] in GHC.Hs.Expr
---
--- NB: 'e' cannot be HsApp, HsTyApp, HsPrag, HsPar, because those
---     cases are dealt with by collectHsArgs.
---
--- See Note [Typechecking applications]
-tcInferAppHead e
-  = case e of
-      HsVar _ (L _ nm)        -> tcInferId nm
-      HsRecFld _ f            -> tcInferRecSelId f
-      ExprWithTySig _ e hs_ty -> add_ctxt $ tcExprWithSig e hs_ty
-      _                       -> add_ctxt $ tcInfer (tcExpr e)
-  where
-    add_ctxt thing = addErrCtxt (exprCtxt e) thing
-
-----------------
--- | Type-check the arguments to a function, possibly including visible type
--- applications
-tcArgs :: HsExpr GhcRn   -- ^ The function itself (for err msgs only)
-       -> TcSigmaType    -- ^ the (uninstantiated) type of the function
-       -> [LHsExprArgIn] -- ^ the args
-       -> TcM ([LHsExprArgOut], TcSigmaType)
-          -- ^ (a wrapper for the function, the tc'd args, result type)
-tcArgs fun orig_fun_ty orig_args
-  = go 1 [] orig_fun_ty orig_args
-  where
-    fun_orig = exprCtOrigin fun
-    herald = sep [ text "The function" <+> quotes (ppr fun)
-                 , text "is applied to"]
-
-    -- Count value args only when complaining about a function
-    -- applied to too many value args
-    -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
-    n_val_args = count isHsValArg orig_args
-
-    fun_is_out_of_scope  -- See Note [VTA for out-of-scope functions]
-      = case fun of
-          HsUnboundVar {} -> True
-          _               -> False
-
-    go :: Int           -- Which argment number this is (incl type args)
-       -> [Scaled TcSigmaType] -- Value args to which applied so far
-       -> TcSigmaType
-       -> [LHsExprArgIn] -> TcM ([LHsExprArgOut], TcSigmaType)
-    go _ _ fun_ty [] = traceTc "tcArgs:ret" (ppr fun_ty) >> return ([], fun_ty)
-
-    go n so_far fun_ty (HsEPar sp : args)
-      = do { (args', res_ty) <- go n so_far fun_ty args
-           ; return (HsEPar sp : args', res_ty) }
-
-    go n so_far fun_ty (HsEPrag sp prag : args)
-      = do { (args', res_ty) <- go n so_far fun_ty args
-           ; return (HsEPrag sp (tcExprPrag prag) : args', res_ty) }
-
-    go n so_far fun_ty (HsETypeArg loc hs_ty_arg _ : args)
-      | fun_is_out_of_scope   -- See Note [VTA for out-of-scope functions]
-      = go (n+1) so_far fun_ty args
-
-      | otherwise
-      = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty
-               -- wrap1 :: fun_ty "->" upsilon_ty
-           ; case tcSplitForAllTy_maybe upsilon_ty of
-               Just (tvb, inner_ty)
-                 | binderArgFlag tvb == Specified ->
-                   -- It really can't be Inferred, because we've justn
-                   -- instantiated those. But, oddly, it might just be Required.
-                   -- See Note [Required quantifiers in the type of a term]
-                 do { let tv   = binderVar tvb
-                          kind = tyVarKind tv
-                    ; ty_arg <- tcHsTypeApp hs_ty_arg kind
-
-                    ; inner_ty <- zonkTcType inner_ty
-                          -- See Note [Visible type application zonk]
-                    ; let in_scope  = mkInScopeSet (tyCoVarsOfTypes [upsilon_ty, ty_arg])
-                          insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
-                                      -- NB: tv and ty_arg have the same kind, so this
-                                      --     substitution is kind-respecting
-                    ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
-                                          , debugPprType ty_arg
-                                          , debugPprType (tcTypeKind ty_arg)
-                                          , debugPprType inner_ty
-                                          , debugPprType insted_ty ])
-
-                    ; (args', res_ty) <- go (n+1) so_far insted_ty args
-                    ; return ( addArgWrap wrap1 $ HsETypeArg loc hs_ty_arg ty_arg : args'
-                             , res_ty ) }
-               _ -> ty_app_err upsilon_ty hs_ty_arg }
-
-    go n so_far fun_ty (HsEValArg loc arg : args)
-      = do { (wrap, arg_ty, res_ty)
-               <- matchActualFunTySigma herald fun_orig (Just fun)
-                                        (n_val_args, so_far) fun_ty
-           ; arg' <- tcArg fun arg arg_ty n
-           ; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args
-           ; return ( addArgWrap wrap $ HsEValArg loc arg' : args'
-                    , inner_res_ty ) }
-
-    ty_app_err ty arg
-      = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty
-           ; failWith $
-               text "Cannot apply expression of type" <+> quotes (ppr ty) $$
-               text "to a visible type argument" <+> quotes (ppr arg) }
-
-{- Note [Required quantifiers in the type of a term]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#15859)
-
-  data A k :: k -> Type      -- A      :: forall k -> k -> Type
-  type KindOf (a :: k) = k   -- KindOf :: forall k. k -> Type
-  a = (undefind :: KindOf A) @Int
-
-With ImpredicativeTypes (thin ice, I know), we instantiate
-KindOf at type (forall k -> k -> Type), so
-  KindOf A = forall k -> k -> Type
-whose first argument is Required
-
-We want to reject this type application to Int, but in earlier
-GHCs we had an ASSERT that Required could not occur here.
-
-The ice is thin; c.f. Note [No Required TyCoBinder in terms]
-in GHC.Core.TyCo.Rep.
-
-Note [VTA for out-of-scope functions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose 'wurble' is not in scope, and we have
-   (wurble @Int @Bool True 'x')
-
-Then the renamer will make (HsUnboundVar "wurble) for 'wurble',
-and the typechecker will typecheck it with tcUnboundId, giving it
-a type 'alpha', and emitting a deferred Hole, to be reported later.
-
-But then comes the visible type application. If we do nothing, we'll
-generate an immediate failure (in tc_app_err), saying that a function
-of type 'alpha' can't be applied to Bool.  That's insane!  And indeed
-users complain bitterly (#13834, #17150.)
-
-The right error is the Hole, which has /already/ been emitted by
-tcUnboundId.  It later reports 'wurble' as out of scope, and tries to
-give its type.
-
-Fortunately in tcArgs we still have access to the function, so we can
-check if it is a HsUnboundVar.  We use this info to simply skip over
-any visible type arguments.  We've already inferred the type of the
-function, so we'll /already/ have emitted a Hole;
-failing preserves that constraint.
-
-We do /not/ want to fail altogether in this case (via failM) becuase
-that may abandon an entire instance decl, which (in the presence of
--fdefer-type-errors) leads to leading to #17792.
-
-Downside; the typechecked term has lost its visible type arguments; we
-don't even kind-check them.  But let's jump that bridge if we come to
-it.  Meanwhile, let's not crash!
-
-Note [Visible type application zonk]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
-
-* tcHsTypeApp only guarantees that
-    - ty_arg is zonked
-    - kind(zonk(tv)) = kind(ty_arg)
-  (checkExpectedKind zonks as it goes).
-
-So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
-and inner_ty.  Otherwise we can build an ill-kinded type.  An example was
-#14158, where we had:
-   id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
-and we had the visible type application
-  id @(->)
-
-* We instantiated k := kappa, yielding
-    forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
-* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
-* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
-  Here q1 :: RuntimeRep
-* Now we substitute
-     cat  :->  (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
-  but we must first zonk the inner_ty to get
-      forall (a :: TYPE q1). cat a a
-  so that the result of substitution is well-kinded
-  Failing to do so led to #14158.
--}
-
-----------------
-tcArg :: HsExpr GhcRn                   -- The function (for error messages)
-      -> LHsExpr GhcRn                   -- Actual arguments
-      -> Scaled TcSigmaType              -- expected arg type
-      -> Int                             -- # of argument
-      -> TcM (LHsExpr GhcTc)           -- Resulting argument
-tcArg fun arg (Scaled mult ty) arg_no
-   = addErrCtxt (funAppCtxt fun arg arg_no) $
-     do { traceTc "tcArg" $
-          vcat [ ppr arg_no <+> text "of" <+> ppr fun
-               , text "arg type:" <+> ppr ty
-               , text "arg:" <+> ppr arg ]
-        ; tcScalingUsage mult $ tcCheckPolyExprNC arg ty }
-
 ----------------
 tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc]
 tcTupArgs args tys
   = ASSERT( equalLength args tys ) mapM go (args `zip` tys)
   where
-    go (L l (Missing {}),   arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy
-                                         ; return (L l (Missing (Scaled mult arg_ty))) }
+    go (L l (Missing {}),     arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy
+                                           ; return (L l (Missing (Scaled mult arg_ty))) }
     go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty
                                            ; return (L l (Present x expr')) }
 
@@ -1570,7 +1051,7 @@ tcSyntaxOp :: CtOrigin
            -> TcM (a, SyntaxExprTc)
 -- ^ Typecheck a syntax operator
 -- The operator is a variable or a lambda at this stage (i.e. renamer
--- output)
+-- output)t
 tcSyntaxOp orig expr arg_tys res_ty
   = tcSyntaxOpGen orig expr arg_tys (SynType res_ty)
 
@@ -1583,7 +1064,9 @@ tcSyntaxOpGen :: CtOrigin
               -> ([TcSigmaType] -> [Mult] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside
-  = do { (expr, sigma) <- tcInferAppHead op
+  = do { (expr, sigma) <- tcInferAppHead op [] Nothing
+             -- Nothing here might be improved, but all this
+             -- code is scheduled for demolition anyway
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
        ; (result, expr_wrap, arg_wraps, res_wrap)
            <- tcSynArgA orig sigma arg_tys res_ty $
@@ -1756,497 +1239,14 @@ Here's an example where it actually makes a real difference
 With the change, f1 will type-check, because the 'Char' info from
 the signature is propagated into MkQ's argument. With the check
 in the other order, the extra signature in f2 is reqd.
-
-************************************************************************
-*                                                                      *
-                Expressions with a type signature
-                        expr :: type
-*                                                                      *
-********************************************************************* -}
-
-tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
-tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
-  = setSrcSpan loc $   -- Sets the location for the implication constraint
-    do { let poly_ty = idType poly_id
-       ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
-                          tcCheckMonoExprNC expr rho_ty
-       ; return (mkLHsWrap wrap expr', poly_ty) }
-
-tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
-  = setSrcSpan loc $   -- Sets the location for the implication constraint
-    do { (tclvl, wanted, (expr', sig_inst))
-             <- pushLevelAndCaptureConstraints  $
-                do { sig_inst <- tcInstSig sig
-                   ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
-                              tcExtendNameTyVarEnv (sig_inst_wcs   sig_inst) $
-                              tcCheckPolyExprNC expr (sig_inst_tau sig_inst)
-                   ; return (expr', sig_inst) }
-       -- See Note [Partial expression signatures]
-       ; let tau = sig_inst_tau sig_inst
-             infer_mode | null (sig_inst_theta sig_inst)
-                        , isNothing (sig_inst_wcx sig_inst)
-                        = ApplyMR
-                        | otherwise
-                        = NoRestrictions
-       ; (qtvs, givens, ev_binds, residual, _)
-                 <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
-       ; emitConstraints residual
-
-       ; tau <- zonkTcType tau
-       ; let inferred_theta = map evVarPred givens
-             tau_tvs        = tyCoVarsOfType tau
-       ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
-                                   tau_tvs qtvs (Just sig_inst)
-       ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
-             my_sigma       = mkInvisForAllTys binders (mkPhiTy  my_theta tau)
-       ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
-                 then return idHsWrapper  -- Fast path; also avoids complaint when we infer
-                                          -- an ambiguous type and have AllowAmbiguousType
-                                          -- e..g infer  x :: forall a. F a -> Int
-                 else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
-
-       ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
-       ; let poly_wrap = wrap
-                         <.> mkWpTyLams qtvs
-                         <.> mkWpLams givens
-                         <.> mkWpLet  ev_binds
-       ; return (mkLHsWrap poly_wrap expr', my_sigma) }
-
-
-{- Note [Partial expression signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Partial type signatures on expressions are easy to get wrong.  But
-here is a guiding principile
-    e :: ty
-should behave like
-    let x :: ty
-        x = e
-    in x
-
-So for partial signatures we apply the MR if no context is given.  So
-   e :: IO _          apply the MR
-   e :: _ => IO _     do not apply the MR
-just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan
-
-This makes a difference (#11670):
-   peek :: Ptr a -> IO CLong
-   peek ptr = peekElemOff undefined 0 :: _
-from (peekElemOff undefined 0) we get
-          type: IO w
-   constraints: Storable w
-
-We must NOT try to generalise over 'w' because the signature specifies
-no constraints so we'll complain about not being able to solve
-Storable w.  Instead, don't generalise; then _ gets instantiated to
-CLong, as it should.
 -}
 
 {- *********************************************************************
 *                                                                      *
-                 tcInferId
+                 Record bindings
 *                                                                      *
 ********************************************************************* -}
 
-tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
-tcCheckId name res_ty
-  | name `hasKey` tagToEnumKey
-  = failWithTc (text "tagToEnum# must appear applied to one argument")
-    -- tcApp catches the case (tagToEnum# arg)
-
-  | otherwise
-  = do { (expr, actual_res_ty) <- tcInferId name
-       ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
-       ; addFunResCtxt False expr actual_res_ty res_ty $
-         tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
-                                           actual_res_ty res_ty }
-
-tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-tcCheckRecSelId rn_expr f@(Unambiguous {}) res_ty
-  = do { (expr, actual_res_ty) <- tcInferRecSelId f
-       ; tcWrapResult rn_expr expr actual_res_ty res_ty }
-tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty
-  = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of
-      Nothing       -> ambiguousSelector lbl
-      Just (arg, _) -> do { sel_name <- disambiguateSelector lbl (scaledThing arg)
-                          ; tcCheckRecSelId rn_expr (Unambiguous sel_name lbl)
-                                                    res_ty }
-
-------------------------
-tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> TcM (HsExpr GhcTc, TcRhoType)
-tcInferRecSelId (Unambiguous sel (L _ lbl))
-  = do { (expr', ty) <- tc_infer_id lbl sel
-       ; return (expr', ty) }
-tcInferRecSelId (Ambiguous _ lbl)
-  = ambiguousSelector lbl
-
-------------------------
-tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
--- Look up an occurrence of an Id
--- Do not instantiate its type
-tcInferId id_name
-  | id_name `hasKey` assertIdKey
-  = do { dflags <- getDynFlags
-       ; if gopt Opt_IgnoreAsserts dflags
-         then tc_infer_id (nameRdrName id_name) id_name
-         else tc_infer_assert id_name }
-
-  | otherwise
-  = do { (expr, ty) <- tc_infer_id (nameRdrName id_name) id_name
-       ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty)
-       ; return (expr, ty) }
-
-tc_infer_assert :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
--- Deal with an occurrence of 'assert'
--- See Note [Adding the implicit parameter to 'assert']
-tc_infer_assert assert_name
-  = do { assert_error_id <- tcLookupId assertErrorName
-       ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name)
-                                          (idType assert_error_id)
-       ; return (mkHsWrap wrap (HsVar noExtField (noLoc assert_error_id)), id_rho)
-       }
-
-tc_infer_id :: RdrName -> Name -> TcM (HsExpr GhcTc, TcSigmaType)
-tc_infer_id lbl id_name
- = do { thing <- tcLookup id_name
-      ; case thing of
-             ATcId { tct_id = id }
-               -> do { check_naughty id        -- Note [Local record selectors]
-                     ; checkThLocalId id
-                     ; tcEmitBindingUsage $ unitUE id_name One
-                     ; return_id id }
-
-             AGlobal (AnId id)
-               -> do { check_naughty id
-                     ; return_id id }
-                    -- A global cannot possibly be ill-staged
-                    -- nor does it need the 'lifting' treatment
-                    -- hence no checkTh stuff here
-
-             AGlobal (AConLike cl) -> case cl of
-                 RealDataCon con -> return_data_con con
-                 PatSynCon ps    -> tcPatSynBuilderOcc ps
-
-             _ -> failWithTc $
-                  ppr thing <+> text "used where a value identifier was expected" }
-  where
-    return_id id = return (HsVar noExtField (noLoc id), idType id)
-
-    return_data_con con
-      = do { let tvs = dataConUserTyVarBinders con
-                 theta = dataConOtherTheta con
-                 args = dataConOrigArgTys con
-                 res = dataConOrigResTy con
-
-           -- See Note [Linear fields generalization]
-           ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy
-           ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args'
-                 combine var (Scaled One ty) = Scaled var ty
-                 combine _   scaled_ty       = scaled_ty
-                   -- The combine function implements the fact that, as
-                   -- described in Note [Linear fields generalization], if a
-                   -- field is not linear (last line) it isn't made polymorphic.
-
-                 etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys
-
-           -- See Note [Instantiating stupid theta]
-           ; let shouldInstantiate = (not (null (dataConStupidTheta con)) ||
-                                      isKindLevPoly (tyConResKind (dataConTyCon con)))
-           ; case shouldInstantiate of
-               True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs)
-                           ; let tys'   = mkTyVarTys tvs'
-                                 theta' = substTheta subst theta
-                                 args'  = substScaledTys subst args
-                                 res'   = substTy subst res
-                           ; wrap <- instCall (OccurrenceOf id_name) tys' theta'
-                           ; let scaled_arg_tys = scaleArgs args'
-                                 eta_wrap = etaWrapper scaled_arg_tys
-                           ; addDataConStupidTheta con tys'
-                           ; return ( mkHsWrap (eta_wrap <.> wrap)
-                                               (HsConLikeOut noExtField (RealDataCon con))
-                                    , mkVisFunTys scaled_arg_tys res')
-                           }
-               False -> let scaled_arg_tys = scaleArgs args
-                            wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs)
-                            eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys)
-                            wrap2 = mkWpTyLams $ binderVars tvs
-                        in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1)
-                                             (HsConLikeOut noExtField (RealDataCon con))
-                                  , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res)
-           }
-
-    check_naughty id
-      | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
-      | otherwise                  = return ()
-
-
-tcUnboundId :: HsExpr GhcRn -> OccName -> ExpRhoType -> TcM (HsExpr GhcTc)
--- Typecheck an occurrence of an unbound Id
---
--- Some of these started life as a true expression hole "_".
--- Others might simply be variables that accidentally have no binding site
---
--- We turn all of them into HsVar, since HsUnboundVar can't contain an
--- Id; and indeed the evidence for the ExprHole does bind it, so it's
--- not unbound any more!
-tcUnboundId rn_expr occ res_ty
- = do { ty <- newOpenFlexiTyVarTy  -- Allow Int# etc (#12531)
-      ; name <- newSysName occ
-      ; let ev = mkLocalId name Many ty
-      ; emitNewExprHole occ ev ty
-      ; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr
-          (HsVar noExtField (noLoc ev)) ty res_ty }
-
-
-{-
-Note [Adding the implicit parameter to 'assert']
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The typechecker transforms (assert e1 e2) to (assertError e1 e2).
-This isn't really the Right Thing because there's no way to "undo"
-if you want to see the original source code in the typechecker
-output.  We'll have fix this in due course, when we care more about
-being able to reconstruct the exact original program.
-
-Note [tagToEnum#]
-~~~~~~~~~~~~~~~~~
-Nasty check to ensure that tagToEnum# is applied to a type that is an
-enumeration TyCon.  Unification may refine the type later, but this
-check won't see that, alas.  It's crude, because it relies on our
-knowing *now* that the type is ok, which in turn relies on the
-eager-unification part of the type checker pushing enough information
-here.  In theory the Right Thing to do is to have a new form of
-constraint but I definitely cannot face that!  And it works ok as-is.
-
-Here's are two cases that should fail
-        f :: forall a. a
-        f = tagToEnum# 0        -- Can't do tagToEnum# at a type variable
-
-        g :: Int
-        g = tagToEnum# 0        -- Int is not an enumeration
-
-When data type families are involved it's a bit more complicated.
-     data family F a
-     data instance F [Int] = A | B | C
-Then we want to generate something like
-     tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
-Usually that coercion is hidden inside the wrappers for
-constructors of F [Int] but here we have to do it explicitly.
-
-It's all grotesquely complicated.
-
-Note [Instantiating stupid theta]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Normally, when we infer the type of an Id, we don't instantiate,
-because we wish to allow for visible type application later on.
-But if a datacon has a stupid theta, we're a bit stuck. We need
-to emit the stupid theta constraints with instantiated types. It's
-difficult to defer this to the lazy instantiation, because a stupid
-theta has no spot to put it in a type. So we just instantiate eagerly
-in this case. Thus, users cannot use visible type application with
-a data constructor sporting a stupid theta. I won't feel so bad for
-the users that complain.
-
-Note [Linear fields generalization]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As per Note [Polymorphisation of linear fields], linear field of data
-constructors get a polymorphic type when the data constructor is used as a term.
-
-    Just :: forall {p} a. a #p-> Maybe a
-
-This rule is known only to the typechecker: Just keeps its linear type in Core.
-
-In order to desugar this generalised typing rule, we simply eta-expand:
-
-    \a (x # p :: a) -> Just @a x
-
-has the appropriate type. We insert these eta-expansion with WpFun wrappers.
-
-A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
-certain newtypes with -XUnliftedNewtypes) then this strategy produces
-
-    \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
-
-Which has type
-
-    forall r1 r2 a b. a #p-> b #q-> (# a, b #)
-
-Which violates the levity-polymorphism restriction see Note [Levity polymorphism
-checking] in DsMonad.
-
-So we really must instantiate r1 and r2 rather than quantify over them.  For
-simplicity, we just instantiate the entire type, as described in Note
-[Instantiating stupid theta]. It breaks visible type application with unboxed
-tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
-anywhere.
-
-A better plan: let's force all representation variable to be *inferred*, so that
-they are not subject to visible type applications. Then we can instantiate
-inferred argument eagerly.
--}
-
-isTagToEnum :: HsExpr GhcTc -> Bool
-isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
-isTagToEnum _ = False
-
-tcTagToEnum :: HsExpr GhcRn -> HsExpr GhcTc -> [LHsExprArgOut]
-            -> TcSigmaType -> ExpRhoType
-            -> TcM (HsExpr GhcTc)
--- tagToEnum# :: forall a. Int# -> a
--- See Note [tagToEnum#]   Urgh!
-tcTagToEnum expr fun args app_res_ty res_ty
-  = do { res_ty <- readExpType res_ty
-       ; ty'    <- zonkTcType res_ty
-
-       -- Check that the type is algebraic
-       ; case tcSplitTyConApp_maybe ty' of {
-           Nothing -> do { addErrTc (mk_error ty' doc1)
-                         ; vanilla_result } ;
-           Just (tc, tc_args) ->
-
-    do { -- Look through any type family
-       ; fam_envs <- tcGetFamInstEnvs
-       ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
-           Nothing -> do { check_enumeration ty' tc
-                         ; vanilla_result } ;
-           Just (rep_tc, rep_args, coi) ->
-
-    do { -- coi :: tc tc_args ~R rep_tc rep_args
-         check_enumeration ty' rep_tc
-       ; let val_arg = dropWhile (not . isHsValArg) args
-             rep_ty  = mkTyConApp rep_tc rep_args
-             fun'    = mkHsWrap (WpTyApp rep_ty) fun
-             expr'   = applyHsArgs fun' val_arg
-             df_wrap = mkWpCastR (mkTcSymCo coi)
-       ; return (mkHsWrap df_wrap expr') }}}}}
-
-  where
-    vanilla_result
-      = do { let expr' = applyHsArgs fun args
-           ; tcWrapResult expr expr' app_res_ty res_ty }
-
-    check_enumeration ty' tc
-      | isEnumerationTyCon tc = return ()
-      | otherwise             = addErrTc (mk_error ty' doc2)
-
-    doc1 = vcat [ text "Specify the type by giving a type signature"
-                , text "e.g. (tagToEnum# x) :: Bool" ]
-    doc2 = text "Result type must be an enumeration type"
-
-    mk_error :: TcType -> SDoc -> SDoc
-    mk_error ty what
-      = hang (text "Bad call to tagToEnum#"
-               <+> text "at type" <+> ppr ty)
-           2 what
-
-{-
-************************************************************************
-*                                                                      *
-                 Template Haskell checks
-*                                                                      *
-************************************************************************
--}
-
-checkThLocalId :: Id -> TcM ()
--- The renamer has already done checkWellStaged,
---   in 'GHC.Rename.Splice.checkThLocalName', so don't repeat that here.
--- Here we just add constraints fro cross-stage lifting
-checkThLocalId id
-  = do  { mb_local_use <- getStageAndBindLevel (idName id)
-        ; case mb_local_use of
-             Just (top_lvl, bind_lvl, use_stage)
-                | thLevel use_stage > bind_lvl
-                -> checkCrossStageLifting top_lvl id use_stage
-             _  -> return ()   -- Not a locally-bound thing, or
-                               -- no cross-stage link
-    }
-
---------------------------------------
-checkCrossStageLifting :: TopLevelFlag -> Id -> ThStage -> TcM ()
--- If we are inside typed brackets, and (use_lvl > bind_lvl)
--- we must check whether there's a cross-stage lift to do
--- Examples   \x -> [|| x ||]
---            [|| map ||]
---
--- This is similar to checkCrossStageLifting in GHC.Rename.Splice, but
--- this code is applied to *typed* brackets.
-
-checkCrossStageLifting top_lvl id (Brack _ (TcPending ps_var lie_var q))
-  | isTopLevel top_lvl
-  = when (isExternalName id_name) (keepAlive id_name)
-    -- See Note [Keeping things alive for Template Haskell] in GHC.Rename.Splice
-
-  | otherwise
-  =     -- Nested identifiers, such as 'x' in
-        -- E.g. \x -> [|| h x ||]
-        -- We must behave as if the reference to x was
-        --      h $(lift x)
-        -- We use 'x' itself as the splice proxy, used by
-        -- the desugarer to stitch it all back together.
-        -- If 'x' occurs many times we may get many identical
-        -- bindings of the same splice proxy, but that doesn't
-        -- matter, although it's a mite untidy.
-    do  { let id_ty = idType id
-        ; checkTc (isTauTy id_ty) (polySpliceErr id)
-               -- If x is polymorphic, its occurrence sites might
-               -- have different instantiations, so we can't use plain
-               -- 'x' as the splice proxy name.  I don't know how to
-               -- solve this, and it's probably unimportant, so I'm
-               -- just going to flag an error for now
-
-        ; lift <- if isStringTy id_ty then
-                     do { sid <- tcLookupId GHC.Builtin.Names.TH.liftStringName
-                                     -- See Note [Lifting strings]
-                        ; return (HsVar noExtField (noLoc sid)) }
-                  else
-                     setConstraintVar lie_var   $
-                          -- Put the 'lift' constraint into the right LIE
-                     newMethodFromName (OccurrenceOf id_name)
-                                       GHC.Builtin.Names.TH.liftName
-                                       [getRuntimeRep id_ty, id_ty]
-
-                   -- Update the pending splices
-        ; ps <- readMutVar ps_var
-        ; let pending_splice = PendingTcSplice id_name
-                                 (nlHsApp (mkLHsWrap (applyQuoteWrapper q) (noLoc lift))
-                                          (nlHsVar id))
-        ; writeMutVar ps_var (pending_splice : ps)
-
-        ; return () }
-  where
-    id_name = idName id
-
-checkCrossStageLifting _ _ _ = return ()
-
-polySpliceErr :: Id -> SDoc
-polySpliceErr id
-  = text "Can't splice the polymorphic local variable" <+> quotes (ppr id)
-
-{-
-Note [Lifting strings]
-~~~~~~~~~~~~~~~~~~~~~~
-If we see $(... [| s |] ...) where s::String, we don't want to
-generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc.
-So this conditional short-circuits the lifting mechanism to generate
-(liftString "xy") in that case.  I didn't want to use overlapping instances
-for the Lift class in TH.Syntax, because that can lead to overlapping-instance
-errors in a polymorphic situation.
-
-If this check fails (which isn't impossible) we get another chance; see
-Note [Converting strings] in "GHC.ThToHs"
-
-Local record selectors
-~~~~~~~~~~~~~~~~~~~~~~
-Record selectors for TyCons in this module are ordinary local bindings,
-which show up as ATcIds rather than AGlobals.  So we need to check for
-naughtiness in both branches.  c.f. TcTyClsBindings.mkAuxBinds.
-
-
-************************************************************************
-*                                                                      *
-\subsection{Record bindings}
-*                                                                      *
-************************************************************************
--}
-
 getFixedTyVars :: [FieldLabelString] -> [TyVar] -> [ConLike] -> TyVarSet
 -- These tyvars must not change across the updates
 getFixedTyVars upd_fld_occs univ_tvs cons
@@ -2271,129 +1271,9 @@ getFixedTyVars upd_fld_occs univ_tvs cons
                       , (tv1,tv) <- univ_tvs `zip` u_tvs
                       , tv `elemVarSet` fixed_tvs ]
 
-{-
-Note [Disambiguating record fields]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When the -XDuplicateRecordFields extension is used, and the renamer
-encounters a record selector or update that it cannot immediately
-disambiguate (because it involves fields that belong to multiple
-datatypes), it will defer resolution of the ambiguity to the
-typechecker.  In this case, the `Ambiguous` constructor of
-`AmbiguousFieldOcc` is used.
-
-Consider the following definitions:
-
-        data S = MkS { foo :: Int }
-        data T = MkT { foo :: Int, bar :: Int }
-        data U = MkU { bar :: Int, baz :: Int }
-
-When the renamer sees `foo` as a selector or an update, it will not
-know which parent datatype is in use.
-
-For selectors, there are two possible ways to disambiguate:
-
-1. Check if the pushed-in type is a function whose domain is a
-   datatype, for example:
-
-       f s = (foo :: S -> Int) s
-
-       g :: T -> Int
-       g = foo
-
-    This is checked by `tcCheckRecSelId` when checking `HsRecFld foo`.
-
-2. Check if the selector is applied to an argument that has a type
-   signature, for example:
-
-       h = foo (s :: S)
-
-    This is checked by `tcApp`.
-
-
-Updates are slightly more complex.  The `disambiguateRecordBinds`
-function tries to determine the parent datatype in three ways:
-
-1. Check for types that have all the fields being updated. For example:
-
-        f x = x { foo = 3, bar = 2 }
-
-   Here `f` must be updating `T` because neither `S` nor `U` have
-   both fields. This may also discover that no possible type exists.
-   For example the following will be rejected:
-
-        f' x = x { foo = 3, baz = 3 }
-
-2. Use the type being pushed in, if it is already a TyConApp. The
-   following are valid updates to `T`:
-
-        g :: T -> T
-        g x = x { foo = 3 }
-
-        g' x = x { foo = 3 } :: T
-
-3. Use the type signature of the record expression, if it exists and
-   is a TyConApp. Thus this is valid update to `T`:
-
-        h x = (x :: T) { foo = 3 }
-
-
-Note that we do not look up the types of variables being updated, and
-no constraint-solving is performed, so for example the following will
-be rejected as ambiguous:
-
-     let bad (s :: S) = foo s
-
-     let r :: T
-         r = blah
-     in r { foo = 3 }
-
-     \r. (r { foo = 3 },  r :: T )
-
-We could add further tests, of a more heuristic nature. For example,
-rather than looking for an explicit signature, we could try to infer
-the type of the argument to a selector or the record expression being
-updated, in case we are lucky enough to get a TyConApp straight
-away. However, it might be hard for programmers to predict whether a
-particular update is sufficiently obvious for the signature to be
-omitted. Moreover, this might change the behaviour of typechecker in
-non-obvious ways.
-
-See also Note [HsRecField and HsRecUpdField] in GHC.Hs.Pat.
--}
-
--- Given a RdrName that refers to multiple record fields, and the type
--- of its argument, try to determine the name of the selector that is
--- meant.
-disambiguateSelector :: Located RdrName -> Type -> TcM Name
-disambiguateSelector lr@(L _ rdr) parent_type
- = do { fam_inst_envs <- tcGetFamInstEnvs
-      ; case tyConOf fam_inst_envs parent_type of
-          Nothing -> ambiguousSelector lr
-          Just p  ->
-            do { xs <- lookupParents rdr
-               ; let parent = RecSelData p
-               ; case lookup parent xs of
-                   Just gre -> do { addUsedGRE True gre
-                                  ; return (gre_name gre) }
-                   Nothing  -> failWithTc (fieldNotInType parent rdr) } }
-
--- This field name really is ambiguous, so add a suitable "ambiguous
--- occurrence" error, then give up.
-ambiguousSelector :: Located RdrName -> TcM a
-ambiguousSelector (L _ rdr)
-  = do { addAmbiguousNameErr rdr
-       ; failM }
-
--- | This name really is ambiguous, so add a suitable "ambiguous
--- occurrence" error, then continue
-addAmbiguousNameErr :: RdrName -> TcM ()
-addAmbiguousNameErr rdr
-  = do { env <- getGlobalRdrEnv
-       ; let gres = lookupGRE_RdrName rdr env
-       ; setErrCtxt [] $ addNameClashErrRn rdr gres}
 
 -- Disambiguate the fields in a record update.
--- See Note [Disambiguating record fields]
+-- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
 disambiguateRecordBinds :: LHsExpr GhcRn -> TcRhoType
                  -> [LHsRecUpdField GhcRn] -> ExpRhoType
                  -> TcM [LHsRecField' (AmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)]
@@ -2488,44 +1368,6 @@ disambiguateRecordBinds record_expr record_rho rbnds res_ty
                                   = L loc (Unambiguous i (L loc lbl)) } }
 
 
--- Extract the outermost TyCon of a type, if there is one; for
--- data families this is the representation tycon (because that's
--- where the fields live).
-tyConOf :: FamInstEnvs -> TcSigmaType -> Maybe TyCon
-tyConOf fam_inst_envs ty0
-  = case tcSplitTyConApp_maybe ty of
-      Just (tc, tys) -> Just (fstOf3 (tcLookupDataFamInst fam_inst_envs tc tys))
-      Nothing        -> Nothing
-  where
-    (_, _, ty) = tcSplitSigmaTy ty0
-
--- Variant of tyConOf that works for ExpTypes
-tyConOfET :: FamInstEnvs -> ExpRhoType -> Maybe TyCon
-tyConOfET fam_inst_envs ty0 = tyConOf fam_inst_envs =<< checkingExpType_maybe ty0
-
--- For an ambiguous record field, find all the candidate record
--- selectors (as GlobalRdrElts) and their parents.
-lookupParents :: RdrName -> RnM [(RecSelParent, GlobalRdrElt)]
-lookupParents rdr
-  = do { env <- getGlobalRdrEnv
-       ; let gres = lookupGRE_RdrName rdr env
-       ; mapM lookupParent gres }
-  where
-    lookupParent :: GlobalRdrElt -> RnM (RecSelParent, GlobalRdrElt)
-    lookupParent gre = do { id <- tcLookupId (gre_name gre)
-                          ; if isRecordSelector id
-                              then return (recordSelectorTyCon id, gre)
-                              else failWithTc (notSelector (gre_name gre)) }
-
--- A type signature on the argument of an ambiguous record selector or
--- the record expression in an update must be "obvious", i.e. the
--- outermost constructor ignoring parentheses.
-obviousSig :: HsExpr GhcRn -> Maybe (LHsSigWcType GhcRn)
-obviousSig (ExprWithTySig _ _ ty) = Just ty
-obviousSig (HsPar _ p)          = obviousSig (unLoc p)
-obviousSig _                    = Nothing
-
-
 {-
 Game plan for record bindings
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2538,7 +1380,7 @@ For each binding field = value
 3. Instantiate the field type (from the field label) using the type
    envt from step 2.
 
-4  Type check the value using tcArg, passing the field type as
+4  Type check the value using tcValArg, passing the field type as
    the expected argument type.
 
 This extends OK when the field types are universally quantified.
@@ -2678,103 +1520,8 @@ fieldCtxt :: FieldLabelString -> SDoc
 fieldCtxt field_name
   = text "In the" <+> quotes (ppr field_name) <+> ptext (sLit "field of a record")
 
-addExprCtxt :: LHsExpr GhcRn -> TcRn a -> TcRn a
-addExprCtxt e thing_inside = addErrCtxt (exprCtxt (unLoc e)) thing_inside
-
-exprCtxt :: HsExpr GhcRn -> SDoc
-exprCtxt expr = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr))
-
-addFunResCtxt :: Bool  -- There is at least one argument
-              -> HsExpr GhcTc -> TcType -> ExpRhoType
-              -> TcM a -> TcM a
--- When we have a mis-match in the return type of a function
--- try to give a helpful message about too many/few arguments
---
--- Used for naked variables too; but with has_args = False
-addFunResCtxt has_args fun fun_res_ty env_ty
-  = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg)
-      -- NB: use a landmark error context, so that an empty context
-      -- doesn't suppress some more useful context
-  where
-    mk_msg
-      = do { mb_env_ty <- readExpType_maybe env_ty
-                     -- by the time the message is rendered, the ExpType
-                     -- will be filled in (except if we're debugging)
-           ; fun_res' <- zonkTcType fun_res_ty
-           ; env'     <- case mb_env_ty of
-                           Just env_ty -> zonkTcType env_ty
-                           Nothing     ->
-                             do { dumping <- doptM Opt_D_dump_tc_trace
-                                ; MASSERT( dumping )
-                                ; newFlexiTyVarTy liftedTypeKind }
-           ; let -- See Note [Splitting nested sigma types in mismatched
-                 --           function types]
-                 (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res'
-                 -- No need to call tcSplitNestedSigmaTys here, since env_ty is
-                 -- an ExpRhoTy, i.e., it's already instantiated.
-                 (_, _, env_tau) = tcSplitSigmaTy env'
-                 (args_fun, res_fun) = tcSplitFunTys fun_tau
-                 (args_env, res_env) = tcSplitFunTys env_tau
-                 n_fun = length args_fun
-                 n_env = length args_env
-                 info  | n_fun == n_env = Outputable.empty
-                       | n_fun > n_env
-                       , not_fun res_env
-                       = text "Probable cause:" <+> quotes (ppr fun)
-                         <+> text "is applied to too few arguments"
-
-                       | has_args
-                       , not_fun res_fun
-                       = text "Possible cause:" <+> quotes (ppr fun)
-                         <+> text "is applied to too many arguments"
-
-                       | otherwise
-                       = Outputable.empty  -- Never suggest that a naked variable is                                         -- applied to too many args!
-           ; return info }
-      where
-        not_fun ty   -- ty is definitely not an arrow type,
-                     -- and cannot conceivably become one
-          = case tcSplitTyConApp_maybe ty of
-              Just (tc, _) -> isAlgTyCon tc
-              Nothing      -> False
-
-{-
-Note [Splitting nested sigma types in mismatched function types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When one applies a function to too few arguments, GHC tries to determine this
-fact if possible so that it may give a helpful error message. It accomplishes
-this by checking if the type of the applied function has more argument types
-than supplied arguments.
-
-Previously, GHC computed the number of argument types through tcSplitSigmaTy.
-This is incorrect in the face of nested foralls, however! This caused Trac
-#13311, for instance:
-
-  f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b
-
-If one uses `f` like so:
-
-  do { f; putChar 'a' }
-
-Then tcSplitSigmaTy will decompose the type of `f` into:
-
-  Tyvars: [a]
-  Context: (Monoid a)
-  Argument types: []
-  Return type: forall b. Monoid b => Maybe a -> Maybe b
-
-That is, it will conclude that there are *no* argument types, and since `f`
-was given no arguments, it won't print a helpful error message. On the other
-hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to:
-
-  Tyvars: [a, b]
-  Context: (Monoid a, Monoid b)
-  Argument types: [Maybe a]
-  Return type: Maybe b
-
-So now GHC recognizes that `f` has one more argument type than it was actually
-provided.
--}
+mk_op_msg :: LHsExpr GhcRn -> SDoc
+mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
 
 badFieldTypes :: [(FieldLabelString,TcType)] -> SDoc
 badFieldTypes prs
@@ -2818,7 +1565,7 @@ badFieldsUpd rbinds data_cons
     -- For each field, which constructors contain the field?
     membership :: [(FieldLabelString, [Bool])]
     membership = sortMembership $
-        map (\fld -> (fld, map (elementOfUniqSet fld) fieldLabelSets)) $
+        map (\fld -> (fld, map (fld `elementOfUniqSet`) fieldLabelSets)) $
           map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc . unLoc . hsRecFieldLbl . unLoc) rbinds
 
     fieldLabelSets :: [UniqSet FieldLabelString]
@@ -2858,16 +1605,6 @@ Finding the smallest subset is hard, so the code here makes
 a decent stab, no more.  See #7989.
 -}
 
-naughtyRecordSel :: RdrName -> SDoc
-naughtyRecordSel sel_id
-  = text "Cannot use record selector" <+> quotes (ppr sel_id) <+>
-    text "as a function due to escaped type variables" $$
-    text "Probable fix: use pattern-matching syntax instead"
-
-notSelector :: Name -> SDoc
-notSelector field
-  = hsep [quotes (ppr field), text "is not a record selector"]
-
 mixedSelectors :: [Id] -> [Id] -> SDoc
 mixedSelectors data_sels@(dc_rep_id:_) pat_syn_sels@(ps_rep_id:_)
   = ptext
@@ -2918,10 +1655,6 @@ noPossibleParents rbinds
 badOverloadedUpdate :: SDoc
 badOverloadedUpdate = text "Record update is ambiguous, and requires a type signature"
 
-fieldNotInType :: RecSelParent -> RdrName -> SDoc
-fieldNotInType p rdr
-  = unknownSubordinateErr (text "field of type" <+> quotes (ppr p)) rdr
-
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot
index 0676799b11..0a04b6d9e9 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs-boot
+++ b/compiler/GHC/Tc/Gen/Expr.hs-boot
@@ -1,13 +1,13 @@
 module GHC.Tc.Gen.Expr where
-import GHC.Types.Name
-import GHC.Hs              ( HsExpr, LHsExpr, SyntaxExprRn, SyntaxExprTc )
+import GHC.Hs              ( HsExpr, LHsExpr, SyntaxExprRn
+                           , SyntaxExprTc )
 import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType )
 import GHC.Tc.Types        ( TcM )
 import GHC.Tc.Types.Origin ( CtOrigin )
 import GHC.Core.Type ( Mult )
 import GHC.Hs.Extension    ( GhcRn, GhcTc )
 
-tcCheckPolyExpr ::
+tcCheckPolyExpr, tcCheckPolyExprNC ::
           LHsExpr GhcRn
        -> TcSigmaType
        -> TcM (LHsExpr GhcTc)
@@ -23,8 +23,6 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
 
 tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
 
-tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)
-
 tcInferRho, tcInferRhoNC ::
           LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
 
@@ -42,5 +40,3 @@ tcSyntaxOpGen :: CtOrigin
               -> ([TcSigmaType] -> [Mult] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 
-
-tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
new file mode 100644
index 0000000000..530f985a95
--- /dev/null
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -0,0 +1,1143 @@
+{-
+%
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+-}
+
+{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
+
+module GHC.Tc.Gen.Head
+       ( HsExprArg(..), EValArg(..), TcPass(..), Rebuilder
+       , splitHsApps
+       , addArgWrap, eValArgExpr, isHsValArg, setSrcSpanFromArgs
+       , countLeadingValArgs, isVisibleArg, pprHsExprArgTc, rebuildPrefixApps
+
+       , tcInferAppHead, tcInferAppHead_maybe
+       , tcInferId, tcCheckId
+       , obviousSig, addAmbiguousNameErr
+       , tyConOf, tyConOfET, lookupParents, fieldNotInType
+       , notSelector, nonBidirectionalErr
+
+       , addExprCtxt, addLExprCtxt, addFunResCtxt ) where
+
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC )
+
+import GHC.Tc.Gen.HsType
+import GHC.Tc.Gen.Pat
+import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )
+import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig )
+import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc )
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Unify
+import GHC.Types.Basic
+import GHC.Tc.Utils.Instantiate
+import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst )
+import GHC.Core.FamInstEnv    ( FamInstEnvs )
+import GHC.Core.UsageEnv      ( unitUE )
+import GHC.Rename.Env         ( addUsedGRE )
+import GHC.Rename.Utils       ( addNameClashErrRn, unknownSubordinateErr )
+import GHC.Tc.Solver          ( InferMode(..), simplifyInfer )
+import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.TcMType
+import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcType as TcType
+import GHC.Hs
+import GHC.Types.Id
+import GHC.Types.Id.Info
+import GHC.Core.ConLike
+import GHC.Core.DataCon
+import GHC.Types.Name
+import GHC.Types.Name.Reader
+import GHC.Core.TyCon
+import GHC.Core.TyCo.Rep
+import GHC.Core.Type
+import GHC.Tc.Types.Evidence
+import GHC.Builtin.Types( multiplicityTy )
+import GHC.Builtin.Names
+import GHC.Builtin.Names.TH( liftStringName, liftName )
+import GHC.Driver.Session
+import GHC.Types.SrcLoc
+import GHC.Utils.Misc
+import GHC.Data.Maybe
+import GHC.Utils.Outputable as Outputable
+import GHC.Utils.Panic
+import Control.Monad
+
+import Data.Function
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+
+{- *********************************************************************
+*                                                                      *
+              HsExprArg: auxiliary data type
+*                                                                      *
+********************************************************************* -}
+
+{- Note [HsExprArg]
+~~~~~~~~~~~~~~~~~~~
+The data type HsExprArg :: TcPass -> Type
+is a very local type, used only within this module and GHC.Tc.Gen.App
+
+* It's really a zipper for an application chain
+  See Note [Application chains and heads] in GHC.Tc.Gen.App for
+  what an "application chain" is.
+
+* It's a GHC-specific type, so using TTG only where necessary
+
+* It is indexed by TcPass, meaning
+  - HsExprArg TcpRn:
+      The result of splitHsApps, which decomposes a HsExpr GhcRn
+
+  - HsExprArg TcpInst:
+      The result of tcInstFun, which instantiates the function type
+      Adds EWrap nodes, the argument type in EValArg,
+      and the kind-checked type in ETypeArg
+
+  - HsExprArg TcpTc:
+      The result of tcArg, which typechecks the value args
+      In EValArg we now have a (LHsExpr GhcTc)
+
+* rebuildPrefixApps is dual to splitHsApps, and zips an application
+  back into a HsExpr
+
+Note [EValArg]
+~~~~~~~~~~~~~~
+The data type EValArg is the payload of the EValArg constructor of
+HsExprArg; i.e. a value argument of the application.  EValArg has two
+forms:
+
+* ValArg: payload is just the expression itself. Simple.
+
+* ValArgQL: captures the results of applying quickLookArg to the
+  argument in a ValArg.  When we later want to typecheck that argument
+  we can just carry on from where quick-look left off.  The fields of
+  ValArgQL exactly capture what is needed to complete the job.
+
+Invariants:
+
+1. With QL switched off, all arguments are ValArg; no ValArgQL
+
+2. With QL switched on, tcInstFun converts some ValArgs to ValArgQL,
+   under the conditions when quick-look should happen (eg the argument
+   type is guarded) -- see quickLookArg
+
+Note [splitHsApps and Rebuilder]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The key function
+  splitHsApps :: HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder)
+takes apart either an HsApp, or an infix OpApp, returning
+
+* The "head" of the application, an expression that is often a variable
+
+* A list of HsExprArg, the arguments
+
+* A Rebuilder function which reconstructs the original form, given the
+  head and arguments.  This allows us to reconstruct infix
+  applications (OpApp) as well as prefix applications (HsApp),
+  thereby retaining the structure of the original tree.
+-}
+
+data TcPass = TcpRn     -- Arguments decomposed
+            | TcpInst   -- Function instantiated
+            | TcpTc     -- Typechecked
+
+data HsExprArg (p :: TcPass)
+  = -- See Note [HsExprArg]
+    EValArg  { eva_loc    :: SrcSpan        -- Of the function
+             , eva_arg    :: EValArg p
+             , eva_arg_ty :: !(XEVAType p) }
+
+  | ETypeArg { eva_loc   :: SrcSpan          -- Of the function
+             , eva_hs_ty :: LHsWcType GhcRn  -- The type arg
+             , eva_ty    :: !(XETAType p) }  -- Kind-checked type arg
+
+  | EPrag    SrcSpan
+             (HsPragE (GhcPass (XPass p)))
+
+  | EPar     SrcSpan         -- Of the nested expr
+
+  | EWrap    !(XEWrap p)     -- Wrapper, after instantiation
+
+data EValArg (p :: TcPass) where  -- See Note [EValArg]
+  ValArg   :: LHsExpr (GhcPass (XPass p))
+           -> EValArg p
+  ValArgQL :: { va_expr :: LHsExpr GhcRn        -- Original expression
+                                                -- For location and error msgs
+              , va_fun  :: HsExpr GhcTc         -- Function, typechecked
+              , va_args :: [HsExprArg 'TcpInst] -- Args, instantiated
+              , va_ty   :: TcRhoType            -- Result type
+              , va_rebuild :: Rebuilder }       -- How to reassemble
+           -> EValArg 'TcpInst  -- Only exists in TcpInst phase
+
+type Rebuilder = HsExpr GhcTc -> [HsExprArg 'TcpTc]-> HsExpr GhcTc
+-- See Note [splitHsApps and Rebuilder]
+
+type family XPass p where
+  XPass 'TcpRn   = 'Renamed
+  XPass 'TcpInst = 'Renamed
+  XPass 'TcpTc   = 'Typechecked
+
+type family XETAType p where  -- Type arguments
+  XETAType 'TcpRn = NoExtField
+  XETAType _      = Type
+
+type family XEVAType p where  -- Value arguments
+  XEVAType 'TcpRn = NoExtField
+  XEVAType _      = Scaled Type
+
+type family XEWrap p where
+  XEWrap 'TcpRn = NoExtCon
+  XEWrap _      = HsWrapper
+
+mkEValArg :: SrcSpan -> LHsExpr GhcRn -> HsExprArg 'TcpRn
+mkEValArg l e = EValArg { eva_loc = l, eva_arg = ValArg e
+                        , eva_arg_ty = noExtField }
+
+mkETypeArg :: SrcSpan -> LHsWcType GhcRn -> HsExprArg 'TcpRn
+mkETypeArg l hs_ty = ETypeArg { eva_loc = l, eva_hs_ty = hs_ty
+                              , eva_ty = noExtField }
+
+eValArgExpr :: EValArg 'TcpInst -> LHsExpr GhcRn
+eValArgExpr (ValArg e)                 = e
+eValArgExpr (ValArgQL { va_expr = e }) = e
+
+addArgWrap :: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
+addArgWrap wrap args
+ | isIdHsWrapper wrap = args
+ | otherwise          = EWrap wrap : args
+
+splitHsApps :: HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder)
+-- See Note [splitHsApps and Rebuilder]
+splitHsApps e
+  = go e []
+  where
+    go (HsPar _     (L l fun))       args = go fun (EPar       l       : args)
+    go (HsPragE _ p (L l fun))       args = go fun (EPrag      l p     : args)
+    go (HsAppType _ (L l fun) hs_ty) args = go fun (mkETypeArg l hs_ty : args)
+    go (HsApp _     (L l fun) arg)   args = go fun (mkEValArg  l arg   : args)
+
+    go (OpApp fix arg1 (L l op) arg2) args
+      = (op, mkEValArg l arg1 : mkEValArg l arg2 : args, rebuild_infix fix)
+
+    go e args = (e, args, rebuildPrefixApps)
+
+    rebuild_infix :: Fixity -> Rebuilder
+    rebuild_infix fix fun args
+      = go fun args
+      where
+        go fun (EValArg { eva_arg = ValArg arg1, eva_loc = l } :
+                EValArg { eva_arg = ValArg arg2 } : args)
+                                   = rebuildPrefixApps (OpApp fix arg1 (L l fun) arg2) args
+        go fun (EWrap wrap : args) = go (mkHsWrap wrap fun) args
+        go fun args                = rebuildPrefixApps fun args
+           -- This last case fails to rebuild a OpApp, which is sad.
+           -- It can happen if we have (e1 `op` e2),
+           -- and op :: Int -> forall a. a -> Int, and e2 :: Bool
+           -- Then we'll get   [ e1, @Bool, e2 ]
+           -- Could be fixed with WpFun, but extra complexity.
+
+rebuildPrefixApps :: Rebuilder
+rebuildPrefixApps fun args
+  = go fun args
+  where
+    go fun [] = fun
+    go fun (EWrap wrap : args)               = go (mkHsWrap wrap fun) args
+    go fun (EValArg { eva_arg = ValArg arg
+                    , eva_loc = l } : args)  = go (HsApp noExtField (L l fun) arg) args
+    go fun (ETypeArg { eva_hs_ty = hs_ty
+                     , eva_ty  = ty
+                     , eva_loc = l } : args) = go (HsAppType ty (L l fun) hs_ty) args
+    go fun (EPar l : args)                   = go (HsPar noExtField (L l fun)) args
+    go fun (EPrag l p : args)                = go (HsPragE noExtField p (L l fun)) args
+
+isHsValArg :: HsExprArg id -> Bool
+isHsValArg (EValArg {}) = True
+isHsValArg _            = False
+
+countLeadingValArgs :: [HsExprArg id] -> Int
+countLeadingValArgs (EValArg {} : args) = 1 + countLeadingValArgs args
+countLeadingValArgs (EPar {}    : args) = countLeadingValArgs args
+countLeadingValArgs (EPrag {}   : args) = countLeadingValArgs args
+countLeadingValArgs _                   = 0
+
+isValArg :: HsExprArg id -> Bool
+isValArg (EValArg {}) = True
+isValArg _            = False
+
+isVisibleArg :: HsExprArg id -> Bool
+isVisibleArg (EValArg {})  = True
+isVisibleArg (ETypeArg {}) = True
+isVisibleArg _             = False
+
+setSrcSpanFromArgs :: [HsExprArg 'TcpRn] -> TcM a -> TcM a
+setSrcSpanFromArgs [] thing_inside
+  = thing_inside
+setSrcSpanFromArgs (arg:_) thing_inside
+  = setSrcSpan (argFunLoc arg) thing_inside
+
+argFunLoc :: HsExprArg 'TcpRn -> SrcSpan
+argFunLoc (EValArg { eva_loc = l }) = l
+argFunLoc (ETypeArg { eva_loc = l}) = l
+argFunLoc (EPrag l _)               = l
+argFunLoc (EPar l)                  = l
+
+instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
+  ppr (EValArg { eva_arg = arg })      = text "EValArg" <+> ppr arg
+  ppr (EPrag _ p)                      = text "EPrag" <+> ppr p
+  ppr (ETypeArg { eva_hs_ty = hs_ty }) = char '@' <> ppr hs_ty
+  ppr (EPar _)                         = text "EPar"
+  ppr (EWrap _)                        = text "EWrap"
+  -- ToDo: to print the wrapper properly we'll need to work harder
+  -- "Work harder" = replicate the ghcPass approach, but I didn't
+  -- think it was worth the effort to do so.
+
+instance OutputableBndrId (XPass p) => Outputable (EValArg p) where
+  ppr (ValArg e) = ppr e
+  ppr (ValArgQL { va_fun = fun, va_args = args, va_ty = ty})
+    = hang (text "ValArgQL" <+> ppr fun)
+         2 (vcat [ ppr args, text "va_ty:" <+> ppr ty ])
+
+pprHsExprArgTc :: HsExprArg 'TcpInst -> SDoc
+pprHsExprArgTc (EValArg { eva_arg = tm, eva_arg_ty = ty })
+  = text "EValArg" <+> hang (ppr tm) 2 (dcolon <+> ppr ty)
+pprHsExprArgTc arg = ppr arg
+
+
+{- *********************************************************************
+*                                                                      *
+                 tcInferAppHead
+*                                                                      *
+********************************************************************* -}
+
+tcInferAppHead :: HsExpr GhcRn
+               -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+               -- These two args are solely for tcInferRecSelId
+               -> TcM (HsExpr GhcTc, TcSigmaType)
+-- Infer type of the head of an application
+--   i.e. the 'f' in (f e1 ... en)
+-- See Note [Application chains and heads] in GHC.Tc.Gen.App
+-- We get back a /SigmaType/ because we have special cases for
+--   * A bare identifier (just look it up)
+--     This case also covers a record selectro HsRecFld
+--   * An expression with a type signature (e :: ty)
+-- See Note [Application chains and heads] in GHC.Tc.Gen.App
+--
+-- Why do we need the arguments to infer the type of the head of
+-- the application?  For two reasons:
+--   * (Legitimate) The first arg has the source location of the head
+--   * (Disgusting) Needed for record disambiguation; see tcInferRecSelId
+--
+-- Note that [] and (,,) are both HsVar:
+--   see Note [Empty lists] and [ExplicitTuple] in GHC.Hs.Expr
+--
+-- NB: 'e' cannot be HsApp, HsTyApp, HsPrag, HsPar, because those
+--     cases are dealt with by splitHsApps.
+--
+-- See Note [tcApp: typechecking applications] in GHC.Tc.Gen.App
+tcInferAppHead fun args mb_res_ty
+  = setSrcSpanFromArgs args $
+    do { mb_tc_fun <- tcInferAppHead_maybe fun args mb_res_ty
+       ; case mb_tc_fun of
+            Just (fun', fun_sigma) -> return (fun', fun_sigma)
+            Nothing -> add_head_ctxt fun args $
+                       tcInfer (tcExpr fun) }
+
+tcInferAppHead_maybe :: HsExpr GhcRn
+                     -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+                        -- These two args are solely for tcInferRecSelId
+                     -> TcM (Maybe (HsExpr GhcTc, TcSigmaType))
+-- See Note [Application chains and heads] in GHC.Tc.Gen.App
+-- Returns Nothing for a complicated head
+tcInferAppHead_maybe fun args mb_res_ty
+  = case fun of
+      HsVar _ (L _ nm)          -> Just <$> tcInferId nm
+      HsRecFld _ f              -> Just <$> tcInferRecSelId f args mb_res_ty
+      ExprWithTySig _ e hs_ty   -> add_head_ctxt fun args $
+                                   Just <$> tcExprWithSig e hs_ty
+      _                         -> return Nothing
+
+add_head_ctxt :: HsExpr GhcRn -> [HsExprArg 'TcpRn] -> TcM a -> TcM a
+-- Don't push an expression context if the arguments are empty,
+-- because it has already been pushed by tcExpr
+add_head_ctxt fun args thing_inside
+  | null args = thing_inside
+  | otherwise = addExprCtxt fun thing_inside
+
+
+{- *********************************************************************
+*                                                                      *
+                 Record selectors
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Disambiguating record fields]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When the -XDuplicateRecordFields extension is used, and the renamer
+encounters a record selector or update that it cannot immediately
+disambiguate (because it involves fields that belong to multiple
+datatypes), it will defer resolution of the ambiguity to the
+typechecker.  In this case, the `Ambiguous` constructor of
+`AmbiguousFieldOcc` is used.
+
+Consider the following definitions:
+
+        data S = MkS { foo :: Int }
+        data T = MkT { foo :: Int, bar :: Int }
+        data U = MkU { bar :: Int, baz :: Int }
+
+When the renamer sees `foo` as a selector or an update, it will not
+know which parent datatype is in use.
+
+For selectors, there are two possible ways to disambiguate:
+
+1. Check if the pushed-in type is a function whose domain is a
+   datatype, for example:
+
+       f s = (foo :: S -> Int) s
+
+       g :: T -> Int
+       g = foo
+
+    This is checked by `tcCheckRecSelId` when checking `HsRecFld foo`.
+
+2. Check if the selector is applied to an argument that has a type
+   signature, for example:
+
+       h = foo (s :: S)
+
+    This is checked by `tcInferRecSelId`.
+
+
+Updates are slightly more complex.  The `disambiguateRecordBinds`
+function tries to determine the parent datatype in three ways:
+
+1. Check for types that have all the fields being updated. For example:
+
+        f x = x { foo = 3, bar = 2 }
+
+   Here `f` must be updating `T` because neither `S` nor `U` have
+   both fields. This may also discover that no possible type exists.
+   For example the following will be rejected:
+
+        f' x = x { foo = 3, baz = 3 }
+
+2. Use the type being pushed in, if it is already a TyConApp. The
+   following are valid updates to `T`:
+
+        g :: T -> T
+        g x = x { foo = 3 }
+
+        g' x = x { foo = 3 } :: T
+
+3. Use the type signature of the record expression, if it exists and
+   is a TyConApp. Thus this is valid update to `T`:
+
+        h x = (x :: T) { foo = 3 }
+
+
+Note that we do not look up the types of variables being updated, and
+no constraint-solving is performed, so for example the following will
+be rejected as ambiguous:
+
+     let bad (s :: S) = foo s
+
+     let r :: T
+         r = blah
+     in r { foo = 3 }
+
+     \r. (r { foo = 3 },  r :: T )
+
+We could add further tests, of a more heuristic nature. For example,
+rather than looking for an explicit signature, we could try to infer
+the type of the argument to a selector or the record expression being
+updated, in case we are lucky enough to get a TyConApp straight
+away. However, it might be hard for programmers to predict whether a
+particular update is sufficiently obvious for the signature to be
+omitted. Moreover, this might change the behaviour of typechecker in
+non-obvious ways.
+
+See also Note [HsRecField and HsRecUpdField] in GHC.Hs.Pat.
+-}
+
+tcInferRecSelId :: AmbiguousFieldOcc GhcRn
+                -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+                -> TcM (HsExpr GhcTc, TcSigmaType)
+tcInferRecSelId (Unambiguous sel_name lbl) _args _mb_res_ty
+   = do { sel_id <- tc_rec_sel_id lbl sel_name
+        ; let expr = HsRecFld noExtField (Unambiguous sel_id lbl)
+        ; return (expr, idType sel_id) }
+
+tcInferRecSelId (Ambiguous _ lbl) args mb_res_ty
+   = do { sel_name <- tcInferAmbiguousRecSelId lbl args mb_res_ty
+        ; sel_id   <- tc_rec_sel_id lbl sel_name
+        ; let expr = HsRecFld noExtField (Ambiguous sel_id lbl)
+        ; return (expr, idType sel_id) }
+
+------------------------
+tc_rec_sel_id :: Located RdrName -> Name -> TcM TcId
+-- Like tc_infer_id, but returns an Id not a HsExpr,
+-- so we can wrap it back up into a HsRecFld
+tc_rec_sel_id lbl sel_name
+  = do { thing <- tcLookup sel_name
+       ; case thing of
+             ATcId { tct_id = id }
+               -> do { check_local_id occ id
+                     ; return id }
+
+             AGlobal (AnId id)
+               -> do { check_global_id occ id
+                     ; return id }
+                    -- A global cannot possibly be ill-staged
+                    -- nor does it need the 'lifting' treatment
+                    -- hence no checkTh stuff here
+
+             _ -> failWithTc $
+                  ppr thing <+> text "used where a value identifier was expected" }
+  where
+    occ = rdrNameOcc (unLoc lbl)
+
+------------------------
+tcInferAmbiguousRecSelId :: Located RdrName
+                         -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+                         -> TcM Name
+-- Disgusting special case for ambiguous record selectors
+-- Given a RdrName that refers to multiple record fields, and the type
+-- of its argument, try to determine the name of the selector that is
+-- meant.
+-- See Note [Disambiguating record fields]
+tcInferAmbiguousRecSelId lbl args mb_res_ty
+  | arg1 : _ <- dropWhile (not . isVisibleArg) args -- A value arg is first
+  , EValArg { eva_arg = ValArg (L _ arg) } <- arg1
+  , Just sig_ty <- obviousSig arg  -- A type sig on the arg disambiguates
+  = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
+       ; finish_ambiguous_selector lbl sig_tc_ty }
+
+  | Just res_ty <- mb_res_ty
+  , Just (arg_ty,_) <- tcSplitFunTy_maybe res_ty
+  = finish_ambiguous_selector lbl (scaledThing arg_ty)
+
+  | otherwise
+  = ambiguousSelector lbl
+
+finish_ambiguous_selector :: Located RdrName -> Type -> TcM Name
+finish_ambiguous_selector lr@(L _ rdr) parent_type
+ = do { fam_inst_envs <- tcGetFamInstEnvs
+      ; case tyConOf fam_inst_envs parent_type of {
+          Nothing -> ambiguousSelector lr ;
+          Just p  ->
+
+    do { xs <- lookupParents rdr
+       ; let parent = RecSelData p
+       ; case lookup parent xs of {
+           Nothing  -> failWithTc (fieldNotInType parent rdr) ;
+           Just gre ->
+
+    do { addUsedGRE True gre
+       ; return (gre_name gre) } } } } }
+
+-- This field name really is ambiguous, so add a suitable "ambiguous
+-- occurrence" error, then give up.
+ambiguousSelector :: Located RdrName -> TcM a
+ambiguousSelector (L _ rdr)
+  = do { addAmbiguousNameErr rdr
+       ; failM }
+
+-- | This name really is ambiguous, so add a suitable "ambiguous
+-- occurrence" error, then continue
+addAmbiguousNameErr :: RdrName -> TcM ()
+addAmbiguousNameErr rdr
+  = do { env <- getGlobalRdrEnv
+       ; let gres = lookupGRE_RdrName rdr env
+       ; setErrCtxt [] $ addNameClashErrRn rdr gres}
+
+-- A type signature on the argument of an ambiguous record selector or
+-- the record expression in an update must be "obvious", i.e. the
+-- outermost constructor ignoring parentheses.
+obviousSig :: HsExpr GhcRn -> Maybe (LHsSigWcType GhcRn)
+obviousSig (ExprWithTySig _ _ ty) = Just ty
+obviousSig (HsPar _ p)            = obviousSig (unLoc p)
+obviousSig (HsPragE _ _ p)        = obviousSig (unLoc p)
+obviousSig _                      = Nothing
+
+-- Extract the outermost TyCon of a type, if there is one; for
+-- data families this is the representation tycon (because that's
+-- where the fields live).
+tyConOf :: FamInstEnvs -> TcSigmaType -> Maybe TyCon
+tyConOf fam_inst_envs ty0
+  = case tcSplitTyConApp_maybe ty of
+      Just (tc, tys) -> Just (fstOf3 (tcLookupDataFamInst fam_inst_envs tc tys))
+      Nothing        -> Nothing
+  where
+    (_, _, ty) = tcSplitSigmaTy ty0
+
+-- Variant of tyConOf that works for ExpTypes
+tyConOfET :: FamInstEnvs -> ExpRhoType -> Maybe TyCon
+tyConOfET fam_inst_envs ty0 = tyConOf fam_inst_envs =<< checkingExpType_maybe ty0
+
+
+-- For an ambiguous record field, find all the candidate record
+-- selectors (as GlobalRdrElts) and their parents.
+lookupParents :: RdrName -> RnM [(RecSelParent, GlobalRdrElt)]
+lookupParents rdr
+  = do { env <- getGlobalRdrEnv
+       ; let gres = lookupGRE_RdrName rdr env
+       ; mapM lookupParent gres }
+  where
+    lookupParent :: GlobalRdrElt -> RnM (RecSelParent, GlobalRdrElt)
+    lookupParent gre = do { id <- tcLookupId (gre_name gre)
+                          ; if isRecordSelector id
+                              then return (recordSelectorTyCon id, gre)
+                              else failWithTc (notSelector (gre_name gre)) }
+
+
+fieldNotInType :: RecSelParent -> RdrName -> SDoc
+fieldNotInType p rdr
+  = unknownSubordinateErr (text "field of type" <+> quotes (ppr p)) rdr
+
+notSelector :: Name -> SDoc
+notSelector field
+  = hsep [quotes (ppr field), text "is not a record selector"]
+
+naughtyRecordSel :: OccName -> SDoc
+naughtyRecordSel lbl
+  = text "Cannot use record selector" <+> quotes (ppr lbl) <+>
+    text "as a function due to escaped type variables" $$
+    text "Probable fix: use pattern-matching syntax instead"
+
+
+{- *********************************************************************
+*                                                                      *
+                Expressions with a type signature
+                        expr :: type
+*                                                                      *
+********************************************************************* -}
+
+tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
+              -> TcM (HsExpr GhcTc, TcSigmaType)
+tcExprWithSig expr hs_ty
+  = do { sig_info <- checkNoErrs $  -- Avoid error cascade
+                     tcUserTypeSig loc hs_ty Nothing
+       ; (expr', poly_ty) <- tcExprSig expr sig_info
+       ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
+  where
+    loc = getLoc (hsSigWcType hs_ty)
+
+tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
+tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
+  = setSrcSpan loc $   -- Sets the location for the implication constraint
+    do { let poly_ty = idType poly_id
+       ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
+                          tcCheckMonoExprNC expr rho_ty
+       ; return (mkLHsWrap wrap expr', poly_ty) }
+
+tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
+  = setSrcSpan loc $   -- Sets the location for the implication constraint
+    do { (tclvl, wanted, (expr', sig_inst))
+             <- pushLevelAndCaptureConstraints  $
+                do { sig_inst <- tcInstSig sig
+                   ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
+                              tcExtendNameTyVarEnv (sig_inst_wcs   sig_inst) $
+                              tcCheckPolyExprNC expr (sig_inst_tau sig_inst)
+                   ; return (expr', sig_inst) }
+       -- See Note [Partial expression signatures]
+       ; let tau = sig_inst_tau sig_inst
+             infer_mode | null (sig_inst_theta sig_inst)
+                        , isNothing (sig_inst_wcx sig_inst)
+                        = ApplyMR
+                        | otherwise
+                        = NoRestrictions
+       ; (qtvs, givens, ev_binds, residual, _)
+                 <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
+       ; emitConstraints residual
+
+       ; tau <- zonkTcType tau
+       ; let inferred_theta = map evVarPred givens
+             tau_tvs        = tyCoVarsOfType tau
+       ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
+                                   tau_tvs qtvs (Just sig_inst)
+       ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
+             my_sigma       = mkInvisForAllTys binders (mkPhiTy  my_theta tau)
+       ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
+                 then return idHsWrapper  -- Fast path; also avoids complaint when we infer
+                                          -- an ambiguous type and have AllowAmbiguousType
+                                          -- e..g infer  x :: forall a. F a -> Int
+                 else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
+
+       ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
+       ; let poly_wrap = wrap
+                         <.> mkWpTyLams qtvs
+                         <.> mkWpLams givens
+                         <.> mkWpLet  ev_binds
+       ; return (mkLHsWrap poly_wrap expr', my_sigma) }
+
+
+{- Note [Partial expression signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Partial type signatures on expressions are easy to get wrong.  But
+here is a guiding principile
+    e :: ty
+should behave like
+    let x :: ty
+        x = e
+    in x
+
+So for partial signatures we apply the MR if no context is given.  So
+   e :: IO _          apply the MR
+   e :: _ => IO _     do not apply the MR
+just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan
+
+This makes a difference (#11670):
+   peek :: Ptr a -> IO CLong
+   peek ptr = peekElemOff undefined 0 :: _
+from (peekElemOff undefined 0) we get
+          type: IO w
+   constraints: Storable w
+
+We must NOT try to generalise over 'w' because the signature specifies
+no constraints so we'll complain about not being able to solve
+Storable w.  Instead, don't generalise; then _ gets instantiated to
+CLong, as it should.
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+                 tcInferId, tcCheckId
+*                                                                      *
+********************************************************************* -}
+
+tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcCheckId name res_ty
+  = do { (expr, actual_res_ty) <- tcInferId name
+       ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
+       ; addFunResCtxt expr [] actual_res_ty res_ty $
+         tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
+                                           actual_res_ty res_ty }
+
+------------------------
+tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
+-- Look up an occurrence of an Id
+-- Do not instantiate its type
+tcInferId id_name
+  | id_name `hasKey` assertIdKey
+  = do { dflags <- getDynFlags
+       ; if gopt Opt_IgnoreAsserts dflags
+         then tc_infer_id id_name
+         else tc_infer_assert id_name }
+
+  | otherwise
+  = do { (expr, ty) <- tc_infer_id id_name
+       ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty)
+       ; return (expr, ty) }
+
+tc_infer_assert :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
+-- Deal with an occurrence of 'assert'
+-- See Note [Adding the implicit parameter to 'assert']
+tc_infer_assert assert_name
+  = do { assert_error_id <- tcLookupId assertErrorName
+       ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name)
+                                          (idType assert_error_id)
+       ; return (mkHsWrap wrap (HsVar noExtField (noLoc assert_error_id)), id_rho)
+       }
+
+tc_infer_id :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
+tc_infer_id id_name
+ = do { thing <- tcLookup id_name
+      ; case thing of
+             ATcId { tct_id = id }
+               -> do { check_local_id occ id
+                     ; return_id id }
+
+             AGlobal (AnId id)
+               -> do { check_global_id occ id
+                     ; return_id id }
+
+             AGlobal (AConLike cl) -> case cl of
+                 RealDataCon con -> return_data_con con
+                 PatSynCon ps
+                   | Just (expr, ty) <- patSynBuilderOcc ps
+                   -> return (expr, ty)
+                   | otherwise
+                   -> nonBidirectionalErr id_name
+
+             _ -> failWithTc $
+                  ppr thing <+> text "used where a value identifier was expected" }
+  where
+    occ = nameOccName id_name
+
+    return_id id = return (HsVar noExtField (noLoc id), idType id)
+
+    return_data_con con
+      = do { let tvs = dataConUserTyVarBinders con
+                 theta = dataConOtherTheta con
+                 args = dataConOrigArgTys con
+                 res = dataConOrigResTy con
+
+           -- See Note [Linear fields generalization]
+           ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy
+           ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args'
+                 combine var (Scaled One ty) = Scaled var ty
+                 combine _   scaled_ty       = scaled_ty
+                   -- The combine function implements the fact that, as
+                   -- described in Note [Linear fields generalization], if a
+                   -- field is not linear (last line) it isn't made polymorphic.
+
+                 etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys
+
+           -- See Note [Instantiating stupid theta]
+           ; let shouldInstantiate = (not (null (dataConStupidTheta con)) ||
+                                      isKindLevPoly (tyConResKind (dataConTyCon con)))
+           ; case shouldInstantiate of
+               True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs)
+                           ; let tys'   = mkTyVarTys tvs'
+                                 theta' = substTheta subst theta
+                                 args'  = substScaledTys subst args
+                                 res'   = substTy subst res
+                           ; wrap <- instCall (OccurrenceOf id_name) tys' theta'
+                           ; let scaled_arg_tys = scaleArgs args'
+                                 eta_wrap = etaWrapper scaled_arg_tys
+                           ; addDataConStupidTheta con tys'
+                           ; return ( mkHsWrap (eta_wrap <.> wrap)
+                                               (HsConLikeOut noExtField (RealDataCon con))
+                                    , mkVisFunTys scaled_arg_tys res')
+                           }
+               False -> let scaled_arg_tys = scaleArgs args
+                            wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs)
+                            eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys)
+                            wrap2 = mkWpTyLams $ binderVars tvs
+                        in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1)
+                                             (HsConLikeOut noExtField (RealDataCon con))
+                                  , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res)
+           }
+
+check_local_id :: OccName -> Id -> TcM ()
+check_local_id occ id
+  = do { check_naughty occ id  -- See Note [HsVar: naughty record selectors]
+       ; checkThLocalId id
+       ; tcEmitBindingUsage $ unitUE (idName id) One }
+
+check_global_id :: OccName -> Id -> TcM ()
+check_global_id occ id
+  = check_naughty occ id  -- See Note [HsVar: naughty record selectors]
+  -- A global cannot possibly be ill-staged
+  -- nor does it need the 'lifting' treatment
+  -- Hence no checkTh stuff here
+
+check_naughty :: OccName -> TcId -> TcM ()
+check_naughty lbl id
+  | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
+  | otherwise                  = return ()
+
+nonBidirectionalErr :: Outputable name => name -> TcM a
+nonBidirectionalErr name = failWithTc $
+    text "non-bidirectional pattern synonym"
+    <+> quotes (ppr name) <+> text "used in an expression"
+
+{- Note [HsVar: naughty record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All record selectors should really be HsRecFld (ambiguous or
+unambiguous), but currently not all of them are: see #18452.  So we
+need to check for naughty record selectors in tc_infer_id, as well as
+in tc_rec_sel_id.
+
+Remove this code when fixing #18452.
+
+Note [Linear fields generalization]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As per Note [Polymorphisation of linear fields], linear field of data
+constructors get a polymorphic type when the data constructor is used as a term.
+
+    Just :: forall {p} a. a #p-> Maybe a
+
+This rule is known only to the typechecker: Just keeps its linear type in Core.
+
+In order to desugar this generalised typing rule, we simply eta-expand:
+
+    \a (x # p :: a) -> Just @a x
+
+has the appropriate type. We insert these eta-expansion with WpFun wrappers.
+
+A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
+certain newtypes with -XUnliftedNewtypes) then this strategy produces
+
+    \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
+
+Which has type
+
+    forall r1 r2 a b. a #p-> b #q-> (# a, b #)
+
+Which violates the levity-polymorphism restriction see Note [Levity polymorphism
+checking] in DsMonad.
+
+So we really must instantiate r1 and r2 rather than quantify over them.  For
+simplicity, we just instantiate the entire type, as described in Note
+[Instantiating stupid theta]. It breaks visible type application with unboxed
+tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
+anywhere.
+
+A better plan: let's force all representation variable to be *inferred*, so that
+they are not subject to visible type applications. Then we can instantiate
+inferred argument eagerly.
+
+Note [Adding the implicit parameter to 'assert']
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The typechecker transforms (assert e1 e2) to (assertError e1 e2).
+This isn't really the Right Thing because there's no way to "undo"
+if you want to see the original source code in the typechecker
+output.  We'll have fix this in due course, when we care more about
+being able to reconstruct the exact original program.
+
+
+Note [Instantiating stupid theta]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Normally, when we infer the type of an Id, we don't instantiate,
+because we wish to allow for visible type application later on.
+But if a datacon has a stupid theta, we're a bit stuck. We need
+to emit the stupid theta constraints with instantiated types. It's
+difficult to defer this to the lazy instantiation, because a stupid
+theta has no spot to put it in a type. So we just instantiate eagerly
+in this case. Thus, users cannot use visible type application with
+a data constructor sporting a stupid theta. I won't feel so bad for
+the users that complain.
+-}
+
+{-
+************************************************************************
+*                                                                      *
+                 Template Haskell checks
+*                                                                      *
+************************************************************************
+-}
+
+checkThLocalId :: Id -> TcM ()
+-- The renamer has already done checkWellStaged,
+--   in RnSplice.checkThLocalName, so don't repeat that here.
+-- Here we just add constraints for cross-stage lifting
+checkThLocalId id
+  = do  { mb_local_use <- getStageAndBindLevel (idName id)
+        ; case mb_local_use of
+             Just (top_lvl, bind_lvl, use_stage)
+                | thLevel use_stage > bind_lvl
+                -> checkCrossStageLifting top_lvl id use_stage
+             _  -> return ()   -- Not a locally-bound thing, or
+                               -- no cross-stage link
+    }
+
+--------------------------------------
+checkCrossStageLifting :: TopLevelFlag -> Id -> ThStage -> TcM ()
+-- If we are inside typed brackets, and (use_lvl > bind_lvl)
+-- we must check whether there's a cross-stage lift to do
+-- Examples   \x -> [|| x ||]
+--            [|| map ||]
+--
+-- This is similar to checkCrossStageLifting in GHC.Rename.Splice, but
+-- this code is applied to *typed* brackets.
+
+checkCrossStageLifting top_lvl id (Brack _ (TcPending ps_var lie_var q))
+  | isTopLevel top_lvl
+  = when (isExternalName id_name) (keepAlive id_name)
+    -- See Note [Keeping things alive for Template Haskell] in GHC.Rename.Splice
+
+  | otherwise
+  =     -- Nested identifiers, such as 'x' in
+        -- E.g. \x -> [|| h x ||]
+        -- We must behave as if the reference to x was
+        --      h $(lift x)
+        -- We use 'x' itself as the splice proxy, used by
+        -- the desugarer to stitch it all back together.
+        -- If 'x' occurs many times we may get many identical
+        -- bindings of the same splice proxy, but that doesn't
+        -- matter, although it's a mite untidy.
+    do  { let id_ty = idType id
+        ; checkTc (isTauTy id_ty) (polySpliceErr id)
+               -- If x is polymorphic, its occurrence sites might
+               -- have different instantiations, so we can't use plain
+               -- 'x' as the splice proxy name.  I don't know how to
+               -- solve this, and it's probably unimportant, so I'm
+               -- just going to flag an error for now
+
+        ; lift <- if isStringTy id_ty then
+                     do { sid <- tcLookupId GHC.Builtin.Names.TH.liftStringName
+                                     -- See Note [Lifting strings]
+                        ; return (HsVar noExtField (noLoc sid)) }
+                  else
+                     setConstraintVar lie_var   $
+                          -- Put the 'lift' constraint into the right LIE
+                     newMethodFromName (OccurrenceOf id_name)
+                                       GHC.Builtin.Names.TH.liftName
+                                       [getRuntimeRep id_ty, id_ty]
+
+                   -- Update the pending splices
+        ; ps <- readMutVar ps_var
+        ; let pending_splice = PendingTcSplice id_name
+                                 (nlHsApp (mkLHsWrap (applyQuoteWrapper q) (noLoc lift))
+                                          (nlHsVar id))
+        ; writeMutVar ps_var (pending_splice : ps)
+
+        ; return () }
+  where
+    id_name = idName id
+
+checkCrossStageLifting _ _ _ = return ()
+
+polySpliceErr :: Id -> SDoc
+polySpliceErr id
+  = text "Can't splice the polymorphic local variable" <+> quotes (ppr id)
+
+{-
+Note [Lifting strings]
+~~~~~~~~~~~~~~~~~~~~~~
+If we see $(... [| s |] ...) where s::String, we don't want to
+generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc.
+So this conditional short-circuits the lifting mechanism to generate
+(liftString "xy") in that case.  I didn't want to use overlapping instances
+for the Lift class in TH.Syntax, because that can lead to overlapping-instance
+errors in a polymorphic situation.
+
+If this check fails (which isn't impossible) we get another chance; see
+Note [Converting strings] in Convert.hs
+
+Local record selectors
+~~~~~~~~~~~~~~~~~~~~~~
+Record selectors for TyCons in this module are ordinary local bindings,
+which show up as ATcIds rather than AGlobals.  So we need to check for
+naughtiness in both branches.  c.f. TcTyClsBindings.mkAuxBinds.
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+         Error reporting for function result mis-matches
+*                                                                      *
+********************************************************************* -}
+
+addFunResCtxt :: HsExpr GhcTc -> [HsExprArg 'TcpTc]
+              -> TcType -> ExpRhoType
+              -> TcM a -> TcM a
+-- When we have a mis-match in the return type of a function
+-- try to give a helpful message about too many/few arguments
+addFunResCtxt fun args fun_res_ty env_ty
+  = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg)
+      -- NB: use a landmark error context, so that an empty context
+      -- doesn't suppress some more useful context
+  where
+    mk_msg
+      = do { mb_env_ty <- readExpType_maybe env_ty
+                     -- by the time the message is rendered, the ExpType
+                     -- will be filled in (except if we're debugging)
+           ; fun_res' <- zonkTcType fun_res_ty
+           ; env'     <- case mb_env_ty of
+                           Just env_ty -> zonkTcType env_ty
+                           Nothing     ->
+                             do { dumping <- doptM Opt_D_dump_tc_trace
+                                ; MASSERT( dumping )
+                                ; newFlexiTyVarTy liftedTypeKind }
+           ; let -- See Note [Splitting nested sigma types in mismatched
+                 --           function types]
+                 (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res'
+                 -- No need to call tcSplitNestedSigmaTys here, since env_ty is
+                 -- an ExpRhoTy, i.e., it's already instantiated.
+                 (_, _, env_tau) = tcSplitSigmaTy env'
+                 (args_fun, res_fun) = tcSplitFunTys fun_tau
+                 (args_env, res_env) = tcSplitFunTys env_tau
+                 n_fun = length args_fun
+                 n_env = length args_env
+                 info  | -- Check for too few args
+                         --  fun_tau = a -> b, res_tau = Int
+                         n_fun > n_env
+                       , not_fun res_env
+                       = text "Probable cause:" <+> quotes (ppr fun)
+                         <+> text "is applied to too few arguments"
+
+                       | -- Check for too many args
+                         -- fun_tau = a -> Int,   res_tau = a -> b -> c -> d
+                         -- The final guard suppresses the message when there
+                         -- aren't enough args to drop; eg. the call is (f e1)
+                         n_fun < n_env
+                       , not_fun res_fun
+                       , (n_fun + count isValArg args) >= n_env
+                          -- Never suggest that a naked variable is
+                                           -- applied to too many args!
+                       = text "Possible cause:" <+> quotes (ppr fun)
+                         <+> text "is applied to too many arguments"
+
+                       | otherwise
+                       = Outputable.empty
+
+           ; return info }
+      where
+        not_fun ty   -- ty is definitely not an arrow type,
+                     -- and cannot conceivably become one
+          = case tcSplitTyConApp_maybe ty of
+              Just (tc, _) -> isAlgTyCon tc
+              Nothing      -> False
+
+{-
+Note [Splitting nested sigma types in mismatched function types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When one applies a function to too few arguments, GHC tries to determine this
+fact if possible so that it may give a helpful error message. It accomplishes
+this by checking if the type of the applied function has more argument types
+than supplied arguments.
+
+Previously, GHC computed the number of argument types through tcSplitSigmaTy.
+This is incorrect in the face of nested foralls, however! This caused Trac
+#13311, for instance:
+
+  f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b
+
+If one uses `f` like so:
+
+  do { f; putChar 'a' }
+
+Then tcSplitSigmaTy will decompose the type of `f` into:
+
+  Tyvars: [a]
+  Context: (Monoid a)
+  Argument types: []
+  Return type: forall b. Monoid b => Maybe a -> Maybe b
+
+That is, it will conclude that there are *no* argument types, and since `f`
+was given no arguments, it won't print a helpful error message. On the other
+hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to:
+
+  Tyvars: [a, b]
+  Context: (Monoid a, Monoid b)
+  Argument types: [Maybe a]
+  Return type: Maybe b
+
+So now GHC recognizes that `f` has one more argument type than it was actually
+provided.
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+             Misc utility functions
+*                                                                      *
+********************************************************************* -}
+
+addLExprCtxt :: LHsExpr GhcRn -> TcRn a -> TcRn a
+addLExprCtxt (L _ e) thing_inside = addExprCtxt e thing_inside
+
+addExprCtxt :: HsExpr GhcRn -> TcRn a -> TcRn a
+addExprCtxt e thing_inside
+  = case e of
+      HsUnboundVar {} -> thing_inside
+      _ -> addErrCtxt (exprCtxt e) thing_inside
+   -- The HsUnboundVar special case addresses situations like
+   --    f x = _
+   -- when we don't want to say "In the expression: _",
+   -- because it is mentioned in the error message itself
+
+exprCtxt :: HsExpr GhcRn -> SDoc
+exprCtxt expr = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr))
+
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index d978f5dbf3..30fe0cad44 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -39,13 +39,14 @@ import GHC.Prelude
 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
                                        , tcMonoExpr, tcMonoExprNC, tcExpr
                                        , tcCheckMonoExpr, tcCheckMonoExprNC
-                                       , tcCheckPolyExpr, tcCheckId )
+                                       , tcCheckPolyExpr )
 
 import GHC.Types.Basic (LexicalFixity(..))
 import GHC.Hs
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.Pat
+import GHC.Tc.Gen.Head( tcCheckId )
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Gen.Bind
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index f01f67b39b..27b2b1358b 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -426,10 +426,9 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
                -- Note [View patterns and polymorphism]
 
          -- Expression must be a function
-        ; let expr_orig = lexprCtOrigin expr
-              herald    = text "A view pattern expression expects"
+        ; let herald = text "A view pattern expression expects"
         ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
-            <- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty
+            <- matchActualFunTySigma herald (Just (ppr expr)) (1,[]) expr_ty
                -- See Note [View patterns and polymorphism]
                -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
 
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 20538dd230..f29378122c 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -74,6 +74,8 @@ import GHC.Builtin.Utils
 import GHC.Types.Name.Reader
 import GHC.Tc.Utils.Zonk
 import GHC.Tc.Gen.Expr
+import GHC.Tc.Errors( reportAllUnsolved )
+import GHC.Tc.Gen.App( tcInferSigma )
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Gen.Export
 import GHC.Tc.Types.Evidence
@@ -99,6 +101,7 @@ import GHC.Tc.TyCl.Instance
 import GHC.IfaceToCore
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Instantiate (tcGetInsts)
 import GHC.Tc.Solver
 import GHC.Tc.TyCl
 import GHC.Tc.Instance.Typeable ( mkTypeableBinds )
@@ -136,7 +139,6 @@ import GHC.Data.FastString
 import GHC.Data.Maybe
 import GHC.Utils.Misc
 import GHC.Data.Bag
-import GHC.Tc.Utils.Instantiate (tcGetInsts)
 import qualified GHC.LanguageExtensions as LangExt
 import Data.Data ( Data )
 import GHC.Hs.Dump
@@ -2478,9 +2480,9 @@ isGHCiMonad hsc_env ty
             Nothing -> failWithTc $ text ("Can't find type:" ++ ty)
 
 -- | How should we infer a type? See Note [TcRnExprMode]
-data TcRnExprMode = TM_Inst    -- ^ Instantiate the type fully (:type)
-                  | TM_NoInst  -- ^ Do not instantiate the type (:type +v)
-                  | TM_Default -- ^ Default the type eagerly (:type +d)
+data TcRnExprMode = TM_Inst     -- ^ Instantiate inferred quantifiers only (:type)
+                  | TM_Default  -- ^ Instantiate all quantifiers,
+                                --   and do eager defaulting (:type +d)
 
 -- | tcRnExpr just finds the type of an expression
 --   for :type
@@ -2495,16 +2497,15 @@ tcRnExpr hsc_env mode rdr_expr
     (rn_expr, _fvs) <- rnLExpr rdr_expr ;
     failIfErrsM ;
 
-        -- Now typecheck the expression, and generalise its type
-        -- it might have a rank-2 type (e.g. :t runST)
-    uniq <- newUnique ;
-    let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
-    ((tclvl, (_tc_expr, res_ty)), lie)
+    -- Typecheck the expression
+    ((tclvl, res_ty), lie)
           <- captureTopConstraints $
              pushTcLevelM          $
-             tc_infer rn_expr ;
+             tcInferSigma inst rn_expr ;
 
     -- Generalise
+    uniq <- newUnique ;
+    let { fresh_it = itName uniq (getLoc rdr_expr) } ;
     (qtvs, dicts, _, residual, _)
          <- simplifyInfer tclvl infer_mode
                           []    {- No sig vars -}
@@ -2528,14 +2529,10 @@ tcRnExpr hsc_env mode rdr_expr
     return (snd (normaliseType fam_envs Nominal ty))
     }
   where
-    tc_infer expr | inst      = tcInferRho expr
-                  | otherwise = tcInferSigma expr
-                  -- tcInferSigma: see Note [Implementing :type]
-
+    -- Optionally instantiate the type of the expression
     -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
-      TM_Inst    -> (True,  NoRestrictions, id)
-      TM_NoInst  -> (False, NoRestrictions, id)
+      TM_Inst    -> (False, NoRestrictions,  id)
       TM_Default -> (True,  EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults)
 
 {- Note [Implementing :type]
@@ -2621,32 +2618,20 @@ tcRnType hsc_env flexi normalise rdr_type
 {- Note [TcRnExprMode]
 ~~~~~~~~~~~~~~~~~~~~~~
 How should we infer a type when a user asks for the type of an expression e
-at the GHCi prompt? We offer 3 different possibilities, described below. Each
-considers this example, with -fprint-explicit-foralls enabled:
-
-  foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
-  :type{,-spec,-def} foo @Int
+at the GHCi prompt? We offer 2 different possibilities, described below. Each
+considers this example, with -fprint-explicit-foralls enabled.  See also
+https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0179-printing-foralls.rst
 
 :type / TM_Inst
 
-  In this mode, we report the type that would be inferred if a variable
-  were assigned to expression e, without applying the monomorphism restriction.
-  This means we instantiate the type and then regeneralize, as discussed
-  in #11376.
+  In this mode, we report the type obained by instantiating only the
+  /inferred/ quantifiers of e's type, solving constraints, and
+  re-generalising, as discussed in #11376.
 
-  > :type foo @Int
-  forall {b} {f :: * -> *}. (Foldable f, Num b) => Int -> f b -> String
-
-  Note that the variables and constraints are reordered here, because this
-  is possible during regeneralization. Also note that the variables are
-  reported as Inferred instead of Specified.
-
-:type +v / TM_NoInst
-
-  This mode is for the benefit of users using TypeApplications. It does no
-  instantiation whatsoever, sometimes meaning that class constraints are not
-  solved.
+  > :type reverse
+  reverse :: forall a. [a] -> [a]
 
+  -- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
   > :type +v foo @Int
   forall f b. (Show Int, Num b, Foldable f) => Int -> f b -> String
 
@@ -2655,12 +2640,17 @@ considers this example, with -fprint-explicit-foralls enabled:
 
 :type +d / TM_Default
 
-  This mode is for the benefit of users who wish to see instantiations of
-  generalized types, and in particular to instantiate Foldable and Traversable.
-  In this mode, any type variable that can be defaulted is defaulted. Because
-  GHCi uses -XExtendedDefaultRules, this means that Foldable and Traversable are
+  This mode is for the benefit of users who wish to see instantiations
+  of generalized types, and in particular to instantiate Foldable and
+  Traversable.  In this mode, all type variables (inferred or
+  specified) are instantiated.  Because GHCi uses
+  -XExtendedDefaultRules, this means that Foldable and Traversable are
   defaulted.
 
+  > :type +d reverse
+  reverse :: forall {a}. [a] -> [a]
+
+  -- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
   > :type +d foo @Int
   Int -> [Integer] -> String
 
@@ -2676,6 +2666,10 @@ considers this example, with -fprint-explicit-foralls enabled:
   modified to include an element that is both Num and Monoid, the defaulting
   would succeed, of course.)
 
+  Note that the variables and constraints are reordered here, because this
+  is possible during regeneralization. Also note that the variables are
+  reported as Inferred instead of Specified.
+
 Note [Kind-generalise in tcRnType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We switch on PolyKinds when kind-checking a user type, so that we will
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 557e56f48f..8cf326bac0 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -96,8 +96,8 @@ canonicalize (CNonCanonical { cc_ev = ev })
                                   canEqNC    ev eq_rel ty1 ty2
       IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr pred)
                                   canIrred OtherCIS ev
-      ForAllPred tvs theta p -> do traceTcS "canEvNC:forall" (ppr pred)
-                                   canForAllNC ev tvs theta p
+      ForAllPred tvs th p   -> do traceTcS "canEvNC:forall" (ppr pred)
+                                  canForAllNC ev tvs th p
   where
     pred = ctEvPred ev
 
@@ -708,11 +708,16 @@ canIrred status ev
        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
        ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+
     do { -- Re-classify, in case flattening has improved its shape
+         -- Code is like the CNonCanonical case of canonicalize, except
+         -- that the IrredPred branch stops work
        ; case classifyPredType (ctEvPred new_ev) of
            ClassPred cls tys     -> canClassNC new_ev cls tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
-           _                     -> continueWith $
+           ForAllPred tvs th p   -> do traceTcS "canEvNC:forall" (ppr pred)
+                                       canForAllNC ev tvs th p
+           IrredPred {}          -> continueWith $
                                     mkIrredCt status new_ev } }
 
 {- *********************************************************************
@@ -2106,6 +2111,10 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
        ; continueWith (mkIrredCt status new_ev) }
   where
     mtvu = metaTyVarUpdateOK dflags tv1 rhs
+           -- Despite the name of the function, tv1 may not be a
+           -- unification variable; we are really checking that this
+           -- equality is ok to be used to rewrite others, i.e.  that
+           -- it satisfies the conditions for CTyEqCan
 
     role = eqRelRole eq_rel
 
@@ -2135,7 +2144,7 @@ k2 and use this to cast. To wit, from
 
   [X] (tv :: k1) ~ (rhs :: k2)
 
-we go to
+(where [X] is [G], [W], or [D]), we go to
 
   [noDerived X] co :: k2 ~ k1
   [X]           (tv :: k1) ~ ((rhs |> co) :: k1)
@@ -2145,6 +2154,9 @@ where
   noDerived G = G
   noDerived _ = W
 
+For Wanted/Derived, the [X] constraint is "blocked" (not CTyEqCan, is CIrred)
+until the k1~k2 constraint solved: Wrinkle (2).
+
 Wrinkles:
 
  (1) The noDerived step is because Derived equalities have no evidence.
@@ -2157,7 +2169,7 @@ Wrinkles:
        [W] (tv :: k1) ~ ((rhs |> co) :: k1)
      as canonical in the inert set. In particular, we must not unify tv.
      If we did, the Wanted becomes a Given (effectively), and then can
-     rewrite other Wanteds. But that's bad: See Note [Wanteds to not rewrite Wanteds]
+     rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds]
      in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for
      tales of destruction.
 
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index a99ab10404..88a0e4eeef 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -15,8 +15,7 @@
 module GHC.Tc.TyCl.PatSyn
    ( tcPatSynDecl
    , tcPatSynBuilderBind
-   , tcPatSynBuilderOcc
-   , nonBidirectionalErr
+   , patSynBuilderOcc
    )
 where
 
@@ -884,13 +883,12 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name
     add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                              pprMatches other_mg
 
-tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTc, TcSigmaType)
--- monadic only for failure
-tcPatSynBuilderOcc ps
-  | Just (builder_id, add_void_arg) <- builder
+patSynBuilderOcc :: PatSyn -> Maybe (HsExpr GhcTc, TcSigmaType)
+patSynBuilderOcc ps
+  | Just (builder_id, add_void_arg) <- patSynBuilder ps
   , let builder_expr = HsConLikeOut noExtField (PatSynCon ps)
         builder_ty   = idType builder_id
-  = return $
+  = Just $
     if add_void_arg
     then ( builder_expr   -- still just return builder_expr; the void# arg is added
                           -- by dsConLike in the desugarer
@@ -898,10 +896,7 @@ tcPatSynBuilderOcc ps
     else (builder_expr, builder_ty)
 
   | otherwise  -- Unidirectional
-  = nonBidirectionalErr name
-  where
-    name    = patSynName ps
-    builder = patSynBuilder ps
+  = Nothing
 
 add_void :: Bool -> Type -> Type
 add_void need_dummy_arg ty
@@ -1091,11 +1086,6 @@ want to avoid difficult to decipher core lint errors!
  -}
 
 
-nonBidirectionalErr :: Outputable name => name -> TcM a
-nonBidirectionalErr name = failWithTc $
-    text "non-bidirectional pattern synonym"
-    <+> quotes (ppr name) <+> text "used in an expression"
-
 -- Walk the whole pattern and for all ConPatOuts, collect the
 -- existentially-bound type variables and evidence binding variables.
 --
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
index fb4ac51013..38fc4b52f1 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
@@ -3,7 +3,6 @@ module GHC.Tc.TyCl.PatSyn where
 import GHC.Hs    ( PatSynBind, LHsBinds )
 import GHC.Tc.Types ( TcM, TcSigInfo )
 import GHC.Tc.Utils.Monad ( TcGblEnv)
-import GHC.Utils.Outputable ( Outputable )
 import GHC.Hs.Extension ( GhcRn, GhcTc )
 import Data.Maybe  ( Maybe )
 
@@ -13,4 +12,3 @@ tcPatSynDecl :: PatSynBind GhcRn GhcRn
 
 tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn -> TcM (LHsBinds GhcTc)
 
-nonBidirectionalErr :: Outputable name => name -> TcM a
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index e7b067e946..0528976a6b 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -1095,9 +1095,4 @@ Therefore, when used in the right-hand side of `unT`, GHC attempts to
 instantiate `a` with `(forall b. b -> b) -> Int`, which is impredicative.
 To make sure that GHC is OK with this, we enable ImpredicativeTypes interally
 when typechecking these HsBinds so that the user does not have to.
-
-Although ImpredicativeTypes is somewhat fragile and unpredictable in GHC right
-now, it will become robust when Quick Look impredicativity is implemented. In
-the meantime, using ImpredicativeTypes to instantiate the `a` type variable in
-recSelError's type does actually work, so its use here is benign.
 -}
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index d93e8fc84f..0e928ed5fd 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -12,7 +12,7 @@
 
 module GHC.Tc.Utils.Instantiate (
        topSkolemise,
-       topInstantiate, topInstantiateInferred,
+       topInstantiate, instantiateSigma,
        instCall, instDFunType, instStupidTheta, instTyVarsWith,
        newWanted, newWanteds,
 
@@ -72,6 +72,7 @@ import GHC.Types.Name
 import GHC.Types.Var
 import GHC.Core.DataCon
 import GHC.Types.Var.Env
+import GHC.Types.Var.Set
 import GHC.Builtin.Names
 import GHC.Types.SrcLoc as SrcLoc
 import GHC.Driver.Session
@@ -189,66 +190,44 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 -- and   e :: ty
 -- then  wrap e :: rho  (that is, wrap :: ty "->" rho)
 -- NB: always returns a rho-type, with no top-level forall or (=>)
-topInstantiate = top_instantiate True
+topInstantiate orig ty
+  | (tvs, theta, body) <- tcSplitSigmaTy ty
+  , not (null tvs && null theta)
+  = do { (_, wrap1, body1) <- instantiateSigma orig tvs theta body
 
--- | Instantiate all outer 'Inferred' binders
--- and any context. Never looks through arrows or specified type variables.
--- Used for visible type application.
-topInstantiateInferred :: CtOrigin -> TcSigmaType
-                       -> TcM (HsWrapper, TcSigmaType)
--- if    topInstantiate ty = (wrap, rho)
--- and   e :: ty
--- then  wrap e :: rho
--- NB: may return a sigma-type
-topInstantiateInferred = top_instantiate False
-
-top_instantiate :: Bool   -- True  <=> instantiate *all* variables
-                          -- False <=> instantiate only the inferred ones
-                -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-top_instantiate inst_all orig ty
-  | (binders, phi) <- tcSplitForAllVarBndrs ty
-  , (theta, rho)   <- tcSplitPhiTy phi
-  , not (null binders && null theta)
-  = do { let (inst_bndrs, leave_bndrs) = span should_inst binders
-             (inst_theta, leave_theta)
-               | null leave_bndrs = (theta, [])
-               | otherwise        = ([], theta)
-             in_scope    = mkInScopeSet (tyCoVarsOfType ty)
-             empty_subst = mkEmptyTCvSubst in_scope
-             inst_tvs    = binderVars inst_bndrs
-       ; (subst, inst_tvs') <- mapAccumLM newMetaTyVarX empty_subst inst_tvs
-       ; let inst_theta' = substTheta subst inst_theta
-             sigma'      = substTy subst (mkForAllTys leave_bndrs $
-                                          mkPhiTy leave_theta rho)
-             inst_tv_tys' = mkTyVarTys inst_tvs'
-
-       ; wrap1 <- instCall orig inst_tv_tys' inst_theta'
-       ; traceTc "Instantiating"
-                 (vcat [ text "all tyvars?" <+> ppr inst_all
-                       , text "origin" <+> pprCtOrigin orig
-                       , text "type" <+> debugPprType ty
-                       , text "theta" <+> ppr theta
-                       , text "leave_bndrs" <+> ppr leave_bndrs
-                       , text "with" <+> vcat (map debugPprType inst_tv_tys')
-                       , text "theta:" <+>  ppr inst_theta' ])
-
-       ; (wrap2, rho2) <-
-           if null leave_bndrs   -- NB: if inst_all is True then leave_bndrs = []
+       -- Loop, to account for types like
+       --       forall a. Num a => forall b. Ord b => ...
+       ; (wrap2, rho) <- topInstantiate orig body1
 
-         -- account for types like forall a. Num a => forall b. Ord b => ...
-           then top_instantiate inst_all orig sigma'
+       ; return (wrap2 <.> wrap1, rho) }
 
-         -- but don't loop if there were any un-inst'able tyvars
-           else return (idHsWrapper, sigma')
+  | otherwise = return (idHsWrapper, ty)
 
-       ; return (wrap2 <.> wrap1, rho2) }
+instantiateSigma :: CtOrigin -> [TyVar] -> TcThetaType -> TcSigmaType
+                 -> TcM ([TcTyVar], HsWrapper, TcSigmaType)
+-- (instantiate orig tvs theta ty)
+-- instantiates the the type variables tvs, emits the (instantiated)
+-- constraints theta, and returns the (instantiated) type ty
+instantiateSigma orig tvs theta body_ty
+  = do { (subst, inst_tvs) <- mapAccumLM newMetaTyVarX empty_subst tvs
+       ; let inst_theta  = substTheta subst theta
+             inst_body   = substTy subst body_ty
+             inst_tv_tys = mkTyVarTys inst_tvs
+
+       ; wrap <- instCall orig inst_tv_tys inst_theta
+       ; traceTc "Instantiating"
+                 (vcat [ text "origin" <+> pprCtOrigin orig
+                       , text "tvs"   <+> ppr tvs
+                       , text "theta" <+> ppr theta
+                       , text "type" <+> debugPprType body_ty
+                       , text "with" <+> vcat (map debugPprType inst_tv_tys)
+                       , text "theta:" <+>  ppr inst_theta ])
 
-  | otherwise = return (idHsWrapper, ty)
+      ; return (inst_tvs, wrap, inst_body) }
   where
-
-    should_inst bndr
-      | inst_all  = True
-      | otherwise = binderArgFlag bndr == Inferred
+    free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta
+    in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs)
+    empty_subst = mkEmptyTCvSubst in_scope
 
 instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
 -- Use this when you want to instantiate (forall a b c. ty) with
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 0995eb51e9..62e39879d7 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -801,10 +801,11 @@ influences the way it is tidied; see TypeRep.tidyTyVarBndr.
 metaInfoToTyVarName :: MetaInfo -> FastString
 metaInfoToTyVarName  meta_info =
   case meta_info of
-       TauTv       -> fsLit "t"
-       FlatMetaTv  -> fsLit "fmv"
-       FlatSkolTv  -> fsLit "fsk"
-       TyVarTv     -> fsLit "a"
+       TauTv        -> fsLit "t"
+       FlatMetaTv   -> fsLit "fmv"
+       FlatSkolTv   -> fsLit "fsk"
+       TyVarTv      -> fsLit "a"
+       RuntimeUnkTv -> fsLit "r"
 
 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 21b6b962d9..6d5ef37442 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -57,7 +57,7 @@ module GHC.Tc.Utils.TcType (
   -- These are important because they do not look through newtypes
   getTyVar,
   tcSplitForAllTy_maybe,
-  tcSplitForAllTys,
+  tcSplitForAllTys, tcSplitSomeForAllTys,
   tcSplitForAllTysReq, tcSplitForAllTysInvis,
   tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
@@ -561,6 +561,9 @@ data MetaInfo
                    -- It is filled in /only/ by unflattenGivens
                    -- See Note [The flattening story] in GHC.Tc.Solver.Flatten
 
+   | RuntimeUnkTv  -- A unification variable used in the GHCi debugger.
+                   -- It /is/ allowed to unify with a polytype, unlike TauTv
+
 instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
@@ -570,6 +573,7 @@ instance Outputable MetaInfo where
   ppr TyVarTv       = text "tyv"
   ppr FlatMetaTv    = text "fmv"
   ppr FlatSkolTv    = text "fsk"
+  ppr RuntimeUnkTv  = text "rutv"
 
 {- *********************************************************************
 *                                                                      *
@@ -1222,6 +1226,19 @@ tcSplitForAllTys ty
   = ASSERT( all isTyVar (fst sty) ) sty
   where sty = splitForAllTys ty
 
+-- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
+-- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
+-- @argf_pred@ is a predicate over visibilities provided as an argument to this
+-- function.
+tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyVar], Type)
+tcSplitSomeForAllTys argf_pred ty
+  = split ty ty []
+  where
+    split _ (ForAllTy (Bndr tv argf) ty) tvs
+      | argf_pred argf                             = split ty ty (tv:tvs)
+    split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
+    split orig_ty _                            tvs = (reverse tvs, orig_ty)
+
 -- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type
 -- variable binders. All split tyvars are annotated with '()'.
 tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type)
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 6a83348b2a..0c29a6557f 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -32,8 +32,8 @@ module GHC.Tc.Utils.Unify (
   matchExpectedTyConApp,
   matchExpectedAppTy,
   matchExpectedFunTys,
-  matchActualFunTysRho, matchActualFunTySigma,
   matchExpectedFunKind,
+  matchActualFunTySigma, matchActualFunTysRho,
 
   metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
 
@@ -69,13 +69,155 @@ import GHC.Driver.Session
 import GHC.Types.Basic
 import GHC.Data.Bag
 import GHC.Utils.Misc
-import qualified GHC.LanguageExtensions as LangExt
 import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
 
 import Control.Monad
 import Control.Arrow ( second )
 
+
+{- *********************************************************************
+*                                                                      *
+              matchActualFunTys
+*                                                                      *
+********************************************************************* -}
+
+-- | matchActualFunTySigma does looks for just one function arrow
+--   returning an uninstantiated sigma-type
+matchActualFunTySigma
+  :: SDoc -- See Note [Herald for matchExpectedFunTys]
+  -> Maybe SDoc                    -- The thing with type TcSigmaType
+  -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and
+                                   -- types of values args to which function has
+                                   --   been applied already (reversed)
+                                   -- Both are used only for error messages)
+  -> TcRhoType                     -- Type to analyse: a TcRhoType
+  -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
+-- The /argument/ is a RhoType
+-- The /result/   is an (uninstantiated) SigmaType
+--
+-- See Note [matchActualFunTy error handling] for the first three arguments
+
+-- If   (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty
+-- then wrap :: fun_ty ~> (arg_ty -> res_ty)
+-- and NB: res_ty is an (uninstantiated) SigmaType
+
+matchActualFunTySigma herald mb_thing err_info fun_ty
+  = ASSERT2( isRhoTy fun_ty, ppr fun_ty )
+    go fun_ty
+  where
+    -- Does not allocate unnecessary meta variables: if the input already is
+    -- a function, we just take it apart.  Not only is this efficient,
+    -- it's important for higher rank: the argument might be of form
+    --              (forall a. ty) -> other
+    -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
+    -- hide the forall inside a meta-variable
+    go :: TcRhoType   -- The type we're processing, perhaps after
+                      -- expanding any type synonym
+       -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
+    go ty | Just ty' <- tcView ty = go ty'
+
+    go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
+      = ASSERT( af == VisArg )
+        return (idHsWrapper, Scaled w arg_ty, res_ty)
+
+    go ty@(TyVarTy tv)
+      | isMetaTyVar tv
+      = do { cts <- readMetaTyVar tv
+           ; case cts of
+               Indirect ty' -> go ty'
+               Flexi        -> defer ty }
+
+       -- In all other cases we bale out into ordinary unification
+       -- However unlike the meta-tyvar case, we are sure that the
+       -- number of arguments doesn't match arity of the original
+       -- type, so we can add a bit more context to the error message
+       -- (cf #7869).
+       --
+       -- It is not always an error, because specialized type may have
+       -- different arity, for example:
+       --
+       -- > f1 = f2 'a'
+       -- > f2 :: Monad m => m Bool
+       -- > f2 = undefined
+       --
+       -- But in that case we add specialized type into error context
+       -- anyway, because it may be useful. See also #9605.
+    go ty = addErrCtxtM (mk_ctxt ty) (defer ty)
+
+    ------------
+    defer fun_ty
+      = do { arg_ty <- newOpenFlexiTyVarTy
+           ; res_ty <- newOpenFlexiTyVarTy
+           ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty
+           ; co <- unifyType mb_thing fun_ty unif_fun_ty
+           ; return (mkWpCastN co, unrestricted arg_ty, res_ty) }
+
+    ------------
+    mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+    mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far)
+                                     res_ty n_val_args_in_call
+    (n_val_args_in_call, arg_tys_so_far) = err_info
+
+{- Note [matchActualFunTy error handling]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+matchActualFunTySigma is made much more complicated by the
+desire to produce good error messages. Consider the application
+    f @Int x y
+In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
+and then call matchActualFunTysPart for each individual value
+argument. It, in turn, must instantiate any type/dictionary args,
+before looking for an arrow type.
+
+But if it doesn't find an arrow type, it wants to generate a message
+like "f is applied to two arguments but its type only has one".
+To do that, it needs to konw about the args that tcArgs has already
+munched up -- hence passing in n_val_args_in_call and arg_tys_so_far;
+and hence also the accumulating so_far arg to 'go'.
+
+This allows us (in mk_ctxt) to construct f's /instantiated/ type,
+with just the values-arg arrows, which is what we really want
+in the error message.
+
+Ugh!
+-}
+
+-- Like 'matchExpectedFunTys', but used when you have an "actual" type,
+-- for example in function application
+matchActualFunTysRho :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+                     -> CtOrigin
+                     -> Maybe SDoc  -- the thing with type TcSigmaType
+                     -> Arity
+                     -> TcSigmaType
+                     -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
+-- If    matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
+-- then  wrap : ty ~> (t1 -> ... -> tn -> res_ty)
+--       and res_ty is a RhoType
+-- NB: the returned type is top-instantiated; it's a RhoType
+matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
+  = go n_val_args_wanted [] fun_ty
+  where
+    go n so_far fun_ty
+      | not (isRhoTy fun_ty)
+      = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty
+           ; (wrap2, arg_tys, res_ty) <- go n so_far rho
+           ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
+
+    go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
+
+    go n so_far fun_ty
+      = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma
+                                                 herald mb_thing
+                                                 (n_val_args_wanted, so_far)
+                                                 fun_ty
+           ; (wrap_res, arg_tys, res_ty)   <- go (n-1) (arg_ty1:so_far) res_ty1
+           ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc
+           ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
+      where
+        doc = text "When inferring the argument type of a function with type" <+>
+              quotes (ppr fun_ty)
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -226,167 +368,32 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
     ------------
     mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
     mk_ctxt arg_tys res_ty env
-      = do { (env', ty) <- zonkTidyTcType env (mkVisFunTys arg_tys' res_ty)
-           ; return ( env', mk_fun_tys_msg herald ty arity) }
+      = mkFunTysMsg env herald arg_tys' res_ty arity
       where
-        arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) (reverse arg_tys)
+        arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $
+                   reverse arg_tys
             -- this is safe b/c we're called from "go"
 
--- Like 'matchExpectedFunTys', but used when you have an "actual" type,
--- for example in function application
-matchActualFunTysRho :: SDoc   -- See Note [Herald for matchExpectedFunTys]
-                     -> CtOrigin
-                     -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
-                     -> Arity
-                     -> TcSigmaType
-                     -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
--- If    matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
--- then  wrap : ty ~> (t1 -> ... -> tn -> res_ty)
---       and res_ty is a RhoType
--- NB: the returned type is top-instantiated; it's a RhoType
-matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
-  = go n_val_args_wanted [] fun_ty
-  where
-    go 0 _ fun_ty
-      = do { (wrap, rho) <- topInstantiate ct_orig fun_ty
-           ; return (wrap, [], rho) }
-    go n so_far fun_ty
-      = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma
-                                                 herald ct_orig mb_thing
-                                                 (n_val_args_wanted, so_far)
-                                                 fun_ty
-           ; (wrap_res, arg_tys, res_ty)   <- go (n-1) (arg_ty1:so_far) res_ty1
-           ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc
-           ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
-      where
-        doc = text "When inferring the argument type of a function with type" <+>
-              quotes (ppr fun_ty)
-
--- | matchActualFunTySigm does looks for just one function arrow
---   returning an uninstantiated sigma-type
-matchActualFunTySigma
-  :: SDoc -- See Note [Herald for matchExpectedFunTys]
-  -> CtOrigin
-  -> Maybe (HsExpr GhcRn)   -- The thing with type TcSigmaType
-  -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and
-                            -- types of values args to which function has
-                            --   been applied already (reversed)
-                            -- Both are used only for error messages)
-  -> TcSigmaType            -- Type to analyse
-  -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
--- See Note [matchActualFunTys error handling] for all these arguments
-
--- If   (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty
--- then wrap :: fun_ty ~> (arg_ty -> res_ty)
--- and NB: res_ty is an (uninstantiated) SigmaType
-
-matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty
-  = go fun_ty
--- Does not allocate unnecessary meta variables: if the input already is
--- a function, we just take it apart.  Not only is this efficient,
--- it's important for higher rank: the argument might be of form
---              (forall a. ty) -> other
--- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
--- hide the forall inside a meta-variable
-
--- (*) Sometimes it's necessary to call matchActualFunTys with only part
--- (that is, to the right of some arrows) of the type of the function in
--- question. (See GHC.Tc.Gen.Expr.tcArgs.) This argument is the reversed list of
--- arguments already seen (that is, not part of the TcSigmaType passed
--- in elsewhere).
+mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity
+            -> TcM (TidyEnv, MsgDoc)
+mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
+  = do { (env', fun_rho) <- zonkTidyTcType env $
+                            mkVisFunTys arg_tys res_ty
 
-  where
-    go :: TcSigmaType   -- The remainder of the type as we're processing
-       -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-    go ty | Just ty' <- tcView ty = go ty'
+       ; let (all_arg_tys, _) = splitFunTys fun_rho
+             n_fun_args = length all_arg_tys
 
-    go ty
-      | not (null tvs && null theta)
-      = do { (wrap1, rho) <- topInstantiate ct_orig ty
-           ; (wrap2, arg_ty, res_ty) <- go rho
-           ; return (wrap2 <.> wrap1, arg_ty, res_ty) }
-      where
-        (tvs, theta, _) = tcSplitSigmaTy ty
-
-    go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
-      = ASSERT( af == VisArg )
-        return (idHsWrapper, Scaled w arg_ty, res_ty)
+             msg | n_val_args_in_call <= n_fun_args  -- Enough args, in the end
+                 = text "In the result of a function call"
+                 | otherwise
+                 = hang (full_herald <> comma)
+                      2 (sep [ text "but its type" <+> quotes (pprType fun_rho)
+                             , if n_fun_args == 0 then text "has none"
+                               else text "has only" <+> speakN n_fun_args])
 
-    go ty@(TyVarTy tv)
-      | isMetaTyVar tv
-      = do { cts <- readMetaTyVar tv
-           ; case cts of
-               Indirect ty' -> go ty'
-               Flexi        -> defer ty }
-
-       -- In all other cases we bale out into ordinary unification
-       -- However unlike the meta-tyvar case, we are sure that the
-       -- number of arguments doesn't match arity of the original
-       -- type, so we can add a bit more context to the error message
-       -- (cf #7869).
-       --
-       -- It is not always an error, because specialized type may have
-       -- different arity, for example:
-       --
-       -- > f1 = f2 'a'
-       -- > f2 :: Monad m => m Bool
-       -- > f2 = undefined
-       --
-       -- But in that case we add specialized type into error context
-       -- anyway, because it may be useful. See also #9605.
-    go ty = addErrCtxtM (mk_ctxt ty) (defer ty)
-
-    ------------
-    defer fun_ty
-      = do { arg_ty <- newOpenFlexiTyVarTy
-           ; res_ty <- newOpenFlexiTyVarTy
-           ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty
-           ; co <- unifyType mb_thing fun_ty unif_fun_ty
-           ; return (mkWpCastN co, unrestricted arg_ty, res_ty) }
-
-    ------------
-    mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
-    mk_ctxt res_ty env
-      = do { (env', ty) <- zonkTidyTcType env $
-                           mkVisFunTys (reverse arg_tys_so_far) res_ty
-           ; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) }
-    (n_val_args_in_call, arg_tys_so_far) = err_info
-
-mk_fun_tys_msg :: SDoc -> TcType -> Arity -> SDoc
-mk_fun_tys_msg herald ty n_args_in_call
-  | n_args_in_call <= n_fun_args  -- Enough args, in the end
-  = text "In the result of a function call"
-  | otherwise
-  = hang (herald <+> speakNOf n_args_in_call (text "value argument") <> comma)
-       2 (sep [ text "but its type" <+> quotes (pprType ty)
-              , if n_fun_args == 0 then text "has none"
-                else text "has only" <+> speakN n_fun_args])
-  where
-    (args, _) = tcSplitFunTys ty
-    n_fun_args = length args
-
-{- Note [matchActualFunTys error handling]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-matchActualFunTysPart is made much more complicated by the
-desire to produce good error messages. Consider the application
-    f @Int x y
-In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
-and then call matchActualFunTysPart for each individual value
-argument. It, in turn, must instantiate any type/dictionary args,
-before looking for an arrow type.
-
-But if it doesn't find an arrow type, it wants to generate a message
-like "f is applied to two arguments but its type only has one".
-To do that, it needs to konw about the args that tcArgs has already
-munched up -- hence passing in n_val_args_in_call and arg_tys_so_far;
-and hence also the accumulating so_far arg to 'go'.
-
-This allows us (in mk_ctxt) to construct f's /instantiated/ type,
-with just the values-arg arrows, which is what we really want
-in the error message.
-
-Ugh!
--}
+       ; return (env', msg) }
+ where
+  full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument")
 
 ----------------------
 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
@@ -519,7 +526,7 @@ tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpR
 tcWrapResultO orig rn_expr expr actual_ty res_ty
   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                       , text "Expected:" <+> ppr res_ty ])
-       ; wrap <- tcSubTypeNC orig GenSigCtxt (Just rn_expr) actual_ty res_ty
+       ; wrap <- tcSubTypeNC orig GenSigCtxt (Just (ppr rn_expr)) actual_ty res_ty
        ; return (mkHsWrap wrap expr) }
 
 tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
@@ -533,7 +540,7 @@ tcWrapResultMono rn_expr expr act_ty res_ty
   = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr )
     do { co <- case res_ty of
                   Infer inf_res -> fillInferResult act_ty inf_res
-                  Check exp_ty  -> unifyType (Just rn_expr) act_ty exp_ty
+                  Check exp_ty  -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
        ; return (mkHsWrapCo co expr) }
 
 ------------------------
@@ -565,7 +572,7 @@ tcSubType orig ctxt ty_actual ty_expected
 
 tcSubTypeNC :: CtOrigin       -- Used when instantiating
             -> UserTypeCtxt   -- Used when skolemising
-            -> Maybe (HsExpr GhcRn)   -- The expression that has type 'actual' (if known)
+            -> Maybe SDoc     -- The expression that has type 'actual' (if known)
             -> TcSigmaType            -- Actual type
             -> ExpRhoType             -- Expected type
             -> TcM HsWrapper
@@ -661,12 +668,7 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected
 
        ; return (sk_wrap <.> inner_wrap) }
   where
-    possibly_poly ty
-      | isForAllTy ty                        = True
-      | Just (_, _, res) <- splitFunTy_maybe ty = possibly_poly res
-      | otherwise                            = False
-      -- NB *not* tcSplitFunTy, because here we want
-      -- to decompose type-class arguments too
+    possibly_poly ty = not (isRhoTy ty)
 
     definitely_poly ty
       | (tvs, theta, tau) <- tcSplitSigmaTy ty
@@ -719,9 +721,6 @@ So roughly:
 then we can revert to simple equality.  But we need to be careful.
 These examples are all fine:
 
- * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
-      Polymorphism is buried in ty_actual
-
  * (Char->Char) <= (forall a. Char -> Char)
       ty_expected isn't really polymorphic
 
@@ -832,10 +831,11 @@ to checkConstraints.
 
 tcSkolemiseScoped is very similar, but differs in two ways:
 
-* It deals specially with just the outer forall, bringing those
-  type variables into lexical scope.  To my surprise, I found that
-  doing this regardless (in tcSkolemise) caused a non-trivial (1%-ish)
-  perf hit on the compiler.
+* It deals specially with just the outer forall, bringing those type
+  variables into lexical scope.  To my surprise, I found that doing
+  this unconditionally in tcSkolemise (i.e. doing it even if we don't
+  need to bring the variables into lexical scope, which is harmless)
+  caused a non-trivial (1%-ish) perf hit on the compiler.
 
 * It always calls checkConstraints, even if there are no skolem
   variables at all.  Reason: there might be nested deferred errors
@@ -848,6 +848,8 @@ tcSkolemise, tcSkolemiseScoped
     -> (TcType -> TcM result)
     -> TcM (HsWrapper, result)
         -- ^ The wrapper has type: spec_ty ~> expected_ty
+-- See Note [Skolemisation] for the differences between
+-- tcSkolemiseScoped and tcSkolemise
 
 tcSkolemiseScoped ctxt expected_ty thing_inside
   = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
@@ -1039,7 +1041,7 @@ take care:
       [W] C Int b2    -- from g_blan
   and fundpes can yield [D] b1 ~ b2, even though the two functions have
   literally nothing to do with each other.  #14185 is an example.
-  Building an implication keeps them separage.
+  Building an implication keeps them separate.
 -}
 
 {-
@@ -1053,8 +1055,9 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
-unifyType :: Maybe (HsExpr GhcRn)   -- ^ If present, has type 'ty1'
-          -> TcTauType -> TcTauType -> TcM TcCoercionN
+unifyType :: Maybe SDoc  -- ^ If present, the thing that has type ty1
+          -> TcTauType -> TcTauType    -- ty1, ty2
+          -> TcM TcCoercionN           -- :: ty1 ~# ty2
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
 unifyType thing ty1 ty2
@@ -1077,13 +1080,13 @@ unifyTypeET ty1 ty2
                           , uo_visible  = True }
 
 
-unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
-unifyKind thing ty1 ty2
+unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN
+unifyKind mb_thing ty1 ty2
   = uType KindLevel origin ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual   = ty1
                           , uo_expected = ty2
-                          , uo_thing    = ppr <$> thing
+                          , uo_thing    = mb_thing
                           , uo_visible  = True }
 
 
@@ -1186,10 +1189,12 @@ uType t_or_k origin orig_ty1 orig_ty2
       | Just ty1' <- tcView ty1 = go ty1' ty2
       | Just ty2' <- tcView ty2 = go ty1  ty2'
 
-        -- Functions (or predicate functions) just check the two parts
-    go (FunTy _ w1 fun1 arg1) (FunTy _ w2 fun2 arg2)
-      = do { co_l <- uType t_or_k origin fun1 fun2
-           ; co_r <- uType t_or_k origin arg1 arg2
+    -- Functions (t1 -> t2) just check the two parts
+    -- Do not attempt (c => t); just defer
+    go (FunTy { ft_af = VisArg, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
+       (FunTy { ft_af = VisArg, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
+      = do { co_l <- uType t_or_k origin arg1 arg2
+           ; co_r <- uType t_or_k origin res1 res2
            ; co_w <- uType t_or_k origin w1 w2
            ; return $ mkFunCo Nominal co_w co_l co_r }
 
@@ -1479,6 +1484,7 @@ swapOverTyVars is_given tv1 tv2
 
 lhsPriority :: TcTyVar -> Int
 -- Higher => more important to be on the LHS
+--        => more likely to be eliminated
 -- See Note [TyVar/TyVar orientation]
 lhsPriority tv
   = ASSERT2( isTyVar tv, ppr tv)
@@ -1486,10 +1492,12 @@ lhsPriority tv
       RuntimeUnk  -> 0
       SkolemTv {} -> 0
       MetaTv { mtv_info = info } -> case info of
-                                     FlatSkolTv -> 1
-                                     TyVarTv    -> 2
-                                     TauTv      -> 3
-                                     FlatMetaTv -> 4
+                                     FlatSkolTv   -> 1
+                                     TyVarTv      -> 2
+                                     TauTv        -> 3
+                                     FlatMetaTv   -> 4
+                                     RuntimeUnkTv -> 5
+
 {- Note [TyVar/TyVar orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
@@ -1855,7 +1863,7 @@ matchExpectedFunKind hs_ty n k = go n k
                 Indirect fun_kind -> go n fun_kind
                 Flexi ->             defer n k }
 
-    go n (FunTy _ w arg res)
+    go n (FunTy { ft_mult = w, ft_arg = arg, ft_res = res })
       = do { co <- go (n-1) res
            ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) }
 
@@ -1943,7 +1951,7 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
 --   a) the given variable occurs in the given type.
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes)
 occCheckForErrors dflags tv ty
-  = case preCheck dflags True tv ty of
+  = case mtvu_check dflags True tv ty of
       MTVU_OK _        -> MTVU_OK ()
       MTVU_Bad         -> MTVU_Bad
       MTVU_HoleBlocker -> MTVU_HoleBlocker
@@ -1957,13 +1965,20 @@ metaTyVarUpdateOK :: DynFlags
                   -> TcType              -- ty :: k2
                   -> MetaTyVarUpdateResult TcType        -- possibly-expanded ty
 -- (metaTyVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty
--- Check (a) that tv doesn't occur in ty (occurs check)
+-- Checks that the equality tv~ty is OK to be used to rewrite
+-- other equalities.  Equivalently, checks the conditions for CTyEqCan
+--       (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
 --           (in the impredicative case), or type functions
 --       (c) that ty does not have any blocking coercion holes
 --           See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical"
 --
+-- Used in two places:
+--   - In the eager unifier: uUnfilledVar2
+--   - In the canonicaliser: GHC.Tc.Solver.Canonical.canEqTyVar2
+-- Note that in the latter case tv is not necessarily a meta-tyvar,
+-- despite the name of this function.
+
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with,
 --        [we know the update is ok]
@@ -1982,7 +1997,7 @@ metaTyVarUpdateOK :: DynFlags
 -- See Note [Refactoring hazard: checkTauTvUpdate]
 
 metaTyVarUpdateOK dflags tv ty
-  = case preCheck dflags False tv ty of
+  = case mtvu_check dflags False tv ty of
          -- False <=> type families not ok
          -- See Note [Prevent unification with type families]
       MTVU_OK _        -> MTVU_OK ty
@@ -1992,11 +2007,11 @@ metaTyVarUpdateOK dflags tv ty
                             Just expanded_ty -> MTVU_OK expanded_ty
                             Nothing          -> MTVU_Occurs
 
-preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
--- A quick check for
---   (a) a forall type (unless -XImpredicativeTypes)
---   (b) a predicate type (unless -XImpredicativeTypes)
---   (c) a type family
+mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
+-- Checks the invariants for CTyEqCan.   In particular:
+--   (a) a forall type (forall a. blah)
+--   (b) a predicate type (c => ty)
+--   (c) a type family; see Note [Prevent unification with type families]
 --   (d) a blocking coercion hole
 --   (e) an occurrence of the type variable (occurs check)
 --
@@ -2004,15 +2019,20 @@ preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
 -- inside the kinds of variables it mentions.  For (d) we look deeply
 -- in coercions, and for (e) we do look in the kinds of course.
 
-preCheck dflags ty_fam_ok tv ty
+mtvu_check dflags ty_fam_ok tv ty
   = fast_check ty
   where
-    details          = tcTyVarDetails tv
-    impredicative_ok = canUnifyWithPolyType dflags details
-
     ok :: MetaTyVarUpdateResult ()
     ok = MTVU_OK ()
 
+    -- The GHCi runtime debugger does its type-matching with
+    -- unification variables that can unify with a polytype
+    -- or a TyCon that would usually be disallowed by bad_tc
+    -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect
+    ghci_tv = case tcTyVarDetails tv of
+                MetaTv { mtv_info = RuntimeUnkTv } -> True
+                _                                  -> False
+
     fast_check :: TcType -> MetaTyVarUpdateResult ()
     fast_check (TyVarTy tv')
       | tv == tv' = MTVU_Occurs
@@ -2021,19 +2041,19 @@ preCheck dflags ty_fam_ok tv ty
            -- in GHC.Core.Type
 
     fast_check (TyConApp tc tys)
-      | bad_tc tc              = MTVU_Bad
+      | bad_tc tc, not ghci_tv = MTVU_Bad
       | otherwise              = mapM fast_check tys >> ok
     fast_check (LitTy {})      = ok
     fast_check (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
       | InvisArg <- af
-      , not impredicative_ok   = MTVU_Bad
+      , not ghci_tv            = MTVU_Bad
       | otherwise              = fast_check w   >> fast_check a >> fast_check r
     fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
     fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
     fast_check (CoercionTy co) = fast_check_co co
     fast_check (ForAllTy (Bndr tv' _) ty)
-       | not impredicative_ok = MTVU_Bad
-       | tv == tv'            = ok
+       | not ghci_tv = MTVU_Bad
+       | tv == tv'   = ok
        | otherwise = do { fast_check_occ (tyVarKind tv')
                         ; fast_check_occ ty }
        -- Under a forall we look only for occurrences of
@@ -2056,14 +2076,6 @@ preCheck dflags ty_fam_ok tv ty
 
     bad_tc :: TyCon -> Bool
     bad_tc tc
-      | not (impredicative_ok || isTauTyCon tc)     = True
-      | not (ty_fam_ok        || isFamFreeTyCon tc) = True
-      | otherwise                                   = False
-
-canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
-canUnifyWithPolyType dflags details
-  = case details of
-      MetaTv { mtv_info = TyVarTv }    -> False
-      MetaTv { mtv_info = TauTv }      -> xopt LangExt.ImpredicativeTypes dflags
-      _other                           -> True
-          -- We can have non-meta tyvars in given constraints
+      | not (isTauTyCon tc)                  = True
+      | not (ty_fam_ok || isFamFreeTyCon tc) = True
+      | otherwise                            = False
diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot
index a54107fe07..7b4561420c 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs-boot
+++ b/compiler/GHC/Tc/Utils/Unify.hs-boot
@@ -5,14 +5,14 @@ import GHC.Tc.Utils.TcType   ( TcTauType )
 import GHC.Tc.Types          ( TcM )
 import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper )
 import GHC.Tc.Types.Origin ( CtOrigin )
-import GHC.Hs.Expr      ( HsExpr )
-import GHC.Hs.Type     ( HsType, Mult )
-import GHC.Hs.Extension ( GhcRn )
+import GHC.Utils.Outputable( SDoc )
+import GHC.Hs.Type     ( Mult )
+
 
 -- This boot file exists only to tie the knot between
 --              GHC.Tc.Utils.Unify and Inst
 
-unifyType :: Maybe (HsExpr GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion
-unifyKind :: Maybe (HsType GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion
+unifyType :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion
+unifyKind :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion
 
 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 296dfa79a4..e00b5a09e3 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -723,6 +723,14 @@ zonkExpr env (HsVar x (L l id))
   = ASSERT2( isNothing (isDataConId_maybe id), ppr id )
     return (HsVar x (L l (zonkIdOcc env id)))
 
+zonkExpr env (HsUnboundVar v occ)
+  = return (HsUnboundVar (zonkIdOcc env v) occ)
+
+zonkExpr env (HsRecFld _ (Ambiguous v occ))
+  = return (HsRecFld noExtField (Ambiguous (zonkIdOcc env v) occ))
+zonkExpr env (HsRecFld _ (Unambiguous v occ))
+  = return (HsRecFld noExtField (Unambiguous (zonkIdOcc env v) occ))
+
 zonkExpr _ e@(HsConLikeOut {}) = return e
 
 zonkExpr _ (HsIPVar x id)
@@ -915,9 +923,6 @@ zonkExpr env (XExpr (WrapExpr (HsWrap co_fn expr)))
 zonkExpr env (XExpr (ExpansionExpr (HsExpanded a b)))
   = XExpr . ExpansionExpr . HsExpanded a <$> zonkExpr env b
 
-zonkExpr _ e@(HsUnboundVar {})
-  = return e
-
 zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr)
 
 -------------------------------------------------------------------------
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index f89ec4d966..e00b39b20e 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -456,7 +456,7 @@ instance Outputable Rank where
 
 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
 rankZeroMonoType   = MonoType (text "Perhaps you intended to use RankNTypes")
-tyConArgMonoType   = MonoType (text "GHC doesn't yet support impredicative polymorphism")
+tyConArgMonoType   = MonoType (text "Perhaps you intended to use ImpredicativeTypes")
 synArgMonoType     = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
 constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
                                     , text "Perhaps you intended to use QuantifiedConstraints" ])
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index b58ae7f38e..9665b5e4e2 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -475,6 +475,8 @@ Library
         GHC.Tc.Deriv.Utils
         GHC.Tc.Utils.Env
         GHC.Tc.Gen.Expr
+        GHC.Tc.Gen.App
+        GHC.Tc.Gen.Head
         GHC.Tc.Gen.Foreign
         GHC.Tc.Deriv.Generate
         GHC.Tc.Deriv.Functor