-- CAUTION: Any changes to tcApp should be reflected here

 -- cf. T19167. the head is an expanded expression applied to a type

 -- TODO: Use runInfer for tcExprSigma?

 tcExprSigma :: Bool -> HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType)

 tcExprSigma inst rn_expr

   = do { (fun@(rn_fun,fun_ctxt), rn_args) <- splitHsApps rn_expr

        ; code_orig <- getSrcCodeOrigin

        ; let fun_orig = srcCodeOriginCtOrigin rn_expr code_orig

        ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst fun_orig (tc_fun, rn_fun, fun_ctxt) fun_sigma rn_args

        ; let tc_expr = rebuildHsApps (tc_fun, fun_ctxt) tc_args

        ; return (tc_expr, app_res_sigma) }

 -- See Note [tcApp: typechecking applications]

 tcApp rn_expr exp_res_ty

   = do { -- Step 1: Split the application chain

        ; inGenCode <- inGeneratedCode

        ; traceTc "tcApp {" $

            vcat [ text "generated? " <+> ppr inGenCode

                 , text "rn_expr:" <+> ppr rn_expr

                 , text "rn_fun:" <+> ppr rn_fun

                 , text "rn_args:" <+> ppr rn_args ]

        -- Step 2: Infer the type of `fun`, the head of the application

        ; (tc_fun, fun_sigma) <- tcInferAppHead fun

              -- inst_final: top-instantiate the result type of the application,

              -- EXCEPT if we are trying to infer a sigma-type

              inst_final = case exp_res_ty of

               , text "fun_origin" <+> ppr fun_orig

               , text "do_ql:" <+> ppr do_ql]

        ; (inst_args, app_res_rho)

          -- See (TCAPP1) and (TCAPP2) in

          -- Note [tcApp: typechecking applications]

                                                    app_res_rho exp_res_ty

                          -- Step 4.2: typecheck the  arguments

                          -- Step 4.3: wrap up

                        ; finishApp tc_head tc_args app_res_rho res_wrap }

                          -- Step 5.2: typecheck the arguments, and monomorphise

                          --           any un-unified instantiation variables

                          -- Step 5.3: zonk to expose the polymorphism hidden under

                          --           QuickLook instantiation variables in `app_res_rho`

                        ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

         thing_inside

 ----------------

 -- Importantly, tcValArgs works left-to-right, so that by the time we

 -- encounter an argument, we have monomorphised all the instantiation

 -- variables that its type contains.  All that is left to do is an ordinary

 -- zonkTcType.  See Note [Monomorphise instantiation variables].

   where

     go _ _ [] = return []

     go do_ql pos (arg : args) =

          ; args' <- go do_ql pos' args

          ; return (arg' : args') }

       where

              = pos

          -> TcM (HsExprArg 'TcpTc)          -- Resulting argument

 tcValArg _     _ _ (EPrag l p)         = return (EPrag l (tcExprPrag p))

 tcValArg _     _ _ (ETypeArg l hty ty) = return (ETypeArg l hty ty)

   -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]

 tcValArg _     _ _ (EWrap ew)          = return (EWrap ew)

                             , ea_arg    = larg@(L arg_loc arg)

                             , ea_arg_ty = sc_arg_ty })

     do { -- Crucial step: expose QL results before checking exp_arg_ty

          -- So far as the paper is concerned, this step applies

          -- the poly-substitution Theta, learned by QL, so that we

               NoQL -> return sc_arg_ty

        ; traceTc "tcValArg {" $

          vcat [ text "lspan:" <+> ppr lspan

               , text "sigma_type" <+> ppr (mkCheckExpType exp_arg_ty)

               , text "arg:" <+> ppr larg

               ]

                          , ea_arg = L arg_loc arg'

                          , ea_arg_ty = noExtField }) }

                         eaql_wanted   = wanted

                       , eaql_loc_span = lspan

                       , eaql_arg_ty   = sc_arg_ty

                       , eaql_args     = inst_args

                       , eaql_encl     = arg_influences_enclosing_call

                       , eaql_res_rho  = app_res_rho })

     do { -- Expose QL results to tcSkolemise, as in EValArg case

          Scaled mult exp_arg_ty <- liftZonkM $ zonkScaledTcType sc_arg_ty

                                        , text "args:" <+> ppr inst_args

                                        , text "mult:" <+> ppr mult

                                        , text "fun" <+> ppr fun

                                        , text "tc_head" <+> ppr tc_head])

        ; ds_flag <- getDeepSubsumptionFlag

                   ; unless arg_influences_enclosing_call $  -- Don't repeat

                     qlUnify app_res_rho exp_arg_rho         -- the qlUnify

                   ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

                   ; res_wrap <- checkResultTy rn_expr tc_head inst_args

                                               app_res_rho (mkCheckExpType exp_arg_rho)

                     -- Generally speaking we pass in True; in Fig 5 of the paper

                     --    |-inst returns a rho-type

           -> CtOrigin

           -> TcSigmaType -> [HsExprArg 'TcpRn]

           -> TcM ( [HsExprArg 'TcpInst]

                  , TcSigmaType )   -- Does not instantiate trailing invisible foralls

 -- This crucial function implements the |-inst judgement in Fig 4, plus the

 -- modification in Fig 5, of the QL paper:

 -- "A quick look at impredicativity" (ICFP'20).

   = do { traceTc "tcInstFun" (vcat [ text "origin" <+> ppr fun_orig

                                    , text "tc_fun" <+> ppr tc_fun

                                    , text "fun_sigma" <+> ppr fun_sigma

                                    , text "args:" <+> ppr rn_args

                                    , text "do_ql" <+> ppr do_ql

        ; setQLInstLevel do_ql $  -- See (TCAPP1) and (TCAPP2) in

                                  -- Note [tcApp: typechecking applications]

                  go 1 [] fun_sigma rn_args }

       = do { (_inst_tvs, wrap, fun_rho) <-

                 -- addHeadCtxt: important for the class constraints

                 -- that may be emitted from instantiating fun_sigma

                 instantiateSigma fun_orig fun_conc_tvs tvs theta body2

                   -- See Note [Representation-polymorphism checking built-ins]

                   -- in GHC.Tc.Utils.Concrete.

                   (Just $ HsExprTcThing tc_fun)

                   (n_val_args, fun_sigma) fun_ty

            ; let acc' = arg' : addArgWrap wrap acc

            ; go (pos+1) acc' res_ty rest_args }

     _           -> False

 looks_like_type_arg _ = False

            -> TcM a -> TcM a

 -- There are 2 cases:

 -- 1. In the normal case, we add an informative context (<=> `inGeneratedCode` is `False`)

 --    (iii) if arg_loc is RealSrcLoc then update tcl_loc and add "In the expression: arg" to ErrCtxtStack

 --  See Note [Rebindable syntax and XXExprGhcRn] in GHC.Hs.Expr

 --  See Note [Expanding HsDo with XXExprGhcRn] in GHC.Tc.Gen.Do

   = do { in_generated_code <- inGeneratedCode

        ; err_ctx <- getErrCtxt

        ; env0 <- liftZonkM tcInitTidyEnv

                                     , text "arg: " <+> ppr (arg, arg_no)

                                     , text "arg_loc:" <+> ppr arg_loc

                                     , text "fun:" <+> ppr fun

                                     ])

          then updCtxtForArg (L arg_loc arg) $

                    thing_inside

          else do setSrcSpanA arg_loc                    $

 -}

              -> LHsExpr GhcRn          -- ^ Argument

              -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function

              -> TcM (HsExprArg 'TcpInst)

 -- See Note [Quick Look at value arguments]

   = do { is_rho <- tcIsDeepRho (scaledThing orig_arg_ty)

        ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)

        ; if not is_rho

 skipQuickLook :: SrcSpan -> LHsExpr GhcRn -> Scaled TcRhoType

               -> TcM (HsExprArg 'TcpInst)

                     , ea_arg    = larg

                     , ea_arg_ty = arg_ty })

   | Just {} <- tcSplitAppTy_maybe ty        = True

   | otherwise                               = False

               -> Scaled TcRhoType  -- Deeply skolemised

               -> TcM (HsExprArg 'TcpInst)

 -- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper

                            -- generated by calls in arg

        -- Step 1: get the type of the head of the argument

        ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun

               , text "args:" <+> ppr rn_args ]

        ; case mb_fun_ty of {

            Just (tc_fun, fun_sigma) ->

        -- step 2: use |-inst to instantiate the head applied to the arguments

        ; do_ql <- wantQuickLook rn_fun

        ; ((inst_args, app_res_rho), wanted)

              <- captureConstraints $

                 -- We must capture type-class and equality constraints here, but

                 -- not equality constraints.  See (QLA6) in Note [Quick Look at

                 -- value arguments]

        ; traceTc "quickLookArg done }" (ppr rn_fun)

                            , eaql_arg_ty   = sc_arg_ty

                            , eaql_larg     = larg

                            , eaql_tc_fun   = tc_head

 -- See `checkLastStmt` and `Syntax.Expr.StmtLR.LastStmt`

    | NoSyntaxExprRn <- ret_expr

    -- Last statement is just body if we are not in ListComp context. See Syntax.Expr.LastStmt

    | SyntaxExprRn ret <- ret_expr  -- We have unfortunately lost the location on the return function :(

    --

    --               return e  ~~> return e

    -- to make T18324 work

    = do let expansion = L body_loc (genHsApp ret body)

 expand_do_stmts doFlavour (stmt@(L loc (LetStmt _ bs)) : lstmts) =

 -- See  Note [Expanding HsDo with XXExprGhcRn] Equation (3) below

   | otherwise

   = pprPanic "expand_do_stmts: The impossible happened, missing bind operator from renamer" (text "stmt" <+> ppr  stmt)

 -- See Note [BodyStmt] in Language.Haskell.Syntax.Expr

 -- See  Note [Expanding HsDo with XXExprGhcRn] Equation (1) below

 --              stmts ~~> stmts'

 --      e ; stmts ~~> (>>) e stmts'

   do expand_stmts_expr <- expand_do_stmts doFlavour lstmts

      let expansion = genHsExpApps then_op  -- (>>)

                      , expand_stmts_expr ]

      return $ L loc (mkExpandedStmt stmt doFlavour expansion)

 mkExpandedPatRn :: Pat GhcRn -> HsExpr GhcRn -> HsExpr GhcRn

 mkExpandedPatRn pat e = XExpr (ExpandedThingRn (OrigPat pat) e)

                , eaql_larg    :: LHsExpr GhcRn       -- Original application, for

                                                      -- location and error msgs

                , eaql_rn_fun  :: HsExpr GhcRn  -- Head of the argument if it is an application

                , eaql_fun_ue  :: UsageEnv -- Usage environment of the typechecked head (QLA5)

                , eaql_args    :: [HsExprArg 'TcpInst]    -- Args: instantiated, not typechecked

                , eaql_wanted  :: WantedConstraints

 --     cases are dealt with by splitHsApps.

 --

 -- See Note [tcApp: typechecking applications] in GHC.Tc.Gen.App

     do { mb_tc_fun <- tcInferAppHead_maybe fun

        ; case mb_tc_fun of

             Just (fun', fun_sigma) -> return (fun', fun_sigma)

     case fun of

       HsVar _ nm                  -> Just <$> tcInferId nm

       XExpr (HsRecSelRn f)        -> Just <$> tcInferRecSelId f

                                                     tcExprSigma False e)

       ExprWithTySig _ e hs_ty     -> Just <$> tcExprWithSig e hs_ty

       HsOverLit _ lit             -> Just <$> tcInferOverLit lit