-> TcSigmaType -> [HsExprArg 'TcpRn]

           -> TcM ( [HsExprArg 'TcpInst]

                  , TcSigmaType )   -- Does not instantiate trailing invisible foralls

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

 tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args

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

                                    , text "fun_sigma" <+> ppr fun_sigma

                                    , text "args:" <+> ppr rn_args

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

        ; traceTc "tcInstFun:ret" (ppr fun_ty)

        ; return res

        }

      = return $ exprCtOrigin rn_fun

      | otherwise -- If the location is generated, the best we can do is to

      = do { err_ctxt_stack <- getErrCtxt

           ; let hs_ctxt = case err_ctxt_stack of

                              (c:_) -> c

           ; return $ hsCtxtCtOrigin hs_ctxt

           }

     -- These are the type variables which must be instantiated to concrete

     -- types. See Note [Representation-polymorphic Ids with no binding]

     -- in GHC.Tc.Utils.Concrete

     inst_fun _                = isInferredForAllTyFlag

     -----------

             -> [HsExprArg 'TcpInst]     -- Accumulator, reversed

             -> TcSigmaType -> [HsExprArg 'TcpRn]

             -> TcM ([HsExprArg 'TcpInst], TcSigmaType)

     -- go: If fun_ty=kappa, look it up in Theta

       | Just kappa <- getTyVar_maybe fun_ty

       , isQLInstTyVar kappa

       = do { cts <- readMetaTyVar kappa

            ; case cts of

      | otherwise

     -- go1: fun_ty is not filled-in instantiation variable

     --      ('go' dealt with that case)

     -- Handle out-of-scope functions gracefully

       | fun_is_out_of_scope, looks_like_type_arg arg   -- See Note [VTA for out-of-scope functions]

     -- Rule IALL from Fig 4 of the QL paper; applies even if args = []

     -- Instantiate invisible foralls and dictionaries.

     -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate

       | (tvs,   body1) <- tcSplitSomeForAllTyVars (inst_fun args) fun_ty

       , (theta, body2) <- if inst_fun args Inferred

                           then tcSplitPhiTy body1

       , let no_tvs   = null tvs

             no_theta = null theta

       , not (no_tvs && no_theta)

                 -- addHeadCtxt: important for the class constraints

                 -- that may be emitted from instantiating fun_sigma

                 setSrcSpan fun_lspan $

                   -- argument of (#,#) to @LiftedRep, but want to rule out the

                   -- second instantiation @r.

                 -- Going around again means we deal easily with

                 -- nested  forall a. Eq a => forall b. Show b => blah

     -- Rule IRESULT from Fig 4 of the QL paper; no more arguments

        | XExpr (ConLikeTc (RealDataCon dc)) <- tc_fun

        , isNewDataCon dc

        , [Scaled _ orig_arg_ty] <- dataConOrigArgTys dc

       = return (reverse acc, fun_ty)

     -- Rule ITVDQ from the GHC Proposal #281

       | Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty

       = assertPpr (binderFlag tvb == Required) (ppr fun_ty $$ ppr arg) $

         -- Any invisible binders have been instantiated by IALL above,

         -- so this forall must be visible (i.e. Required)

         do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg

            ; let wrap = mkWpTyApps [ty_arg]

     -- Rule ITYARG from Fig 4 of the QL paper

       = do { (ty_arg, inst_ty) <- tcVTA fun_conc_tvs fun_ty hs_ty

            ; let arg' = ETypeArg { ea_loc_span = ctxt, ea_hs_ty = hs_ty, ea_ty_arg = ty_arg }

     -- Rule IVAR from Fig 4 of the QL paper:

       | Just kappa <- getTyVar_maybe fun_ty

       , isQLInstTyVar kappa

       = -- Function type was of form   f :: forall a b. t1 -> t2 -> b

         --   - We must be sure to actually update the variable right now,

         --     not defer in any way, because this is a QL instantiation variable.

         -- It's easier just to do the job directly here.

            ; res_ty  <- newOpenFlexiTyVarTyQL do_ql TauTv

            ; let fun_ty' = mkScaledFunTys arg_tys res_ty

                  -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk

                  --      co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'

     -- Rule IARG from Fig 4 of the QL paper:

         (EValArg { ea_arg = arg, ea_loc_span = ctxt } : rest_args)

            ; (fun_co, arg_ty, res_ty) <-

                 -- NB: matchActualFunTy does the rep-poly check.

                 -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int

                   (n_val_args, fun_sigma) fun_ty

            ; arg' <- quickLookArg do_ql pos ctxt rn_head arg arg_ty

            ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc

     -- Make a fresh nus for each argument in rule IVAR

                        FRRExpectedFunTy (mk_herald fun_orig tc_fun arg) i

                -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],

                -- thereby ensuring that the arguments have concrete runtime representations

          tcInferRhoFRR, tcInferRhoFRRNC,

          tcPolyLExpr,  tcPolyLExprSig, tcPolyLExprNC,

          tcPolyExpr, tcExpr,

          tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,

          tcCheckId,

          ) where

 import GHC.Hs

 import GHC.Hs.Syn.Type

 import GHC.Rename.Utils

 import GHC.Rename.Env         ( addUsedGRE, getUpdFieldLbls )

 import GHC.Tc.Gen.App

 import GHC.Tc.Gen.Head

 import GHC.Tc.Gen.Do

 ************************************************************************

 -}

 tcHsExpansion :: HsExpansion GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)

 tcHsExpansion (HSE { hse_ctxt = o, hse_exp = e }) res_ty

    = do { e' <- tcMonoLExpr e res_ty

           HSE { hse_ctxt = o, hse_exp = e' } }

 {-

 ************************************************************************

 *                                                                      *

 import GHC.Tc.Types.Origin ( CtOrigin, FixedRuntimeRepContext )

 import GHC.Core.Type ( Mult )

 import GHC.Hs.Extension ( GhcRn, GhcTc )

 tcCheckPolyExpr, tcCheckPolyExprNC ::

           LHsExpr GhcRn

 tcInferExpr :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType)

 tcSyntaxOp :: CtOrigin

            -> SyntaxExprRn

            -> [SyntaxOpType]           -- ^ shape of syntax operator arguments

        , pprArgInst, addFunResCtxt ) where

 import GHC.Prelude

 import GHC.Hs

 import GHC.Hs.Syn.Type

 import GHC.Tc.Gen.HsType

 import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )

 import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig )

 import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc )

         GHC.Tc.Gen.Bind

         GHC.Tc.Gen.Default

         GHC.Tc.Gen.Do

         GHC.Tc.Gen.Export

         GHC.Tc.Gen.Expr

         GHC.Tc.Gen.Foreign