[Git][ghc/ghc][wip/T17173] Major refactor of typechecking applications

Simon Peyton Jones gitlab at gitlab.haskell.org
Mon Apr 13 23:29:06 UTC 2020



Simon Peyton Jones pushed to branch wip/T17173 at Glasgow Haskell Compiler / GHC


Commits:
f39a0d86 by Simon Peyton Jones at 2020-04-14T00:26:04+01:00
Major refactor of typechecking applications

Following conversation with Richard today, I have done
major surgery on tcApp and friends.  Fewer arguments, less
plumbing, all good.

I also completely killed off ir_inst.

It's not as well documented as I want, yet, but I'm pushing
it up for Richard's review.

(This message will be replaced with a proper commit message.)

- - - - -


24 changed files:

- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/Utils.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/Tc/Gen/Arrow.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Expr.hs-boot
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Gen/Rule.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Utils/Zonk.hs
- testsuite/tests/typecheck/should_fail/tcfail007.stderr
- testsuite/tests/typecheck/should_fail/tcfail010.stderr
- testsuite/tests/typecheck/should_fail/tcfail029.stderr
- testsuite/tests/typecheck/should_fail/tcfail034.stderr
- testsuite/tests/typecheck/should_fail/tcfail133.hs
- testsuite/tests/typecheck/should_fail/tcfail143.stderr
- testsuite/tests/typecheck/should_fail/tcfail208.stderr


Changes:

=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -599,7 +599,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


=====================================
compiler/GHC/Hs/Utils.hs
=====================================
@@ -185,8 +185,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
=====================================
@@ -319,9 +319,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' (mkTyArg ty)) }
 
 {-
 Note [Desugaring vars]


=====================================
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, tcPolyExpr )
 
 import GHC.Hs
 import GHC.Tc.Gen.Match
@@ -161,7 +161,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')
@@ -179,7 +179,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
@@ -206,9 +206,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
@@ -233,7 +233,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') }
 
 -------------------------------------------


=====================================
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"
@@ -1267,9 +1267,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
@@ -1366,7 +1364,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) $
-               tcInferInst $ \ exp_ty ->   -- The ir_inst field is irrelevant for patterns
+               tcInfer $ \ exp_ty ->
                tcLetPat inst_sig_fun no_gen pat exp_ty $
                mapM lookup_info nosig_names
 


=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -7,20 +7,21 @@
 
 {-# 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
-   , tcInferRho, tcInferRhoNC, tcInferAppHead
+   , tcLExpr, tcLExprNC, tcExpr
+   , tcInferRho, tcInferRhoNC, tcInferApp
    , tcSyntaxOp, tcSyntaxOpGen
    , SyntaxOpType(..)
    , synKnownType
    , tcCheckId
-   , addExprErrCtxt
    , addAmbiguousNameErr
    , getFixedTyVars
    )
@@ -43,7 +44,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 )
@@ -73,7 +74,6 @@ import GHC.Core.Type
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
 import TysWiredIn
-import TysPrim( intPrimTy )
 import PrimOp( tagToEnumKey )
 import PrelNames
 import GHC.Driver.Session
@@ -104,7 +104,7 @@ import qualified Data.Set as Set
 tcPolyExpr, tcPolyExprNC
   :: 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)
 -- place to add context information.
@@ -116,9 +116,9 @@ tcPolyExprNC expr res_ty = tc_poly_expr_nc expr (mkCheckExpType res_ty)
 
 -- these versions take an ExpType
 tc_poly_expr, tc_poly_expr_nc :: LHsExpr GhcRn -> ExpSigmaType
-                              -> TcM (LHsExpr GhcTcId)
+                              -> TcM (LHsExpr GhcTc)
 tc_poly_expr expr res_ty
-  = addExprErrCtxt expr $
+  = addErrCtxt (exprCtxt expr) $
     do { traceTc "tcPolyExpr" (ppr res_ty); tc_poly_expr_nc expr res_ty }
 
 tc_poly_expr_nc (L loc expr) res_ty
