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

 pprArising ct_loc

   | suppress_origin   = empty

   | otherwise         = pprCtOrigin orig

   where

     orig = ctLocOrigin ct_loc

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

 quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho

 quickLookResultType  _           _              = return ()

           -> TcRhoType -> HsWrapper

           -> TcM (HsExpr GhcTc)

 -- Do final checks and wrap up the result

        ; return (mkHsWrap res_wrap res_expr) }

 checkResultTy :: HsExpr GhcRn

               -> [HsExprArg p]            -- Arguments, just error messages

               -> TcRhoType  -- Inferred type of the application; zonked to

                             --   expose foralls, but maybe not deeply instantiated

     -- the source program; it was added by the renamer.  See

     -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr

     perhaps_add_res_ty_ctxt thing_inside

       = thing_inside

       | otherwise

       = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $

         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_tc_fun  = tc_head

                       , eaql_fun_ue  = head_ue

                       , 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

        ; traceTc "tcEValArgQL {" (vcat [ text "app_res_rho:" <+> ppr app_res_rho

                                        , text "exp_arg_ty:" <+> ppr exp_arg_ty

                                        , text "args:" <+> ppr inst_args

        ; ds_flag <- getDeepSubsumptionFlag

        ; (wrap, arg')

                   ; 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

               -> TcM (HsExprArg 'TcpInst)

 skipQuickLook ctxt larg arg_ty

   = return (EValArg { ea_ctxt   = ctxt

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

                            , eaql_arg_ty  = sc_arg_ty

                            , eaql_larg    = larg

                            , eaql_tc_fun  = tc_head

                            , eaql_fun_ue  = fun_ue

                            , eaql_args    = inst_args

                            , eaql_wanted  = wanted

 isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey

 isTagToEnum _ = False

             -> TcRhoType

             -> TcM (HsExpr GhcTc)

 -- tagToEnum# :: forall a. Int# -> a

 -- if the representation of its argument isn't known.

 --

 -- See Note [Eta-expanding rep-poly unlifted newtypes].

                       -> TcRhoType

                       -> TcM ()

 rejectRepPolyNewtypes (fun,_) app_res_rho = case fun of

 {-# LANGUAGE DataKinds           #-}

 {-# LANGUAGE FlexibleContexts    #-}

 {-# LANGUAGE ScopedTypeVariables #-}

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

 data HsExprArg (p :: TcPass) where -- See Note [HsExprArg]

   -- Data constructor EValArg represents a value argument

              , ea_arg_ty :: !(XEVAType p)

              , ea_arg    :: LHsExpr (GhcPass (XPass p)) }

           -> HsExprArg p

   -- Data constructor EValArgQL represents an argument that has been

   -- partly-type-checked by Quick Look; see Note [EValArgQL]

                , eaql_arg_ty  :: Scaled TcSigmaType  -- Argument type expected by function

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

                                                      -- location and error msgs

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

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

                , eaql_wanted  :: WantedConstraints

                , eaql_res_rho :: TcRhoType }           -- Result type of the application

             -> HsExprArg 'TcpInst  -- Only exists in TcpInst phase

               , ea_hs_ty  :: LHsWcType GhcRn  -- The type arg

               , ea_ty_arg :: !(XETAType p) }  -- Kind-checked type arg

            -> HsExprArg p

   EWrap :: EWrap                                    -> HsExprArg p

 type family XETAType (p :: TcPass) where  -- Type arguments

 data QLFlag = DoQL | NoQL

            | EExpand (HsExpr GhcRn)

            | EHsWrap HsWrapper

 instance Outputable QLFlag where

   ppr DoQL = text "DoQL"

   ppr NoQL = text "NoQL"

 type family XPass (p :: TcPass) where

   XPass 'TcpRn   = 'Renamed

   XPass 'TcpInst = 'Renamed

   XPass 'TcpTc   = 'Typechecked

 mkEValArg ctxt e = EValArg { ea_arg = e, ea_ctxt = ctxt

                            , ea_arg_ty = noExtField }

 mkETypeArg ctxt hs_ty =

   ETypeArg { ea_ctxt = ctxt

            , ea_hs_ty = hs_ty

 splitHsApps :: HsExpr GhcRn

                    , [HsExprArg 'TcpRn])      -- Args

 -- See Note [splitHsApps].

 --

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

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

       = do { fun <- getUntypedSpliceBody splice_res

            ; go fun ctxt' (EWrap (EExpand e) : args) }

       where

         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

 -- representation-polymorphic unlifted newtypes have been eta-expanded.

 --

 -- See Note [Eta-expanding rep-poly unlifted newtypes].

                       -- ^ the function being applied

               -> [HsExprArg 'TcpTc]

                       -- ^ the arguments to the function

       EWrap (EHsWrap wrap)

         -> rebuildHsApps (mkHsWrap wrap fun, ctxt) args

   where

 isHsValArg :: HsExprArg id -> Bool

 isHsValArg (EValArg {}) = True

 *                                                                      *

 ********************************************************************* -}

                -> TcM (HsExpr GhcTc, TcSigmaType)

 -- Infer type of the head of an application

 --   i.e. the 'f' in (f e1 ... en)

       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