module GHC.Tc.Gen.App

        ( tcApp

        , tcExprPrag ) where

 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )

 -}

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

 *                                                                      *

               Typechecking n-ary applications

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

 -}

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

       -> TcM (HsExpr GhcTc)

 -- See Note [tcApp: typechecking applications]

        ; traceTc "tcApp {" $

                 , text "fun_lspan:" <+> ppr fun_lspan

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

        -- Step 2: Infer the type of `fun`, the head of the application

        ; let tc_head = (tc_fun, fun_lspan)

              -- inst_final: top-instantiate the result type of the application,

              -- EXCEPT if we are trying to infer a sigma-type

        -- Step 3.1: Instantiate the function type (taking a quick look at args)

        ; do_ql <- wantQuickLook rn_fun

        ; traceTc "tcApp:inferAppHead" $

          vcat [ text "tc_fun:" <+> ppr tc_fun

               , text "fun_sigma:" <+> ppr fun_sigma

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

        ; (inst_args, app_res_rho)

          -- See (TCAPP1) and (TCAPP2) in

          -- Note [tcApp: typechecking applications]

                          -- Step 4.2: typecheck the  arguments

                        ; tc_args <- tcValArgs NoQL (rn_fun, fun_lspan) inst_args

                          -- Step 4.3: wrap up

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

                        ; res_wrap <- checkResultTy rn_expr tc_head inst_args

                                                     app_res_rho exp_res_ty

                          -- Step 5.5: wrap up

 quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()

 -- This function implements the shaded bit of rule APP-Downarrow in

 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

   = do {

        -- Reconstruct, with a horrible special case for tagToEnum#.

          res_expr <- if isTagToEnum tc_fun

        ; traceTc "End tcApp }" (ppr tc_fun)

        ; return (mkHsWrap res_wrap res_expr) }

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

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

               -> TcM HsWrapper

   = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun

        ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res }

 checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho (Check res_ty)

 -- Unify with expected type from the context

 -- See Note [Unify with expected type before typechecking arguments]

              | EValArgQL{} <- arg

              = pos + 1

              | ETypeArg{ ea_loc_span = l } <- arg

              = pos + 1

              | otherwise

              = pos

                       , eaql_loc_span = lspan

                       , eaql_arg_ty   = sc_arg_ty

                       , eaql_larg     = larg@(L arg_loc rn_expr)

                       , eaql_rn_fun   = rn_fun

                       , eaql_fun_ue   = head_ue

                       , eaql_args     = inst_args

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

                   ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

                   ; res_wrap <- checkResultTy rn_expr tc_head inst_args

                                               app_res_rho (mkCheckExpType exp_arg_rho)

        ; traceTc "tcEValArgQL }" $

            vcat [ text "app_res_rho:" <+> ppr app_res_rho ]

                     --           always return a rho-type (but not a deep-rho type)

                     -- Generally speaking we pass in True; in Fig 5 of the paper

                     --    |-inst returns a rho-type

           -> HsExpr GhcTc

           -> TcSigmaType -> [HsExprArg 'TcpRn]

           -> TcM ( [HsExprArg 'TcpInst]

                  , TcSigmaType )   -- Does not instantiate trailing invisible foralls

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

                                    , text "fun_sigma" <+> ppr fun_sigma

                                    , text "args:" <+> ppr rn_args

        ; traceTc "tcInstFun:ret" (ppr fun_ty)

        ; return res

        }

   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

     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

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

                 matchActualFunTy herald

                   (Just $ HsExprTcThing tc_fun)

                   (n_val_args, fun_sigma) fun_ty

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

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

       = do { arg_nu <- newArgTyVarTyQL do_ql $

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

                -- thereby ensuring that the arguments have concrete runtime representations

            ; return (mkScaled mult_ty arg_nu) }

       = case fun_orig of

            DoStmtOrigin -> ExpectedFunTySyntaxOp DoStmtOrigin tc_fun

            _ -> ExpectedFunTyArg (HsExprTcThing tc_fun) arg

 -- Is the argument supposed to instantiate a forall?

 --

 -- In other words, given a function application `fn arg`,

 -}

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

          else quickLookArg1 pos app_lspan fun_and_lspan larg orig_arg_ty }

               -> TcM (HsExprArg 'TcpInst)

 skipQuickLook app_lspan larg arg_ty

   = return (EValArg { ea_loc_span   = app_lspan

 whenQL DoQL thing_inside = liftZonkM thing_inside

 whenQL NoQL _            = return ()

   where

       | isSigmaTy ty

       = return False

       , isQLInstTyVar kappa

       = do { info <- readMetaTyVar kappa

            ; case info of

                Flexi            -> return True }

       | Deep {} <- ds_flag

       , Just (_, res_ty) <- tcSplitFunTy_maybe ty

       | otherwise

       = return True

   | 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

 quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)

   = addArgCtxt pos (fun, fun_lspan) larg $ -- Context needed for constraints

        -- Step 1: get the type of the head of the argument

        ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun_arg

     do { let arg_tc_head = (tc_fun_arg_head, fun_lspan_arg)

        ; do_ql <- wantQuickLook rn_fun_arg

        ; ((inst_args, app_res_rho), wanted)

              <- captureConstraints $

                 -- We must capture type-class and equality constraints here, but

                 -- not usage information.  See (QLA6) in Note [Quick Look at

                 -- value arguments]

        ; traceTc "quickLookArg 2" $

          vcat [ text "arg:" <+> ppr arg

               , text "orig_arg_rho:" <+> ppr orig_arg_rho

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

                            , eaql_res_rho  = app_res_rho }) }}}

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

 *                                                                      *

                  Folding over instantiation variables

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

 isTagToEnum _ = False

             -> TcM (HsExpr GhcTc)

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

 -- See Note [tagToEnum#]   Urgh!

   | [val_arg] <- dropWhile (not . isHsValArg) tc_args

   = do { res_ty <- liftZonkM $ zonkTcType res_ty

        ; let rep_ty  = mkTyConApp rep_tc rep_args

              tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun

              df_wrap = mkWpCastR (mkSymCo coi)

        ; return (mkHsWrap df_wrap tc_expr) }}}}}

   | otherwise

   = failWithTc TcRnTagToEnumMissingValArg

   where

     check_enumeration ty' tc

       | -- isTypeDataTyCon: see wrinkle (W1) in

 module GHC.Tc.Gen.Expr

        ( tcCheckPolyExpr, tcCheckPolyExprNC,

          tcCheckMonoExpr, tcCheckMonoExprNC,

          tcInferRho, tcInferRhoNC,

          tcMonoLExpr, tcMonoLExprNC,

          tcInferRhoFRR, tcInferRhoFRRNC,

 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

 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

     do  { expr' <- tcExpr expr res_ty

         ; return (L loc expr') }

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

 tcExpr :: HsExpr GhcRn

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

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

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

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