@@ -130,31 +130,22 @@ tc_poly_expr_nc (L loc expr) 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') }
-
----------------
-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)
+tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
+-- Infer a *rho*-type. The return type is always instantiated.
+-- Don't wrap in "In the expression Wrap in a context iff non-atom
+tcInferRho le@(L _ e)
+  | isAtomicHsExpr e = tcInferRhoNC le
+  | otherwise        = addErrCtxt (exprCtxt le) (tcInferRhoNC le)
 
 tcInferRhoNC (L loc expr)
   = setSrcSpan loc $
-    do { (expr', rho) <- tcInferInst (tcExpr expr)
+    do { (expr', rho) <- tcInfer (tcExpr expr)
        ; return (L loc expr', rho) }
 
+exprCtxt :: LHsExpr GhcRn -> SDoc
+exprCtxt expr
+  = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr))
+
 {-
 ************************************************************************
 *                                                                      *
@@ -165,29 +156,38 @@ tcInferRhoNC (L loc 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
+  = addErrCtxt (exprCtxt 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
-    tc_prag (XHsPragE x) = noExtCon x
+  = do { expr' <- tcLExpr expr res_ty
+       ; return (HsPragE x (tcExprPrag prag) expr') }
 
 tcExpr (HsOverLit x lit) res_ty
   = do  { lit' <- newOverloadedLit lit res_ty
@@ -197,7 +197,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
@@ -332,7 +332,7 @@ 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) <- tcInferAppHead arg1
+       ; (arg1', arg1_ty) <- tcInferRho arg1
 
        ; let doc   = text "The first argument of ($) takes"
              orig1 = lexprCtOrigin arg1
@@ -373,7 +373,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
@@ -384,16 +384,24 @@ 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) <- tcInferRho op
+
+       ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
+                  <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
+       ; arg1' <- tcArg op arg1 arg1_ty 1
+       ; arg2' <- tcArg 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 = lexprCtOrigin 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) <- tcInferAppHead op
+  = do { (op', op_ty) <- tcInferRho 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)
@@ -408,7 +416,7 @@ tcExpr expr@(SectionR x op arg2) res_ty
     -- See #13285
 
 tcExpr expr@(SectionL x arg1 op) res_ty
-  = do { (op', op_ty) <- tcInferAppHead op
+  = do { (op', op_ty) <- tcInferRho op
        ; dflags <- getDynFlags      -- Note [Left sections]
        ; let n_reqd_args | xopt LangExt.PostfixOperators dflags = 1
                          | otherwise                            = 2
@@ -504,7 +512,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
@@ -527,13 +535,13 @@ 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
@@ -985,11 +993,24 @@ 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
+tcExprPrag (XHsPragE x) = noExtCon x
+
+
 {- *********************************************************************
 *                                                                      *
              Expression with type signature e::ty
@@ -1015,7 +1036,7 @@ tcExprWithSig expr hs_ty
 -}
 
 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
@@ -1074,111 +1095,118 @@ 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
+-- HsExprArg is a specialised verion HsArg is defined in GHC.Hs.Types
+
+-- The outer location is the location of the application itself
+type LHsExprArgIn  = HsExprArg 'Renamed
+type LHsExprArgOut = HsExprArg 'Typechecked
+
+-- A GHC specific type, so using TTG only where necessary
+data HsExprArg id
+  = HsExprValArg  SrcSpan        -- Of the application
+                  (LHsExpr (GhcPass id))
+  | HsExprTypeArg SrcSpan        -- Of the application
+                  (LHsWcType (NoGhcTc (GhcPass id)))
+                  !(XExprTypeArg id)
+  | HsExprPar     SrcSpan        -- Of the (expr)
+  | HsArgWrap    !(XArgWrap id)   -- Wrapper, after typechecking
+
+instance OutputableBndrId id => Outputable (HsExprArg id) where
+  ppr (HsExprValArg _ tm)       = ppr tm
+  ppr (HsExprTypeArg _ hs_ty _) = char '@' <> ppr hs_ty
+  ppr (HsExprPar _)             = text "HsExprPar"
+  ppr (HsArgWrap w)             = case ghcPass @id of
+                                    GhcTc -> text "HsArgWrap" <+> ppr w
+                                    _     -> empty
+
+type family XExprTypeArg id where
+  XExprTypeArg 'Parsed      = NoExtField
+  XExprTypeArg 'Renamed     = NoExtField
+  XExprTypeArg 'Typechecked = Type
+
+type family XArgWrap id where
+  XArgWrap 'Parsed      = NoExtField
+  XArgWrap 'Renamed     = NoExtField
+  XArgWrap 'Typechecked = HsWrapper
+
+addArgWrap :: HsWrapper -> [LHsExprArgOut] -> [LHsExprArgOut]
+addArgWrap wrap args
+ | isIdHsWrapper wrap = args
+ | otherwise          = HsArgWrap wrap : args
+
+wrapHsArgs :: LHsExpr GhcTc -> [LHsExprArgOut]-> LHsExpr GhcTc
+wrapHsArgs fun args
+  = go fun args
+  where
+    go fun [] = fun
+    go (L l fun) (HsArgWrap wrap : args)      = go (L l $ mkHsWrap wrap fun) args
+    go fun (HsExprValArg l arg : args)        = go (L l $ HsApp noExtField fun arg) args
+    go fun (HsExprTypeArg l hs_ty ty : args)  = go (L l $ HsAppType ty fun hs_ty) args
+    go fun (HsExprPar l : args)               = go (L l $ HsPar noExtField fun) args
+
+collectHsArgs :: LHsExpr GhcRn -> (LHsExpr GhcRn, [LHsExprArgIn])
+collectHsArgs e = go e []
+  where
+    go (L l (HsPar _     fun))       args = go fun (HsExprPar l : args)
+    go (L l (HsApp _     fun arg))   args = go fun (HsExprValArg l arg : args)
+    go (L l (HsAppType _ fun hs_ty)) args = go fun (HsExprTypeArg l hs_ty noExtField : args)
+    go e                             args = (e,args)
+
+isHsValArg :: HsExprArg id -> Bool
+isHsValArg (HsExprValArg {}) = True
+isHsValArg _                 = False
+
+isArgPar :: HsExprArg id -> Bool
+isArgPar (HsExprPar {}) = True
+isArgPar _              = False
+
+tcApp :: HsExpr GhcRn  -- either HsApp or HsAppType
+       -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcApp expr res_ty
+  = do { (fun, args, app_res_ty) <- tcInferApp (noLoc expr)
+       ; if isTagToEnum fun
+         then tcTagToEnum expr fun args app_res_ty res_ty
+         else
+    do { let expr' = wrapHsArgs fun args
+       ; addFunResCtxt True (unLoc fun) app_res_ty res_ty $
+         tcWrapResult expr (unLoc expr') app_res_ty res_ty } }
+
+tcInferApp :: LHsExpr GhcRn
+           -> TcM ( LHsExpr 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
+    L loc (HsRecFld _ fld_lbl)   <- fun
+  , Ambiguous _ lbl              <- fld_lbl  -- Still ambiguous
+  , HsExprValArg _ (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 }
-
-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
-  where
-    n_val_args = count isHsValArg args
+       ; tcInferApp_finish fun (L loc tc_fun) fun_ty args }
 
-tcApp m_herald fun args res_ty
+  | otherwise
   = do { (tc_fun, fun_ty) <- tcInferAppHead fun
-       ; tcFunApp m_herald fun tc_fun fun_ty args res_ty }
+       ; tcInferApp_finish fun tc_fun fun_ty args }
+  where
+    (fun, args) = collectHsArgs expr
 
 ---------------------
-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) }
+tcInferApp_finish
+    :: LHsExpr GhcRn                  -- Renamed function
+    -> LHsExpr GhcTc -> TcSigmaType -- Function and its type
+    -> [LHsExprArgIn]                 -- Arguments
+    -> TcM (LHsExpr GhcTc, [LHsExprArgOut], TcSigmaType)
+
+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 ]
+
+       ; (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args
+
+       ; return (tc_fun, tc_args, actual_res_ty) }
 
 mk_app_msg :: LHsExpr GhcRn -> [LHsExprArgIn] -> SDoc
 mk_app_msg fun args = sep [ text "The" <+> text what <+> quotes (ppr expr)
@@ -1189,26 +1217,32 @@ mk_app_msg fun args = sep [ text "The" <+> text what <+> quotes (ppr expr)
     -- 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]
+    type_app_args = [hs_ty | HsExprTypeArg _ hs_ty _ <- args]
 
 mk_op_msg :: LHsExpr GhcRn -> SDoc
 mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
 
 ----------------
-tcInferAppHead :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
+tcInferAppHead :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)
 -- Infer type of the head of an application,
 --   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
 
 tcInferAppHead el@(L loc e)
   = case e of
+      HsPar _ e               -> tcInferAppHead e
+      HsPragE x prag e        -> do { (e',ty) <- tcInferAppHead e
+                                    ; return (L loc $ HsPragE x (tcExprPrag prag) e', ty) }
       HsVar _ (L _ nm)        -> add_loc $ tcInferId nm
       HsRecFld _ f            -> add_loc $ tcInferRecSelId f
       ExprWithTySig _ e hs_ty -> add_loc_ctxt $ tcExprWithSig e hs_ty
-      _                       -> add_loc_ctxt $ tcInferInst (tcExpr e)
+      _                       -> add_loc_ctxt $ tcInfer (tcExpr e)
   where
     add_loc_ctxt thing = addErrCtxt (exprCtxt el) $
                          add_loc thing
@@ -1222,35 +1256,42 @@ tcInferAppHead el@(L loc e)
 -- applications
 tcArgs :: LHsExpr 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
+    fun_orig = lexprCtOrigin fun
+    herald = mk_app_msg fun orig_args
+
+    -- commented out
     -- 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.
     -- 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
 
-    go _ _ fun_ty [] = return (idHsWrapper, [], fun_ty)
+    go :: Int -> TcSigmaType -> [LHsExprArgIn] -> TcM ([LHsExprArgOut], TcSigmaType)
+    go n fun_ty args
+      = do { traceTc "tcArgs:go {" (ppr n <+> ppr fun_ty $$ ppr args)
+           ; (args', res_ty) <- go' n fun_ty args
+           ; traceTc "tcArgs:go }" (ppr res_ty $$ ppr args')
+           ; return (args', res_ty) }
+    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 fun_ty (HsExprPar sp : args)
+      = do { (args', res_ty) <- go n fun_ty args
+           ; return (HsExprPar sp : args', res_ty) }
 
-    go acc_args n fun_ty (HsTypeArg l hs_ty_arg : args)
+    go' n fun_ty (HsExprTypeArg 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) fun_ty args
 
       | otherwise
       = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty
@@ -1278,30 +1319,22 @@ 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) insted_ty args
+                    ; return ( addArgWrap wrap1 $ HsExprTypeArg 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 fun_ty (HsExprValArg 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 (unLoc fun)) orig_fun_ty
+                                        n_val_args 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) res_ty args
+           ; return ( addArgWrap wrap $ HsExprValArg loc arg' : args'
                     , inner_res_ty ) }
-      where
-        doc = text "When checking the" <+> speakNth n <+>
-              text "argument to" <+> quotes (ppr fun)
+
+    go' n fun_ty (HsArgWrap {} : args)
+      = do { traceTc "tcArgs:wrap" empty; go n fun_ty args }
 
     ty_app_err ty arg
       = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty
@@ -1393,14 +1426,20 @@ and we had the visible type application
 ----------------
 tcArg :: LHsExpr 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' <- tcPolyExprNC 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
@@ -1611,7 +1650,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
@@ -1706,18 +1745,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 }
 
-tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
+tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
 tcCheckRecSelId rn_expr f@(Unambiguous _ (L _ lbl)) res_ty
   = do { (expr, actual_res_ty) <- tcInferRecSelId f
-       ; addFunResCtxt False (HsRecFld noExtField f) actual_res_ty res_ty $
+       ; addFunResCtxt False expr actual_res_ty res_ty $
          tcWrapResultO (OccurrenceOfRecSel lbl) rn_expr expr actual_res_ty res_ty }
 tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty
   = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of
@@ -1728,7 +1772,7 @@ tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty
 tcCheckRecSelId _ (XAmbiguousFieldOcc nec) _ = noExtCon nec
 
 ------------------------
-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) }
@@ -1737,14 +1781,10 @@ tcInferRecSelId (Ambiguous _ lbl)
 tcInferRecSelId (XAmbiguousFieldOcc nec) = noExtCon nec
 
 ------------------------
-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
@@ -1756,7 +1796,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
@@ -1766,7 +1806,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
@@ -1817,7 +1857,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 "_".
@@ -1886,60 +1926,50 @@ the users that complain.
 
 -}
 
-tcTagToEnum :: SrcSpan -> Name -> [LHsExprArgIn] -> ExpRhoType
-            -> TcM (HsWrapper, LHsExpr GhcTcId, [LHsExprArgOut])
+isTagToEnum :: LHsExpr GhcTc -> Bool
+isTagToEnum (L _ (HsVar _ (L _ fun_id))) = fun_id `hasKey` tagToEnumKey
+isTagToEnum _ = False
+
+tcTagToEnum :: HsExpr GhcRn -> LHsExpr 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'    = mkLHsWrap (WpTyApp rep_ty) fun
+             expr'   = wrapHsArgs fun' val_arg
+             df_wrap = mkWpCastR (mkTcSymCo coi)
+       ; return (mkHsWrap df_wrap (unLoc expr')) }}}}}
+
   where
+    vanilla_result
+      = do { let expr' = wrapHsArgs fun args
+           ; tcWrapResult expr (unLoc 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"
@@ -1950,18 +1980,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 (HsValArg e)                             = ppr e
-    pp (HsTypeArg _ (HsWC { hswc_body = L _ t })) = pprHsType t
-    pp (HsTypeArg _ (XHsWildCardBndrs nec)) = noExtCon nec
-    pp (HsArgPar _) = empty
-
-
 {-
 ************************************************************************
 *                                                                      *
@@ -2374,7 +2392,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
@@ -2384,7 +2402,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 }))
 
@@ -2398,7 +2416,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
@@ -2406,7 +2424,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
@@ -2501,19 +2519,12 @@ 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")
 
 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


=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -8,14 +8,13 @@ import GHC.Hs.Extension    ( GhcRn, GhcTcId )
 
 tcPolyExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId)
 
-tcMonoExpr, tcMonoExprNC
-  :: LHsExpr GhcRn -> ExpRhoType -> 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)
 
-tcInferAppHead :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
-
 tcSyntaxOp :: CtOrigin
            -> SyntaxExprRn
            -> [SyntaxOpType]           -- ^ shape of syntax operator arguments


=====================================
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
+                                     , tcPolyExpr )
 
 import GHC.Types.Basic (LexicalFixity(..))
 import GHC.Hs
@@ -335,7 +336,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
         }
 
 {-
@@ -415,7 +416,7 @@ 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) }
 
@@ -448,21 +449,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])
+        ; 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) }
 
@@ -563,7 +564,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) }
 
@@ -579,7 +580,7 @@ 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)
+               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) }
@@ -605,7 +606,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) }
@@ -665,7 +666,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') }
 
@@ -825,7 +826,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) }
 
@@ -838,7 +839,7 @@ 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)
+                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) }
@@ -866,7 +867,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) }
@@ -882,7 +883,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)
@@ -894,7 +895,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 ()
@@ -959,7 +960,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).
 
