tcInferSigma inst (L loc rn_expr)

   = addExprCtxt rn_expr $

     setSrcSpanA loc     $

        ; return app_res_sigma }

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

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

        ; do_ql <- wantQuickLook rn_fun

        ; (tc_fun, fun_sigma) <- tcInferAppHead fun

        ; tc_args <- tcValArgs do_ql inst_args

        ; let tc_expr = rebuildHsApps (tc_fun, fun_ctxt) tc_args

        ; return (tc_expr, app_res_sigma) }

 The latter is much better. That is why we call checkResultType before tcValArgs.

 -}

       -> ExpRhoType   -- When checking, -XDeepSubsumption <=> deeply skolemised

       -> TcM (HsExpr GhcTc)

 -- See Note [tcApp: typechecking applications]

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

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

        ; traceTc "tcApp {" $

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

        ; (inst_args, app_res_rho)

        ; case do_ql of

             NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)

                     --    in tcInferSigma, which is used only to implement :type

                     -- Otherwise we do eager instantiation; in Fig 5 of the paper

                     --    |-inst returns a rho-type

           -> TcSigmaType -> [HsExprArg 'TcpRn]

           -> TcM ( [HsExprArg 'TcpInst]

                  , TcSigmaType )

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

                                    , text "fun_sigma" <+> ppr fun_sigma

                                    , text "args:" <+> ppr rn_args

                                    , text "do_ql" <+> ppr do_ql

                                  -- Note [tcApp: typechecking applications]

                  go 1 [] fun_sigma rn_args }

   where

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

        ; 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]

 import GHC.Hs ( HsExpr )

 import GHC.Tc.Types  ( TcM )

 import GHC.Tc.Utils.TcType ( TcSigmaType )

 import GHC.Hs.Extension ( GhcRn, GhcTc )

 import GHC.Prelude (Bool)

       -- The special case for lambda: go to tcLambdaMatches, passing pat_tys

       tc_body e@(HsLam x lam_variant matches)

                                                    (mkCheckExpType rho_ty)

                -- NB: tcLambdaMatches concludes with deep skolemisation,

                --     if DeepSubsumption is on;  hence no need to do that here

     do  { expr' <- tcExpr expr res_ty

         ; return (L loc expr') }

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

 tcExpr :: HsExpr GhcRn

        -> ExpRhoType   -- DeepSubsumption <=> when checking, this type

 -- These constructors are the union of

 --   - ones taken apart by GHC.Tc.Gen.Head.splitHsApps

 --   - ones understood by GHC.Tc.Gen.Head.tcInferAppHead_maybe

 -- Typecheck an occurrence of an unbound Id

 --

          -- See Note [Short cut for overloaded literals] in GHC.Tc.Utils.TcMType

        ; case mb_res of

            Just lit' -> return (HsOverLit noExtField lit')

            -- Why go via tcApp? See Note [Typechecking overloaded literals]

 {- Note [Typechecking overloaded literals]

 tcXExpr :: XXExprGhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)

 tcXExpr (PopErrCtxt e) res_ty

    = mkExpandedTc o <$> -- necessary for breakpoints

 -- For record selection, same as HsVar case

 {-

 module GHC.Tc.Gen.Head

        ( HsExprArg(..), TcPass(..), QLFlag(..), EWrap(..)

        , splitHsApps, rebuildHsApps

        , addArgWrap, isHsValArg

        , leadingValArgs, isVisibleArg

 appCtxtLoc (VACall _ _ l)    = l

 insideExpansion :: AppCtxt -> Bool

 instance Outputable QLFlag where

   ppr DoQL = text "DoQL"

                      -> TcM (Maybe (HsExpr GhcTc, TcSigmaType))

 -- See Note [Application chains and heads] in GHC.Tc.Gen.App

 -- Returns Nothing for a complicated head

       HsVar _ nm                  -> Just <$> tcInferId nm

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

       XExpr (PopErrCtxt e)        -> tcInferAppHead_maybe e

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

       _                           -> return Nothing

 addHeadCtxt :: AppCtxt -> TcM a -> TcM a

 import GHC.Tc.Utils.TcMType

 import GHC.Tc.Types.Evidence

 import GHC.Tc.Types.CtLoc

 import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst, FamInstEnvs )

 import GHC.Rename.Env( addUsedGRE, addUsedDataCons, DeprecationWarnings (..) )

     -- GHC.Tc.Gen.App.tcInstFun arranges that the CtOrigin of (r.x) is GetFieldOrigin,

     -- despite the expansion to (getField @"x" r)

     isGetFieldOrigin _                   = False

 lookupHasFieldLabel

 exprCtOrigin (HsForAll {})       = Shouldn'tHappenOrigin "forall telescope"    -- See Note [Types in terms]

 exprCtOrigin (HsQual {})         = Shouldn'tHappenOrigin "constraint context"  -- See Note [Types in terms]

 exprCtOrigin (HsFunArr {})       = Shouldn'tHappenOrigin "function arrow"      -- See Note [Types in terms]

 exprCtOrigin (XExpr (HsRecSelRn f))  = OccurrenceOfRecSel (foExt f)

 -- | Extract a suitable CtOrigin from a MatchGroup

         do prize <- lift uniform [1, 2, ....]

            return False