--   expose foralls, but maybe not /deeply/ instantiated

               -> ExpRhoType -- Expected type; this is deeply skolemised

               -> TcM HsWrapper

        ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res }

                                        , text "app_lspan" <+> ppr lspan

                                        , text "head_lspan" <+> ppr fun_lspan

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

        ; (wrap, arg')

             <- tcScalingUsage mult  $

                tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->

                 matchActualFunTy herald

                   (Just $ HsExprTcThing tc_fun)

                   (n_val_args, fun_sigma) fun_ty

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

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

 -}

              -> SrcSpan -- ^ location span of the whole application

              -> (HsExpr GhcRn, SrcSpan) -- ^ Head of the application chain and its source span

              -> LHsExpr GhcRn          -- ^ Argument

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

              -> TcM (HsExprArg 'TcpInst)

 -- See Note [Quick Look at value arguments]

   = skipQuickLook app_lspan larg orig_arg_ty

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

        ; if not is_rho

          then skipQuickLook app_lspan larg orig_arg_ty

 module GHC.Tc.Gen.Expr

        ( tcCheckPolyExpr, tcCheckPolyExprNC,

          tcCheckMonoExpr, tcCheckMonoExprNC,

          tcInferRho, tcInferRhoNC,

          tcMonoLExpr, tcMonoLExprNC,

          tcInferRhoFRR, tcInferRhoFRRNC,

 tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)

 tcInferSigma = tcInferExpr IIF_Sigma

 tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)

 -- Infer a *rho*-type. The return type is always instantiated.

 tcInferRho   = tcInferExpr   IIF_DeepRho

 tcExpr e@(ExprWithTySig {})      res_ty = tcApp e res_ty

 tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse res_ty

 -- Typecheck an occurrence of an unbound Id

 --

 tcExpr (HsIf x pred b1 b2) res_ty

   = do { pred'    <- tcCheckMonoExpr pred boolTy

        ; tcEmitBindingUsage (supUE u1 u2)

        ; return (HsIf x pred' b1' b2') }

 tcInferRhoFRR, tcInferRhoFRRNC ::

   FixedRuntimeRepContext -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)

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

 tcSyntaxOp :: CtOrigin

        , pprArgInst, addFunResCtxt ) where

 import {-# SOURCE #-} GHC.Tc.Gen.Splice( getUntypedSpliceBody )

 import GHC.Prelude

 import GHC.Hs

 import GHC.Hs.Syn.Type

 import GHC.Tc.Gen.HsType

 import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )

     do { mb_tc_fun <- tcInferAppHead_maybe fun

        ; case mb_tc_fun of

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

        }

         -> Just <$> tcInferOverLit lit

       XExpr (HsRecSelRn f)

         -> Just <$> tcInferRecSelId f

       _

         -> return Nothing

           -> MatchGroup GhcRn (LocatedA (body GhcRn))

           -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))

                                           , mg_ext = origin })

   | null matches  -- Deal with case e of {}

     -- when in inference mode, so we must do it ourselves,

     -- here, using expTypeToType

   = do { tcEmitBindingUsage bottomUE

            [ExpForAllPatTy tvb] -> failWithTc $ TcRnEmptyCase ctxt (EmptyCaseForall tvb)

            []                   -> panic "tcMatches: no arguments in EmptyCase"

            _t1:(_t2:_ts)        -> panic "tcMatches: multiple arguments in EmptyCase"

        ; return (MG { mg_alts = L l []

                     , mg_ext = MatchGroupTc [pat_ty] rhs_ty origin

                     }) }

   | otherwise

        ; tcEmitBindingUsage $ supUEs usages

        ; pat_tys  <- mapM readScaledExpType (filter_out_forall_pat_tys pat_tys)

        ; traceTc "tcMatches" (ppr matches' $$ ppr pat_tys $$ ppr rhs_ty)

        ; return (MG { mg_alts   = L l matches'

                     , mg_ext    = MatchGroupTc pat_tys rhs_ty origin

   mkCheckExpType, newInferExpType, newInferExpTypeFRR,

   runInfer, runInferRho, runInferSigma, runInferKind, runInferRhoFRR, runInferSigmaFRR,

   readExpType, readExpType_maybe, readScaledExpType,

   checkingExpType_maybe, checkingExpType,

   inferResultToType, ensureMonoType, promoteTcType,

                             ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr

                             ; return tau }

 {- Note [inferResultToType]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~

 expTypeToType and inferResultType convert an InferResult to a monotype.

 tcSkolemiseGeneral

   :: HasDebugCallStack

   -> UserTypeCtxt

   -> TcType -> TcType   -- top_ty and expected_ty

         -- Here, top_ty      is the type we started to skolemise; used only in SigSkol

                      ; return final_co } }

 -- See Note [Instantiation of InferResult]

 fillInferResult ds_flag ct_orig res_ty ires@(IR { ir_inst = iif })

   = case iif of

         T1 -> e1

         T2 -> e2

 * The RHS of a existential or GADT alternative must always be a

   monotype, regardless of the number of alternatives.

        We use choice (2) in that Section.

        (GHC 8.10 and earlier used choice (1).)

 Then, before filling the hole use promoteTcType to promote the type

 to the outer ir_lvl.  promoteTcType does this

 only unify with monotypes); and catches skolem-escapes because the

 alpha is untouchable until the equality floats out.

 (FIR1) There is one wrinkle.  Suppose we have

              case e of

                 T1 -> e1 :: (forall a. a->a) -> Int

     So if we check G2 second, we still want to emit a constraint that restricts

     the RHS to be a monotype. This is done by ensureMonoType, and it works

     by simply generating a constraint (alpha ~ ty), where alpha is a fresh

 Note [Instantiation of InferResult]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 -- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption

 -- in order to implement the plan of Note [Typechecking data constructors].

 getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag

 -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.

 --