@@ -991,7 +992,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
@@ -1035,7 +1036,7 @@ 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)
+        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
@@ -1051,7 +1052,7 @@ 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
+                  { ret'      <- tcExpr ret res_ty
                   ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                  return ()
                   ; return (ret', pat')


=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -28,7 +28,7 @@ where
 
 import GhcPrelude
 
-import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferAppHead )
+import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho )
 
 import GHC.Hs
 import GHC.Tc.Utils.Zonk
@@ -116,7 +116,7 @@ tcInferPat :: HsMatchContext GhcRn -> LPat GhcRn
            -> TcM a
            -> TcM ((LPat GhcTcId, a), TcSigmaType)
 tcInferPat ctxt pat thing_inside
-  = tcInferInst $ \ exp_ty ->    -- The ir_inst flag is irrelevant in tcPat
+  = tcInfer $ \ exp_ty ->
     tc_lpat pat exp_ty penv thing_inside
  where
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
@@ -399,12 +399,17 @@ 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  {
-         -- Using tcInferAppHead here, rather than tcMonoExpr, lets us
-         -- have view functions with types like:
-         --    (forall a. blah) -> forall b. burble
-         -- So the overall_pat_ty is (forall a. blah), while the
-         -- inner pattern is checked with (forall b. burble)
-        ; (expr',expr_ty) <- tcInferAppHead expr
+         -- 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
+         -- Until simple subsumption, it'll be deeply instantiated, but
+         -- probably no one will notice.
+         -- An exotic example:
+         --    pair :: forall a. a -> forall b. b -> (a,b)
+         --    f (pair True -> x) = ...here (x :: forall b. b -> (Bool,b))
+        ; (expr',expr_ty) <- tcInferRho expr
 
          -- Expression must be a function
         ; let expr_orig = lexprCtOrigin expr


=====================================
compiler/GHC/Tc/Gen/Rule.hs
=====================================
@@ -201,7 +201,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
=====================================
@@ -617,7 +617,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)
@@ -640,7 +640,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
@@ -677,7 +677,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)
        }


