-- Used for the main, top-level error message

 -- We've done special processing for TypeEq, KindEq, givens

 pprArising ct_loc

   | suppress_origin   = empty

   | otherwise         = pprCtOrigin orig

   where

 {-# LANGUAGE DataKinds           #-}

 {-# LANGUAGE FlexibleContexts    #-}

 {-# LANGUAGE GADTs               #-}

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

        ; do_ql <- wantQuickLook rn_fun

        ; (tc_fun, fun_sigma) <- tcInferAppHead fun

        ; let tc_expr = rebuildHsApps (tc_fun, fun_ctxt) tc_args

        ; return (tc_expr, app_res_sigma) }

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

                                                    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 }

                        ; quickLookResultType app_res_rho exp_res_ty

                          -- Step 5.2: typecheck the arguments, and monomorphise

                          --           any un-unified instantiation variables

                          -- Step 5.3: typecheck the arguments

                        ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

                          -- Step 5.4: subsumption check against the expected type

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

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

   -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]

     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

                          , ea_arg = L arg_loc arg'

                          , ea_arg_ty = noExtField }) }

                       , eaql_ctxt    = ctxt

                       , eaql_arg_ty  = sc_arg_ty

                       , eaql_larg    = larg@(L arg_loc rn_expr)

                       , 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

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

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

                     --    |-inst returns a rho-type

           -> CtOrigin

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

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

                                    , text "tc_fun" <+> ppr tc_fun

                                    , text "fun_sigma" <+> ppr fun_sigma

                   (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

 --   Unless the arg is also a generated thing, in which case do nothing.

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

        ; traceTc "addArgCtxt" (vcat [ text "generated:" <+> ppr in_generated_code

                                     , text "arg: " <+> ppr arg

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

 {- *********************************************************************

 *                                                                      *

 -}

              -> LHsExpr GhcRn          -- ^ Argument

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

              -> TcM (HsExprArg 'TcpInst)

 -- See Note [Quick Look at value arguments]

   = skipQuickLook ctxt larg orig_arg_ty

   = do { is_rho <- tcIsDeepRho (scaledThing orig_arg_ty)

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

        ; if not is_rho

          then skipQuickLook ctxt larg orig_arg_ty

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

               -> TcM (HsExprArg 'TcpInst)

   | 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

     do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg

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

 {-# LANGUAGE DataKinds           #-}

 {-# LANGUAGE FlexibleContexts    #-}

 {-# LANGUAGE ScopedTypeVariables #-}

 -- These constructors are the union of

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

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

 tcExpr e@(HsVar {})              res_ty = tcApp (exprCtOrigin e) e res_ty

 tcExpr e@(HsApp {})              res_ty = tcApp (exprCtOrigin e) e res_ty

 tcExpr e@(OpApp {})              res_ty = tcApp (exprCtOrigin e) e res_ty

               -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)

               -> TcM (a, SyntaxExprTc)

 tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside

              -- Ugh!! But all this code is scheduled for demolition anyway

        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)

        ; (result, expr_wrap, arg_wraps, res_wrap)

 {-# LANGUAGE DataKinds           #-}

 {-# LANGUAGE FlexibleContexts    #-}

 {-# LANGUAGE GADTs               #-}

 module GHC.Tc.Gen.Head

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

        , splitHsApps, rebuildHsApps

        , addArgWrap, isHsValArg

        , leadingValArgs, isVisibleArg

            | EExpand (HsExpr GhcRn)

            | EHsWrap HsWrapper

 {- Note [AppCtxt]

 -}

 appCtxtLoc :: AppCtxt -> SrcSpan

 insideExpansion :: AppCtxt -> Bool

 instance Outputable QLFlag where

   ppr DoQL = text "DoQL"

   ppr NoQL = text "NoQL"

 type family XPass (p :: TcPass) where

   XPass 'TcpRn   = 'Renamed

   XPass 'TcpInst = 'Renamed

 -- This uses the TcM monad solely because we must run modFinalizers when looking

 -- through HsUntypedSplices

 -- (see Note [Looking through Template Haskell splices in splitHsApps]).

   where

     go :: HsExpr GhcRn -> AppCtxt -> [HsExprArg 'TcpRn]

        -> TcM ((HsExpr GhcRn, AppCtxt), [HsExprArg 'TcpRn])

     -- Modify the AppCtxt as we walk inwards, so it describes the next argument

     -- See Note [Looking through Template Haskell splices in splitHsApps]

     go e@(HsUntypedSplice splice_res splice) ctxt args

       where

         ctxt' :: AppCtxt

         ctxt' = case splice of

     -- See Note [Desugar OpApp in the typechecker]

     go e@(OpApp _ arg1 (L l op) arg2) _ args

                     -- generatedSrcSpan because this the span of the call,

                     -- and its hard to say exactly what that is

                : EWrap (EExpand e)

     go e ctxt args = pure ((e,ctxt), args)

 -- | Rebuild an application: takes a type-checked application head

 -- expression together with arguments in the form of typechecked 'HsExprArg's

       HsOverLit _ lit             -> Just <$> tcInferOverLit lit

       _                           -> return Nothing

   | not (isGoodSrcSpan fun_loc)       -- noSrcSpan => no arguments

   = thing_inside                      -- => context is already set

   | otherwise

   = setSrcSpan fun_loc thing_inside

 {- *********************************************************************

 --          else go dbg 0 env ctxts

  = go False 0 env ctxts -- regular error ctx

  where

    go _ _ _   [] = return []

    go dbg n env ((is_landmark, ctxt) : ctxts)

      | is_landmark || n < mAX_CONTEXTS -- Too verbose || dbg

 T5439.hs:83:33: error: [GHC-83865]

     • Couldn't match expected type: Attempt (HElemOf rs)

                   with actual type: Attempt (HHead (HDrop n0 l0))

     • Probable cause: ‘($)’ is applied to too few arguments

       In the second argument of ‘($)’, namely

         ‘inj $ Failure (e :: SomeException)’

       In the expression:

         do c <- complete ev $ inj $ Failure (e :: SomeException)

            return $ c || not first

         ‘Failure (e :: SomeException)’

       In the second argument of ‘($)’, namely

         ‘inj $ Failure (e :: SomeException)’