compiler/GHC/Core/Ppr.hs

@@ -123,11 +123,13 @@ ppr_binding ann (val_bdr, expr)
          , pp_bind
          ]
   where
+    pp_val_bdr = pprPrefixOcc val_bdr
+
     pp_bind = case bndrIsJoin_maybe val_bdr of
                 Nothing -> pp_normal_bind
                 Just ar -> pp_join_bind ar
 
-    pp_normal_bind = hang (ppr val_bdr) 2 (equals <+> pprCoreExpr expr)
+    pp_normal_bind = hang pp_val_bdr 2 (equals <+> pprCoreExpr expr)
 
       -- For a join point of join arity n, we want to print j = \x1 ... xn -> e
       -- as "j x1 ... xn = e" to differentiate when a join point returns a
@@ -135,7 +137,7 @@ ppr_binding ann (val_bdr, expr)
       -- an n-argument function).
     pp_join_bind join_arity
       | bndrs `lengthAtLeast` join_arity
-      = hang (ppr val_bdr <+> sep (map (pprBndr LambdaBind) lhs_bndrs))
+      = hang (pp_val_bdr <+> sep (map (pprBndr LambdaBind) lhs_bndrs))
            2 (equals <+> pprCoreExpr rhs)
       | otherwise -- Yikes!  A join-binding with too few lambda
                   -- Lint will complain, but we don't want to crash
@@ -164,8 +166,10 @@ ppr_expr :: OutputableBndr b => (SDoc -> SDoc) -> Expr b -> SDoc
         -- an atomic value (e.g. function args)
 
 ppr_expr add_par (Var name)
- | isJoinId name               = add_par ((text "jump") <+> ppr name)
- | otherwise                   = ppr name
+ | isJoinId name               = add_par ((text "jump") <+> pp_name)
+ | otherwise                   = pp_name
+ where
+   pp_name = pprPrefixOcc name
 ppr_expr add_par (Type ty)     = add_par (text "TYPE:" <+> ppr ty)       -- Weird
 ppr_expr add_par (Coercion co) = add_par (text "CO:" <+> ppr co)
 ppr_expr add_par (Lit lit)     = pprLiteral add_par lit
@@ -429,7 +433,7 @@ pprKindedTyVarBndr tyvar
 -- pprIdBndr does *not* print the type
 -- When printing any Id binder in debug mode, we print its inline pragma and one-shot-ness
 pprIdBndr :: Id -> SDoc
-pprIdBndr id = ppr id <+> pprIdBndrInfo (idInfo id)
+pprIdBndr id = pprPrefixOcc id <+> pprIdBndrInfo (idInfo id)
 
 pprIdBndrInfo :: IdInfo -> SDoc
 pprIdBndrInfo info

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
@@ -2538,7 +2546,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

compiler/GHC/Hs/Utils.hs

@@ -186,8 +186,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

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]

compiler/GHC/Rename/Splice.hs

@@ -48,7 +48,7 @@ import GHC.Driver.Hooks
 import THNames          ( 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)

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) }
 

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
 

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

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
 

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
@@ -3323,58 +3322,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.

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 _ pat rhs bind_op fail_op) res_ty thing_inside
             <- tcSyntaxOp MCompOrigin bind_op
                           [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) }
 
@@ -601,7 +601,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) }
@@ -661,7 +661,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') }
 
@@ -687,7 +687,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)
@@ -697,7 +697,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 ----------------
@@ -759,7 +759,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))
@@ -821,7 +821,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) }
 
@@ -834,9 +834,8 @@ tcDoStmt ctxt (BindStmt _ pat rhs bind_op fail_op) res_ty thing_inside
           ((rhs', pat', new_res_ty, thing), bind_op')
             <- tcSyntaxOp DoOrigin bind_op [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) }
 
@@ -863,7 +862,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) }
@@ -879,7 +878,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)
@@ -891,7 +890,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 ()
@@ -956,7 +955,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).
 
@@ -988,7 +987,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
@@ -1032,8 +1031,8 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
                     }, pat_ty, exp_ty)
       = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $
         addErrCtxt (pprStmtInCtxt ctxt (mkBindStmt 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' <- tcMonadFailOp (DoPatOrigin pat) pat' fail_op body_ty
 
@@ -1048,8 +1047,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')
                   }

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' $$

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) } }
 

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

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
@@ -2122,7 +2121,7 @@ tcRnStmt hsc_env rdr_stmt
     }
   where
     bad_unboxed id = addErr (sep [text "GHCi can't bind a variable of unlifted type:",
-                                  nest 2 (ppr id <+> dcolon <+> ppr (idType id))])
+                                  nest 2 (pprPrefixOcc id <+> dcolon <+> ppr (idType id))])
 
 {-
 --------------------------------------------------------------------------
@@ -2489,15 +2488,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, _)
@@ -2523,12 +2518,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]
@@ -2903,7 +2921,7 @@ ppr_types debug type_env
              -- etc are suppressed (unless -dppr-debug),
              -- because they appear elsewhere
 
-    ppr_sig id = hang (ppr id <+> dcolon) 2 (ppr (tidyTopType (idType id)))
+    ppr_sig id = hang (pprPrefixOcc id <+> dcolon) 2 (ppr (tidyTopType (idType id)))
 
 ppr_tycons :: Bool -> [FamInst] -> TypeEnv -> SDoc
 ppr_tycons debug fam_insts type_env
@@ -2921,7 +2939,7 @@ ppr_tycons debug fam_insts type_env
                      | otherwise  = isExternalName (tyConName tycon) &&
                                     not (tycon `elem` fi_tycons)
     ppr_tc tc
-       = vcat [ hang (ppr (tyConFlavour tc) <+> ppr tc
+       = vcat [ hang (ppr (tyConFlavour tc) <+> pprPrefixOcc (tyConName tc)
                       <> braces (ppr (tyConArity tc)) <+> dcolon)
                    2 (ppr (tidyTopType (tyConKind tc)))
               , nest 2 $
@@ -2955,7 +2973,7 @@ ppr_patsyns type_env
   = ppr_things "PATTERN SYNONYMS" ppr_ps
                (typeEnvPatSyns type_env)
   where
-    ppr_ps ps = ppr ps <+> dcolon <+> pprPatSynType ps
+    ppr_ps ps = pprPrefixOcc ps <+> dcolon <+> pprPatSynType ps
 
 ppr_insts :: [ClsInst] -> SDoc
 ppr_insts ispecs

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

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

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

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) =