=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -1787,8 +1787,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
@@ -2495,8 +2495,7 @@ tcRnExpr hsc_env mode rdr_expr
     ((tclvl, res_ty), lie)
           <- captureTopConstraints $
              pushTcLevelM          $
-             do { (_tc_expr, expr_ty) <- tc_infer rn_expr
-                ; return expr_ty } ;
+             tc_infer rn_expr ;
 
     -- Generalise
     (qtvs, dicts, _, residual, _)
@@ -2522,8 +2521,10 @@ tcRnExpr hsc_env mode rdr_expr
     return (snd (normaliseType fam_envs Nominal ty))
     }
   where
-    tc_infer | inst      = tcInferRhoNC
-             | otherwise = tcInferAppHead
+    tc_infer expr | inst      = do { (_, ty)    <- tcInferRhoNC expr
+                                   ; return ty }
+                  | otherwise = do { (_, _, ty) <- tcInferApp expr
+                                   ; return ty }
     -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
       TM_Inst    -> (True,  NoRestrictions, id)


=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -1063,7 +1063,7 @@ tcTryM :: TcRn r -> TcRn (Maybe r)
 tcTryM thing_inside
   = do { either_res <- tryM thing_inside
        ; return (case either_res of
-                    Left _  -> Nothing
+                    Left exn  -> pprTrace "tcTryM" (text (show exn)) Nothing
                     Right r -> Just r) }
          -- In the Left case the exception is always the IOEnv
          -- built-in in exception; see IOEnv.failM


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


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


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -26,7 +26,7 @@ module GHC.Tc.Utils.Unify (
 
   --------------------------------
   -- Holes
-  tcInferInst, tcInferNoInst,
+  tcInfer,
   matchExpectedListTy,
   matchExpectedTyConApp,
   matchExpectedAppTy,
@@ -199,8 +199,8 @@ matchExpectedFunTys herald arity orig_ty thing_inside
     ------------
     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
@@ -231,22 +231,24 @@ 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 fun_ty 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
+                      -> TcSigmaType           -- Original function type
+                      -> Arity                 -- And number of args to which it is applied
+                      -> Arity                 -- Number of new value args wanted
+                      -> TcSigmaType           -- Type to analyse
                       -> 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 herald ct_orig mb_thing
+                      orig_fun_ty n_val_args_in_call
+                      n_val_args_wanted fun_ty
+  = go n_val_args_wanted 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 +276,35 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
     --
     -- Refactoring is welcome.
     go :: Arity
-       -> [TcSigmaType] -- accumulator of arguments (reversed)
        -> TcSigmaType   -- the remainder of the type as we're processing
        -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
-    go 0 _ ty = return (idHsWrapper, [], ty)
+    go 0 ty = return (idHsWrapper, [], ty)
 
-    go n acc_args ty
+    go n 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 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 ty
+      | Just ty' <- tcView ty = go n ty'
 
-    go n acc_args (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+    go n (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) 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 orig_fun_ty)
 
-    go n acc_args ty@(TyVarTy tv)
+    go n ty@(TyVarTy tv)
       | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
-               Indirect ty' -> go n acc_args ty'
+               Indirect ty' -> go n ty'
                Flexi        -> defer n ty }
 
        -- In all other cases we bale out into ordinary unification
