diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index d52f9cac65b774b1be096b28f768983deef4a356..290a9716e28c0e29b1d7602c756d7349837d4a17 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -293,7 +293,9 @@ data HsExpr p
 
   | HsApp     (XApp p) (LHsExpr p) (LHsExpr p) -- ^ Application
 
-  | HsAppType (XAppTypeE p) (LHsExpr p) (LHsWcType (NoGhcTc p))  -- ^ Visible type application
+  | HsAppType (XAppTypeE p) -- After typechecking: the type argument
+              (LHsExpr p)
+              (LHsWcType (NoGhcTc p))  -- ^ Visible type application
        --
        -- Explicit type argument; e.g  f @Int x y
        -- NB: Has wildcards, but no implicit quantification
@@ -599,7 +601,9 @@ type instance XLam           (GhcPass _) = NoExtField
 type instance XLamCase       (GhcPass _) = NoExtField
 type instance XApp           (GhcPass _) = NoExtField
 
-type instance XAppTypeE      (GhcPass _) = NoExtField
+type instance XAppTypeE      GhcPs = NoExtField
+type instance XAppTypeE      GhcRn = NoExtField
+type instance XAppTypeE      GhcTc = Type
 
 type instance XOpApp         GhcPs = NoExtField
 type instance XOpApp         GhcRn = Fixity
@@ -1214,8 +1218,12 @@ parenthesizeHsExpr p le@(L loc e)
   | hsExprNeedsParens p e = L loc (HsPar noExtField le)
   | otherwise             = le
 
-stripParensHsExpr :: LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
-stripParensHsExpr (L _ (HsPar _ e)) = stripParensHsExpr e
+stripParensLHsExpr :: LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
+stripParensLHsExpr (L _ (HsPar _ e)) = stripParensLHsExpr e
+stripParensLHsExpr e = e
+
+stripParensHsExpr :: HsExpr (GhcPass p) -> HsExpr (GhcPass p)
+stripParensHsExpr (HsPar _ (L _ e)) = stripParensHsExpr e
 stripParensHsExpr e = e
 
 isAtomicHsExpr :: forall p. IsPass p => HsExpr (GhcPass p) -> Bool
@@ -2566,7 +2574,7 @@ instance (OutputableBndrId p) => Outputable (HsSplice (GhcPass p)) where
 
 pprPendingSplice :: (OutputableBndrId p)
                  => SplicePointName -> LHsExpr (GhcPass p) -> SDoc
-pprPendingSplice n e = angleBrackets (ppr n <> comma <+> ppr (stripParensHsExpr e))
+pprPendingSplice n e = angleBrackets (ppr n <> comma <+> ppr (stripParensLHsExpr e))
 
 pprSpliceDecl ::  (OutputableBndrId p)
           => HsSplice (GhcPass p) -> SpliceExplicitFlag -> SDoc
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 5daa380819bd9f95d0aa4c6d844f163ca57e8d40..0b3300719ed4aad56e14b843c10c5a7097906d27 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -187,8 +187,7 @@ mkLocatedList ms = L (combineLocs (head ms) (last ms)) ms
 mkHsApp :: LHsExpr (GhcPass id) -> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
 mkHsApp e1 e2 = addCLoc e1 e2 (HsApp noExtField e1 e2)
 