@@ -321,8 +322,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 ty = addErrCtxtM mk_ctxt (defer n ty)
 
     ------------
     defer n fun_ty
@@ -333,16 +333,16 @@ 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 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
+    mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
+    mk_ctxt env
+      = do { (env1, zonked) <- zonkTidyTcType env orig_fun_ty
+                   -- Zonking might change # of args
+           ; let (zonked_args, _)   = tcSplitPiTys zonked
+                 n_val_args_in_type = count isVisibleBinder zonked_args
+                 (env2, unzonked)   = tidyOpenType env1 orig_fun_ty
            ; return ( env2
-                    , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) }
+                    , mk_fun_tys_msg unzonked zonked n_val_args_in_type
+                                     n_val_args_in_call herald) }
 
 mk_fun_tys_msg :: TcType  -- the full type passed in (unzonked)
                -> TcType  -- the full type passed in (zonked)
@@ -350,15 +350,15 @@ mk_fun_tys_msg :: TcType  -- the full type passed in (unzonked)
                -> 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
+mk_fun_tys_msg full_ty ty n_args_in_type n_args_in_call herald
+  = herald <+> speakNOf n_args_in_call (text "argument") <> comma $$
+    if n_args_in_type == n_args_in_call
       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]
+                if n_args_in_type == 0 then text "has none"
+                else text "has only" <+> speakN n_args_in_type]
 
 ----------------------
 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
@@ -564,8 +564,7 @@ tcSubTypeET orig ctxt (Check ty_actual) ty_expected
 
 tcSubTypeET _ _ (Infer inf_res) ty_expected
   = do { co <- fillInferResult ty_expected inf_res
-               -- In patterns we ignore the ir_inst field
-               -- and never instantatiate
+               -- In patterns we do not instantatiate
 
        ; return (mkWpCastN (mkTcSymCo co)) }
 
@@ -866,16 +865,9 @@ tcWrapResultO orig rn_expr expr actual_ty res_ty
 
 -- | 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) }
@@ -884,16 +876,11 @@ instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrap
 -- If wrap = instantiateAndFillInferResult t1 t2
 --    => wrap :: t1 ~> t2
 -- See Note [Deep instantiation of InferResult]
-instantiateAndFillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
-  | instantiate_me   -- This is *the* place where ir_inst is consulted
+instantiateAndFillInferResult orig ty inf_res
   = do { (wrap, rho) <- deeplyInstantiate orig ty
        ; co <- fillInferResult rho inf_res
        ; return (mkWpCastN co <.> wrap) }
 
-  | otherwise
-  = do { co <- fillInferResult ty inf_res
-       ; return (mkWpCastN co) }
-
 fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
 -- If wrap = fillInferResult t1 t2
 --    => wrap :: t1 ~> t2
@@ -925,9 +912,8 @@ fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
 
 {- Note [Deep 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 alwayd deeply instantiate before filling in InferResult,
+and in some cases not: see #17775
 
 ir_inst = True: deeply instantiate
 ----------------------------------


=====================================
compiler/GHC/Tc/Utils/Zonk.hs
=====================================
@@ -770,9 +770,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 _ _ _)


=====================================
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’:


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


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


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


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


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


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



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f39a0d86de843c105dc9cd4e0bd631176300d7f7

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f39a0d86de843c105dc9cd4e0bd631176300d7f7
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200413/502494d2/attachment-0001.html>


More information about the ghc-commits mailing list