-mkHsAppType :: (NoGhcTc (GhcPass id) ~ GhcRn)
-            => LHsExpr (GhcPass id) -> LHsWcType GhcRn -> LHsExpr (GhcPass id)
+mkHsAppType :: LHsExpr GhcRn -> LHsWcType GhcRn -> LHsExpr GhcRn
 mkHsAppType e t = addCLoc e t_body (HsAppType noExtField e paren_wct)
   where
     t_body    = hswc_body t
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index eaae002ea21986c232eae5d7ab85e159cb0492d7..5bd2326e628abfd30d283c5325345232a92f4d9f 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -316,9 +316,9 @@ dsExpr e@(HsApp _ fun arg)
        ; dsWhenNoErrs (dsLExprNoLP arg)
                       (\arg' -> mkCoreAppDs (text "HsApp" <+> ppr e) fun' arg') }
 
-dsExpr (HsAppType _ e _)
-    -- ignore type arguments here; they're in the wrappers instead at this point
-  = dsLExpr e
+dsExpr (HsAppType ty e _)
+  = do { e' <- dsLExpr e
+       ; return (App e' (Type ty)) }
 
 {-
 Note [Desugaring vars]
diff --git a/compiler/GHC/Rename/Splice.hs b/compiler/GHC/Rename/Splice.hs
index a0f0bb24194bbf32b24c5d17682e3e4744d9e94e..c8aa73554f2d9a586063f01faaf37eea9b8ddada 100644
--- a/compiler/GHC/Rename/Splice.hs
+++ b/compiler/GHC/Rename/Splice.hs
@@ -48,7 +48,7 @@ import GHC.Driver.Hooks
 import GHC.Builtin.Names.TH ( quoteExpName, quotePatName, quoteDecName, quoteTypeName
                             , decsQTyConName, expQTyConName, patQTyConName, typeQTyConName, )
 
-import {-# SOURCE #-} GHC.Tc.Gen.Expr   ( tcPolyExpr )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr   ( tcCheckExpr )
 import {-# SOURCE #-} GHC.Tc.Gen.Splice
     ( runMetaD
     , runMetaE
@@ -324,7 +324,7 @@ runRnSplice flavour run_meta ppr_res splice
        ; meta_exp_ty   <- tcMetaTy meta_ty_name
        ; zonked_q_expr <- zonkTopLExpr =<<
                             tcTopSpliceExpr Untyped
-                              (tcPolyExpr the_expr meta_exp_ty)
+                              (tcCheckExpr the_expr meta_exp_ty)
 
              -- Run the expression
        ; mod_finalizers_ref <- newTcRef []
@@ -760,7 +760,7 @@ traceSplice (SpliceInfo { spliceDescription = sd, spliceSource = mb_src
     spliceDebugDoc loc
       = let code = case mb_src of
                      Nothing -> ending
-                     Just e  -> nest 2 (ppr (stripParensHsExpr e)) : ending
+                     Just e  -> nest 2 (ppr (stripParensLHsExpr e)) : ending
             ending = [ text "======>", nest 2 gen ]
         in  hang (ppr loc <> colon <+> text "Splicing" <+> text sd)
                2 (sep code)
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 58bbb40da27723382c8a9a21b518cd5c4ab95d62..94e90acd246af0fb089edc0b21449806d15fa407 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -14,7 +14,7 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where
 
 import GhcPrelude
 
-import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcMonoExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcPolyExpr )
+import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcLExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcCheckExpr )
 
 import GHC.Hs
 import GHC.Tc.Gen.Match
@@ -91,7 +91,7 @@ tcProc pat cmd exp_ty
         ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
         ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
-        ; (pat', cmd') <- tcPat ProcExpr pat (mkCheckExpType arg_ty) $
+        ; (pat', cmd') <- tcCheckPat ProcExpr pat arg_ty $
                           tcCmdTop cmd_env cmd (unitTy, res_ty)
         ; let res_co = mkTcTransCo co
                          (mkTcAppCo co1 (mkTcNomReflCo res_ty))
@@ -160,7 +160,7 @@ tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty)
                               ; tcCmd env body (stk, res_ty') }
 
 tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty    -- Ordinary 'if'
-  = do  { pred' <- tcMonoExpr pred (mkCheckExpType boolTy)
+  = do  { pred' <- tcLExpr pred (mkCheckExpType boolTy)
         ; b1'   <- tcCmd env b1 res_ty
         ; b2'   <- tcCmd env b2 res_ty
         ; return (HsCmdIf x NoSyntaxExprTc pred' b1' b2')
@@ -178,7 +178,7 @@ tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syn
         ; (pred', fun')
             <- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty])
                                        (mkCheckExpType r_ty) $ \ _ ->
-               tcMonoExpr pred (mkCheckExpType pred_ty)
+               tcLExpr pred (mkCheckExpType pred_ty)
 
         ; b1'   <- tcCmd env b1 res_ty
         ; b2'   <- tcCmd env b2 res_ty
@@ -205,9 +205,9 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty)
   = addErrCtxt (cmdCtxt cmd)    $
     do  { arg_ty <- newOpenFlexiTyVarTy
         ; let fun_ty = mkCmdArrTy env arg_ty res_ty
-        ; fun' <- select_arrow_scope (tcMonoExpr fun (mkCheckExpType fun_ty))
+        ; fun' <- select_arrow_scope (tcLExpr fun (mkCheckExpType fun_ty))
 
-        ; arg' <- tcMonoExpr arg (mkCheckExpType arg_ty)
+        ; arg' <- tcLExpr arg (mkCheckExpType arg_ty)
 
         ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) }
   where
@@ -232,7 +232,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty)
   = addErrCtxt (cmdCtxt cmd)    $
     do  { arg_ty <- newOpenFlexiTyVarTy
         ; fun'   <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty)
-        ; arg'   <- tcMonoExpr arg (mkCheckExpType arg_ty)
+        ; arg'   <- tcLExpr arg (mkCheckExpType arg_ty)
         ; return (HsCmdApp x fun' arg') }
 
 -------------------------------------------
@@ -309,7 +309,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
         ; let e_ty = mkInvForAllTy alphaTyVar $
                      mkVisFunTys cmd_tys $
                      mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
-        ; expr' <- tcPolyExpr expr e_ty
+        ; expr' <- tcCheckExpr expr e_ty
         ; return (HsCmdArrForm x expr' f fixity cmd_args') }
 
   where
@@ -366,7 +366,7 @@ tcArrDoStmt env _ (BodyStmt _ rhs _ _) res_ty thing_inside
 
 tcArrDoStmt env ctxt (BindStmt _ pat rhs) res_ty thing_inside
   = do  { (rhs', pat_ty) <- tc_arr_rhs env rhs
-        ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+        ; (pat', thing)  <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                             thing_inside res_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 0773e943c78416282b875c3affbe210bb95a7239..a8a8d027f01b058c65b3c6bc3cd3c00db005da47 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -23,7 +23,7 @@ where
 import GhcPrelude
 
 import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun )
-import {-# SOURCE #-} GHC.Tc.Gen.Expr  ( tcMonoExpr )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr  ( tcLExpr )
 import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
 import GHC.Core (Tickish (..))
 import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC))
@@ -354,7 +354,7 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
        = do { ty <- newOpenFlexiTyVarTy
             ; let p = mkStrLitTy $ hsIPNameFS ip
             ; ip_id <- newDict ipClass [ p, ty ]
-            ; expr' <- tcMonoExpr expr (mkCheckExpType ty)
+            ; expr' <- tcLExpr expr (mkCheckExpType ty)
             ; let d = toDict ipClass p ty `fmap` expr'
             ; return (ip_id, (IPBind noExtField (Right ip_id) d)) }
     tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind"
@@ -1263,9 +1263,7 @@ tcMonoBinds is_rec sig_fn no_gen
         --      We want to infer a higher-rank type for f
     setSrcSpan b_loc    $
     do  { ((co_fn, matches'), rhs_ty)
-            <- tcInferInst $ \ exp_ty ->
-                  -- tcInferInst: see GHC.Tc.Utils.Unify,
-                  -- Note [Deep instantiation of InferResult] in GHC.Tc.Utils.Unify
+            <- tcInfer $ \ exp_ty ->
                tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
@@ -1362,7 +1360,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
             -- See Note [Existentials in pattern bindings]
         ; ((pat', nosig_mbis), pat_ty)
             <- addErrCtxt (patMonoBindsCtxt pat grhss) $
-               tcInferNoInst $ \ exp_ty ->
+               tcInfer $ \ exp_ty ->
                tcLetPat inst_sig_fun no_gen pat exp_ty $
                mapM lookup_info nosig_names
 
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 3048b78afaab7d04f1b0e70fecd42d24c336304f..70201773b962d5d1efc5064224f01d0efdf0114f 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -7,25 +7,22 @@
 
 {-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilies, DataKinds, TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
+                                      -- in module GHC.Hs.Extension
 
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 
 -- | Typecheck an expression
 module GHC.Tc.Gen.Expr
-   ( tcPolyExpr
-   , tcMonoExpr
-   , tcMonoExprNC
+   ( tcCheckExpr
+   , tcLExpr, tcLExprNC, tcExpr
    , tcInferSigma
-   , tcInferSigmaNC
-   , tcInferRho
-   , tcInferRhoNC
-   , tcSyntaxOp
-   , tcSyntaxOpGen
+   , tcInferRho, tcInferRhoNC
+   , tcSyntaxOp, tcSyntaxOpGen
    , SyntaxOpType(..)
    , synKnownType
    , tcCheckId
-   , addExprErrCtxt
    , addAmbiguousNameErr
    , getFixedTyVars
    )
@@ -48,7 +45,7 @@ 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 )
+import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst, tcLookupDataFamInst_maybe )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
 import GHC.Rename.Env         ( addUsedGRE )
 import GHC.Rename.Utils       ( addNameClashErrRn, unknownSubordinateErr )
@@ -78,7 +75,6 @@ import GHC.Core.Type
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
 import GHC.Builtin.Types
-import GHC.Builtin.Types.Prim( intPrimTy )
 import GHC.Builtin.PrimOps( tagToEnumKey )
 import GHC.Builtin.Names
 import GHC.Driver.Session
@@ -106,69 +102,47 @@ import qualified Data.Set as Set
 ************************************************************************
 -}
 
-tcPolyExpr, tcPolyExprNC
+tcCheckExpr, tcCheckExprNC
   :: LHsExpr GhcRn         -- Expression to type check
   -> TcSigmaType           -- Expected type (could be a polytype)
-  -> TcM (LHsExpr GhcTcId) -- Generalised expr with expected type
+  -> TcM (LHsExpr GhcTc) -- Generalised expr with expected type
 
--- tcPolyExpr is a convenient place (frequent but not too frequent)
+-- tcCheckExpr is a convenient place (frequent but not too frequent)
 -- place to add context information.
 -- The NC version does not do so, usually because the caller wants
 -- to do so himself.
 
-tcPolyExpr   expr res_ty = tc_poly_expr expr (mkCheckExpType res_ty)
-tcPolyExprNC expr res_ty = tc_poly_expr_nc expr (mkCheckExpType res_ty)
+tcCheckExpr expr res_ty
+  = addExprCtxt expr $
+    tcCheckExprNC expr res_ty
 
--- these versions take an ExpType
-tc_poly_expr, tc_poly_expr_nc :: LHsExpr GhcRn -> ExpSigmaType
-                              -> TcM (LHsExpr GhcTcId)
-tc_poly_expr expr res_ty
-  = addExprErrCtxt expr $
-    do { traceTc "tcPolyExpr" (ppr res_ty); tc_poly_expr_nc expr res_ty }
-
-tc_poly_expr_nc (L loc expr) res_ty
+tcCheckExprNC (L loc expr) res_ty
   = setSrcSpan loc $
-    do { traceTc "tcPolyExprNC" (ppr res_ty)
-       ; (wrap, expr')
-           <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
-              tcExpr expr res_ty
+    do { traceTc "tcCheckExprNC" (ppr res_ty)
+       ; (wrap, expr') <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty ->
+                          tcExpr expr (mkCheckExpType res_ty)
        ; return $ L loc (mkHsWrap wrap expr') }
 
 ---------------
-tcMonoExpr, tcMonoExprNC
-    :: LHsExpr GhcRn     -- Expression to type check
-    -> ExpRhoType        -- Expected type
-                         -- Definitely no foralls at the top
-    -> TcM (LHsExpr GhcTcId)
-
-tcMonoExpr expr res_ty
-  = addErrCtxt (exprCtxt expr) $
-    tcMonoExprNC expr res_ty
-
-tcMonoExprNC (L loc expr) res_ty
-  = setSrcSpan loc $
-    do  { expr' <- tcExpr expr res_ty
-        ; return (L loc expr') }
+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) }
 
 ---------------
-tcInferSigma, tcInferSigmaNC :: LHsExpr GhcRn -> TcM ( LHsExpr GhcTcId
-                                                    , TcSigmaType )
--- Infer a *sigma*-type.
-tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
+tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
+-- Infer a *rho*-type. The return type is always instantiated.
+tcInferRho le = addExprCtxt le (tcInferRhoNC le)
 
-tcInferSigmaNC (L loc expr)
+tcInferRhoNC (L loc expr)
   = setSrcSpan loc $
-    do { (expr', sigma) <- tcInferNoInst (tcExpr expr)
-       ; return (L loc expr', sigma) }
-
-tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcRhoType)
--- Infer a *rho*-type. The return type is always (shallowly) instantiated.
-tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)
-
-tcInferRhoNC expr
-  = do { (expr', sigma) <- tcInferSigmaNC expr
-       ; (wrap, rho) <- topInstantiate (lexprCtOrigin expr) sigma
-       ; return (mkLHsWrap wrap expr', rho) }
+    do { (expr', rho) <- tcInfer (tcExpr expr)
+       ; return (L loc expr', rho) }
 
 
 {-
@@ -181,28 +155,37 @@ tcInferRhoNC expr
 NB: The res_ty is always deeply skolemised.
 -}
 
-tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
+tcLExpr, tcLExprNC
+    :: LHsExpr GhcRn     -- Expression to type check
+    -> ExpRhoType        -- Expected type
+                         -- Definitely no foralls at the top
+    -> TcM (LHsExpr GhcTc)
+
+tcLExpr expr res_ty
+  = 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 = tcApp1 e res_ty
-tcExpr e@(HsAppType {}) res_ty = tcApp1 e res_ty
+tcExpr e@(HsApp {})     res_ty = tcApp e res_ty
+tcExpr e@(HsAppType {}) res_ty = tcApp e 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' <- tcMonoExprNC expr res_ty
+tcExpr (HsPar x expr) res_ty = do { expr' <- tcLExprNC expr res_ty
                                   ; return (HsPar x expr') }
 
 tcExpr (HsPragE x prag expr) res_ty
-  = do { expr' <- tcMonoExpr expr res_ty
-       ; return (HsPragE x (tc_prag prag) expr') }
-  where
-    tc_prag :: HsPragE GhcRn -> HsPragE GhcTc
-    tc_prag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-    tc_prag (HsPragCore x1 src lbl) = HsPragCore x1 src lbl
-    tc_prag (HsPragTick x1 src info srcInfo) = HsPragTick x1 src info srcInfo
+  = do { expr' <- tcLExpr expr res_ty
+       ; return (HsPragE x (tcExprPrag prag) expr') }
 
 tcExpr (HsOverLit x lit) res_ty
   = do  { lit' <- newOverloadedLit lit res_ty
@@ -212,7 +195,7 @@ tcExpr (NegApp x expr neg_expr) res_ty
   = do  { (expr', neg_expr')
             <- tcSyntaxOp NegateOrigin neg_expr [SynAny] res_ty $
                \[arg_ty] ->
-               tcMonoExpr expr (mkCheckExpType arg_ty)
+               tcLExpr expr (mkCheckExpType arg_ty)
         ; return (NegApp x expr' neg_expr') }
 
 tcExpr e@(HsIPVar _ x) res_ty
@@ -280,13 +263,9 @@ tcExpr e@(HsLamCase x matches) res_ty
               , text "requires"]
     match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
 
-tcExpr e@(ExprWithTySig _ expr sig_ty) res_ty
-  = do { let loc = getLoc (hsSigWcType sig_ty)
-       ; sig_info <- checkNoErrs $  -- Avoid error cascade
-                     tcUserTypeSig loc sig_ty Nothing
-       ; (expr', poly_ty) <- tcExprSig expr sig_info
-       ; let expr'' = ExprWithTySig noExtField expr' sig_ty
-       ; tcWrapResult e expr'' poly_ty res_ty }
+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]
@@ -351,7 +330,8 @@ 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) <- tcInferSigma arg1
+       ; (arg1', arg1_ty) <- addErrCtxt (funAppCtxt op arg1 1) $
+                             tcInferRhoNC arg1
 
        ; let doc   = text "The first argument of ($) takes"
              orig1 = lexprCtOrigin arg1
@@ -362,7 +342,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
          -- So: arg1_ty = arg2_ty -> op_res_ty
          -- where arg2_sigma maybe polymorphic; that's the point
 
-       ; arg2' <- tcArg op arg2 arg2_sigma 2
+       ; 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
@@ -392,7 +372,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
 
        ; tcWrapResult expr expr' op_res_ty res_ty }
 
-  | (L loc (HsRecFld _ (Ambiguous _ lbl))) <- op
+  | 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
@@ -403,21 +383,33 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
 
   | otherwise
   = do { traceTc "Non Application rule" (ppr op)
-       ; (wrap, op', [HsValArg arg1', HsValArg arg2'])
-           <- tcApp (Just $ mk_op_msg op)
-                     op [HsValArg arg1, HsValArg arg2] res_ty
-       ; return (mkHsWrap wrap $ OpApp fix arg1' op' arg2') }
+       ; (op', op_ty) <- tcInferRhoNC op
+
+       ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
+                  <- matchActualFunTys (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
 
 -- Right sections, equivalent to \ x -> x `op` expr, or
 --      \ x -> op x expr
 
 tcExpr expr@(SectionR x op arg2) res_ty
-  = do { (op', op_ty) <- tcInferFun op
+  = do { (op', op_ty) <- tcInferRhoNC op
        ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
                   <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
                                  (mkVisFunTy arg1_ty op_res_ty) res_ty
-       ; arg2' <- tcArg op arg2 arg2_ty 2
+       ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2
        ; return ( mkHsWrap wrap_res $
                   SectionR x (mkLHsWrap wrap_fun op') arg2' ) }
   where
@@ -427,7 +419,7 @@ tcExpr expr@(SectionR x op arg2) res_ty
     -- See #13285
 
 tcExpr expr@(SectionL x arg1 op) res_ty
-  = do { (op', op_ty) <- tcInferFun op
+  = do { (op', op_ty) <- tcInferRhoNC op
        ; dflags <- getDynFlags      -- Note [Left sections]
        ; let n_reqd_args | xopt LangExt.PostfixOperators dflags = 1
                          | otherwise                            = 2
@@ -437,7 +429,7 @@ tcExpr expr@(SectionL x arg1 op) res_ty
                                 n_reqd_args op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
                                  (mkVisFunTys arg_tys op_res_ty) res_ty
-       ; arg1' <- tcArg op arg1 arg1_ty 1
+       ; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1
        ; return ( mkHsWrap wrap_res $
                   SectionL x arg1' (mkLHsWrap wrap_fn op') ) }
   where
@@ -489,7 +481,7 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty
        ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty
        ; -- Drop levity vars, we don't care about them here
          let arg_tys' = drop arity arg_tys
-       ; expr' <- tcPolyExpr expr (arg_tys' `getNth` (alt - 1))
+       ; expr' <- tcCheckExpr expr (arg_tys' `getNth` (alt - 1))
        ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) }
 
 -- This will see the empty list only when -XOverloadedLists.
@@ -511,7 +503,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty
                                ; return (exprs', elt_ty) }
 
                      ; return $ ExplicitList elt_ty (Just fln') exprs' }
-     where tc_elt elt_ty expr = tcPolyExpr expr elt_ty
+     where tc_elt elt_ty expr = tcCheckExpr expr elt_ty
 
 {-
 ************************************************************************
@@ -523,7 +515,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty
 
 tcExpr (HsLet x (L l binds) expr) res_ty
   = do  { (binds', expr') <- tcLocalBinds binds $
-                             tcMonoExpr expr res_ty
+                             tcLExpr expr res_ty
         ; return (HsLet x (L l binds') expr') }
 
 tcExpr (HsCase x scrut matches) res_ty
@@ -546,22 +538,22 @@ tcExpr (HsCase x scrut matches) res_ty
                       mc_body = tcBody }
 
 tcExpr (HsIf x NoSyntaxExprRn pred b1 b2) res_ty    -- Ordinary 'if'
-  = do { pred' <- tcMonoExpr pred (mkCheckExpType boolTy)
+  = do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
        ; res_ty <- tauifyExpType res_ty
            -- Just like Note [Case branches must never infer a non-tau type]
            -- in GHC.Tc.Gen.Match (See #10619)
 
-       ; b1' <- tcMonoExpr b1 res_ty
-       ; b2' <- tcMonoExpr b2 res_ty
+       ; b1' <- tcLExpr b1 res_ty
+       ; b2' <- tcLExpr b2 res_ty
        ; return (HsIf x NoSyntaxExprTc pred' b1' b2') }
 
 tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty
   = do { ((pred', b1', b2'), fun')
            <- tcSyntaxOp IfOrigin fun [SynAny, SynAny, SynAny] res_ty $
               \ [pred_ty, b1_ty, b2_ty] ->
-              do { pred' <- tcPolyExpr pred pred_ty
-                 ; b1'   <- tcPolyExpr b1   b1_ty
-                 ; b2'   <- tcPolyExpr b2   b2_ty
+              do { pred' <- tcCheckExpr pred pred_ty
+                 ; b1'   <- tcCheckExpr b1   b1_ty
+                 ; b2'   <- tcCheckExpr b2   b2_ty
                  ; return (pred', b1', b2') }
        ; return (HsIf x fun' pred' b1' b2') }
 
@@ -600,7 +592,7 @@ tcExpr (HsStatic fvs expr) res_ty
             addErrCtxt (hang (text "In the body of a static form:")
                              2 (ppr expr)
                        ) $
-            tcPolyExprNC expr expr_ty
+            tcCheckExprNC expr expr_ty
 
         -- Check that the free variables of the static form are closed.
         -- It's OK to use nonDetEltsUniqSet here as the only side effects of
@@ -1004,10 +996,39 @@ tcExpr e@(HsRnBracketOut _ brack ps) res_ty
 ************************************************************************
 -}
 
-tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
+tcExpr other _ = pprPanic "tcLExpr" (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
+tcExprPrag (HsPragCore x1 src lbl) = HsPragCore x1 src lbl
+tcExprPrag (HsPragTick x1 src info srcInfo) = HsPragTick x1 src info srcInfo
+
+
+{- *********************************************************************
+*                                                                      *
+             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)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1017,11 +1038,11 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
 -}
 
 tcArithSeq :: Maybe (SyntaxExpr GhcRn) -> ArithSeqInfo GhcRn -> ExpRhoType
-           -> TcM (HsExpr GhcTcId)
+           -> TcM (HsExpr GhcTc)
 
 tcArithSeq witness seq@(From expr) res_ty
   = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr' <- tcPolyExpr expr elt_ty
+       ; expr' <- tcCheckExpr expr elt_ty
        ; enum_from <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromName [elt_ty]
        ; return $ mkHsWrap wrap $
@@ -1029,8 +1050,8 @@ tcArithSeq witness seq@(From expr) res_ty
 
 tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
   = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr1' <- tcPolyExpr expr1 elt_ty
-       ; expr2' <- tcPolyExpr expr2 elt_ty
+       ; expr1' <- tcCheckExpr expr1 elt_ty
+       ; expr2' <- tcCheckExpr expr2 elt_ty
        ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromThenName [elt_ty]
        ; return $ mkHsWrap wrap $
@@ -1038,8 +1059,8 @@ tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
 
 tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
   = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
-       ; expr1' <- tcPolyExpr expr1 elt_ty
-       ; expr2' <- tcPolyExpr expr2 elt_ty
+       ; expr1' <- tcCheckExpr expr1 elt_ty
+       ; expr2' <- tcCheckExpr expr2 elt_ty
        ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromToName [elt_ty]
        ; return $ mkHsWrap wrap $
@@ -1047,9 +1068,9 @@ tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
 
 tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
   = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
-        ; expr1' <- tcPolyExpr expr1 elt_ty
-        ; expr2' <- tcPolyExpr expr2 elt_ty
-        ; expr3' <- tcPolyExpr expr3 elt_ty
+        ; expr1' <- tcCheckExpr expr1 elt_ty
+        ; expr2' <- tcCheckExpr expr2 elt_ty
+        ; expr3' <- tcCheckExpr expr3 elt_ty
         ; eft <- newMethodFromName (ArithSeqOrigin seq)
                               enumFromThenToName [elt_ty]
         ; return $ mkHsWrap wrap $
@@ -1076,179 +1097,245 @@ arithSeqEltType (Just fl) res_ty
 ************************************************************************
 -}
 
--- HsArg is defined in GHC.Hs.Types
-
-wrapHsArgs :: (NoGhcTc (GhcPass id) ~ GhcRn)
-           => LHsExpr (GhcPass id)
-           -> [HsArg (LHsExpr (GhcPass id)) (LHsWcType GhcRn)]
-           -> LHsExpr (GhcPass id)
-wrapHsArgs f []                     = f
-wrapHsArgs f (HsValArg  a : args)   = wrapHsArgs (mkHsApp f a)          args
-wrapHsArgs f (HsTypeArg _ t : args) = wrapHsArgs (mkHsAppType f t)      args
-wrapHsArgs f (HsArgPar sp : args)   = wrapHsArgs (L sp $ HsPar noExtField f) args
-
-isHsValArg :: HsArg tm ty -> Bool
-isHsValArg (HsValArg {})  = True
-isHsValArg (HsTypeArg {}) = False
-isHsValArg (HsArgPar {})  = False
-
-isArgPar :: HsArg tm ty -> Bool
-isArgPar (HsArgPar {})  = True
-isArgPar (HsValArg {})  = False
-isArgPar (HsTypeArg {}) = False
-
-isArgPar_maybe :: HsArg a b -> Maybe (HsArg c d)
-isArgPar_maybe (HsArgPar sp) = Just $ HsArgPar sp
-isArgPar_maybe _ = Nothing
-
-type LHsExprArgIn  = HsArg (LHsExpr GhcRn)   (LHsWcType GhcRn)
-type LHsExprArgOut = HsArg (LHsExpr GhcTcId) (LHsWcType GhcRn)
-
-tcApp1 :: HsExpr GhcRn  -- either HsApp or HsAppType
-       -> ExpRhoType -> TcM (HsExpr GhcTcId)
-tcApp1 e res_ty
-  = do { (wrap, fun, args) <- tcApp Nothing (noLoc e) [] res_ty
-       ; return (mkHsWrap wrap $ unLoc $ wrapHsArgs fun args) }
-
-tcApp :: Maybe SDoc  -- like "The function `f' is applied to"
-                     -- or leave out to get exactly that message
-      -> LHsExpr GhcRn -> [LHsExprArgIn] -- Function and args
-      -> ExpRhoType -> TcM (HsWrapper, LHsExpr GhcTcId, [LHsExprArgOut])
-           -- (wrap, fun, args). For an ordinary function application,
-           -- these should be assembled as (wrap (fun args)).
-           -- But OpApp is slightly different, so that's why the caller
-           -- must assemble
-
-tcApp m_herald (L sp (HsPar _ fun)) args res_ty
-  = tcApp m_herald fun (HsArgPar sp : args) res_ty
-
-tcApp m_herald (L _ (HsApp _ fun arg1)) args res_ty
-  = tcApp m_herald fun (HsValArg arg1 : args) res_ty
-
-tcApp m_herald (L _ (HsAppType _ fun ty1)) args res_ty
-  = tcApp m_herald fun (HsTypeArg noSrcSpan ty1 : args) res_ty
-
-tcApp m_herald fun@(L loc (HsRecFld _ fld_lbl)) args res_ty
-  | Ambiguous _ lbl        <- fld_lbl  -- Still ambiguous
-  , HsValArg (L _ arg) : _ <- filterOut isArgPar args -- A value arg is first
-  , Just sig_ty     <- obviousSig arg  -- A type sig on the arg disambiguates
+{- 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
+                                    _     -> empty
+
+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
+         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)
-       ; tcFunApp m_herald fun (L loc tc_fun) fun_ty args res_ty }
+       ; tcInferApp_finish fun tc_fun fun_ty args }
 
-tcApp _m_herald (L loc (HsVar _ (L _ fun_id))) args res_ty
-  -- Special typing rule for tagToEnum#
-  | fun_id `hasKey` tagToEnumKey
-  , n_val_args == 1
-  = tcTagToEnum loc fun_id args res_ty
+  | otherwise  -- The wildly common case
+  = do { (tc_fun, fun_ty) <- set_fun_loc (tcInferAppHead fun)
+       ; tcInferApp_finish fun tc_fun fun_ty args }
   where
-    n_val_args = count isHsValArg args
-
-tcApp m_herald fun args res_ty
-  = do { (tc_fun, fun_ty) <- tcInferFun fun
-       ; tcFunApp m_herald fun tc_fun fun_ty args res_ty }
+    (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
 
 ---------------------
-tcFunApp :: Maybe SDoc  -- like "The function `f' is applied to"
-                        -- or leave out to get exactly that message
-         -> LHsExpr GhcRn                  -- Renamed function
-         -> LHsExpr GhcTcId -> TcSigmaType -- Function and its type
-         -> [LHsExprArgIn]                 -- Arguments
-         -> ExpRhoType                     -- Overall result type
-         -> TcM (HsWrapper, LHsExpr GhcTcId, [LHsExprArgOut])
-            -- (wrapper-for-result, fun, args)
-            -- For an ordinary function application,
-            -- these should be assembled as wrap_res[ fun args ]
-            -- But OpApp is slightly different, so that's why the caller
-            -- must assemble
-
--- tcFunApp deals with the general case;
--- the special cases are handled by tcApp
-tcFunApp m_herald rn_fun tc_fun fun_sigma rn_args res_ty
-  = do { let orig = lexprCtOrigin rn_fun
-
-       ; traceTc "tcFunApp" (ppr rn_fun <+> dcolon <+> ppr fun_sigma $$ ppr rn_args $$ ppr res_ty)
-       ; (wrap_fun, tc_args, actual_res_ty)
-           <- tcArgs rn_fun fun_sigma orig rn_args
-                     (m_herald `orElse` mk_app_msg rn_fun rn_args)
-
-            -- this is just like tcWrapResult, but the types don't line
-            -- up to call that function
-       ; wrap_res <- addFunResCtxt True (unLoc rn_fun) actual_res_ty res_ty $
-                     tcSubTypeDS_NC_O orig GenSigCtxt
-                       (Just $ unLoc $ wrapHsArgs rn_fun rn_args)
-                       actual_res_ty res_ty
-
-       ; return (wrap_res, mkLHsWrap wrap_fun tc_fun, tc_args) }
-
-mk_app_msg :: LHsExpr GhcRn -> [LHsExprArgIn] -> SDoc
-mk_app_msg fun args = sep [ text "The" <+> text what <+> quotes (ppr expr)
-                          , text "is applied to"]
-  where
-    what | null type_app_args = "function"
-         | otherwise          = "expression"
-    -- Include visible type arguments (but not other arguments) in the herald.
-    -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
-    expr = mkHsAppTypes fun type_app_args
-    type_app_args = [hs_ty | HsTypeArg _ hs_ty <- args]
+tcInferApp_finish
+    :: HsExpr GhcRn                 -- Renamed function
+    -> HsExpr GhcTc -> TcSigmaType  -- Function and its type
+    -> [LHsExprArgIn]               -- Arguments
+    -> TcM (HsExpr GhcTc, [LHsExprArgOut], TcSigmaType)
 
-mk_op_msg :: LHsExpr GhcRn -> SDoc
-mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
+tcInferApp_finish rn_fun tc_fun fun_sigma rn_args
+  = do { traceTc "tcInferApp_finish" $
+         vcat [ ppr rn_fun <+> dcolon <+> ppr fun_sigma, ppr rn_args ]
 
-----------------
-tcInferFun :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
--- Infer type of a function
-tcInferFun (L loc (HsVar _ (L _ name)))
-  = do { (fun, ty) <- setSrcSpan loc (tcInferId name)
-               -- Don't wrap a context around a plain Id
-       ; return (L loc fun, ty) }
+       ; (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args
 
-tcInferFun (L loc (HsRecFld _ f))
-  = do { (fun, ty) <- setSrcSpan loc (tcInferRecSelId f)
-               -- Don't wrap a context around a plain Id
-       ; return (L loc fun, ty) }
+       ; return (tc_fun, tc_args, actual_res_ty) }
 
-tcInferFun fun
-  = tcInferSigma fun
-      -- NB: tcInferSigma; see GHC.Tc.Utils.Unify
-      -- Note [Deep instantiation of InferResult] in GHC.Tc.Utils.Unify
+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 :: LHsExpr GhcRn   -- ^ The function itself (for err msgs only)
+tcArgs :: HsExpr GhcRn   -- ^ The function itself (for err msgs only)
        -> TcSigmaType    -- ^ the (uninstantiated) type of the function
-       -> CtOrigin       -- ^ the origin for the function's type
        -> [LHsExprArgIn] -- ^ the args
-       -> SDoc           -- ^ the herald for matchActualFunTys
-       -> TcM (HsWrapper, [LHsExprArgOut], TcSigmaType)
+       -> TcM ([LHsExprArgOut], TcSigmaType)
           -- ^ (a wrapper for the function, the tc'd args, result type)
-tcArgs fun orig_fun_ty fun_orig orig_args herald
-  = go [] 1 orig_fun_ty orig_args
+tcArgs fun orig_fun_ty orig_args
+  = go 1 [] orig_fun_ty orig_args
   where
-    -- Don't count visible type arguments when determining how many arguments
-    -- an expression is given in an arity mismatch error, since visible type
-    -- arguments reported as a part of the expression herald itself.
+    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.
-    orig_expr_args_arity = count isHsValArg orig_args
+    n_val_args = count isHsValArg orig_args
 
     fun_is_out_of_scope  -- See Note [VTA for out-of-scope functions]
       = case fun of
-          L _ (HsUnboundVar {}) -> True
-          _                     -> False
+          HsUnboundVar {} -> True
+          _               -> False
 
-    go _ _ fun_ty [] = return (idHsWrapper, [], fun_ty)
+    go :: Int           -- Which argment number this is (incl type args)
+       -> [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 acc_args n fun_ty (HsArgPar sp : args)
-      = do { (inner_wrap, args', res_ty) <- go acc_args n fun_ty args
-           ; return (inner_wrap, HsArgPar sp : args', res_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 acc_args n fun_ty (HsTypeArg l hs_ty_arg : args)
+    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 acc_args (n+1) fun_ty args
+      = go (n+1) so_far fun_ty args
 
       | otherwise
       = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty
@@ -1266,7 +1353,6 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                     ; 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
@@ -1276,30 +1362,19 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                                           , debugPprType inner_ty
                                           , debugPprType insted_ty ])
 
-                    ; (inner_wrap, args', res_ty)
-                        <- go acc_args (n+1) insted_ty args
-                   -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
-                    ; let inst_wrap = mkWpTyApps [ty_arg]
-                    ; return ( inner_wrap <.> inst_wrap <.> wrap1
-                             , HsTypeArg l hs_ty_arg : args'
+                    ; (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 acc_args n fun_ty (HsValArg arg : args)
+    go n so_far fun_ty (HsEValArg loc arg : args)
       = do { (wrap, [arg_ty], res_ty)
-               <- matchActualFunTysPart herald fun_orig (Just (unLoc fun)) 1 fun_ty
-                                        acc_args orig_expr_args_arity
-               -- wrap :: fun_ty "->" arg_ty -> res_ty
+               <- matchActualFunTysPart herald fun_orig (Just fun)
+                                        n_val_args so_far 1 fun_ty
            ; arg' <- tcArg fun arg arg_ty n
-           ; (inner_wrap, args', inner_res_ty)
-               <- go (arg_ty : acc_args) (n+1) res_ty args
-               -- inner_wrap :: res_ty "->" (map typeOf args') -> inner_res_ty
-           ; return ( mkWpFun idHsWrapper inner_wrap arg_ty res_ty doc <.> wrap
-                    , HsValArg arg' : args'
+           ; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args
+           ; return ( addArgWrap wrap $ HsEValArg loc arg' : args'
                     , inner_res_ty ) }
-      where
-        doc = text "When checking the" <+> speakNth n <+>
-              text "argument to" <+> quotes (ppr fun)
 
     ty_app_err ty arg
       = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty
@@ -1389,21 +1464,27 @@ and we had the visible type application
 -}
 
 ----------------
-tcArg :: LHsExpr GhcRn                   -- The function (for error messages)
+tcArg :: HsExpr GhcRn                   -- The function (for error messages)
       -> LHsExpr GhcRn                   -- Actual arguments
-      -> TcRhoType                       -- expected arg type
+      -> TcSigmaType                     -- expected arg type
       -> Int                             -- # of argument
-      -> TcM (LHsExpr GhcTcId)           -- Resulting argument
-tcArg fun arg ty arg_no = addErrCtxt (funAppCtxt fun arg arg_no) $
-                          tcPolyExprNC arg ty
+      -> TcM (LHsExpr GhcTc)           -- Resulting argument
+tcArg fun arg ty arg_no
+  = addErrCtxt (funAppCtxt fun arg arg_no) $
+    do { traceTc "tcArg {" $
+           vcat [ text "arg #" <> ppr arg_no <+> dcolon <+> ppr ty
+                , text "arg:" <+> ppr arg ]
+       ; arg' <- tcCheckExprNC arg ty
+       ; traceTc "tcArg }" empty
+       ; return arg' }
 
 ----------------
-tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTcId]
+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) = return (L l (Missing arg_ty))
-    go (L l (Present x expr), arg_ty) = do { expr' <- tcPolyExpr expr arg_ty
+    go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckExpr expr arg_ty
                                            ; return (L l (Present x expr')) }
 
 ---------------------------
@@ -1429,13 +1510,13 @@ tcSyntaxOpGen :: CtOrigin
               -> ([TcSigmaType] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside
-  = do { (expr, sigma) <- tcInferSigma $ noLoc op
+  = do { (expr, sigma) <- tcInferAppHead op
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
        ; (result, expr_wrap, arg_wraps, res_wrap)
            <- tcSynArgA orig sigma arg_tys res_ty $
               thing_inside
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma )
-       ; return (result, SyntaxExprTc { syn_expr = mkHsWrap expr_wrap $ unLoc expr
+       ; return (result, SyntaxExprTc { syn_expr = mkHsWrap expr_wrap expr
                                       , syn_arg_wraps = arg_wraps
                                       , syn_res_wrap  = res_wrap }) }
 tcSyntaxOpGen _ NoSyntaxExprRn _ _ _ = panic "tcSyntaxOpGen"
@@ -1511,7 +1592,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
         doc = text "When checking a rebindable syntax operator arising from" <+> ppr orig
 
     go rho_ty (SynType the_ty)
-      = do { wrap   <- tcSubTypeET orig GenSigCtxt the_ty rho_ty
+      = do { wrap   <- tcSubTypePat orig GenSigCtxt the_ty rho_ty
            ; result <- thing_inside []
            ; return (result, wrap) }
 
@@ -1608,7 +1689,7 @@ in the other order, the extra signature in f2 is reqd.
 *                                                                      *
 ********************************************************************* -}
 
-tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTcId, TcType)
+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 { (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
@@ -1621,7 +1702,7 @@ tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
              skol_tvs  = map snd tv_prs
        ; (ev_binds, expr') <- checkConstraints skol_info skol_tvs given $
                               tcExtendNameTyVarEnv tv_prs $
-                              tcPolyExprNC expr tau
+                              tcCheckExprNC expr tau
 
        ; let poly_wrap = mkWpTyLams   skol_tvs
                          <.> mkWpLams given
@@ -1635,7 +1716,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                 do { sig_inst <- tcInstSig sig
                    ; expr' <- tcExtendNameTyVarEnv (sig_inst_skols sig_inst) $
                               tcExtendNameTyVarEnv (sig_inst_wcs   sig_inst) $
-                              tcPolyExprNC expr (sig_inst_tau sig_inst)
+                              tcCheckExprNC expr (sig_inst_tau sig_inst)
                    ; return (expr', sig_inst) }
        -- See Note [Partial expression signatures]
        ; let tau = sig_inst_tau sig_inst
@@ -1703,19 +1784,23 @@ CLong, as it should.
 *                                                                      *
 ********************************************************************* -}
 
-tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTcId)
+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 (HsVar noExtField (noLoc name)) actual_res_ty res_ty $
+       ; addFunResCtxt False expr actual_res_ty res_ty $
          tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
-                                                          actual_res_ty res_ty }
+                                           actual_res_ty res_ty }
 
-tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
-tcCheckRecSelId rn_expr f@(Unambiguous _ (L _ lbl)) 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
-       ; addFunResCtxt False (HsRecFld noExtField f) actual_res_ty res_ty $
-         tcWrapResultO (OccurrenceOfRecSel lbl) rn_expr expr actual_res_ty res_ty }
+       ; 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
@@ -1724,7 +1809,7 @@ tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty
                                                     res_ty }
 
 ------------------------
-tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> TcM (HsExpr GhcTcId, TcRhoType)
+tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> TcM (HsExpr GhcTc, TcRhoType)
 tcInferRecSelId (Unambiguous sel (L _ lbl))
   = do { (expr', ty) <- tc_infer_id lbl sel
        ; return (expr', ty) }
@@ -1732,14 +1817,10 @@ tcInferRecSelId (Ambiguous _ lbl)
   = ambiguousSelector lbl
 
 ------------------------
-tcInferId :: Name -> TcM (HsExpr GhcTcId, TcSigmaType)
+tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
 -- Look up an occurrence of an Id
 -- Do not instantiate its type
 tcInferId id_name
-  | id_name `hasKey` tagToEnumKey
-  = failWithTc (text "tagToEnum# must appear applied to one argument")
-        -- tcApp catches the case (tagToEnum# arg)
-
   | id_name `hasKey` assertIdKey
   = do { dflags <- getDynFlags
        ; if gopt Opt_IgnoreAsserts dflags
@@ -1751,7 +1832,7 @@ tcInferId id_name
        ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty)
        ; return (expr, ty) }
 
-tc_infer_assert :: Name -> TcM (HsExpr GhcTcId, TcSigmaType)
+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
@@ -1761,7 +1842,7 @@ tc_infer_assert assert_name
        ; return (mkHsWrap wrap (HsVar noExtField (noLoc assert_error_id)), id_rho)
        }
 
-tc_infer_id :: RdrName -> Name -> TcM (HsExpr GhcTcId, TcSigmaType)
+tc_infer_id :: RdrName -> Name -> TcM (HsExpr GhcTc, TcSigmaType)
 tc_infer_id lbl id_name
  = do { thing <- tcLookup id_name
       ; case thing of
@@ -1812,7 +1893,7 @@ tc_infer_id lbl id_name
       | otherwise                  = return ()
 
 
-tcUnboundId :: HsExpr GhcRn -> OccName -> ExpRhoType -> TcM (HsExpr GhcTcId)
+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 "_".
@@ -1881,60 +1962,50 @@ the users that complain.
 
 -}
 
-tcTagToEnum :: SrcSpan -> Name -> [LHsExprArgIn] -> ExpRhoType
-            -> TcM (HsWrapper, LHsExpr GhcTcId, [LHsExprArgOut])
+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 loc fun_name args res_ty
-  = do { fun <- tcLookupId fun_name
-
-       ; let pars1 = mapMaybe isArgPar_maybe before
-             pars2 = mapMaybe isArgPar_maybe after
-             -- args contains exactly one HsValArg
-             (before, _:after) = break isHsValArg args
-
-       ; arg <- case filterOut isArgPar args of
-           [HsTypeArg _ hs_ty_arg, HsValArg term_arg]
-             -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind
-                   ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg res_ty
-                     -- other than influencing res_ty, we just
-                     -- don't care about a type arg passed in.
-                     -- So drop the evidence.
-                   ; return term_arg }
-           [HsValArg term_arg] -> do { _ <- expTypeToType res_ty
-                                     ; return term_arg }
-           _          -> too_many_args "tagToEnum#" args
-
-       ; res_ty <- readExpType res_ty
+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
-       ; let mb_tc_app = tcSplitTyConApp_maybe ty'
-             Just (tc, tc_args) = mb_tc_app
-       ; checkTc (isJust mb_tc_app)
-                 (mk_error ty' doc1)
+       ; case tcSplitTyConApp_maybe ty' of {
+           Nothing -> do { addErrTc (mk_error ty' doc1)
+                         ; vanilla_result } ;
+           Just (tc, tc_args) ->
 
-       -- Look through any type family
+    do { -- Look through any type family
        ; fam_envs <- tcGetFamInstEnvs
-       ; let (rep_tc, rep_args, coi)
-               = tcLookupDataFamInst fam_envs tc tc_args
-            -- coi :: tc tc_args ~R rep_tc rep_args
-
-       ; checkTc (isEnumerationTyCon rep_tc)
-                 (mk_error ty' doc2)
-
-       ; arg' <- tcMonoExpr arg (mkCheckExpType intPrimTy)
-       ; let fun' = L loc (mkHsWrap (WpTyApp rep_ty) (HsVar noExtField (L loc fun)))
-             rep_ty = mkTyConApp rep_tc rep_args
-             out_args = concat
-              [ pars1
-              , [HsValArg arg']
-              , pars2
-              ]
-
-       ; return (mkWpCastR (mkTcSymCo coi), fun', out_args) }
-                 -- coi is a Representational coercion
+       ; 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"
@@ -1945,18 +2016,6 @@ tcTagToEnum loc fun_name args res_ty
                <+> text "at type" <+> ppr ty)
            2 what
 
-too_many_args :: String -> [LHsExprArgIn] -> TcM a
-too_many_args fun args
-  = failWith $
-    hang (text "Too many type arguments to" <+> text fun <> colon)
-       2 (sep (map pp args))
-  where
-    pp :: LHsExprArgIn -> SDoc
-    pp (HsValArg e)                             = ppr e
-    pp (HsTypeArg _ (HsWC { hswc_body = L _ t })) = pprHsType t
-    pp (HsArgPar _) = empty
-
-
 {-
 ************************************************************************
 *                                                                      *
@@ -2368,7 +2427,7 @@ tcRecordBinds
         :: ConLike
         -> [TcType]     -- Expected type for each field
         -> HsRecordBinds GhcRn
-        -> TcM (HsRecordBinds GhcTcId)
+        -> TcM (HsRecordBinds GhcTc)
 
 tcRecordBinds con_like arg_tys (HsRecFields rbinds dd)
   = do  { mb_binds <- mapM do_bind rbinds
@@ -2378,7 +2437,7 @@ tcRecordBinds con_like arg_tys (HsRecFields rbinds dd)
     flds_w_tys = zipEqual "tcRecordBinds" fields arg_tys
 
     do_bind :: LHsRecField GhcRn (LHsExpr GhcRn)
-            -> TcM (Maybe (LHsRecField GhcTcId (LHsExpr GhcTcId)))
+            -> TcM (Maybe (LHsRecField GhcTc (LHsExpr GhcTc)))
     do_bind (L l fld@(HsRecField { hsRecFieldLbl = f
                                  , hsRecFieldArg = rhs }))
 
@@ -2392,7 +2451,7 @@ tcRecordUpd
         :: ConLike
         -> [TcType]     -- Expected type for each field
         -> [LHsRecField' (AmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)]
-        -> TcM [LHsRecUpdField GhcTcId]
+        -> TcM [LHsRecUpdField GhcTc]
 
 tcRecordUpd con_like arg_tys rbinds = fmap catMaybes $ mapM do_bind rbinds
   where
@@ -2400,7 +2459,7 @@ tcRecordUpd con_like arg_tys rbinds = fmap catMaybes $ mapM do_bind rbinds
     flds_w_tys = zipEqual "tcRecordUpd" fields arg_tys
 
     do_bind :: LHsRecField' (AmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)
-            -> TcM (Maybe (LHsRecUpdField GhcTcId))
+            -> TcM (Maybe (LHsRecUpdField GhcTc))
     do_bind (L l fld@(HsRecField { hsRecFieldLbl = L loc af
                                  , hsRecFieldArg = rhs }))
       = do { let lbl = rdrNameAmbiguousFieldOcc af
@@ -2423,7 +2482,7 @@ tcRecordField :: ConLike -> Assoc Name Type
 tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs
   | Just field_ty <- assocMaybe flds_w_tys sel_name
       = addErrCtxt (fieldCtxt field_lbl) $
-        do { rhs' <- tcPolyExprNC rhs field_ty
+        do { rhs' <- tcCheckExprNC rhs field_ty
            ; let field_id = mkUserLocal (nameOccName sel_name)
                                         (nameUnique sel_name)
                                         field_ty loc
@@ -2494,19 +2553,18 @@ checkMissingFields con_like rbinds
 Boring and alphabetical:
 -}
 
-addExprErrCtxt :: LHsExpr GhcRn -> TcM a -> TcM a
-addExprErrCtxt expr = addErrCtxt (exprCtxt expr)
-
-exprCtxt :: LHsExpr GhcRn -> SDoc
-exprCtxt expr
-  = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr))
-
 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 GhcRn -> TcType -> ExpRhoType
+              -> 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
diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot
index 27ebefc9a3587356f15765145800e23522088d24..d9138a4d7e9c657a9e00ff3b4340cd1d6a791f0b 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs-boot
+++ b/compiler/GHC/Tc/Gen/Expr.hs-boot
@@ -6,23 +6,16 @@ import GHC.Tc.Types        ( TcM )
 import GHC.Tc.Types.Origin ( CtOrigin )
 import GHC.Hs.Extension    ( GhcRn, GhcTcId )
 
-tcPolyExpr ::
-          LHsExpr GhcRn
-       -> TcSigmaType
-       -> TcM (LHsExpr GhcTcId)
-
-tcMonoExpr, tcMonoExprNC ::
-          LHsExpr GhcRn
-       -> ExpRhoType
-       -> TcM (LHsExpr GhcTcId)
-
-tcInferSigma ::
-          LHsExpr GhcRn
-       -> TcM (LHsExpr GhcTcId, TcSigmaType)
-
-tcInferRho, tcInferRhoNC ::
-          LHsExpr GhcRn
-       -> TcM (LHsExpr GhcTcId, TcRhoType)
+tcCheckExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId)
+
+tcLExpr, tcLExprNC
+       :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId)
+tcExpr :: HsExpr GhcRn  -> ExpRhoType -> TcM (HsExpr GhcTcId)
+
+tcInferRho, tcInferRhoNC
+  :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcRhoType)
+
+tcInferSigma :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcSigmaType)
 
 tcSyntaxOp :: CtOrigin
            -> SyntaxExprRn
diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs
index f1031d6e14359430bf08d4fa1d3f137655a76607..858d8650267a0cba814709082b1238d4dd6d4870 100644
--- a/compiler/GHC/Tc/Gen/Foreign.hs
+++ b/compiler/GHC/Tc/Gen/Foreign.hs
@@ -388,7 +388,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
   = addErrCtxt (foreignDeclCtxt fo) $ do
 
     sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
-    rhs <- tcPolyExpr (nlHsVar nm) sig_ty
+    rhs <- tcCheckExpr (nlHsVar nm) sig_ty
 
     (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
 
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 313ae9cf585fbfb5ccfe6d5e13de7b111fc37459..a25a7320e4d9210586fab059259786e8f76a8680 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -60,7 +60,7 @@ module GHC.Tc.Gen.HsType (
         checkClassKindSig,
 
         -- Pattern type signatures
-        tcHsPatSigType, tcPatSig,
+        tcHsPatSigType,
 
         -- Error messages
         funAppCtxt, addTyConFlavCtxt
@@ -75,7 +75,6 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Types.Origin
 import GHC.Core.Predicate
 import GHC.Tc.Types.Constraint
-import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity
@@ -3390,58 +3389,6 @@ tcHsPatSigType ctxt sig_ty
              -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
            ; return (name, tv) }
 
-tcPatSig :: Bool                    -- True <=> pattern binding
-         -> LHsSigWcType GhcRn
-         -> ExpSigmaType
-         -> TcM (TcType,            -- The type to use for "inside" the signature
-                 [(Name,TcTyVar)],  -- The new bit of type environment, binding
-                                    -- the scoped type variables
-                 [(Name,TcTyVar)],  -- The wildcards
-                 HsWrapper)         -- Coercion due to unification with actual ty
-                                    -- Of shape:  res_ty ~ sig_ty
-tcPatSig in_pat_bind sig res_ty
- = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
-        -- sig_tvs are the type variables free in 'sig',
-        -- and not already in scope. These are the ones
-        -- that should be brought into scope
-
-        ; if null sig_tvs then do {
-                -- Just do the subsumption check and return
-                  wrap <- addErrCtxtM (mk_msg sig_ty) $
-                          tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
-                ; return (sig_ty, [], sig_wcs, wrap)
-        } else do
-                -- Type signature binds at least one scoped type variable
-
-                -- A pattern binding cannot bind scoped type variables
-                -- It is more convenient to make the test here
-                -- than in the renamer
-        { when in_pat_bind (addErr (patBindSigErr sig_tvs))
-
-        -- Now do a subsumption check of the pattern signature against res_ty
-        ; wrap <- addErrCtxtM (mk_msg sig_ty) $
-                  tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
-
-        -- Phew!
-        ; return (sig_ty, sig_tvs, sig_wcs, wrap)
-        } }
-  where
-    mk_msg sig_ty tidy_env
-       = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
-            ; res_ty <- readExpType res_ty   -- should be filled in by now
-            ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
-            ; let msg = vcat [ hang (text "When checking that the pattern signature:")
-                                  4 (ppr sig_ty)
-                             , nest 2 (hang (text "fits the type of its context:")
-                                          2 (ppr res_ty)) ]
-            ; return (tidy_env, msg) }
-
-patBindSigErr :: [(Name,TcTyVar)] -> SDoc
-patBindSigErr sig_tvs
-  = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
-          <+> pprQuotedList (map fst sig_tvs))
-       2 (text "in a pattern binding signature")
-
 {- Note [Pattern signature binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Type variables in the type environment] in GHC.Tc.Utils.
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 339093b47c3d78fac0abdd8c15ca926188796e3c..45fece68c0b52da0b5abe8c7c0fa41c8e0a3e1bf 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -37,7 +37,8 @@ where
 import GhcPrelude
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRhoNC, tcInferRho
-                                     , tcCheckId, tcMonoExpr, tcMonoExprNC, tcPolyExpr )
+                                     , tcCheckId, tcLExpr, tcLExprNC, tcExpr
+                                     , tcCheckExpr )
 
 import GHC.Types.Basic (LexicalFixity(..))
 import GHC.Hs
@@ -331,7 +332,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt)
 tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId)
 tcBody body res_ty
   = do  { traceTc "tcBody" (ppr res_ty)
-        ; tcMonoExpr body res_ty
+        ; tcLExpr body res_ty
         }
 
 {-
@@ -411,15 +412,15 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside
 
 tcGuardStmt :: TcExprStmtChecker
 tcGuardStmt _ (BodyStmt _ guard _ _) res_ty thing_inside
-  = do  { guard' <- tcMonoExpr guard (mkCheckExpType boolTy)
+  = do  { guard' <- tcLExpr guard (mkCheckExpType boolTy)
         ; thing  <- thing_inside res_ty
         ; return (BodyStmt boolTy guard' noSyntaxExpr noSyntaxExpr, thing) }
 
 tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside
   = do  { (rhs', rhs_ty) <- tcInferRhoNC rhs
                                    -- Stmt has a context already
-        ; (pat', thing)  <- tcPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs)
-                                    pat (mkCheckExpType rhs_ty) $
+        ; (pat', thing)  <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs)
+                                         pat rhs_ty $
                             thing_inside res_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 
@@ -444,21 +445,21 @@ tcLcStmt :: TyCon       -- The list type constructor ([])
          -> TcExprStmtChecker
 
 tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside
-  = do { body' <- tcMonoExprNC body elt_ty
+  = do { body' <- tcLExprNC body elt_ty
        ; thing <- thing_inside (panic "tcLcStmt: thing_inside")
        ; return (LastStmt x body' noret noSyntaxExpr, thing) }
 
 -- A generator, pat <- rhs
 tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside
  = do   { pat_ty <- newFlexiTyVarTy liftedTypeKind
-        ; rhs'   <- tcMonoExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty])
-        ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+        ; rhs'   <- tcLExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty])
+        ; (pat', thing)  <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                             thing_inside elt_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 
 -- A boolean guard
 tcLcStmt _ _ (BodyStmt _ rhs _ _) elt_ty thing_inside
-  = do  { rhs'  <- tcMonoExpr rhs (mkCheckExpType boolTy)
+  = do  { rhs'  <- tcLExpr rhs (mkCheckExpType boolTy)
         ; thing <- thing_inside elt_ty
         ; return (BodyStmt boolTy rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
@@ -516,7 +517,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
                              by_arrow $
                              poly_arg_ty `mkVisFunTy` poly_res_ty
 
-       ; using' <- tcPolyExpr using using_poly_ty
+       ; using' <- tcCheckExpr using using_poly_ty
        ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
 
              -- 'stmts' returns a result of type (m1_ty tuple_ty),
@@ -558,7 +559,7 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside
   = do  { (body', return_op')
             <- tcSyntaxOp MCompOrigin return_op [SynRho] res_ty $
                \ [a_ty] ->
-               tcMonoExprNC body (mkCheckExpType a_ty)
+               tcLExprNC body (mkCheckExpType a_ty)
         ; thing      <- thing_inside (panic "tcMcStmt: thing_inside")
         ; return (LastStmt x body' noret return_op', thing) }
 
@@ -574,9 +575,8 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
             <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn)
                           [SynRho, SynFun SynAny SynRho] res_ty $
                \ [rhs_ty, pat_ty, new_res_ty] ->
-               do { rhs' <- tcMonoExprNC rhs (mkCheckExpType rhs_ty)
-                  ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat
-                                           (mkCheckExpType pat_ty) $
+               do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
+                  ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                      thing_inside (mkCheckExpType new_res_ty)
                   ; return (rhs', pat', thing, new_res_ty) }
 
@@ -607,7 +607,7 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside
                       <- tcSyntaxOp MCompOrigin guard_op [SynAny]
                                     (mkCheckExpType rhs_ty) $
                          \ [test_ty] ->
-                         tcMonoExpr rhs (mkCheckExpType test_ty)
+                         tcLExpr rhs (mkCheckExpType test_ty)
                   ; thing <- thing_inside (mkCheckExpType new_res_ty)
                   ; return (thing, rhs', rhs_ty, guard_op') }
         ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) }
@@ -667,7 +667,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
                            (mkCheckExpType using_arg_ty) $ \res_ty' -> do
                 { by' <- case by of
                            Nothing -> return Nothing
-                           Just e  -> do { e' <- tcMonoExpr e
+                           Just e  -> do { e' <- tcLExpr e
                                                    (mkCheckExpType by_e_ty)
                                          ; return (Just e') }
 
@@ -693,7 +693,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
        --------------- Typecheck the 'fmap' function -------------
        ; fmap_op' <- case form of
                        ThenForm -> return noExpr
-                       _ -> fmap unLoc . tcPolyExpr (noLoc fmap_op) $
+                       _ -> fmap unLoc . tcCheckExpr (noLoc fmap_op) $
                             mkInvForAllTy alphaTyVar $
                             mkInvForAllTy betaTyVar  $
                             (alphaTy `mkVisFunTy` betaTy)
@@ -703,7 +703,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
        --------------- Typecheck the 'using' function -------------
        -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c))
 
-       ; using' <- tcPolyExpr using using_poly_ty
+       ; using' <- tcCheckExpr using using_poly_ty
        ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
 
        --------------- Building the bindersMap ----------------
@@ -765,7 +765,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
                         (m_ty `mkAppTy` betaTy)
                         `mkVisFunTy`
                         (m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy])
-       ; mzip_op' <- unLoc `fmap` tcPolyExpr (noLoc mzip_op) mzip_ty
+       ; mzip_op' <- unLoc `fmap` tcCheckExpr (noLoc mzip_op) mzip_ty
 
         -- type dummies since we don't know all binder types yet
        ; id_tys_s <- (mapM . mapM) (const (newFlexiTyVarTy liftedTypeKind))
@@ -827,7 +827,7 @@ tcMcStmt _ stmt _ _
 tcDoStmt :: TcExprStmtChecker
 
 tcDoStmt _ (LastStmt x body noret _) res_ty thing_inside
-  = do { body' <- tcMonoExprNC body res_ty
+  = do { body' <- tcLExprNC body res_ty
        ; thing <- thing_inside (panic "tcDoStmt: thing_inside")
        ; return (LastStmt x body' noret noSyntaxExpr, thing) }
 
@@ -840,9 +840,8 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
           ((rhs', pat', new_res_ty, thing), bind_op')
             <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $
                 \ [rhs_ty, pat_ty, new_res_ty] ->
-                do { rhs' <- tcMonoExprNC rhs (mkCheckExpType rhs_ty)
-                   ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat
-                                            (mkCheckExpType pat_ty) $
+                do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
+                   ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                       thing_inside (mkCheckExpType new_res_ty)
                    ; return (rhs', pat', new_res_ty, thing) }
 
@@ -874,7 +873,7 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside
         ; ((rhs', rhs_ty, thing), then_op')
             <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $
                \ [rhs_ty, new_res_ty] ->
-               do { rhs' <- tcMonoExprNC rhs (mkCheckExpType rhs_ty)
+               do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
                   ; thing <- thing_inside (mkCheckExpType new_res_ty)
                   ; return (rhs', rhs_ty, thing) }
         ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) }
@@ -890,7 +889,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
 
         ; tcExtendIdEnv tup_ids $ do
         { ((stmts', (ret_op', tup_rets)), stmts_ty)
-                <- tcInferInst $ \ exp_ty ->
+                <- tcInfer $ \ exp_ty ->
                    tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty ->
                    do { tup_rets <- zipWithM tcCheckId tup_names
                                       (map mkCheckExpType tup_elt_tys)
@@ -902,7 +901,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
                       ; return (ret_op', tup_rets) }
 
         ; ((_, mfix_op'), mfix_res_ty)
-            <- tcInferInst $ \ exp_ty ->
+            <- tcInfer $ \ exp_ty ->
                tcSyntaxOp DoOrigin mfix_op
                           [synKnownType (mkVisFunTy tup_ty stmts_ty)] exp_ty $
                \ _ -> return ()
@@ -968,7 +967,7 @@ When typechecking
         do { bar; ... } :: IO ()
 we want to typecheck 'bar' in the knowledge that it should be an IO thing,
 pushing info from the context into the RHS.  To do this, we check the
-rebindable syntax first, and push that information into (tcMonoExprNC rhs).
+rebindable syntax first, and push that information into (tcLExprNC rhs).
 Otherwise the error shows up when checking the rebindable syntax, and
 the expected/inferred stuff is back to front (see #3613).
 
@@ -1000,7 +999,7 @@ tcApplicativeStmts
 tcApplicativeStmts ctxt pairs rhs_ty thing_inside
  = do { body_ty <- newFlexiTyVarTy liftedTypeKind
       ; let arity = length pairs
-      ; ts <- replicateM (arity-1) $ newInferExpTypeInst
+      ; ts <- replicateM (arity-1) $ newInferExpType
       ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
       ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
       ; let fun_ty = mkVisFunTys pat_tys body_ty
@@ -1044,8 +1043,8 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
                     }, pat_ty, exp_ty)
       = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $
         addErrCtxt (pprStmtInCtxt ctxt (mkRnBindStmt pat rhs))   $
-        do { rhs' <- tcMonoExprNC rhs (mkCheckExpType exp_ty)
-           ; (pat', _) <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+        do { rhs' <- tcLExprNC rhs (mkCheckExpType exp_ty)
+           ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                           return ()
            ; fail_op' <- fmap join . forM fail_op $ \fail ->
                tcMonadFailOp (DoPatOrigin pat) pat' fail body_ty
@@ -1061,8 +1060,8 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
       = do { (stmts', (ret',pat')) <-
                 tcStmtsAndThen ctxt tcDoStmt stmts (mkCheckExpType exp_ty) $
                 \res_ty  -> do
-                  { L _ ret' <- tcMonoExprNC (noLoc ret) res_ty
-                  ; (pat', _) <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+                  { ret'      <- tcExpr ret res_ty
+                  ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                  return ()
                   ; return (ret', pat')
                   }
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 9b3318a78f65db87ffc568aba2e7950f8d9b7e51..2ae1f1cfb9f8d5c9d176d687062c5ba85456c676 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -16,8 +16,7 @@ module GHC.Tc.Gen.Pat
    ( tcLetPat
    , newLetBndr
    , LetBndrSpec(..)
-   , tcPat
-   , tcPat_O
+   , tcCheckPat, tcCheckPat_O, tcInferPat
    , tcPats
    , addDataConStupidTheta
    , badFieldCon
@@ -63,6 +62,7 @@ import Util
 import Outputable
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Arrow  ( second )
+import Control.Monad  ( when )
 import ListSetOps ( getNth )
 
 {-
@@ -112,20 +112,29 @@ tcPats ctxt pats pat_tys thing_inside
   where
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
 
-tcPat :: HsMatchContext GhcRn
-      -> LPat GhcRn -> ExpSigmaType
-      -> TcM a                     -- Checker for body
-      -> TcM (LPat GhcTcId, a)
-tcPat ctxt = tcPat_O ctxt PatOrigin
+tcInferPat :: HsMatchContext GhcRn -> LPat GhcRn
+           -> TcM a
+           -> TcM ((LPat GhcTcId, a), TcSigmaType)
+tcInferPat ctxt pat thing_inside
+  = tcInfer $ \ exp_ty ->
+    tc_lpat pat exp_ty penv thing_inside
+ where
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
+
+tcCheckPat :: HsMatchContext GhcRn
+           -> LPat GhcRn -> TcSigmaType
+           -> TcM a                     -- Checker for body
+           -> TcM (LPat GhcTcId, a)
+tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
 
 -- | A variant of 'tcPat' that takes a custom origin
-tcPat_O :: HsMatchContext GhcRn
-        -> CtOrigin              -- ^ origin to use if the type needs inst'ing
-        -> LPat GhcRn -> ExpSigmaType
-        -> TcM a                 -- Checker for body
-        -> TcM (LPat GhcTcId, a)
-tcPat_O ctxt orig pat pat_ty thing_inside
-  = tc_lpat pat pat_ty penv thing_inside
+tcCheckPat_O :: HsMatchContext GhcRn
+             -> CtOrigin              -- ^ origin to use if the type needs inst'ing
+             -> LPat GhcRn -> TcSigmaType
+             -> TcM a                 -- Checker for body
+             -> TcM (LPat GhcTcId, a)
+tcCheckPat_O ctxt orig pat pat_ty thing_inside
+  = tc_lpat pat (mkCheckExpType pat_ty) penv thing_inside
   where
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
 
@@ -199,7 +208,7 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl    = bind_lvl
   -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
 
   | Just bndr_id <- sig_fn bndr_name   -- There is a signature
-  = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id)
+  = do { wrap <- tc_sub_type penv exp_pat_ty (idType bndr_id)
            -- See Note [Subsumption check at pattern variables]
        ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
        ; return (wrap, bndr_id) }
@@ -243,10 +252,10 @@ newLetBndr LetLclBndr name ty
 newLetBndr (LetGblBndr prags) name ty
   = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
 
-tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
+tc_sub_type :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
 -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
--- Used when typechecking patterns
-tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2
+-- Used during typechecking patterns
+tc_sub_type penv t1 t2 = tcSubTypePat (pe_orig penv) GenSigCtxt t1 t2
 
 {- Note [Subsumption check at pattern variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -390,22 +399,31 @@ tc_pat penv (AsPat x (L nm_loc name) pat) pat_ty thing_inside
 
 tc_pat penv (ViewPat _ expr pat) overall_pat_ty thing_inside
   = do  {
-         -- Expr must have type `forall a1...aN. OPT' -> B`
-         -- where overall_pat_ty is an instance of OPT'.
-        ; (expr',expr'_inferred) <- tcInferSigma expr
-
-         -- expression must be a function
+         -- We use tcInferRho here.
+         -- If we have a view function with types like:
+         --    blah -> forall b. burble
+         -- then simple-subsumption means that 'forall b' won't be instantiated
+         -- so we can typecheck the inner pattern with that type
+         -- An exotic example:
+         --    pair :: forall a. a -> forall b. b -> (a,b)
+         --    f (pair True -> x) = ...here (x :: forall b. b -> (Bool,b))
+         --
+         -- TEMPORARY: pending simple subsumption, use tcInferSigma
+         -- When removing this, remove it from Expr.hs-boot too
+        ; (expr',expr_ty) <- tcInferSigma expr
+
+         -- Expression must be a function
         ; let expr_orig = lexprCtOrigin expr
               herald    = text "A view pattern expression expects"
         ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
-            <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr'_inferred
-            -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
+            <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr_ty
+            -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty)
 
-         -- check that overall pattern is more polymorphic than arg type
-        ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
+         -- Check that overall pattern is more polymorphic than arg type
+        ; expr_wrap2 <- tc_sub_type penv overall_pat_ty inf_arg_ty
             -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
 
-         -- pattern must have inf_res_ty
+         -- Pattern must have inf_res_ty
         ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside
 
         ; overall_pat_ty <- readExpType overall_pat_ty
@@ -510,7 +528,7 @@ tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
 -- Literal patterns
 tc_pat penv (LitPat x simple_lit) pat_ty thing_inside
   = do  { let lit_ty = hsLitType simple_lit
-        ; wrap   <- tcSubTypePat penv pat_ty lit_ty
+        ; wrap   <- tc_sub_type penv pat_ty lit_ty
         ; res    <- thing_inside
         ; pat_ty <- readExpType pat_ty
         ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty
@@ -665,6 +683,66 @@ because they won't be in scope when we do the desugaring
 
 
 ************************************************************************
+*                                                                      *
+            Pattern signatures   (pat :: type)
+*                                                                      *
+************************************************************************
+-}
+
+tcPatSig :: Bool                    -- True <=> pattern binding
+         -> LHsSigWcType GhcRn
+         -> ExpSigmaType
+         -> TcM (TcType,            -- The type to use for "inside" the signature
+                 [(Name,TcTyVar)],  -- The new bit of type environment, binding
+                                    -- the scoped type variables
+                 [(Name,TcTyVar)],  -- The wildcards
+                 HsWrapper)         -- Coercion due to unification with actual ty
+                                    -- Of shape:  res_ty ~ sig_ty
+tcPatSig in_pat_bind sig res_ty
+ = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
+        -- sig_tvs are the type variables free in 'sig',
+        -- and not already in scope. These are the ones
+        -- that should be brought into scope
+
+        ; if null sig_tvs then do {
+                -- Just do the subsumption check and return
+                  wrap <- addErrCtxtM (mk_msg sig_ty) $
+                          tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
+                ; return (sig_ty, [], sig_wcs, wrap)
+        } else do
+                -- Type signature binds at least one scoped type variable
+
+                -- A pattern binding cannot bind scoped type variables
+                -- It is more convenient to make the test here
+                -- than in the renamer
+        { when in_pat_bind (addErr (patBindSigErr sig_tvs))
+
+        -- Now do a subsumption check of the pattern signature against res_ty
+        ; wrap <- addErrCtxtM (mk_msg sig_ty) $
+                  tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
+
+        -- Phew!
+        ; return (sig_ty, sig_tvs, sig_wcs, wrap)
+        } }
+  where
+    mk_msg sig_ty tidy_env
+       = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
+            ; res_ty <- readExpType res_ty   -- should be filled in by now
+            ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
+            ; let msg = vcat [ hang (text "When checking that the pattern signature:")
+                                  4 (ppr sig_ty)
+                             , nest 2 (hang (text "fits the type of its context:")
+                                          2 (ppr res_ty)) ]
+            ; return (tidy_env, msg) }
+
+patBindSigErr :: [(Name,TcTyVar)] -> SDoc
+patBindSigErr sig_tvs
+  = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
+          <+> pprQuotedList (map fst sig_tvs))
+       2 (text "in a pattern binding signature")
+
+
+{- *********************************************************************
 *                                                                      *
         Most of the work for constructors is here
         (the rest is in the ConPatIn case of tc_pat)
@@ -855,7 +933,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
               prov_theta' = substTheta tenv prov_theta
               req_theta'  = substTheta tenv req_theta
 
-        ; wrap <- tcSubTypePat penv pat_ty ty'
+        ; wrap <- tc_sub_type penv pat_ty ty'
         ; traceTc "tcPatSynPat" (ppr pat_syn $$
                                  ppr pat_ty $$
                                  ppr ty' $$
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index eaa0534770e1687c79f5362d68fa3f23480e5d35..35b20acaa89cf0bed1e3456394d36a0bbb2d0616 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -199,7 +199,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
     do { -- See Note [Solve order for RULES]
          ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
        ; (rhs',            rhs_wanted) <- captureConstraints $
-                                          tcMonoExpr rhs (mkCheckExpType rule_ty)
+                                          tcLExpr rhs (mkCheckExpType rule_ty)
        ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
        ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
 
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 87b23a8b274ccf7a4a25e1fbbbeee5c882810a8a..830e17abd4b905724e46b5c7357c63d27dd94221 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -286,7 +286,7 @@ tcPendingSplice m_var (PendingRnSplice flavour splice_name expr)
   = do { meta_ty <- tcMetaTy meta_ty_name
          -- Expected type of splice, e.g. m Exp
        ; let expected_type = mkAppTy m_var meta_ty
-       ; expr' <- tcPolyExpr expr expected_type
+       ; expr' <- tcCheckExpr expr expected_type
        ; return (PendingTcSplice splice_name expr') }
   where
      meta_ty_name = case flavour of
@@ -616,7 +616,7 @@ tcNestedSplice pop_stage (TcPending ps_var lie_var q@(QuoteWrapper _ m_var)) spl
        ; meta_exp_ty <- tcTExpTy m_var res_ty
        ; expr' <- setStage pop_stage $
                   setConstraintVar lie_var $
-                  tcMonoExpr expr (mkCheckExpType meta_exp_ty)
+                  tcLExpr expr (mkCheckExpType meta_exp_ty)
        ; untypeq <- tcLookupId unTypeQName
        ; let expr'' = mkHsApp
                         (mkLHsWrap (applyQuoteWrapper q)
@@ -639,7 +639,7 @@ tcTopSplice expr res_ty
        -- Top level splices must still be of type Q (TExp a)
        ; meta_exp_ty <- tcTExpTy q_type res_ty
        ; q_expr <- tcTopSpliceExpr Typed $
-                          tcMonoExpr expr (mkCheckExpType meta_exp_ty)
+                          tcLExpr expr (mkCheckExpType meta_exp_ty)
        ; lcl_env <- getLclEnv
        ; let delayed_splice
               = DelayedSplice lcl_env expr res_ty q_expr
@@ -676,7 +676,7 @@ runTopSplice (DelayedSplice lcl_env orig_expr res_ty q_expr)
             captureConstraints $
               addErrCtxt (spliceResultDoc zonked_q_expr) $ do
                 { (exp3, _fvs) <- rnLExpr expr2
-                ; tcMonoExpr exp3 (mkCheckExpType zonked_ty)}
+                ; tcLExpr exp3 (mkCheckExpType zonked_ty)}
        ; ev <- simplifyTop wcs
        ; return $ unLoc (mkHsDictLet (EvBinds ev) res)
        }
@@ -709,7 +709,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc)
 -- Note that set the level to Splice, regardless of the original level,
 -- before typechecking the expression.  For example:
 --      f x = $( ...$(g 3) ... )
--- The recursive call to tcPolyExpr will simply expand the
+-- The recursive call to tcCheckExpr will simply expand the
 -- inner escape before dealing with the outer one
 
 tcTopSpliceExpr isTypedSplice tc_action
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 17f2dd69d5a03e6e7bce09ff8949873ee344981a..cc3bf4a2cc8d386fbe8940807f3eb662e301a798 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -56,7 +56,6 @@ import GHC.Iface.Env     ( externaliseName )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Validity( checkValidType )
 import GHC.Tc.Gen.Match
-import GHC.Tc.Utils.Instantiate( deeplyInstantiate )
 import GHC.Tc.Utils.Unify( checkConstraints )
 import GHC.Rename.HsType
 import GHC.Rename.Expr
@@ -1785,8 +1784,8 @@ check_main dflags tcg_env explicit_mod_hdr export_ies
         ; (ev_binds, main_expr)
                <- checkConstraints skol_info [] [] $
                   addErrCtxt mainCtxt    $
-                  tcMonoExpr (L loc (HsVar noExtField (L loc main_name)))
-                             (mkCheckExpType io_ty)
+                  tcLExpr (L loc (HsVar noExtField (L loc main_name)))
+                          (mkCheckExpType io_ty)
 
                 -- See Note [Root-main Id]
                 -- Construct the binding
@@ -2491,15 +2490,11 @@ tcRnExpr hsc_env mode rdr_expr
         -- 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)
-        ; orig = lexprCtOrigin rn_expr } ;
-    ((tclvl, res_ty), lie)
+    let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
+    ((tclvl, (_tc_expr, res_ty)), lie)
           <- captureTopConstraints $
              pushTcLevelM          $
-             do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr
-                ; if inst
-                  then snd <$> deeplyInstantiate orig expr_ty
-                  else return expr_ty } ;
+             tc_infer rn_expr ;
 
     -- Generalise
     (qtvs, dicts, _, residual, _)
@@ -2525,12 +2520,35 @@ 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]
+
     -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
       TM_Inst    -> (True,  NoRestrictions, id)
       TM_NoInst  -> (False, NoRestrictions, id)
       TM_Default -> (True,  EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults)
 
+{- Note [Implementing :type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider   :type const
+
+We want    forall a b. a -> b -> a
+and not    forall {a}{b}. a -> b -> a
+
+The latter is what we'd get if we eagerly instantiated and then
+re-generalised with Inferred binders.  It makes a difference, because
+it tells us we where we can use Visible Type Application (VTA).
+
+And also for   :type const @Int
+we want        forall b. Int -> b -> Int
+and not        forall {b}. Int -> b -> Int
+
+Solution: use tcInferSigma, which in turn uses tcInferApp, which
+has a special case for application chains.
+-}
+
 --------------------------
 tcRnImportDecls :: HscEnv
                 -> [LImportDecl GhcPs]
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 0a719d90d2f063a558bd0eabd9e24cd726a9967f..797ff2f59440cb8a35a25ce1decd40bc6c312b55 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -147,8 +147,7 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
        ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
        ; (tclvl, wanted, ((lpat', args), pat_ty))
             <- pushLevelAndCaptureConstraints  $
-               tcInferNoInst                   $ \ exp_ty ->
-               tcPat PatSyn lpat exp_ty        $
+               tcInferPat PatSyn lpat          $
                mapM tcLookupId arg_names
 
        ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
@@ -386,9 +385,9 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
        ; req_dicts <- newEvVars req_theta
        ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
-           pushLevelAndCaptureConstraints            $
-           tcExtendTyVarEnv univ_tvs                 $
-           tcPat PatSyn lpat (mkCheckExpType pat_ty) $
+           pushLevelAndCaptureConstraints   $
+           tcExtendTyVarEnv univ_tvs        $
+           tcCheckPat PatSyn lpat pat_ty    $
            do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
                     empty_subst = mkEmptyTCvSubst in_scope
               ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index d67cc711507be6541b9d74d7645d576a7ece6ef7..86427853de0399f85fd934c7b192b377fb49ebc3 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -474,7 +474,7 @@ exprCtOrigin :: HsExpr GhcRn -> CtOrigin
 exprCtOrigin (HsVar _ (L _ name)) = OccurrenceOf name
 exprCtOrigin (HsUnboundVar _ uv)  = UnboundOccurrenceOf uv
 exprCtOrigin (HsConLikeOut {})    = panic "exprCtOrigin HsConLikeOut"
-exprCtOrigin (HsRecFld _ f)    = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
+exprCtOrigin (HsRecFld _ f)       = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
 exprCtOrigin (HsOverLabel _ _ l)  = OverLabelOrigin l
 exprCtOrigin (HsIPVar _ ip)       = IPOccOrigin ip
 exprCtOrigin (HsOverLit _ lit)    = LiteralOrigin lit
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index e896c7851ee6f8ee23f58fb90a2ee8fbe7aaaf07..7e45b5d947e5e698d48ef44713b640243b6094ff 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -36,7 +36,7 @@ module GHC.Tc.Utils.Instantiate (
 
 import GhcPrelude
 
-import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcPolyExpr, tcSyntaxOp )
+import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckExpr, tcSyntaxOp )
 import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType, unifyKind )
 
 import GHC.Types.Basic ( IntegralLit(..), SourceText(..) )
@@ -639,7 +639,7 @@ tcSyntaxName orig ty (std_nm, user_nm_expr) = do
         -- same type as the standard one.
         -- Tiresome jiggling because tcCheckSigma takes a located expression
      span <- getSrcSpanM
-     expr <- tcPolyExpr (L span user_nm_expr) sigma1
+     expr <- tcCheckExpr (L span user_nm_expr) sigma1
      return (std_nm, unLoc expr)
 
 syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 0b84f6909655d620319d4d93c1544738a5c1f12f..918a71594d06f6aa76299c5edfd4149f85535cf8 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -835,9 +835,8 @@ addLocM :: (a -> TcM b) -> Located a -> TcM b
 addLocM fn (L loc a) = setSrcSpan loc $ fn a
 
 wrapLocM :: (a -> TcM b) -> Located a -> TcM (Located b)
--- wrapLocM :: (a -> TcM b) -> Located a -> TcM (Located b)
 wrapLocM fn (L loc a) = setSrcSpan loc $ do { b <- fn a
-                                                ; return (L loc b) }
+                                            ; return (L loc b) }
 
 wrapLocFstM :: (a -> TcM (b,c)) -> Located a -> TcM (Located b, c)
 wrapLocFstM fn (L loc a) =
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 53b93f51a3d91e93037e4870e4f173366bbf724d..d37b37efe382679ed8ff9dcee2241ea21f2863f8 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -33,7 +33,7 @@ module GHC.Tc.Utils.TcMType (
   -- Expected types
   ExpType(..), ExpSigmaType, ExpRhoType,
   mkCheckExpType,
-  newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
+  newInferExpType,
   readExpType, readExpType_maybe,
   expTypeToType, checkingExpType_maybe, checkingExpType,
   tauifyExpType, inferResultToType,
@@ -440,21 +440,14 @@ test gadt/gadt-escape1.
 
 -- actual data definition is in GHC.Tc.Utils.TcType
 
--- | Make an 'ExpType' suitable for inferring a type of kind * or #.
-newInferExpTypeNoInst :: TcM ExpSigmaType
-newInferExpTypeNoInst = newInferExpType False
-
-newInferExpTypeInst :: TcM ExpRhoType
-newInferExpTypeInst = newInferExpType True
-
-newInferExpType :: Bool -> TcM ExpType
-newInferExpType inst
+newInferExpType :: TcM ExpType
+newInferExpType
   = do { u <- newUnique
        ; tclvl <- getTcLevel
-       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
+       ; traceTc "newInferExpType" (ppr u <+> ppr tclvl)
        ; ref <- newMutVar Nothing
        ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
-                           , ir_ref = ref, ir_inst = inst })) }
+                           , ir_ref = ref })) }
 
 -- | Extract a type out of an ExpType, if one exists. But one should always
 -- exist. Unless you're quite sure you know what you're doing.
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 8e1cef1a865b734c337f0d59ef16e58093d8768e..dc1ef3a69e34aa1b0f2d9886a95badefabe7ecb1 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -368,13 +368,6 @@ data InferResult
 
        , ir_lvl  :: TcLevel -- See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType
 
-       , ir_inst :: Bool
-         -- True <=> deeply instantiate before returning
-         --           i.e. return a RhoType
-         -- False <=> do not instantiate before returning
-         --           i.e. return a SigmaType
-         -- See Note [Deep instantiation of InferResult] in GHC.Tc.Utils.Unify
-
        , ir_ref  :: IORef (Maybe TcType) }
          -- The type that fills in this hole should be a Type,
          -- that is, its kind should be (TYPE rr) for some rr
@@ -387,9 +380,8 @@ instance Outputable ExpType where
   ppr (Infer ir) = ppr ir
 
 instance Outputable InferResult where
-  ppr (IR { ir_uniq = u, ir_lvl = lvl
-          , ir_inst = inst })
-    = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
+  ppr (IR { ir_uniq = u, ir_lvl = lvl })
+    = text "Infer" <> braces (ppr u <> comma <> ppr lvl)
 
 -- | Make an 'ExpType' suitable for checking.
 mkCheckExpType :: TcType -> ExpType
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index c6b0f8bae4561dd43619c456b3a5807f394ad34d..6a4d61627bbbf40dc51d9301d7f736d6d3441972 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -15,7 +15,7 @@ module GHC.Tc.Utils.Unify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
   tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
-  tcSubTypeDS_NC_O, tcSubTypeET,
+  tcSubTypeDS_NC_O, tcSubTypePat,
   checkConstraints, checkTvConstraints,
   buildImplicationFor, emitResidualTvConstraint,
 
@@ -26,7 +26,7 @@ module GHC.Tc.Utils.Unify (
 
   --------------------------------
   -- Holes
-  tcInferInst, tcInferNoInst,
+  tcInfer,
   matchExpectedListTy,
   matchExpectedTyConApp,
   matchExpectedAppTy,
@@ -193,14 +193,14 @@ matchExpectedFunTys herald arity orig_ty thing_inside
        --
        -- But in that case we add specialized type into error context
        -- anyway, because it may be useful. See also #9605.
-    go acc_arg_tys n ty = addErrCtxtM mk_ctxt $
+    go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
                           defer acc_arg_tys n (mkCheckExpType ty)
 
     ------------
     defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
     defer acc_arg_tys n fun_ty
-      = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
-           ; res_ty       <- newInferExpTypeInst
+      = do { more_arg_tys <- replicateM n newInferExpType
+           ; res_ty       <- newInferExpType
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM readExpType more_arg_tys
            ; res_ty       <- readExpType res_ty
@@ -210,15 +210,12 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; return (result, wrap) }
 
     ------------
-    mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
-    mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_tc_ty
-                     ; let (args, _) = tcSplitFunTys ty
-                           n_actual = length args
-                           (env'', orig_ty') = tidyOpenType env' orig_tc_ty
-                     ; return ( env''
-                              , mk_fun_tys_msg orig_ty' ty n_actual arity herald) }
+    mk_ctxt :: [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) }
       where
-        orig_tc_ty = checkingExpType "matchExpectedFunTys" orig_ty
+        arg_tys' = map (checkingExpType "matchExpectedFunTys") (reverse arg_tys)
             -- this is safe b/c we're called from "go"
 
 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
@@ -231,22 +228,28 @@ matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
 -- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
 -- then  wrap : ty ~> (t1 -> ... -> tn -> ty_r)
-matchActualFunTys herald ct_orig mb_thing arity ty
-  = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
+matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty
+  = matchActualFunTysPart herald ct_orig mb_thing
+                          n_val_args_wanted []
+                          n_val_args_wanted fun_ty
 
 -- | Variant of 'matchActualFunTys' that works when supplied only part
 -- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
-                      -> CtOrigin
-                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
-                      -> Arity
-                      -> TcSigmaType
-                      -> [TcSigmaType] -- reversed args. See (*) below.
-                      -> Arity   -- overall arity of the function, for errs
-                      -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
-matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
-                      orig_old_args full_arity
-  = go arity orig_old_args orig_ty
+matchActualFunTysPart
+  :: SDoc -- See Note [Herald for matchExpectedFunTys]
+  -> CtOrigin
+  -> Maybe (HsExpr GhcRn)  -- The thing with type TcSigmaType
+  -> Arity                 -- Total number of value args in the call
+  -> [TcSigmaType]         -- Types of values args to which function has
+                           --   been applied already (reversed)
+  -> Arity                 -- Number of new value args wanted
+  -> TcSigmaType           -- Type to analyse
+  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+-- See Note [matchActualFunTys error handling] for all these arguments
+matchActualFunTysPart herald ct_orig mb_thing
+                      n_val_args_in_call arg_tys_so_far
+                      n_val_args_wanted fun_ty
+  = go n_val_args_wanted arg_tys_so_far 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
@@ -274,36 +277,38 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
     --
     -- Refactoring is welcome.
     go :: Arity
-       -> [TcSigmaType] -- accumulator of arguments (reversed)
+       -> [TcSigmaType] -- Types of value args to which the function has
+                        -- been applied so far (reversed)
+                        -- Used only for error messages
        -> TcSigmaType   -- the remainder of the type as we're processing
        -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
     go 0 _ ty = return (idHsWrapper, [], ty)
 
-    go n acc_args ty
+    go n so_far ty
       | not (null tvs && null theta)
       = do { (wrap1, rho) <- topInstantiate ct_orig ty
-           ; (wrap2, arg_tys, res_ty) <- go n acc_args rho
+           ; (wrap2, arg_tys, res_ty) <- go n so_far rho
            ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
       where
         (tvs, theta, _) = tcSplitSigmaTy ty
 
-    go n acc_args ty
-      | Just ty' <- tcView ty = go n acc_args ty'
+    go n so_far ty
+      | Just ty' <- tcView ty = go n so_far ty'
 
-    go n acc_args (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+    go n so_far (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
       = ASSERT( af == VisArg )
-        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
+        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty:so_far) res_ty
            ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
                     , arg_ty : tys, ty_r ) }
       where
         doc = text "When inferring the argument type of a function with type" <+>
-              quotes (ppr orig_ty)
+              quotes (ppr fun_ty)
 
-    go n acc_args ty@(TyVarTy tv)
+    go n so_far ty@(TyVarTy tv)
       | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
-               Indirect ty' -> go n acc_args ty'
+               Indirect ty' -> go n so_far ty'
                Flexi        -> defer n ty }
 
        -- In all other cases we bale out into ordinary unification
@@ -321,8 +326,7 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
        --
        -- But in that case we add specialized type into error context
        -- anyway, because it may be useful. See also #9605.
-    go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
-                       defer n ty
+    go n so_far ty = addErrCtxtM (mk_ctxt so_far ty) (defer n ty)
 
     ------------
     defer n fun_ty
@@ -333,32 +337,47 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
            ; return (mkWpCastN co, arg_tys, res_ty) }
 
     ------------
-    mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+    mk_ctxt :: [TcType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
     mk_ctxt arg_tys res_ty env
-      = do { let ty = mkVisFunTys arg_tys res_ty
-           ; (env1, zonked) <- zonkTidyTcType env ty
-                   -- zonking might change # of args
-           ; let (zonked_args, _) = tcSplitFunTys zonked
-                 n_actual         = length zonked_args
-                 (env2, unzonked) = tidyOpenType env1 ty
-           ; return ( env2
-                    , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) }
-
-mk_fun_tys_msg :: TcType  -- the full type passed in (unzonked)
-               -> TcType  -- the full type passed in (zonked)
-               -> Arity   -- the # of args found
-               -> Arity   -- the # of args wanted
-               -> SDoc    -- overall herald
-               -> SDoc
-mk_fun_tys_msg full_ty ty n_args full_arity herald
-  = herald <+> speakNOf full_arity (text "argument") <> comma $$
-    if n_args == full_arity
-      then text "its type is" <+> quotes (pprType full_ty) <>
-           comma $$
-           text "it is specialized to" <+> quotes (pprType ty)
-      else sep [text "but its type" <+> quotes (pprType ty),
-                if n_args == 0 then text "has none"
-                else text "has only" <+> speakN n_args]
+      = do { (env', ty) <- zonkTidyTcType env $
+                           mkVisFunTys (reverse arg_tys) res_ty
+           ; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) }
+
+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!
+-}
 
 ----------------------
 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
@@ -550,11 +569,11 @@ tcSubTypeHR :: CtOrigin               -- ^ of the actual type
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
 ------------------------
-tcSubTypeET :: CtOrigin -> UserTypeCtxt
+tcSubTypePat :: CtOrigin -> UserTypeCtxt
             -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
 -- If wrap = tc_sub_type_et t1 t2
 --    => wrap :: t1 ~> t2
-tcSubTypeET orig ctxt (Check ty_actual) ty_expected
+tcSubTypePat orig ctxt (Check ty_actual) ty_expected
   = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
   where
     eq_orig = TypeEqOrigin { uo_actual   = ty_expected
@@ -562,14 +581,9 @@ tcSubTypeET orig ctxt (Check ty_actual) ty_expected
                            , uo_thing    = Nothing
                            , uo_visible  = True }
 
-tcSubTypeET _ _ (Infer inf_res) ty_expected
-  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
-      -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never
-      -- has the ir_inst field set.  Reason: in patterns (which is what
-      -- tcSubTypeET is used for) do not aggressively instantiate
-    do { co <- fill_infer_result ty_expected inf_res
-               -- Since ir_inst is false, we can skip fillInferResult
-               -- and go straight to fill_infer_result
+tcSubTypePat _ _ (Infer inf_res) ty_expected
+  = do { co <- fillInferResult ty_expected inf_res
+               -- In patterns we do not instantatiate
 
        ; return (mkWpCastN (mkTcSymCo co)) }
 
@@ -643,7 +657,7 @@ tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
 -- ty_expected is deeply skolemised
 tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
   = case ty_expected of
-      Infer inf_res -> fillInferResult inst_orig ty_actual inf_res
+      Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res
       Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
          where
            eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
@@ -864,44 +878,32 @@ tcWrapResultO orig rn_expr expr actual_ty res_ty
 
 {- **********************************************************************
 %*                                                                      *
-            ExpType functions: tcInfer, fillInferResult
+            ExpType functions: tcInfer, instantiateAndFillInferResult
 %*                                                                      *
 %********************************************************************* -}
 
 -- | Infer a type using a fresh ExpType
 -- See also Note [ExpType] in GHC.Tc.Utils.TcMType
--- Does not attempt to instantiate the inferred type
-tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInferNoInst = tcInfer False
-
-tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
-tcInferInst = tcInfer True
-
-tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInfer instantiate tc_check
-  = do { res_ty <- newInferExpType instantiate
+tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer tc_check
+  = do { res_ty <- newInferExpType
        ; result <- tc_check res_ty
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = fillInferResult t1 t2
+instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = instantiateAndFillInferResult t1 t2
 --    => wrap :: t1 ~> t2
--- See Note [Deep instantiation of InferResult]
-fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
-  | instantiate_me
+-- See Note [Instantiation of InferResult]
+instantiateAndFillInferResult orig ty inf_res
   = do { (wrap, rho) <- deeplyInstantiate orig ty
-       ; co <- fill_infer_result rho inf_res
+       ; co <- fillInferResult rho inf_res
        ; return (mkWpCastN co <.> wrap) }
 
-  | otherwise
-  = do { co <- fill_infer_result ty inf_res
-       ; return (mkWpCastN co) }
-
-fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fill_infer_result t1 t2
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fillInferResult t1 t2
 --    => wrap :: t1 ~> t2
-fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
                             , ir_ref = ref })
   = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
 
@@ -927,14 +929,12 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
                                              , ppr already_there ])
                Nothing -> return () }
 
-{- Note [Deep instantiation of InferResult]
+{- Note [Instantiation of InferResult]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In some cases we want to deeply instantiate before filling in
-an InferResult, and in some cases not.  That's why InferReult
-has the ir_inst flag.
+We now always instantiate before filling in InferResult, so that
+the result is a TcRhoType: see #17173 for discussion.
 
-ir_inst = True: deeply instantiate
-----------------------------------
+For example:
 
 1. Consider
     f x = (*)
@@ -954,41 +954,16 @@ ir_inst = True: deeply instantiate
    Here want to instantiate f's type so that the ?x::Int constraint
    gets discharged by the enclosing implicit-parameter binding.
 
-ir_inst = False: do not instantiate
------------------------------------
-
-1. Consider this (which uses visible type application):
-
-    (let { f :: forall a. a -> a; f x = x } in f) @Int
-
-   We'll call GHC.Tc.Gen.Expr.tcInferFun to infer the type of the (let .. in f)
-   And we don't want to instantiate the type of 'f' when we reach it,
-   else the outer visible type application won't work
-
-2. :type +v. When we say
-
-     :type +v const @Int
+3. Suppose one defines plus = (+). If we instantiate lazily, we will
+   infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
+   restriction compels us to infer
+      plus :: Integer -> Integer -> Integer
+   (or similar monotype). Indeed, the only way to know whether to apply
+   the monomorphism restriction at all is to instantiate
 
-   we really want `forall b. Int -> b -> Int`. Note that this is *not*
-   instantiated.
-
-3. Pattern bindings. For example:
-
-     foo x
-       | blah <- const @Int
-       = (blah x False, blah x 'z')
-
-   Note that `blah` is polymorphic. (This isn't a terribly compelling
-   reason, but the choice of ir_inst does matter here.)
-
-Discussion
-----------
-We thought that we should just remove the ir_inst flag, in favor of
-always instantiating. Essentially: motivations (1) and (3) for ir_inst = False
-are not terribly exciting. However, motivation (2) is quite important.
-Furthermore, there really was not much of a simplification of the code
-in removing ir_inst, and working around it to enable flows like what we
-see in (2) is annoying. This was done in #17173.
+There is one place where we don't want to instantiate eagerly,
+namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
+command. See Note [Implementing :type] in GHC.Tc.Module.
 
 -}
 
@@ -1187,8 +1162,8 @@ checkConstraints skol_info skol_tvs given thing_inside
                  ; emitImplications implics
                  ; return (ev_binds, result) }
 
-         else -- Fast path.  We check every function argument with
-              -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
+         else -- Fast path.  We check every function argument with tcCheckExpr,
+              -- which uses tcSkolemise and hence checkConstraints.
               -- So this fast path is well-exercised
               do { res <- thing_inside
                  ; return (emptyTcEvBinds, res) } }
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 4cf02d41e00b4dd726b73a193394a76d222a4a85..00f11c09ae7b896ada53d2f3ed928b631eb99d95 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -754,9 +754,10 @@ zonkExpr env (HsApp x e1 e2)
        new_e2 <- zonkLExpr env e2
        return (HsApp x new_e1 new_e2)
 
-zonkExpr env (HsAppType x e t)
+zonkExpr env (HsAppType ty e t)
   = do new_e <- zonkLExpr env e
-       return (HsAppType x new_e t)
+       new_ty <- zonkTcTypeToTypeX env ty
+       return (HsAppType new_ty new_e t)
        -- NB: the type is an HsType; can't zonk that!
 
 zonkExpr _ e@(HsRnBracketOut _ _ _)
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index 4d151d0ab127cfb660a692cc66039a9afd106155..2d142800caef9234c261cd0b4c955687e5fad449 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -69,6 +69,16 @@ Language
   There is a chance we will tweak the lookup scheme in the future, to make this
   workaround unnecessary.
 
+* GHC now consistently does eager instantiation during type inference.
+  As a consequence, visible type application (VTA) now only works when
+  the head of the application is:
+  * A variable
+  * An expression with a type signature
+  For example `(let x = blah in id) @Bool True` no longer typechecks.
+  You should write `let x = blah in id @Bool True` instead.
+
+  This change prepares the way for Quick Look impredicativity.
+
 Compiler
 ~~~~~~~~
 
diff --git a/libraries/base/tests/T9681.stderr b/libraries/base/tests/T9681.stderr
index af6e7dc63a406ce85a03cb6ecaadf3f91684f842..c3a2f2c3c7d65e63be7a168c55ac8d569535de30 100644
--- a/libraries/base/tests/T9681.stderr
+++ b/libraries/base/tests/T9681.stderr
@@ -1,5 +1,5 @@
 
-T9681.hs:3:7: error:
-    No instance for (Num [Char]) arising from a use of ‘+’
-    In the expression: 1 + "\n"
-    In an equation for ‘foo’: foo = 1 + "\n"
+T9681.hs:3:9: error:
+    • No instance for (Num [Char]) arising from a use of ‘+’
+    • In the expression: 1 + "\n"
+      In an equation for ‘foo’: foo = 1 + "\n"
diff --git a/testsuite/tests/ado/T13242a.stderr b/testsuite/tests/ado/T13242a.stderr
index 039830e63a73f195ec468bd0dc7b6d1fbdfd5b79..9e32035ebb268712a126ac928d2cb7e4793d6f63 100644
--- a/testsuite/tests/ado/T13242a.stderr
+++ b/testsuite/tests/ado/T13242a.stderr
@@ -11,7 +11,7 @@ T13242a.hs:10:5: error:
            _ <- return 'a'
            _ <- return 'b'
            return (x == x)
-    • In an equation for ‘test’:
+      In an equation for ‘test’:
           test
             = do A x <- undefined
                  _ <- return 'a'
@@ -19,7 +19,7 @@ T13242a.hs:10:5: error:
                  return (x == x)
     • Relevant bindings include x :: a (bound at T13242a.hs:10:5)
 
-T13242a.hs:13:11: error:
+T13242a.hs:13:13: error:
     • Ambiguous type variable ‘a0’ arising from a use of ‘==’
       prevents the constraint ‘(Eq a0)’ from being solved.
       Relevant bindings include x :: a0 (bound at T13242a.hs:10:5)
@@ -27,12 +27,12 @@ T13242a.hs:13:11: error:
       These potential instances exist:
         instance Eq Ordering -- Defined in ‘GHC.Classes’
         instance Eq Integer
-          -- Defined in ‘integer-gmp-1.0.2.0:GHC.Integer.Type’
+          -- Defined in ‘integer-gmp-1.0.3.0:GHC.Integer.Type’
         instance Eq () -- Defined in ‘GHC.Classes’
         ...plus 21 others
         ...plus six instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
-      In a stmt of a 'do' block: return (x == x)
+    • In a stmt of a 'do' block: return (x == x)
       In the expression:
         do A x <- undefined
            _ <- return 'a'
diff --git a/testsuite/tests/ado/ado002.stderr b/testsuite/tests/ado/ado002.stderr
index c2fb6b63b1cd0aaf1f9248304ace5011c0f1d50e..d7c0b6da68aeb3a20d5b4fc1a5f266511d135c12 100644
--- a/testsuite/tests/ado/ado002.stderr
+++ b/testsuite/tests/ado/ado002.stderr
@@ -2,8 +2,8 @@
 ado002.hs:8:8: error:
     • Couldn't match expected type ‘Char -> IO b0’
                   with actual type ‘IO Char’
-    • The function ‘getChar’ is applied to one argument,
-      but its type ‘IO Char’ has none
+    • The function ‘getChar’ is applied to one value argument,
+        but its type ‘IO Char’ has none
       In a stmt of a 'do' block: y <- getChar 'a'
       In the expression:
         do x <- getChar
@@ -45,8 +45,8 @@ ado002.hs:15:13: error:
 ado002.hs:23:9: error:
     • Couldn't match expected type ‘Char -> IO t0’
                   with actual type ‘IO Char’
-    • The function ‘getChar’ is applied to one argument,
-      but its type ‘IO Char’ has none
+    • The function ‘getChar’ is applied to one value argument,
+        but its type ‘IO Char’ has none
       In a stmt of a 'do' block: x5 <- getChar x4
       In the expression:
         do x1 <- getChar
diff --git a/testsuite/tests/annotations/should_fail/annfail08.stderr b/testsuite/tests/annotations/should_fail/annfail08.stderr
index 47a54243fefc11aa1510a25952c12189876cc7f6..6fafaf919ecef1ce16e70cbb0d73db620da3d02e 100644
--- a/testsuite/tests/annotations/should_fail/annfail08.stderr
+++ b/testsuite/tests/annotations/should_fail/annfail08.stderr
@@ -5,7 +5,7 @@ annfail08.hs:9:1: error:
         (maybe you haven't applied a function to enough arguments?)
     • In the annotation: {-# ANN f (id + 1) #-}
 
-annfail08.hs:9:12: error:
+annfail08.hs:9:15: error:
     • No instance for (Num (a0 -> a0)) arising from a use of ‘+’
         (maybe you haven't applied a function to enough arguments?)
     • In the annotation: {-# ANN f (id + 1) #-}
diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr
index 770135a3380c7609d14ed99c58a0a153328bf91a..6689c717bb287b5ac6699df18ae49666c4e904b5 100644
--- a/testsuite/tests/driver/T2182.stderr
+++ b/testsuite/tests/driver/T2182.stderr
@@ -5,7 +5,7 @@ T2182.hs:5:5: error:
     • In the expression: show (\ x -> x)
       In an equation for ‘y’: y = show (\ x -> x)
 
-T2182.hs:6:5: error:
+T2182.hs:6:15: error:
     • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
         (maybe you haven't applied a function to enough arguments?)
     • In the expression: (\ x -> x) == (\ y -> y)
@@ -17,7 +17,7 @@ T2182.hs:5:5: error:
     • In the expression: show (\ x -> x)
       In an equation for ‘y’: y = show (\ x -> x)
 
-T2182.hs:6:5: error:
+T2182.hs:6:15: error:
     • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
         (maybe you haven't applied a function to enough arguments?)
     • In the expression: (\ x -> x) == (\ y -> y)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 6673ff68b0892193449c599f2fc21eaa80482e02..cea221944b6ba21316cf38f1383beea1ddac6539 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -8,10 +8,10 @@ gadt13.hs:15:13: error:
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
       ‘p’ is a rigid type variable bound by
-        the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30
+        the inferred type of shw :: Term a -> p
+        at gadt13.hs:15:1-30
       Possible fix: add a type signature for ‘shw’
-    • Possible cause: ‘(.)’ is applied to too many arguments
-      In the expression: ("I " ++) . shows t
+    • In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
         shw :: Term a -> p (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index 63dbc9b0427db158af555e661996b2aba753eea5..0defd52b380964770a11536904d7c6d274409093 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -26,8 +26,8 @@ Defer01.hs:25:4: warning: [-Winaccessible-code (in -Wdefault)]
 
 Defer01.hs:31:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘Char -> t’ with actual type ‘Char’
-    • The function ‘e’ is applied to one argument,
-      but its type ‘Char’ has none
+    • The function ‘e’ is applied to one value argument,
+        but its type ‘Char’ has none
       In the expression: e 'q'
       In an equation for ‘f’: f = e 'q'
     • Relevant bindings include f :: t (bound at Defer01.hs:31:1)
@@ -79,7 +79,7 @@ Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • In the expression: 'p'
       In an equation for ‘a’: a = 'p'
 (deferred type error)
-*** Exception: Defer01.hs:18:7: error:
+*** Exception: Defer01.hs:18:9: error:
     • No instance for (Eq B) arising from a use of ‘==’
     • In the expression: x == x
       In an equation for ‘b’: b x = x == x
@@ -100,8 +100,8 @@ Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
 (deferred type error)
 *** Exception: Defer01.hs:31:5: error:
     • Couldn't match expected type ‘Char -> t’ with actual type ‘Char’
-    • The function ‘e’ is applied to one argument,
-      but its type ‘Char’ has none
+    • The function ‘e’ is applied to one value argument,
+        but its type ‘Char’ has none
       In the expression: e 'q'
       In an equation for ‘f’: f = e 'q'
     • Relevant bindings include f :: t (bound at Defer01.hs:31:1)
diff --git a/testsuite/tests/ghci/scripts/T10963.stderr b/testsuite/tests/ghci/scripts/T10963.stderr
index 2efd138be8032f41342cb44102dc3fb53e9114ad..aa081391c413a3d2e70199d6686f5106ea66070e 100644
--- a/testsuite/tests/ghci/scripts/T10963.stderr
+++ b/testsuite/tests/ghci/scripts/T10963.stderr
@@ -1,12 +1,13 @@
 
 <interactive>:1:1: error:
-    Ambiguous type variable ‘a0’ arising from a use of ‘foo’
-    prevents the constraint ‘(Num a0)’ from being solved.
-    Probable fix: use a type annotation to specify what ‘a0’ should be.
-    These potential instances exist:
-      instance Num Integer -- Defined in ‘GHC.Num’
-      instance Num Double -- Defined in ‘GHC.Float’
-      instance Num Float -- Defined in ‘GHC.Float’
-      ...plus two others
-      ...plus 8 instances involving out-of-scope types
-      (use -fprint-potential-instances to see them all)
+    • Ambiguous type variable ‘a0’ arising from a use of ‘foo’
+      prevents the constraint ‘(Num a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Num Integer -- Defined in ‘GHC.Num’
+        instance Num Double -- Defined in ‘GHC.Float’
+        instance Num Float -- Defined in ‘GHC.Float’
+        ...plus two others
+        ...plus 8 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: foo
diff --git a/testsuite/tests/ghci/scripts/ghci047.stderr b/testsuite/tests/ghci/scripts/ghci047.stderr
index 86130800b08a9f60a4cd1ae132825a449f063b41..90a9bb7c60b180a8f686052b26327fd3af3cb8a6 100644
--- a/testsuite/tests/ghci/scripts/ghci047.stderr
+++ b/testsuite/tests/ghci/scripts/ghci047.stderr
@@ -2,11 +2,13 @@
 <interactive>:40:1: error:
     • Couldn't match type ‘HFalse’ with ‘HTrue’
         arising from a use of ‘f’
-    • In the expression: f $ Baz 'a'
+    • In the first argument of ‘($)’, namely ‘f’
+      In the expression: f $ Baz 'a'
       In an equation for ‘it’: it = f $ Baz 'a'
 
 <interactive>:41:1: error:
     • Couldn't match type ‘HFalse’ with ‘HTrue’
         arising from a use of ‘f’
-    • In the expression: f $ Quz
+    • In the first argument of ‘($)’, namely ‘f’
+      In the expression: f $ Quz
       In an equation for ‘it’: it = f $ Quz
diff --git a/testsuite/tests/indexed-types/should_compile/T10806.stderr b/testsuite/tests/indexed-types/should_compile/T10806.stderr
index 350310549861784d9585af3a461c743814bb733d..c78a10bd7bb8db108cc245521cf4e75660472c4b 100644
--- a/testsuite/tests/indexed-types/should_compile/T10806.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T10806.stderr
@@ -1,9 +1,9 @@
 
 T10806.hs:11:32: error:
-    Couldn't match expected type ‘Char -> Bool’
-                with actual type ‘IO ()’
-    The function ‘print’ is applied to two arguments,
-    but its type ‘Char -> IO ()’ has only one
-    In the expression: print 'x' 'y'
-    In an equation for ‘triggersLoop’:
-        triggersLoop (Q _ _) (Q _ _) = print 'x' 'y'
+    • Couldn't match expected type ‘Char -> Bool’
+                  with actual type ‘IO ()’
+    • The function ‘print’ is applied to two value arguments,
+        but its type ‘Char -> IO ()’ has only one
+      In the expression: print 'x' 'y'
+      In an equation for ‘triggersLoop’:
+          triggersLoop (Q _ _) (Q _ _) = print 'x' 'y'
diff --git a/testsuite/tests/indexed-types/should_fail/T4485.stderr b/testsuite/tests/indexed-types/should_fail/T4485.stderr
index 4cf3b153fd79301bf7aa104cf65904f0c195d6f4..bdf5218b42d86d04b249611f26e840fdc15f874b 100644
--- a/testsuite/tests/indexed-types/should_fail/T4485.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4485.stderr
@@ -13,11 +13,10 @@ T4485.hs:50:15: error:
       (The choice depends on the instantiation of ‘m0’
        To pick the first instance above, use IncoherentInstances
        when compiling the other instance declarations)
-    • In the expression: asChild $ (genElement "foo")
+    • In the first argument of ‘($)’, namely ‘asChild’
+      In the expression: asChild $ (genElement "foo")
       In an equation for ‘asChild’:
           asChild b = asChild $ (genElement "foo")
-      In the instance declaration for
-        ‘EmbedAsChild (IdentityT IO) FooBar’
 
 T4485.hs:50:26: error:
     • Ambiguous type variable ‘m0’ arising from a use of ‘genElement’
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 037bb76bbebbdbd185f965260d266c6fd8510986..b18202fec9cc256e2132a0a1b75b7440310ef46b 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -2,8 +2,8 @@
 T8518.hs:14:18: error:
     • Couldn't match expected type ‘Z c -> B c -> Maybe (F c)’
                   with actual type ‘F c’
-    • The function ‘rpt’ is applied to four arguments,
-      but its type ‘Int -> c -> F c’ has only two
+    • The function ‘rpt’ is applied to four value arguments,
+        but its type ‘Int -> c -> F c’ has only two
       In the expression: rpt (4 :: Int) c z b
       In an equation for ‘callCont’:
           callCont c z b
diff --git a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
index 73a1b9b4d8441c399e3d23a4a288a99dcffbc15d..836b27f9e50db8dc099457831099c94db7c69126 100644
--- a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
+++ b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
@@ -1,7 +1,6 @@
 
 overloadedrecfldsfail07.hs:7:7: error:
     • Couldn't match expected type ‘T’ with actual type ‘T -> Int’
-    • Probable cause: ‘x’ is applied to too few arguments
-      In the first argument of ‘x’, namely ‘x’
+    • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘y’: y = x x
diff --git a/testsuite/tests/parser/should_compile/T2245.stderr b/testsuite/tests/parser/should_compile/T2245.stderr
index b6c20a804e52fba9d2c24c7801a2ab546c8ac22d..b823c00ed0c8fb1955b939f8841351f5676ba941 100644
--- a/testsuite/tests/parser/should_compile/T2245.stderr
+++ b/testsuite/tests/parser/should_compile/T2245.stderr
@@ -13,7 +13,7 @@ T2245.hs:5:10: warning: [-Wmissing-methods (in -Wdefault)]
 
 T2245.hs:7:27: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘T’
-        (Ord a0) arising from a use of ‘<’ at T2245.hs:7:27-33
+        (Ord a0) arising from a use of ‘<’ at T2245.hs:7:27
         (Fractional a0)
           arising from the literal ‘1e400’ at T2245.hs:7:29-33
         (Read a0) arising from a use of ‘read’ at T2245.hs:7:38-41
diff --git a/testsuite/tests/quantified-constraints/T17458.stderr b/testsuite/tests/quantified-constraints/T17458.stderr
index b8468266ddba1da4222239e8c10ca95fb7b40bfa..f77f26efb9e22123fc3facd20ea1ca22d07ff944 100644
--- a/testsuite/tests/quantified-constraints/T17458.stderr
+++ b/testsuite/tests/quantified-constraints/T17458.stderr
@@ -1,5 +1,5 @@
 
-T17458.hs:32:27: error:
+T17458.hs:32:32: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type: Typeable Void
       Use -freduction-depth=0 to disable this check
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index 6561e08032c0e8c9980349aaf09a7714ed55066b..78ad520e46c270fefeb8f8a45de25f3c7b15470d 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,18 +1,18 @@
 
 T5358.hs:7:1: error:
     • Couldn't match expected type ‘Int’ with actual type ‘p1 -> p1’
-    • The equation(s) for ‘t1’ have one argument,
-      but its type ‘Int’ has none
+    • The equation(s) for ‘t1’ have one value argument,
+        but its type ‘Int’ has none
 
 T5358.hs:8:1: error:
     • Couldn't match expected type ‘Int’ with actual type ‘p0 -> p0’
-    • The equation(s) for ‘t2’ have one argument,
-      but its type ‘Int’ has none
+    • The equation(s) for ‘t2’ have one value argument,
+        but its type ‘Int’ has none
 
 T5358.hs:10:13: error:
     • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘t1’ is applied to one argument,
-      but its type ‘Int’ has none
+    • The function ‘t1’ is applied to one value argument,
+        but its type ‘Int’ has none
       In the first argument of ‘(==)’, namely ‘t1 x’
       In the expression: t1 x == t2 x
     • Relevant bindings include
@@ -21,8 +21,8 @@ T5358.hs:10:13: error:
 
 T5358.hs:10:21: error:
     • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘t2’ is applied to one argument,
-      but its type ‘Int’ has none
+    • The function ‘t2’ is applied to one value argument,
+        but its type ‘Int’ has none
       In the second argument of ‘(==)’, namely ‘t2 x’
       In the expression: t1 x == t2 x
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/FD1.stderr b/testsuite/tests/typecheck/should_compile/FD1.stderr
index 380be215bc8b7547ea1379d39a15e44c0325c277..64a01c43e11a152d602addf1b8d2ae0e3aa7075c 100644
--- a/testsuite/tests/typecheck/should_compile/FD1.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD1.stderr
@@ -5,6 +5,6 @@ FD1.hs:16:1: error:
         the type signature for:
           plus :: forall a. E a (Int -> Int) => Int -> a
         at FD1.hs:15:1-38
-    • The equation(s) for ‘plus’ have two arguments,
-      but its type ‘Int -> a’ has only one
+    • The equation(s) for ‘plus’ have two value arguments,
+        but its type ‘Int -> a’ has only one
     • Relevant bindings include plus :: Int -> a (bound at FD1.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_compile/T13050.stderr b/testsuite/tests/typecheck/should_compile/T13050.stderr
index 87b1312b4b5b995d9377f59efc64b7c0e0dfb726..89f2b80d3bb3554960d4e80db5a568213ddd464d 100644
--- a/testsuite/tests/typecheck/should_compile/T13050.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13050.stderr
@@ -87,8 +87,7 @@ T13050.hs:4:9: warning: [-Wtyped-holes (in -Wdefault)]
 
 T13050.hs:5:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int -> Int -> Int
-    • In the expression: _
-      In the expression: x `_` y
+    • In the expression: x `_` y
       In an equation for ‘g’: g x y = x `_` y
     • Relevant bindings include
         y :: Int (bound at T13050.hs:5:5)
@@ -174,8 +173,7 @@ T13050.hs:5:11: warning: [-Wtyped-holes (in -Wdefault)]
 T13050.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _a :: Int -> Int -> Int
       Or perhaps ‘_a’ is mis-spelled, or not in scope
-    • In the expression: _a
-      In the expression: x `_a` y
+    • In the expression: x `_a` y
       In an equation for ‘q’: q x y = x `_a` y
     • Relevant bindings include
         y :: Int (bound at T13050.hs:6:5)
diff --git a/testsuite/tests/typecheck/should_compile/T14590.stderr b/testsuite/tests/typecheck/should_compile/T14590.stderr
index 52ecc8335d413d3b4dab37fb7b97dc3e6da4813f..7ecfa761f11b7a13c013d73c0b13b0fd3938fbfd 100644
--- a/testsuite/tests/typecheck/should_compile/T14590.stderr
+++ b/testsuite/tests/typecheck/should_compile/T14590.stderr
@@ -1,9 +1,9 @@
 
 T14590.hs:4:13: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int -> Int -> Int
-    • In the expression: _
-      In the expression: x `_`
+    • In the expression: x `_`
       In the expression: (x `_`) y
+      In an equation for ‘f1’: f1 x y = (x `_`) y
     • Relevant bindings include
         y :: Int (bound at T14590.hs:4:6)
         x :: Int (bound at T14590.hs:4:4)
@@ -89,9 +89,9 @@ T14590.hs:4:13: warning: [-Wtyped-holes (in -Wdefault)]
 T14590.hs:5:13: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _a :: Int -> Int -> Int
       Or perhaps ‘_a’ is mis-spelled, or not in scope
-    • In the expression: _a
-      In the expression: x `_a`
+    • In the expression: x `_a`
       In the expression: (x `_a`) y
+      In an equation for ‘f2’: f2 x y = (x `_a`) y
     • Relevant bindings include
         y :: Int (bound at T14590.hs:5:6)
         x :: Int (bound at T14590.hs:5:4)
@@ -176,9 +176,9 @@ T14590.hs:5:13: warning: [-Wtyped-holes (in -Wdefault)]
 
 T14590.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int -> Int -> Int
-    • In the expression: _
-      In the expression: `_` x
+    • In the expression: `_` x
       In the expression: (`_` x) y
+      In an equation for ‘f3’: f3 x y = (`_` x) y
     • Relevant bindings include
         y :: Int (bound at T14590.hs:6:6)
         x :: Int (bound at T14590.hs:6:4)
@@ -264,9 +264,9 @@ T14590.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
 T14590.hs:7:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _a :: Int -> Int -> Int
       Or perhaps ‘_a’ is mis-spelled, or not in scope
-    • In the expression: _a
-      In the expression: `_a` x
+    • In the expression: `_a` x
       In the expression: (`_a` x) y
+      In an equation for ‘f4’: f4 x y = (`_a` x) y
     • Relevant bindings include
         y :: Int (bound at T14590.hs:7:6)
         x :: Int (bound at T14590.hs:7:4)
diff --git a/testsuite/tests/typecheck/should_compile/T18005.hs b/testsuite/tests/typecheck/should_compile/T18005.hs
index 9b4ddbd366b41e0df7dabd5eeaf55c4244694fe2..8cd818bc0f52e9298277f89ab6942184c68dfbad 100644
--- a/testsuite/tests/typecheck/should_compile/T18005.hs
+++ b/testsuite/tests/typecheck/should_compile/T18005.hs
@@ -28,3 +28,4 @@ unT2b' (MkT2b x) = x
 
 pattern MkT2b' :: S2 -> T2b
 pattern MkT2b' {unT2b} <- (unT2b' -> unT2b)
+
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
index 18c45a12c08958697c3989da1abe063d7f2a4cf3..71e175ef41d728b64f9fb8b9b21c0ca175690a1d 100644
--- a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
@@ -1,5 +1,5 @@
 
-CustomTypeErrors01.hs:12:9: error:
+CustomTypeErrors01.hs:12:11: error:
     • Values of type 'MyType' cannot be compared for equality.
     • In the expression: x == MyType
       In an equation for ‘err’: err x = x == MyType
diff --git a/testsuite/tests/typecheck/should_fail/T11274.stderr b/testsuite/tests/typecheck/should_fail/T11274.stderr
index b6f1964c14b202fc3929a15995168b7da3bf8b4f..f73131704a69e2aac58d62f70d9e0ffb9f9689f1 100644
--- a/testsuite/tests/typecheck/should_fail/T11274.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11274.stderr
@@ -1,5 +1,5 @@
 
-T11274.hs:10:23: error:
+T11274.hs:10:25: error:
     • No instance for (Eq Asd) arising from a use of ‘==’
     • In the expression: x == y
       In an equation for ‘missingInstance’: missingInstance x y = x == y
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
index 0a24b6ec6d837ad6f9844da621e4684835072cc2..85d7361421d82aed79d1a5cc0fbf7af67804781a 100644
--- a/testsuite/tests/typecheck/should_fail/T12785b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr
@@ -1,5 +1,5 @@
 
-T12785b.hs:29:63: error:
+T12785b.hs:29:65: error:
     • Could not deduce: Payload ('S n) (Payload n s1) ~ s
         arising from a use of ‘SBranchX’
       from the context: m ~ 'S n
diff --git a/testsuite/tests/typecheck/should_fail/T13902.stderr b/testsuite/tests/typecheck/should_fail/T13902.stderr
index 2794ae25ec723805a932fdf932f4571b1242f78e..c7630039aa1cf5721becd2f91af6de2228187cfb 100644
--- a/testsuite/tests/typecheck/should_fail/T13902.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13902.stderr
@@ -1,7 +1,7 @@
 
 T13902.hs:8:5: error:
     • Couldn't match expected type ‘t0 -> Int’ with actual type ‘Int’
-    • The expression ‘f @Int’ is applied to two arguments,
-      but its type ‘Int -> Int’ has only one
+    • The function ‘f’ is applied to two value arguments,
+        but its type ‘Int -> Int’ has only one
       In the expression: f @Int 42 5
       In an equation for ‘g’: g = f @Int 42 5
diff --git a/testsuite/tests/typecheck/should_fail/T17173.hs b/testsuite/tests/typecheck/should_fail/T17173.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d26c5dd61971d5a0fc9d96d6180630682c7d07b5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17173.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RankNTypes, TypeApplications #-}
+
+module T17173 where
+
+-- This now fails with eager instantation
+foo = (let myId :: forall a. a -> a; myId x = x in myId) @Bool True
diff --git a/testsuite/tests/typecheck/should_fail/T17173.stderr b/testsuite/tests/typecheck/should_fail/T17173.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..b5bd059bac22b490ad12b76308dee09c49524120
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17173.stderr
@@ -0,0 +1,17 @@
+
+T17173.hs:6:7: error:
+    • Cannot apply expression of type ‘a0 -> a0’
+      to a visible type argument ‘Bool’
+    • In the expression:
+        (let
+           myId :: forall a. a -> a
+           myId x = x
+         in myId)
+          @Bool True
+      In an equation for ‘foo’:
+          foo
+            = (let
+                 myId :: forall a. a -> a
+                 myId x = x
+               in myId)
+                @Bool True
diff --git a/testsuite/tests/typecheck/should_fail/T3176.stderr b/testsuite/tests/typecheck/should_fail/T3176.stderr
index 50e6b52c78a58fd5a269f0430e288bc79f2be232..1f089da6fe8e48b68d37d7c8cc500ffe0e9e84eb 100644
--- a/testsuite/tests/typecheck/should_fail/T3176.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3176.stderr
@@ -1,7 +1,7 @@
 
-T3176.hs:9:27:
-    Cannot use record selector ‘unES’ as a function due to escaped type variables
-    Probable fix: use pattern-matching syntax instead
-    In the expression: unES
-    In the second argument of ‘($)’, namely ‘unES $ f t’
-    In the expression: show $ unES $ f t
+T3176.hs:9:27: error:
+    • Cannot use record selector ‘unES’ as a function due to escaped type variables
+      Probable fix: use pattern-matching syntax instead
+    • In the first argument of ‘($)’, namely ‘unES’
+      In the second argument of ‘($)’, namely ‘unES $ f t’
+      In the expression: show $ unES $ f t
diff --git a/testsuite/tests/typecheck/should_fail/T5095.stderr b/testsuite/tests/typecheck/should_fail/T5095.stderr
index ccf791dd478d9c03c142e04361b62805414b6660..4f0e6ad3b2d50f35234800aebf38f45f21d45407 100644
--- a/testsuite/tests/typecheck/should_fail/T5095.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5095.stderr
@@ -1,13 +1,13 @@
 
-T5095.hs:9:9: error:
+T5095.hs:9:11: error:
     • Overlapping instances for Eq a arising from a use of ‘==’
       Matching instances:
         instance [overlappable] Show a => Eq a -- Defined at T5095.hs:5:31
         instance Eq Ordering -- Defined in ‘GHC.Classes’
         instance Eq Integer
-          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
+          -- Defined in ‘integer-gmp-1.0.3.0:GHC.Integer.Type’
         ...plus 23 others
-        ...plus N instances involving out-of-scope types
+        ...plus 7 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
       (The choice depends on the instantiation of ‘a’
        To pick the first instance above, use IncoherentInstances
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 573a532f10eb3ad994f508e21aa5227a610f8b4d..6fd62bb79bafd6db5521f3660cdd507b1efe7fa9 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,5 +1,5 @@
 
-T5853.hs:15:46: error:
+T5853.hs:15:52: error:
     • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
         arising from a use of ‘<$>’
       from the context: (F fa, Elem (Subst fa b) ~ b,
diff --git a/testsuite/tests/typecheck/should_fail/T6069.stderr b/testsuite/tests/typecheck/should_fail/T6069.stderr
index 3ee2b2d5e4e3c9575970b5a7f39acf5690096987..e2d3ef4d91e3206ac4744ae5312884307d79491f 100644
--- a/testsuite/tests/typecheck/should_fail/T6069.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6069.stderr
@@ -12,7 +12,7 @@ T6069.hs:14:15: error:
       Expected type: ST s1 Int -> a1
         Actual type: (forall s. ST s a1) -> a1
     • In the second argument of ‘(.)’, namely ‘runST’
-      In the expression: print . runST
+      In the first argument of ‘($)’, namely ‘(print . runST)’
       In the expression: (print . runST) $ fourty_two
 
 T6069.hs:15:16: error:
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index ec991bc39f6c86f927c48530ae52c534f9d3684d..29c5d9df12cab043e792822b6a6d83e4f702a710 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -3,9 +3,9 @@ T8603.hs:33:17: error:
     • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
       Expected type: [a2] -> StateT s RV a0
         Actual type: t0 ((->) [a1]) (RV a1)
-    • The function ‘lift’ is applied to two arguments,
-      but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
-      has only one
+    • The function ‘lift’ is applied to two value arguments,
+        but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
+        has only one
       In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
       In the expression:
         do prize <- lift uniform [1, 2, ....]
diff --git a/testsuite/tests/typecheck/should_fail/T9605.stderr b/testsuite/tests/typecheck/should_fail/T9605.stderr
index db65629fba9aee9afd0eec087bf6ec3a789cfec9..683265c26b98f8934fd1b1bb6aabd55c0b44ce7d 100644
--- a/testsuite/tests/typecheck/should_fail/T9605.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9605.stderr
@@ -3,9 +3,7 @@ T9605.hs:7:6: error:
     • Couldn't match type ‘Bool’ with ‘m Bool’
       Expected type: t0 -> m Bool
         Actual type: t0 -> Bool
-    • The function ‘f1’ is applied to one argument,
-      its type is ‘m0 Bool’,
-      it is specialized to ‘t0 -> Bool’
+    • In the result of a function call
       In the expression: f1 undefined
       In an equation for ‘f2’: f2 = f1 undefined
     • Relevant bindings include f2 :: m Bool (bound at T9605.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index 6d7e519d9164d62f78679e8951e304afebadefe8..f4e1d02eeefb07b69ecd53d08fe6e30778d80cf1 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -2,7 +2,8 @@
 TcCoercibleFail.hs:11:8: error:
     • Couldn't match representation of type ‘Int’ with that of ‘()’
         arising from a use of ‘coerce’
-    • In the expression: coerce $ one :: ()
+    • In the first argument of ‘($)’, namely ‘coerce’
+      In the expression: coerce $ one :: ()
       In an equation for ‘foo1’: foo1 = coerce $ one :: ()
 
 TcCoercibleFail.hs:14:8: error:
@@ -11,7 +12,8 @@ TcCoercibleFail.hs:14:8: error:
         arising from a use of ‘coerce’
       NB: We cannot know what roles the parameters to ‘m’ have;
         we must assume that the role is nominal
-    • In the expression: coerce $ (return one :: m Int)
+    • In the first argument of ‘($)’, namely ‘coerce’
+      In the expression: coerce $ (return one :: m Int)
       In an equation for ‘foo2’: foo2 = coerce $ (return one :: m Int)
     • Relevant bindings include
         foo2 :: m Age (bound at TcCoercibleFail.hs:14:1)
@@ -19,7 +21,8 @@ TcCoercibleFail.hs:14:8: error:
 TcCoercibleFail.hs:16:8: error:
     • Couldn't match type ‘Int’ with ‘Age’
         arising from a use of ‘coerce’
-    • In the expression: coerce $ Map one () :: Map Age ()
+    • In the first argument of ‘($)’, namely ‘coerce’
+      In the expression: coerce $ Map one () :: Map Age ()
       In an equation for ‘foo3’: foo3 = coerce $ Map one () :: Map Age ()
 
 TcCoercibleFail.hs:18:8: error:
@@ -28,7 +31,8 @@ TcCoercibleFail.hs:18:8: error:
         arising from a use of ‘coerce’
       The data constructor ‘Data.Ord.Down’
         of newtype ‘Down’ is not in scope
-    • In the expression: coerce $ one :: Down Int
+    • In the first argument of ‘($)’, namely ‘coerce’
+      In the expression: coerce $ one :: Down Int
       In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int
 
 TcCoercibleFail.hs:21:8: error:
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 14728794ce17950822df1c5efcdafa8cb5f93e94..5155e76a7b2d5dad806f032053313849343f81b4 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -562,3 +562,4 @@ test('T17773', normal, compile_fail, [''])
 test('T17021', normal, compile_fail, [''])
 test('T17021b', normal, compile_fail, [''])
 test('T17955', normal, compile_fail, [''])
+test('T17173', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail001.stderr b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
index 56c28d98b5106613f91cff7f561523e0e4034825..2d4caf2ac721006ad38f35162f63b8737269b883 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail001.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
@@ -2,7 +2,7 @@
 tcfail001.hs:9:2: error:
     • Couldn't match expected type ‘[a]’
                   with actual type ‘[a0] -> [a1]’
-    • The equation(s) for ‘op’ have one argument,
-      but its type ‘[a]’ has none
+    • The equation(s) for ‘op’ have one value argument,
+        but its type ‘[a]’ has none
       In the instance declaration for ‘A [a]’
     • Relevant bindings include op :: [a] (bound at tcfail001.hs:9:2)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail007.stderr b/testsuite/tests/typecheck/should_fail/tcfail007.stderr
index 4c1652fe50aa6e84946ce1f6d68c75b28fd4a1f2..02d25c16e3d0f276eede690563ee031638e3a4ee 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail007.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail007.stderr
@@ -1,5 +1,5 @@
 
-tcfail007.hs:3:14: error:
+tcfail007.hs:3:15: error:
     • No instance for (Num Bool) arising from a use of ‘+’
     • In the expression: x + 1
       In an equation for ‘n’:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail010.stderr b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
index 11e529084f9c59c52f99caff6555636309e2a95c..442a1d43a7d8e3fc2fea53dd227231e507d2b21b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail010.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
@@ -1,5 +1,5 @@
 
-tcfail010.hs:3:16: error:
+tcfail010.hs:3:17: error:
     • No instance for (Num [a0]) arising from a use of ‘+’
     • In the expression: z + 2
       In the expression: \ (y : z) -> z + 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail029.stderr b/testsuite/tests/typecheck/should_fail/tcfail029.stderr
index c31c5869b9f96c37c2b1ef00dc3ac04753d2db1a..02adf4235d4d8dfae6bdd5d5e7219b0cfcdd9f2f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail029.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail029.stderr
@@ -1,5 +1,5 @@
 
-tcfail029.hs:6:7: error:
+tcfail029.hs:6:9: error:
     • No instance for (Ord Foo) arising from a use of ‘>’
     • In the expression: x > Bar
       In an equation for ‘f’: f x = x > Bar
diff --git a/testsuite/tests/typecheck/should_fail/tcfail034.stderr b/testsuite/tests/typecheck/should_fail/tcfail034.stderr
index 9158fd2014acfb5ac191cc312ff2a03224273bcc..02e3bfc5f19b248d2921b1bace5d69da79674d82 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail034.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail034.stderr
@@ -1,5 +1,5 @@
 
-tcfail034.hs:17:11: error:
+tcfail034.hs:17:13: error:
     • Could not deduce (Integral a) arising from a use of ‘mod’
       from the context: (Num a, Eq a)
         bound by the type signature for:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.hs b/testsuite/tests/typecheck/should_fail/tcfail133.hs
index da58021700c354f7728d00fe95be5ca670a55de1..f22feec9aee0102807b8bf3ff28f78b0660dbdb7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.hs
@@ -73,7 +73,7 @@ foo = show $ add (One:@Zero) (One:@One)
 --     Add One One nr', AddDigit (Zero:@nr') One c, Show c
 --
 -- ==> Add One One nr', AddDigit (Zero:@nr') One c, Show c
--- 
+--
 -- ==> Add One One (One:@One), AddDigit (Zero:@(One:@One)) One c, Show c
 --
 -- ==> AddDigit (Zero:@(One:@One)) One c, Show c
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.stderr b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
index bbaf091226721cdae541abbb45295b97df8cdf77..9a70aedf5c17b6c4ffdc36677138f4cec2bb2f9f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
@@ -14,7 +14,8 @@ tcfail133.hs:68:7: error:
         ...plus 25 others
         ...plus 12 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
-    • In the expression: show $ add (One :@ Zero) (One :@ One)
+    • In the first argument of ‘($)’, namely ‘show’
+      In the expression: show $ add (One :@ Zero) (One :@ One)
       In an equation for ‘foo’:
           foo = show $ add (One :@ Zero) (One :@ One)
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 924e14081b6609d96e3f034b647d4fb85153ebae..c0049d0e19f8db96dce2e5d6ba9895bea2c30a0f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -1,16 +1,16 @@
 
 tcfail140.hs:10:7: error:
     • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’
-    • The function ‘f’ is applied to two arguments,
-      but its type ‘Int -> Int’ has only one
+    • The function ‘f’ is applied to two value arguments,
+        but its type ‘Int -> Int’ has only one
       In the expression: f 3 9
       In an equation for ‘bar’: bar = f 3 9
     • Relevant bindings include bar :: t (bound at tcfail140.hs:10:1)
 
 tcfail140.hs:12:10: error:
     • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
-    • The operator ‘f’ takes two arguments,
-      but its type ‘Int -> Int’ has only one
+    • The operator ‘f’ takes two value arguments,
+        but its type ‘Int -> Int’ has only one
       In the expression: 3 `f` 4
       In an equation for ‘rot’: rot xs = 3 `f` 4
     • Relevant bindings include
@@ -18,8 +18,8 @@ tcfail140.hs:12:10: error:
 
 tcfail140.hs:14:15: error:
     • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
-    • The operator ‘f’ takes two arguments,
-      but its type ‘Int -> Int’ has only one
+    • The operator ‘f’ takes two value arguments,
+        but its type ‘Int -> Int’ has only one
       In the first argument of ‘map’, namely ‘(3 `f`)’
       In the expression: map (3 `f`) xs
     • Relevant bindings include
@@ -29,11 +29,11 @@ tcfail140.hs:14:15: error:
 tcfail140.hs:16:8: error:
     • The constructor ‘Just’ should have 1 argument, but has been given none
     • In the pattern: Just
-      The lambda expression ‘\ Just x -> x’ has two arguments,
-      but its type ‘Maybe a -> a’ has only one
+      The lambda expression ‘\ Just x -> x’ has two value arguments,
+        but its type ‘Maybe a -> a’ has only one
       In the expression: (\ Just x -> x) :: Maybe a -> a
 
 tcfail140.hs:19:1: error:
     • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’
-    • The equation(s) for ‘g’ have two arguments,
-      but its type ‘Int -> Int’ has only one
+    • The equation(s) for ‘g’ have two value arguments,
+        but its type ‘Int -> Int’ has only one
diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
index b94266978d7a378a957fc8d7110b0b3f68bbcc1b..576ac1903db3bb55c1e10f3a326f899d4a57e799 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
@@ -1,5 +1,5 @@
 
-tcfail143.hs:29:6: error:
+tcfail143.hs:29:9: error:
     • Couldn't match type ‘S Z’ with ‘Z’
         arising from a functional dependency between:
           constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail175.stderr b/testsuite/tests/typecheck/should_fail/tcfail175.stderr
index 6fbb6d4cd6f72492bfa3da1532f7fa86c95bb83f..90ec5b13a54a045bf4fa6b3ae59f2f59312f19dc 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail175.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail175.stderr
@@ -6,7 +6,7 @@ tcfail175.hs:11:1: error:
         the type signature for:
           evalRHS :: forall a. Int -> a
         at tcfail175.hs:10:1-19
-    • The equation(s) for ‘evalRHS’ have three arguments,
-      but its type ‘Int -> a’ has only one
+    • The equation(s) for ‘evalRHS’ have three value arguments,
+        but its type ‘Int -> a’ has only one
     • Relevant bindings include
         evalRHS :: Int -> a (bound at tcfail175.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index 9f5252539ba26c750f5180284dc095531a3c5c9e..8a8263e8b44a1f6b109717dcdc6e1e58cca88ab6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -3,7 +3,7 @@ tcfail181.hs:17:9: error:
     • Could not deduce (Monad m0) arising from a use of ‘foo’
       from the context: Monad m
         bound by the inferred type of
-                 wog :: Monad m => p -> Something (m Bool) e
+                   wog :: Monad m => p -> Something (m Bool) e
         at tcfail181.hs:17:1-30
       The type variable ‘m0’ is ambiguous
       These potential instances exist:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail208.stderr b/testsuite/tests/typecheck/should_fail/tcfail208.stderr
index cd8e6379e91b21a23de96877ca415e40d4bb3319..978200ad77e07ae7c18383e9786304e7de27809e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail208.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail208.stderr
@@ -1,5 +1,5 @@
 
-tcfail208.hs:4:10: error:
+tcfail208.hs:4:19: error:
     • Could not deduce (Eq (m a)) arising from a use of ‘==’
       from the context: (Monad m, Eq a)
         bound by the type signature for:
diff --git a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
index 532ca18ffc86593789588edc02f9798da0c5d925..6d02807207ad553d6cc6daf4f801e982e55f20c0 100644
--- a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
+++ b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
@@ -55,8 +55,8 @@ CaretDiagnostics1.hs:13:7-11: error:
 
 CaretDiagnostics1.hs:(13,16)-(14,13): error:
     • Couldn't match expected type ‘Char -> p0’ with actual type ‘()’
-    • The function ‘()’ is applied to one argument,
-      but its type ‘()’ has none
+    • The function ‘()’ is applied to one value argument,
+        but its type ‘()’ has none
       In the expression: () '0'
       In a case alternative: "γηξ" -> () '0'
    |