content: 
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE FlexibleContexts    #-}
  {-# LANGUAGE GADTs               #-}
  {-# LANGUAGE MultiWayIf          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies        #-}
  {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
  {-# LANGUAGE TypeApplications #-} -- Wrinkle in Note [Trees That Grow]
  
  {-
  %
  (c) The University of Glasgow 2006
  (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
  -}
  
  module GHC.Tc.Gen.App
         ( tcApp
         , tcExprPrag ) where
  
  import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
  
  import GHC.Hs
  
  import GHC.Tc.Gen.Head
  import GHC.Tc.Errors.Types
  import GHC.Tc.Utils.Monad
  import GHC.Tc.Utils.Unify
  import GHC.Tc.Utils.Instantiate
  import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
  import GHC.Tc.Gen.HsType
  import GHC.Tc.Utils.Concrete  ( unifyConcrete, idConcreteTvs )
  import GHC.Tc.Utils.TcMType
  import GHC.Tc.Types.Evidence
  import GHC.Tc.Types.ErrCtxt ( FunAppCtxtFunArg(..) )
  import GHC.Tc.Types.Origin
  import GHC.Tc.Utils.TcType as TcType
  import GHC.Tc.Utils.Concrete( hasFixedRuntimeRep_syntactic )
  import GHC.Tc.Zonk.TcType
  
  import GHC.Core.ConLike (ConLike(..))
  import GHC.Core.DataCon ( dataConConcreteTyVars, isNewDataCon, dataConTyCon )
  import GHC.Core.TyCon
  import GHC.Core.TyCo.Rep
  import GHC.Core.TyCo.Ppr
  import GHC.Core.TyCo.Subst ( substTyWithInScope )
  import GHC.Core.Type
  import GHC.Core.Coercion
  
  import GHC.Builtin.Types ( multiplicityTy )
  import GHC.Builtin.PrimOps( tagToEnumKey )
  import GHC.Builtin.Names
  
  import GHC.Types.Var
  import GHC.Types.Name
  import GHC.Types.Name.Env
  import GHC.Types.Name.Reader
  import GHC.Types.SrcLoc
  import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
  
  import GHC.Data.Maybe
  
  import GHC.Utils.Misc
  import GHC.Utils.Outputable as Outputable
  import GHC.Utils.Panic
  
  import qualified GHC.LanguageExtensions as LangExt
  import Language.Haskell.Syntax.Basic( isBoxed )
  
  import Control.Monad
  import Data.Function
  import Data.Semigroup
  
  import GHC.Prelude
  
  {- *********************************************************************
  *                                                                      *
                   Quick Look overview
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [Quick Look overview]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  The implementation of Quick Look closely follows the QL paper
     A quick look at impredicativity, Serrano et al, ICFP 2020
     https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/
  
  All the moving parts are in this module, GHC.Tc.Gen.App, so named
  because it deal with n-ary application.  The main workhorse is tcApp.
  
  Some notes relative to the paper
  
  (QL1) The "instantiation variables" of the paper are ordinary unification
    variables.  We keep track of which variables are instantiation variables
    by giving them a TcLevel of QLInstVar, which is like "infinity".
  
  (QL2) When we learn what an instantiation variable must be, we simply unify
    it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2)
    of the paper.  This may fill in a (mutable) instantiation variable with
    a polytype.
  
  (QL3) When QL is done, we turn the instantiation variables into ordinary unification
    variables, using qlZonkTcType.  This function fully zonks the type (thereby
    revealing all the polytypes), and updates any instantiation variables with
    ordinary unification variables.
    See Note [Instantiation variables are short lived].
  
  (QL4) We cleverly avoid the quadratic cost of QL, alluded to in the paper.
    See Note [Quick Look at value arguments]
  
  Note [Instantiation variables are short lived]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  * An instantation variable is a mutable meta-type-variable, whose level number
    is QLInstVar.
  
  * Ordinary unification variables always stand for monotypes; only instantiation
    variables can be unified with a polytype (by `qlUnify`).
  
  * When we start typechecking the argments of the call, in tcValArgs, we will
    (a) monomorphise any un-filled-in instantiation variables
        (see Note [Monomorphise instantiation variables])
    (b) zonk the argument type to reveal any polytypes before typechecking that
        argument (see calls to `zonkTcType` and "Crucial step" in tcValArg)..
    See Section 4.3 "Applications and instantiation" of the paper.
  
  * The constraint solver never sees an instantiation variable [not quite true;
    see below]
  
    However, the constraint solver can see a meta-type-variable filled
    in with a polytype (#18987). Suppose
      f :: forall a. Dict a => [a] -> [a]
      xs :: [forall b. b->b]
    and consider the call (f xs).  QL will
    * Instantiate f, with a := kappa, where kappa is an instantiation variable
    * Emit a constraint (Dict kappa), via instantiateSigma, called from tcInstFun
    * Do QL on the argument, to discover kappa := forall b. b->b
  
    But by the time the third step has happened, the constraint has been emitted
    into the monad.  The constraint solver will later find it, and rewrite it to
    (Dict (forall b. b->b)). That's fine -- the constraint solver does no implicit
    instantiation (which is what makes it so tricky to have foralls hiding inside
    unification variables), so there is no difficulty with allowing those
    filled-in kappa's to persist.  (We could find them and zonk them away, but
    that would cost code and execution time, for no purpose.)
  
    Since the constraint solver does not do implicit instantiation (as the
    constraint generator does), the fact that a unification variable might stand
    for a polytype does not matter.
  
  * Actually, sadly the constraint solver /can/ see an instantiation variable.
    Consider this from test VisFlag1_ql:
       f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
  
       bad_wild :: ()
       bad_wild = f @_ MkV
    In tcInstFun instantiate f with [k:=k0, a:=a0], and then encounter the `@_`,
    expecting it to have kind (forall j. j->Type).  We make a fresh variable (it'll
    be an instantiation variable since we are in tcInstFun) for the `_`, thus
    (_ : k0) and do `checkExpectedKind` to match up `k0` with `forall j. j->Type`.
    The unifier doesn't solve it (it does not unify instantiation variables) so
    it leaves it for the constraint solver.  Yuk.   It's hard to see what to do
    about this, but it seems to do no harm for the constraint solver to see the
    occasional instantiation variable.
  -}
  
  
  {- *********************************************************************
  *                                                                      *
                Typechecking n-ary applications
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [Application chains and heads]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Quick Look treats application chains specially.  What is an
  "application chain"?  See Fig 2, of the QL paper: "A quick look at
  impredicativity" (ICFP'20). Here's the syntax:
  
  app ::= head
       |  app expr            -- HsApp: ordinary application
       |  app @type           -- HsTypeApp: VTA
       |  expr `head` expr    -- OpApp: infix applications
       |  ( app )             -- HsPar: parens
       |  {-# PRAGMA #-} app  -- HsPragE: pragmas
  
  head ::= f                -- HsVar:    variables
        |  fld              -- HsRecSel: record field selectors
        |  (expr :: ty)     -- ExprWithTySig: expr with user type sig
        |  lit              -- HsOverLit: overloaded literals
        |  other_expr       -- Other expressions
  
  When tcExpr sees something that starts an application chain (namely,
  any of the constructors in 'app' or 'head'), it invokes tcApp to
  typecheck it: see Note [tcApp: typechecking applications].  However,
  for HsPar and HsPragE, there is no tcWrapResult (which would
  instantiate types, bypassing Quick Look), so nothing is gained by
  using the application chain route, and we can just recurse to tcExpr.
  
  A "head" has three special cases (for which we can infer a polytype
  using tcInferAppHead_maybe); otherwise is just any old expression (for
  which we can infer a rho-type (via runInferExpr).
  
  There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because
  we can't get a polytype from them.
  
  Left and right sections (e.g. (x +) and (+ x)) are not yet supported.
  Probably left sections (x +) would be easy to add, since x is the
  first arg of (+); but right sections are not so easy.  For symmetry
  reasons I've left both unchanged, in GHC.Tc.Gen.Expr.
  
  It may not be immediately obvious why ExprWithTySig (e::ty) should be
  dealt with by tcApp, even when it is not applied to anything. Consider
     f :: [forall a. a->a] -> Int
     ...(f (undefined :: forall b. b))...
  Clearly this should work!  But it will /only/ work because if we
  instantiate that (forall b. b) impredicatively!  And that only happens
  in tcApp.
  
  Note [tcApp: typechecking applications]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  tcApp implements the APP-Downarrow/Uparrow rule of
  Fig 3, plus the modification in Fig 5, of the QL paper:
  "A quick look at impredicativity" (ICFP'20).
  
  It treats application chains (f e1 @ty e2) specially:
  
  * So we can report errors like "in the third argument of a call of f"
  
  * So we can do Visible Type Application (VTA), for which we must not
    eagerly instantiate the function part of the application.
  
  * So that we can do Quick Look impredicativity.
  
  tcApp works like this:
  
  1. Use splitHsApps, which peels off
       HsApp, HsTypeApp, HsPrag, HsPar
     returning the function in the corner and the arguments
  
     splitHsApps can deal with infix as well as prefix application,
     and returns a Rebuilder to re-assemble the application after
     typechecking.
  
     The "list of arguments" is [HsExprArg], described in Note [HsExprArg].
     in GHC.Tc.Gen.Head
  
  2. Use tcInferAppHead to infer the type of the function,
       as an (uninstantiated) TcSigmaType
     There are special cases for
       HsVar, HsRecSel, and ExprWithTySig
     Otherwise, delegate back to tcExpr, which
       infers an (instantiated) TcRhoType
  
     This isn't perfect. Consider this (which uses visible type application):
      (let { f :: forall a. a -> a; f x = x } in f) @Int
     Since 'let' is not among the special cases for tcInferAppHead,
     we'll delegate back to tcExpr, which will instantiate f's type
     and the type application to @Int will fail.  Too bad!
  
  3. Use tcInstFun to instantiate the function, Quick-Looking as we go.  This
     implements the |-inst judgement in Fig 4, plus the modification in Fig 5, of
     the QL paper: "A quick look at impredicativity" (ICFP'20).
  
     In tcInstFun we take a quick look at value arguments, using quickLookArg.
     See Note [Quick Look at value arguments].
  
     (TCAPP1) Crucially, just before `tcApp` calls `tcInstFun`, it sets the
         ambient TcLevel to QLInstVar, so all unification variables allocated by
         tcInstFun, and in the quick-looks it does at the arguments, will be
         instantiation variables.
  
     Consider (f (g (h x))).`tcApp` instantiates the call to `f`, and in doing
     so quick-looks at the argument(s), in this case (g (h x)).  But
     `quickLookArg` on (g (h x)) in turn instantiates `g` and quick-looks at
     /its/ argument(s), in this case (h x).  And so on recursively.  Key
     point: all these instantiations make instantiation variables.
  
  Now we split into two cases:
  
  4. Case NoQL: no Quick Look
  
     4.1 Use checkResultTy to connect the the result type.
         Do this /before/ checking the arguments; see
         Note [Unify with expected type before typechecking arguments]
  
     4.2 Check the arguments with `tcValArgs`.
  
     4.3 Use `finishApp` to wrap up.
  
  5. Case DoQL: use Quick Look
  
     5.1 Use `quickLookResultType` to take a quick look at the result type,
         when in checking mode.  This is the shaded part of APP-Downarrow
         in Fig 5.  It also implements the key part of
         Note [Unify with expected type before typechecking arguments]
  
     5.2 Check the arguments with `tcValArgs`. Importantly, this will monomorphise
         all the instantiation variables of the call.
         See Note [Monomorphise instantiation variables].
  
     5.3 Use `zonkTcType` to expose the polymophism hidden under instantiation
         variables in `app_res_rho`, and the monomorphic versions of any
         un-unified instantiation variables.
  
     5.4 Use `checkResTy` to do the subsumption check as usual
  
     5.4 Use `finishApp` to wrap up
  
  The funcion `finishApp` mainly calls `rebuildHsApps` to rebuild the
  application; but it also does a couple of gruesome final checks:
    * Horrible newtype check
    * Special case for tagToEnum
  
  (TCAPP2) There is a lurking difficulty in the above plan:
    * Before calling tcInstFun, we set the ambient level in the monad
      to QLInstVar (Step 2 above).
    * Then, when kind-checking the visible type args of the application,
      we may perhaps build an implication constraint.
    * That means we'll try to add 1 to the ambient level; which is a no-op.
    * So skolem escape checks won't work right.
    This is pretty exotic, so I'm just deferring it for now, leaving
    this note to alert you to the possiblity.
  
  Note [Quick Look for particular Ids]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We switch on Quick Look (regardless of -XImpredicativeTypes) for certain
  particular Ids:
  
  * ($): For a long time GHC has had a special typing rule for ($), that
    allows it to type (runST $ foo), which requires impredicative instantiation
    of ($), without language flags.  It's a bit ad-hoc, but it's been that
    way for ages.  Using quickLookKeys is the only special treatment ($) needs
    now, which is a lot better.
  
  * leftSection, rightSection: these are introduced by the expansion step in
    the renamer (Note [Handling overloaded and rebindable constructs] in
    GHC.Rename.Expr), and we want them to be instantiated impredicatively
    so that (f `op`), say, will work OK even if `f` is higher rank.
    See Note [Left and right sections] in GHC.Rename.Expr.
  
  Note [Unify with expected type before typechecking arguments]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider this (#19364)
    data Pair a b = Pair a b
    baz :: MkPair Int Bool
    baz = MkPair "yes" "no"
  
  We instantiate MkPair with `alpha`, `beta`, and push its argument
  types (`alpha` and `beta`) into the arguments ("yes" and "no").
  But if we first unify the result type (Pair alpha beta) with the expected
  type (Pair Int Bool) we will push the much more informative types
  `Int` and `Bool` into the arguments.   This makes a difference:
  
  Unify result type /after/ typechecking the args
      • Couldn't match type ‘[Char]’ with ‘Bool’
        Expected type: Pair Foo Bar
          Actual type: Pair [Char] [Char]
      • In the expression: Pair "yes" "no"
  
  Unify result type /before/ typechecking the args
      • Couldn't match type ‘[Char]’ with ‘Bool’
        Expected: Foo
          Actual: String
      • In the first argument of ‘Pair’, namely ‘"yes"’
  
  The latter is much better. That is why we call checkResultType before tcValArgs.
  -}
  
  tcApp :: HsExpr GhcRn
        -> ExpRhoType   -- When checking, -XDeepSubsumption <=> deeply skolemised
        -> TcM (HsExpr GhcTc)
  -- See Note [tcApp: typechecking applications]
  tcApp rn_expr exp_res_ty
    = do { -- Step 1: Split the application chain
           (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
         ; traceTc "tcApp {" $
             vcat [ text "rn_expr:" <+> ppr rn_expr
                  , text "rn_fun:" <+> ppr rn_fun
                  , text "fun_ctxt:" <+> ppr fun_ctxt
                  , text "rn_args:" <+> ppr rn_args ]
  
         -- Step 2: Infer the type of `fun`, the head of the application
         ; (tc_fun, fun_sigma) <- tcInferAppHead fun
         ; let tc_head = (tc_fun, fun_ctxt)
               -- inst_final: top-instantiate the result type of the application,
               -- EXCEPT if we are trying to infer a sigma-type
               inst_final = case exp_res_ty of
                               Check {} -> True
                               Infer (IR {ir_inst=iif}) ->
                                  case iif of
                                    IIF_ShallowRho -> True
                                    IIF_DeepRho    -> True
                                    IIF_Sigma      -> False
  
         -- Step 3: Instantiate the function type (taking a quick look at args)
         ; do_ql <- wantQuickLook rn_fun
         ; (inst_args, app_res_rho)
                <- setQLInstLevel do_ql $  -- See (TCAPP1) and (TCAPP2) in
                                           -- Note [tcApp: typechecking applications]
                   tcInstFun do_ql inst_final tc_head fun_sigma rn_args
  
         ; case do_ql of
              NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)
  
                           -- Step 4.1: subsumption check against expected result type
                           -- See Note [Unify with expected type before typechecking arguments]
                         ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                                     app_res_rho exp_res_ty
                           -- Step 4.2: typecheck the  arguments
                         ; tc_args <- tcValArgs NoQL inst_args
  
                           -- Step 4.3: wrap up
                         ; finishApp tc_head tc_args app_res_rho res_wrap }
  
              DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho)
  
                           -- Step 5.1: Take a quick look at the result type
                         ; quickLookResultType app_res_rho exp_res_ty
  
                           -- Step 5.2: typecheck the arguments, and monomorphise
                           --           any un-unified instantiation variables
                         ; tc_args <- tcValArgs DoQL inst_args
  
                           -- Step 5.3: zonk to expose the polymorphism hidden under
                           --           QuickLook instantiation variables in `app_res_rho`
                         ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
  
                           -- Step 5.4: subsumption check against the expected type
                         ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                                      app_res_rho exp_res_ty
                           -- Step 5.5: wrap up
                         ; finishApp tc_head tc_args app_res_rho res_wrap } }
  
  setQLInstLevel :: QLFlag -> TcM a -> TcM a
  setQLInstLevel DoQL thing_inside = setTcLevel QLInstVar thing_inside
  setQLInstLevel NoQL thing_inside = thing_inside
  
  quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()
  -- This function implements the shaded bit of rule APP-Downarrow in
  -- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
  quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho
  quickLookResultType  _           _              = return ()
  
  finishApp :: (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc]
            -> TcRhoType -> HsWrapper
            -> TcM (HsExpr GhcTc)
  -- Do final checks and wrap up the result
  finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap
    = do { -- Horrible newtype check
         ; rejectRepPolyNewtypes tc_head app_res_rho
  
         -- Reconstruct, with a horrible special case for tagToEnum#.
         ; res_expr <- if isTagToEnum tc_fun
                       then tcTagToEnum tc_head tc_args app_res_rho
                       else return (rebuildHsApps tc_head tc_args)
         ; traceTc "End tcApp }" (ppr tc_fun)
         ; return (mkHsWrap res_wrap res_expr) }
  
  -- | Connect up the inferred type of an application with the expected type.
  -- This is usually just a unification, but with deep subsumption there is more to do.
  checkResultTy :: HsExpr GhcRn
                -> (HsExpr GhcTc, AppCtxt)  -- Head
                -> [HsExprArg p]            -- Arguments, just error messages
                -> TcRhoType  -- Inferred type of the application; zonked to
                              --   expose foralls, but maybe not /deeply/ instantiated
                -> ExpRhoType -- Expected type; this is deeply skolemised
                -> TcM HsWrapper
  checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res)
    = fillInferResult (exprCtOrigin rn_expr) app_res_rho inf_res
      -- fillInferResult does deep instantiation if DeepSubsumption is on
  
  checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty)
  -- Unify with expected type from the context
  -- See Note [Unify with expected type before typechecking arguments]
  --
  -- Match up app_res_rho: the result type of rn_expr
  --     with res_ty:  the expected result type
   = perhaps_add_res_ty_ctxt $
     do { ds_flag <- getDeepSubsumptionFlag
        ; traceTc "checkResultTy {" $
            vcat [ text "tc_fun:" <+> ppr tc_fun
                 , text "app_res_rho:" <+> ppr app_res_rho
                 , text "res_ty:"  <+> ppr res_ty
                 , text "ds_flag:" <+> ppr ds_flag ]
        ; case ds_flag of
            Shallow -> -- No deep subsumption
               -- app_res_rho and res_ty are both rho-types,
               -- so with simple subsumption we can just unify them
               -- No need to zonk; the unifier does that
               do { co <- unifyExprType rn_expr app_res_rho res_ty
                  ; traceTc "checkResultTy 1 }" (ppr co)
                  ; return (mkWpCastN co) }
  
            Deep ->   -- Deep subsumption
               -- Even though both app_res_rho and res_ty are rho-types,
               -- they may have nested polymorphism, so if deep subsumption
               -- is on we must call tcSubType.
               do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
                  ; traceTc "checkResultTy 2 }" (ppr app_res_rho $$ ppr res_ty)
                  ; return wrap } }
    where
      -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
      -- more confusing than helpful because the function at the head isn't in
      -- 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
        | insideExpansion fun_ctxt
        = addHeadCtxt fun_ctxt thing_inside
        | otherwise
        = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $
          thing_inside
  
  ----------------
  tcValArgs :: QLFlag -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
  -- 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].
  tcValArgs do_ql args = mapM (tcValArg do_ql) args
  
  tcValArg :: QLFlag -> HsExprArg 'TcpInst    -- Actual argument
           -> TcM (HsExprArg 'TcpTc)          -- Resulting argument
  tcValArg _     (EPrag l p)         = return (EPrag l (tcExprPrag p))
  tcValArg _     (ETypeArg l hty ty) = return (ETypeArg l hty ty)
  tcValArg do_ql (EWrap (EHsWrap w)) = do { whenQL do_ql $ qlMonoHsWrapper w
                                          ; return (EWrap (EHsWrap w)) }
    -- qlMonoHsWrapper: see Note [Monomorphise instantiation variables]
  tcValArg _     (EWrap ew)          = return (EWrap ew)
  
  tcValArg do_ql (EValArg { ea_ctxt   = ctxt
                          , ea_arg    = larg@(L arg_loc arg)
                          , ea_arg_ty = sc_arg_ty })
    = addArgCtxt ctxt larg $
      do { traceTc "tcValArg" $
           vcat [ ppr ctxt
                , text "arg type:" <+> ppr sc_arg_ty
                , text "arg:" <+> ppr arg ]
  
           -- 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
           -- "see" the polymorphism in that argument type. E.g.
           --    (:) e ids, where ids :: [forall a. a->a]
           --                     (:) :: forall p. p->[p]->[p]
           -- Then Theta = [p :-> forall a. a->a], and we want
           -- to check 'e' with expected type (forall a. a->a)
           -- See Note [Instantiation variables are short lived]
         ; Scaled mult exp_arg_ty <- case do_ql of
                DoQL -> liftZonkM $ zonkScaledTcType sc_arg_ty
                NoQL -> return sc_arg_ty
  
           -- Now check the argument
         ; arg' <- tcScalingUsage mult $
                   tcPolyExpr arg (mkCheckExpType exp_arg_ty)
  
         ; return (EValArg { ea_ctxt = ctxt
                           , ea_arg = L arg_loc arg'
                           , ea_arg_ty = noExtField }) }
  
  tcValArg _ (EValArgQL { eaql_wanted  = wanted
                        , 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 })
    = addArgCtxt ctxt larg $
      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
                                         , text "mult:" <+> ppr mult])
  
         ; ds_flag <- getDeepSubsumptionFlag
         ; (wrap, arg')
              <- tcScalingUsage mult  $
                 tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
                 do { -- Emit saved-up constraints, /under/ the tcSkolemise
                      -- See (QLA4) in Note [Quick Look at value arguments]
                      emitConstraints wanted
                      -- Emit saved-up usages /under/ the tcScalingUsage.
                      -- See (QLA5) in Note [Quick Look at value arguments]
                    ; tcEmitBindingUsage head_ue
  
                      -- Unify with context if we have not already done so
                      -- See (QLA4) in Note [Quick Look at value arguments]
                    ; unless arg_influences_enclosing_call $  -- Don't repeat
                      qlUnify app_res_rho exp_arg_rho         -- the qlUnify
  
                    ; tc_args <- tcValArgs DoQL inst_args
                    ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
                    ; res_wrap <- checkResultTy rn_expr tc_head inst_args
                                                app_res_rho (mkCheckExpType exp_arg_rho)
                    ; finishApp tc_head tc_args app_res_rho res_wrap }
  
         ; traceTc "tcEValArgQL }" $
             vcat [ text "app_res_rho:" <+> ppr app_res_rho ]
  
         ; return (EValArg { ea_ctxt   = ctxt
                           , ea_arg    = L arg_loc (mkHsWrap wrap arg')
                           , ea_arg_ty = noExtField }) }
  
  
  --------------------
  wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
  wantQuickLook (HsVar _ (L _ (WithUserRdr _ f)))
    | getUnique f `elem` quickLookKeys = return DoQL
  wantQuickLook _                      = do { impred <- xoptM LangExt.ImpredicativeTypes
                                            ; if impred then return DoQL else return NoQL }
  
  quickLookKeys :: [Unique]
  -- See Note [Quick Look for particular Ids]
  quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey]
  
  {- *********************************************************************
  *                                                                      *
                Instantiating the call
  *                                                                      *
  ********************************************************************* -}
  
  tcInstFun :: QLFlag
            -> Bool   -- False <=> Instantiate only /top-level, inferred/ variables;
                      --           so may return a sigma-type
                      -- True  <=> Instantiate /top-level, invisible/ type variables;
                      --           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, AppCtxt)
            -> TcSigmaType -> [HsExprArg 'TcpRn]
            -> TcM ( [HsExprArg 'TcpInst]
                   , TcSigmaType )   -- Does not instantiate trailing invisible foralls
  -- 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).
  tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
    = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun
                                     , text "fun_sigma" <+> ppr fun_sigma
                                     , text "fun_ctxt" <+> ppr fun_ctxt
                                     , text "args:" <+> ppr rn_args
                                     , text "do_ql" <+> ppr do_ql ])
         ; go 1 [] fun_sigma rn_args }
    where
      fun_orig = case fun_ctxt of
        VAExpansion (OrigStmt{}) _ _  -> DoOrigin
        VAExpansion (OrigPat pat) _ _ -> DoPatOrigin pat
        VAExpansion (OrigExpr e) _ _  -> exprCtOrigin e
        VACall e _ _                  -> exprCtOrigin e
  
      -- 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
      fun_conc_tvs
        | HsVar _ (L _ fun_id) <- tc_fun
        = idConcreteTvs fun_id
        -- Recall that DataCons are represented using ConLikeTc at GhcTc stage,
        -- see Note [Typechecking data constructors] in GHC.Tc.Gen.Head.
        | XExpr (ConLikeTc (RealDataCon dc) _ _) <- tc_fun
        = dataConConcreteTyVars dc
        | otherwise
        = noConcreteTyVars
  
      -- Count value args only when complaining about a function
      -- applied to too many value args
      -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
      n_val_args = count isHsValArg rn_args
  
      fun_is_out_of_scope  -- See Note [VTA for out-of-scope functions]
        = case tc_fun of
            HsHole _        -> True
            _               -> False
  
      inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
      -- True <=> instantiate a tyvar that has this ForAllTyFlag
      inst_fun [] | inst_final  = isInvisibleForAllTyFlag
                  | otherwise   = const False
      inst_fun (EValArg {} : _) = isInvisibleForAllTyFlag
      inst_fun _                = isInferredForAllTyFlag
  
      -----------
      go, go1 :: Int                      -- Value-argument position of next arg
              -> [HsExprArg 'TcpInst]     -- Accumulator, reversed
              -> TcSigmaType -> [HsExprArg 'TcpRn]
              -> TcM ([HsExprArg 'TcpInst], TcSigmaType)
  
      -- go: If fun_ty=kappa, look it up in Theta
      go pos acc fun_ty args
        | Just kappa <- getTyVar_maybe fun_ty
        , isQLInstTyVar kappa
        = do { cts <- readMetaTyVar kappa
             ; case cts of
                  Indirect fun_ty' -> go  pos acc fun_ty' args
                  Flexi            -> go1 pos acc fun_ty  args }
       | otherwise
       = go1 pos acc fun_ty args
  
      -- go1: fun_ty is not filled-in instantiation variable
      --      ('go' dealt with that case)
  
      -- Handle out-of-scope functions gracefully
      go1 pos acc fun_ty (arg : rest_args)
        | fun_is_out_of_scope, looks_like_type_arg arg   -- See Note [VTA for out-of-scope functions]
        = go pos acc fun_ty rest_args
  
      -- 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
      go1 pos acc fun_ty args
        | (tvs,   body1) <- tcSplitSomeForAllTyVars (inst_fun args) fun_ty
        , (theta, body2) <- if inst_fun args Inferred
                            then tcSplitPhiTy body1
                            else ([], body1)
          -- inst_fun args Inferred: dictionary parameters are like Inferred foralls
          -- E.g. #22908: f :: Foo => blah
          -- No foralls!  But if inst_final=False, don't instantiate
        , let no_tvs   = null tvs
              no_theta = null theta
        , not (no_tvs && no_theta)
        = do { (_inst_tvs, wrap, fun_rho) <-
                  -- addHeadCtxt: important for the class constraints
                  -- that may be emitted from instantiating fun_sigma
                  addHeadCtxt fun_ctxt $
                  instantiateSigma fun_orig fun_conc_tvs tvs theta body2
                    -- See Note [Representation-polymorphism checking built-ins]
                    -- in GHC.Tc.Utils.Concrete.
                    -- NB: we are doing this even when "acc" is not empty,
                    -- to handle e.g.
                    --
                    --   badTup :: forall r (a :: TYPE r). a -> (# Int, a #)
                    --   badTup = (# , #) @LiftedRep
                    --
                    -- in which we already have instantiated the first RuntimeRep
                    -- argument of (#,#) to @LiftedRep, but want to rule out the
                    -- second instantiation @r.
  
             ; go pos (addArgWrap wrap acc) fun_rho args }
                  -- 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
      go1 _pos acc fun_ty []
         = do { traceTc "tcInstFun:ret" (ppr fun_ty)
              ; return (reverse acc, fun_ty) }
  
      -- Rule ITVDQ from the GHC Proposal #281
      go1 pos acc fun_ty ((EValArg { ea_arg = arg }) : rest_args)
        | 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]
             ; go (pos+1) (addArgWrap wrap acc) inst_body rest_args }
  
      go1 pos acc fun_ty (EWrap w : args)
        = go1 pos (EWrap w : acc) fun_ty args
  
      go1 pos acc fun_ty (EPrag sp prag : args)
        = go1 pos (EPrag sp prag : acc) fun_ty args
  
      -- Rule ITYARG from Fig 4 of the QL paper
      go1 pos acc fun_ty ( ETypeArg { ea_ctxt = ctxt, ea_hs_ty = hs_ty }
                               : rest_args )
        = do { (ty_arg, inst_ty) <- tcVTA fun_conc_tvs fun_ty hs_ty
             ; let arg' = ETypeArg { ea_ctxt = ctxt, ea_hs_ty = hs_ty, ea_ty_arg = ty_arg }
             ; go pos (arg' : acc) inst_ty rest_args }
  
      -- Rule IVAR from Fig 4 of the QL paper:
      go1 pos acc fun_ty args@(EValArg {} : _)
        | Just kappa <- getTyVar_maybe fun_ty
        , isQLInstTyVar kappa
        = -- Function type was of form   f :: forall a b. t1 -> t2 -> b
          -- with 'b', one of the quantified type variables, in the corner
          -- but the call applies it to three or more value args.
          -- Suppose b is instantiated by kappa.  Then we want to make fresh
          -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2
          --
          -- In principle what is happening here is not unlike matchActualFunTys
          -- but there are many small differences:
          --   - We know that the function type in unfilled meta-tyvar
          --     matchActualFunTys is much more general, has a loop, etc.
          --   - 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.
          do { arg_tys <- zipWithM new_arg_ty (leadingValArgs args) [pos..]
             ; res_ty  <- newOpenFlexiTyVarTy
             ; let fun_ty' = mkScaledFunTys arg_tys res_ty
  
             -- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu
             -- NB: kappa is uninstantiated ('go' already checked that)
             ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
                   -- unifyKind: see (UQL3) in Note [QuickLook unification]
             ; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co))
  
             ; let co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
                   acc'    = addArgWrap co_wrap acc
                   -- Suppose kappa :: kk
                   -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
                   --      co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'
  
             ; go pos acc' fun_ty' args }
  
      -- Rule IARG from Fig 4 of the QL paper:
      go1 pos acc fun_ty
          (EValArg { ea_arg = arg, ea_ctxt = ctxt } : rest_args)
        = do { let herald = case fun_ctxt of
                               VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
                               _ ->  ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
             ; (wrap, arg_ty, res_ty) <-
                  -- NB: matchActualFunTy does the rep-poly check.
                  -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
                  -- In an application (f x), we need 'x' to have a fixed runtime
                  -- representation; matchActualFunTy checks that when
                  -- taking apart the arrow type (a -> Int).
                  matchActualFunTy herald
                    (Just $ HsExprTcThing tc_fun)
                    (n_val_args, fun_sigma) fun_ty
  
             ; arg' <- quickLookArg do_ql ctxt arg arg_ty
             ; let acc' = arg' : addArgWrap wrap acc
             ; go (pos+1) acc' res_ty rest_args }
  
      new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
      -- Make a fresh nus for each argument in rule IVAR
      new_arg_ty (L _ arg) i
        = do { arg_nu <- newOpenFlexiFRRTyVarTy $
                         FRRExpectedFunTy (ExpectedFunTyArg (HsExprTcThing tc_fun) arg) i
                 -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],
                 -- thereby ensuring that the arguments have concrete runtime representations
  
             ; mult_ty <- newFlexiTyVarTy multiplicityTy
                 -- mult_ty: e need variables for argument multiplicities (#18731)
                 -- Otherwise, 'undefined x' wouldn't be linear in x
  
             ; return (mkScaled mult_ty arg_nu) }
  
  -- Is the argument supposed to instantiate a forall?
  --
  -- In other words, given a function application `fn arg`,
  -- can we look at the `arg` and conclude that `fn :: forall x. t`
  -- or `fn :: forall x -> t`?
  --
  -- This is a conservative heuristic that returns `False` for "don't know".
  -- Used to improve error messages only.
  -- See Note [VTA for out-of-scope functions].
  looks_like_type_arg :: HsExprArg 'TcpRn -> Bool
  looks_like_type_arg ETypeArg{} =
    -- The argument is clearly supposed to instantiate an invisible forall,
    -- i.e. when we see `f @a`, we expect `f :: forall x. t`.
    True
  looks_like_type_arg EValArg{ ea_arg = L _ e } =
    -- Check if the argument is supposed to instantiate a visible forall,
    -- i.e. when we see `f (type Int)`, we expect `f :: forall x -> t`,
    --      but not if we see `f True`.
    -- We can't say for sure though. Part 2 of GHC Proposal #281 allows
    -- type arguments without the `type` qualifier, so `f True` could
    -- instantiate `forall (b :: Bool) -> t`.
    case stripParensHsExpr e of
      HsEmbTy _ _ -> True
      _           -> False
  looks_like_type_arg _ = False
  
  addArgCtxt :: AppCtxt -> LHsExpr GhcRn
             -> TcM a -> TcM a
  -- There are four cases:
  -- 1. In the normal case, we add an informative context
  --          "In the third argument of f, namely blah"
  -- 2. If we are deep inside generated code (`isGeneratedCode` is `True`)
  --    or if all or part of this particular application is an expansion
  --    `VAExpansion`, just use the less-informative context
  --          "In the expression: arg"
  --   Unless the arg is also a generated thing, in which case do nothing.
  --   See Note [Rebindable syntax and XXExprGhcRn] in GHC.Hs.Expr
  -- 3. We are in an expanded `do`-block's non-bind statement
  --    we simply add the statement context
  --       "In the statement of the `do`-block .."
  -- 4. We are in an expanded do block's bind statement
  --    a. Then either we are typechecking the first argument of the bind which is user located
  --       so we set the location to be that of the argument
  --    b. Or, we are typechecking the second argument which would be a generated lambda
  --       so we set the location to be whatever the location in the context is
  --  See Note [Expanding HsDo with XXExprGhcRn] in GHC.Tc.Gen.Do
  -- For future: we need a cleaner way of doing this bit of adding the right error context.
  -- There is a delicate dance of looking at source locations and reconstructing
  -- whether the piece of code is a `do`-expanded code or some other expanded code.
  addArgCtxt ctxt (L arg_loc arg) thing_inside
    = do { in_generated_code <- inGeneratedCode
         ; case ctxt of
             VACall fun arg_no _ | not in_generated_code
               -> do setSrcSpanA arg_loc                    $
                       addErrCtxt (FunAppCtxt (FunAppCtxtExpr fun arg) arg_no) $
                       thing_inside
  
             VAExpansion (OrigStmt (L _ stmt@(BindStmt {}))) _ loc
               | isGeneratedSrcSpan (locA arg_loc) -- This arg is the second argument to generated (>>=)
               -> setSrcSpan loc $
                    addStmtCtxt stmt $
                    thing_inside
               | otherwise                        -- This arg is the first argument to generated (>>=)
               -> setSrcSpanA arg_loc $
                    addStmtCtxt stmt $
                    thing_inside
             VAExpansion (OrigStmt (L loc stmt)) _ _
               -> setSrcSpanA loc $
                    addStmtCtxt stmt $
                    thing_inside
  
             _ -> setSrcSpanA arg_loc $
                    addExprCtxt arg     $  -- Auto-suppressed if arg_loc is generated
                    thing_inside }
  
  {- *********************************************************************
  *                                                                      *
                Visible type application
  *                                                                      *
  ********************************************************************* -}
  
  -- See Note [Visible type application and abstraction]
  tcVTA :: ConcreteTyVars
           -- ^ Type variables that must be instantiated to concrete types.
           --
           -- See Note [Representation-polymorphism checking built-ins]
           -- in GHC.Tc.Utils.Concrete.
        -> TcType            -- ^ Function type
        -> LHsWcType GhcRn   -- ^ Argument type
        -> TcM (TcType, TcType)
  -- Deal with a visible type application
  -- The function type has already had its Inferred binders instantiated
  tcVTA conc_tvs fun_ty hs_ty
    | Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
    , binderFlag tvb == Specified
    = do { tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty }
  
    | otherwise
    = do { (_, fun_ty) <- liftZonkM $ zonkTidyTcType emptyTidyEnv fun_ty
         ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }
  
  -- See Note [Visible type application and abstraction]
  tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
        -> (ForAllTyBinder, TcType)    -- Function type
        -> LHsExpr GhcRn               -- Argument type
        -> TcM (TcType, TcType)
  tcVDQ conc_tvs (tvb, inner_ty) arg
    = do { hs_wc_ty <- expr_to_type arg
         ; tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_wc_ty }
  
  -- Convert a HsExpr into the equivalent HsType.
  -- See [RequiredTypeArguments and the T2T mapping]
  expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
  expr_to_type earg =
    case stripParensLHsExpr earg of
      L _ (HsEmbTy _ hs_ty) ->
        -- The entire type argument is guarded with the `type` herald,
        -- e.g. `vfun (type (Maybe Int))`. This special case supports
        -- named wildcards. See Note [Wildcards in the T2T translation]
        return hs_ty
      e ->
        -- The type argument is not guarded with the `type` herald, or perhaps
        -- only parts of it are, e.g. `vfun (Maybe Int)` or `vfun (Maybe (type Int))`.
        -- Apply a recursive T2T transformation.
        HsWC [] <$> go e
          <* failIfErrsM   -- Suppress unhelpful errors that arise after a failed T2T
    where
      go :: LHsExpr GhcRn -> TcM (LHsType GhcRn)
      go (L _ (HsEmbTy _ t)) =
        -- HsEmbTy means there is an explicit `type` herald, e.g. vfun :: forall a -> blah
        -- and the call   vfun (type Int)
        --           or   vfun (Int -> type Int)
        -- The T2T transformation can simply discard the herald and use the embedded type.
        unwrap_wc t
      go (L l (HsFunArr _ mult arg res)) =
        do { arg' <- go arg
           ; mult' <- go_arrow mult
           ; res' <- go res
           ; return (L l (HsFunTy noExtField mult' arg' res'))}
           where
            go_arrow :: HsMultAnnOf (LHsExpr GhcRn) GhcRn -> TcM (HsMultAnn GhcRn)
            go_arrow (HsUnannotated _) = pure (HsUnannotated noExtField)
            go_arrow (HsLinearAnn{}) = pure (HsLinearAnn noExtField)
            go_arrow (HsExplicitMult _ exp) = HsExplicitMult noExtField <$> go exp
      go (L l (HsForAll _ tele expr)) =
        do { ty <- go expr
           ; return (L l (HsForAllTy noExtField tele ty))}
      go (L l (HsQual _ (L ann ctxt) expr)) =
        do { ctxt' <- mapM go ctxt
           ; ty <- go expr
           ; return (L l (HsQualTy noExtField (L ann ctxt') ty)) }
      go (L l (HsVar _ lname)) =
        -- GHC Proposal #281, section 7.5 "T2T-Mapping":
        --   variables and constructors (regardless of their namespace)
        --   are mapped directly, without modification.
        do { detect_puns lname
           ; return (L l (HsTyVar noAnn NotPromoted lname)) }
      go (L l (HsApp _ lhs rhs)) =
        do { lhs' <- go lhs
           ; rhs' <- go rhs
           ; return (L l (HsAppTy noExtField lhs' rhs')) }
      go (L l (HsAppType _ lhs rhs)) =
        do { lhs' <- go lhs
           ; rhs' <- unwrap_wc rhs
           ; return (L l (HsAppKindTy noExtField lhs' rhs')) }
      go (L l e@(OpApp _ lhs op rhs)) =
        do { lhs' <- go lhs
           ; op'  <- go op
           ; rhs' <- go rhs
           ; op_id <- unwrap_op_tv op'
           ; return (L l (HsOpTy noExtField NotPromoted lhs' op_id rhs')) }
        where
          unwrap_op_tv (L _ (HsTyVar _ _ op_id)) = return op_id
          unwrap_op_tv _ = failWith $ TcRnIllformedTypeArgument (L l e)
      go (L l (HsOverLit _ lit))
        | Just tylit <- tyLitFromOverloadedLit (ol_val lit)
        = return (L l (HsTyLit noExtField tylit))
      go (L l (HsLit _ lit))
        | Just tylit <- tyLitFromLit lit
        = return (L l (HsTyLit noExtField tylit))
      go (L l (ExplicitTuple _ tup_args boxity))
        -- Neither unboxed tuples (#e1,e2#) nor tuple sections (e1,,e2,) can be promoted
        | isBoxed boxity
        , Just es <- tupArgsPresent_maybe tup_args
        = do { ts <- traverse go es
             ; return (L l (HsExplicitTupleTy noExtField NotPromoted ts)) }
      go (L l (ExplicitList _ es)) =
        do { ts <- traverse go es
           ; return (L l (HsExplicitListTy noExtField NotPromoted ts)) }
      go (L l (ExprWithTySig _ e sig_ty)) =
        do { t <- go e
           ; sig_ki <- (unwrap_sig <=< unwrap_wc) sig_ty
           ; return (L l (HsKindSig noAnn t sig_ki)) }
        where
          unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
          unwrap_sig (L _ (HsSig _ HsOuterImplicit{hso_ximplicit=bndrs} body))
            | null bndrs = return body
            | otherwise  = illegal_implicit_tvs bndrs
          unwrap_sig (L l (HsSig _ HsOuterExplicit{hso_bndrs=bndrs} body)) =
            return $ L l (HsForAllTy noExtField (HsForAllInvis noAnn bndrs) body)
      go (L l (HsPar _ e)) =
        do { t <- go e
           ; return (L l (HsParTy noAnn t)) }
      go (L l (HsUntypedSplice splice_result splice))
        | HsUntypedSpliceTop finalizers e <- splice_result
        = do { t <- go (L l e)
             ; let splice_result' = HsUntypedSpliceTop finalizers t
             ; return (L l (HsSpliceTy splice_result' splice)) }
      go (L l (HsHole (HoleVar (L _ rdr))))
        | isUnderscore occ = return (L l (HsWildCardTy noExtField))
        | startsWithUnderscore occ =
            -- See Note [Wildcards in the T2T translation]
            do { wildcards_enabled <- xoptM LangExt.NamedWildCards
               ; if wildcards_enabled
                 then illegal_wc rdr
                 else not_in_scope }
        | otherwise = not_in_scope
        where occ = occName rdr
              not_in_scope = failWith $ TcRnNotInScope NotInScope rdr
      go (L l (XExpr (ExpandedThingRn (OrigExpr orig) _))) =
        -- Use the original, user-written expression (before expansion).
        -- Example. Say we have   vfun :: forall a -> blah
        --          and the call  vfun (Maybe [1,2,3])
        --          expanded to   vfun (Maybe (fromListN 3 [1,2,3]))
        -- (This happens when OverloadedLists is enabled).
        -- The expanded expression can't be promoted, as there is no type-level
        -- equivalent of fromListN, so we must use the original.
        go (L l orig)
      go e = failWith $ TcRnIllformedTypeArgument e
  
      detect_puns :: LocatedN (WithUserRdr Name) -> TcM ()
        -- GHC Proposal #281, section 7.5 "T2T-Mapping":
        --   there should be no variable of the same name but from
        --   a different namespace, or else raise an ambiguity error
        --   (does not apply to constructors)
      detect_puns (L l (WithUserRdr rdr _))
        | isTermVarOrFieldNameSpace (rdrNameSpace rdr)
        , Just promoted_rdr <- promoteRdrName rdr
        = do { envs <- getRdrEnvs
             ; whenIsJust (lookup_rdr envs rdr) $ \unpromoted ->
               whenIsJust (lookup_rdr envs promoted_rdr) $ \promoted ->
                 addErrAt (locA l) $
                 TcRnIllegalPunnedVarOccInTypeArgument { illegalPunTermName = unpromoted
                                                       , illegalPunTypeName = promoted } }
        | otherwise = return ()
  
      lookup_rdr :: (GlobalRdrEnv, LocalRdrEnv) -> RdrName -> Maybe ResolvedNameInfo
      lookup_rdr (gbl_env, lcl_env) rdr
        | Just name <- lookupLocalRdrEnv lcl_env rdr
        = Just (ResolvedNameInfo [] rdr name)
        | gres@(gre:_) <- lookupGRE gbl_env (LookupRdrName rdr (RelevantGREsFOS WantNormal))
        = Just (ResolvedNameInfo gres rdr (gre_name gre))
        | otherwise = Nothing
  
      unwrap_wc :: HsWildCardBndrs GhcRn t -> TcM t
      unwrap_wc (HsWC wcs t)
        = do { mapM_ (illegal_wc . nameRdrName) wcs
             ; return t }
  
      illegal_wc :: RdrName -> TcM t
      illegal_wc rdr = failWith $ TcRnIllegalNamedWildcardInTypeArgument rdr
  
      illegal_implicit_tvs :: [Name] -> TcM t
      illegal_implicit_tvs tvs
        = do { mapM_ (addErr . TcRnIllegalImplicitTyVarInTypeArgument . nameRdrName) tvs
             ; failM }
  
  {- Note [RequiredTypeArguments and the T2T mapping]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  The "T2T-Mapping" section of GHC Proposal #281 introduces a term-to-type transformation
  that comes into play when we typecheck function applications to required type arguments.
  Say we have a function that expects a required type argument, vfun :: forall a -> ...
  then it is possible to call it as follows:
  
    vfun (Maybe Int)
  
  The Maybe Int argument is parsed and renamed as a term. There is no syntactic marker
  to tell GHC that it is actually a type argument.  We only discover this by the time
  we get to type checking, where we know that f's type has a visible forall at the front,
  so we are expecting a type argument. More precisely, this happens in tcVDQ in GHC/Tc/Gen/App.hs:
  
    tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
          -> (ForAllTyBinder, TcType)    -- Function type
          -> LHsExpr GhcRn               -- Argument type
          -> TcM (TcType, TcType)
  
  What we want is a type to instantiate the forall-bound variable. But what we have is an HsExpr,
  and we need to convert it to an HsType in order to reuse the same code paths as we use for
  checking f @ty (see tc_inst_forall_arg).
  
    f (Maybe Int)
    -- ^^^^^^^^^
    -- parsed and renamed as:   HsApp   (HsVar   "Maybe") (HsVar   "Int")  ::  HsExpr GhcRn
    -- must be converted to:    HsTyApp (HsTyVar "Maybe") (HsTyVar "Int")  ::  HsType GhcRn
  
  We do this using a helper function:
  
    expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
  
  This conversion is in the TcM monad because
  * It can fail, if the expression is not convertible to a type.
        vfun [x | x <- xs]     Can't convert list comprehension to a type
        vfun (\x -> x)         Can't convert a lambda to a type
  * It needs to check for LangExt.NamedWildCards to generate an appropriate
    error message for HsHole (HsVar ...).
       vfun _a    Not in scope: ‘_a’
                     (NamedWildCards disabled)
       vfun _a    Illegal named wildcard in a required type argument: ‘_a’
                     (NamedWildCards enabled)
  
  Note [Wildcards in the T2T translation]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Suppose f1 :: forall a b. blah
          f2 :: forall a b -> blah
  
  Consider the terms
    f1 @_ @(Either _ _)
    f2 (type _) (type (Either _ _))
  Those `_` wildcards are type wildcards, each standing for a monotype.
  All good.
  
  Now consider this, with -XNamedWildCards:
    f1 @_a @(Either _a _a)
    f2 (type _a) (type (Either _a _a))
  Those `_a` are "named wildcards", specified by the user manual like this: "All
  occurrences of the same named wildcard within one type signature will unify to
  the same type".  Note "within one signature".  So each type argument is considered
  separately, and the examples mean the same as:
    f1 @_a1 @(Either _a2 _a2)
    f2 (type _a1) (type (Either _a2 _a2))
  The repeated `_a2` ensures that the two arguments of `Either` are the same type;
  but there is no connection with `_a1`.  (NB: `_a1` and `_a2` only scope within
  their respective type, no further.)
  
  Now, consider the T2T translation for
     f2 _ (Either _ _)
  This is fine: the term wildcard `_` is translated to a type wildcard, so we get
  the same as if we had written
     f2 (type _) (type (Either _ _))
  
  But what about /named/ wildcards?
     f2 _a (Either _a _a)
  Now we are in difficulties.  The renamer looks for a /term/ variable `_a` in scope,
  and won't find one.  Even if it did, the three `_a`'s would not be renamed separately
  as above.
  
  Conclusion: we treat a named wildcard in the T2T translation as an error.  If you
  want that, use a `(type ty)` argument instead.
  -}
  
  tc_inst_forall_arg :: ConcreteTyVars            -- See Note [Representation-polymorphism checking built-ins]
                     -> (ForAllTyBinder, TcType)  -- Function type
                     -> LHsWcType GhcRn           -- Argument type
                     -> TcM (TcType, TcType)
  tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
    = do { let tv   = binderVar tvb
               kind = tyVarKind tv
               tv_nm   = tyVarName tv
               mb_conc = lookupNameEnv conc_tvs tv_nm
         ; ty_arg0 <- tcHsTypeApp hs_ty kind
  
         -- Is this type variable required to be instantiated to a concrete type?
         -- If so, ensure that that is the case.
         --
         -- See [Wrinkle: VTA] in Note [Representation-polymorphism checking built-ins]
         -- in GHC.Tc.Utils.Concrete.
         ; th_lvl <- getThLevel
         ; ty_arg <- case mb_conc of
             Nothing   -> return ty_arg0
             Just conc
               -- See [Wrinkle: Typed Template Haskell]
               -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
               | TypedBrack {} <- th_lvl
               -> return ty_arg0
               | otherwise
               ->
               -- Example: user wrote e.g. (#,#) @(F Bool) for a type family F.
               -- Emit [W] F Bool ~ kappa[conc] and pretend the user wrote (#,#) @kappa.
                 coercionRKind <$> unifyConcrete (occNameFS $ getOccName $ tv_nm) conc ty_arg0
  
         ; let fun_ty    = mkForAllTy tvb inner_ty
               in_scope  = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
               insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
                 -- This substitution is well-kinded even when inner_ty
                 -- is not fully zonked, because ty_arg is fully zonked.
                 -- See Note [Type application substitution].
  
         ; traceTc "tc_inst_forall_arg (VTA/VDQ)" (
                    vcat [ text "fun_ty" <+> ppr fun_ty
                         , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
                         , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
                                         <+> debugPprType (typeKind ty_arg)
                         , text "inner_ty" <+> debugPprType inner_ty
                         , text "insted_ty" <+> debugPprType insted_ty ])
         ; return (ty_arg, insted_ty) }
  
  {- Note [Visible type application and abstraction]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  GHC supports the types
      forall {a}.  a -> t     -- ForAllTyFlag is Inferred
      forall  a.   a -> t     -- ForAllTyFlag is Specified
      forall  a -> a -> t     -- ForAllTyFlag is Required
  
  The design of type abstraction and type application for those types has gradually
  evolved over time, and is based on the following papers and proposals:
    - "Visible Type Application"
      https://richarde.dev/papers/2016/type-app/visible-type-app.pdf
    - "Type Variables in Patterns"
      https://richarde.dev/papers/2018/pat-tyvars/pat-tyvars.pdf
    - "Modern Scoped Type Variables"
      https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst
    - "Visible forall in types of terms"
      https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst
  
  Here we offer an overview of the design mixed with commentary on the
  implementation status. The proposals have not been fully implemented at the
  time of writing this Note (see "not implemented" in the rest of this Note).
  
  Now consider functions
      fi :: forall {a}. a -> t     -- Inferred:  type argument cannot be supplied
      fs :: forall a. a -> t       -- Specified: type argument may    be supplied
      fr :: forall a -> a -> t     -- Required:  type argument must   be supplied
  
  At a call site we may have calls looking like this
      fi             True  -- Inferred: no visible type argument
      fs             True  -- Specified: type argument omitted
      fs      @Bool  True  -- Specified: type argument supplied
      fr (type Bool) True  -- Required: type argument is compulsory, `type` qualifier used
      fr       Bool  True  -- Required: type argument is compulsory, `type` qualifier omitted
  
  At definition sites we may have type /patterns/ to abstract over type variables
     fi           x       = rhs   -- Inferred: no type pattern
     fs           x       = rhs   -- Specified: type pattern omitted
     fs @a       (x :: a) = rhs   -- Specified: type pattern supplied
     fr (type a) (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier used
     fr a        (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
  
  Type patterns in lambdas mostly work the same way as they do in a function LHS,
  except for @-binders
     OK:  fs = \           x       -> rhs   -- Specified: type pattern omitted
     Bad: fs = \ @a       (x :: a) -> rhs   -- Specified: type pattern supplied
     OK:  fr = \ (type a) (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier used
     OK:  fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
  
  When it comes to @-binders in lambdas, they do work, but only in a limited set
  of circumstances:
    * the lambda occurs as an argument to a higher-rank function or constructor
        higher-rank function:  h :: (forall a. blah) -> ...
        call site:             x = h (\ @a -> ... )
    * the lambda is annotated with an inline type signature:
        (\ @a -> ... ) :: forall a. blah
    * the lambda is a field in a data structure, whose type is impredicative
        [ \ @a -> ... ] :: [forall a. blah]
    * the @-binder is not the first binder in the lambda:
        \ x @a -> ...
  
  Type patterns may also occur in a constructor pattern. Consider the following data declaration
     data T where
       MkTI :: forall {a}. Show a => a -> T   -- Inferred
       MkTS :: forall a.   Show a => a -> T   -- Specified
       MkTR :: forall a -> Show a => a -> T   -- Required  (NB: not implemented)
  
  Matching on its constructors may look like this
     f (MkTI           x)       = rhs  -- Inferred: no type pattern
     f (MkTS           x)       = rhs  -- Specified: type pattern omitted
     f (MkTS @a       (x :: a)) = rhs  -- Specified: type pattern supplied
     f (MkTR (type a) (x :: a)) = rhs  -- Required: type pattern is compulsory, `type` qualifier used    (NB: not implemented)
     f (MkTR a        (x :: a)) = rhs  -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
  
  The moving parts are as follows:
    (abbreviations used: "c.o." = "constructor of")
  
  Syntax of types
  ---------------
  * The types are all initially represented with HsForAllTy (c.o. HsType).
    The binders are in the (hst_tele :: HsForAllTelescope pass) field of the HsForAllTy
    At this stage, we have
        forall {a}. t    -- HsForAllInvis (c.o. HsForAllTelescope) and InferredSpec  (c.o. Specificity)
        forall a. t      -- HsForAllInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
        forall a -> t    -- HsForAllVis (c.o. HsForAllTelescope)
  
  * By the time we get to checking applications/abstractions (e.g. GHC.Tc.Gen.App)
    the types have been kind-checked (e.g. by tcLHsType) into ForAllTy (c.o. Type).
    At this stage, we have:
        forall {a}. t    -- ForAllTy (c.o. Type) and Inferred  (c.o. ForAllTyFlag)
        forall a. t      -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
        forall a -> t    -- ForAllTy (c.o. Type) and Required  (c.o. ForAllTyFlag)
  
  Syntax of applications in HsExpr
  --------------------------------
  * We represent type applications in HsExpr like this (ignoring parameterisation)
      data HsExpr = HsApp HsExpr HsExpr      -- (f True)    (plain function application)
                  | HsAppType HsExpr HsType  -- (f @True)   (function application with `@`)
                  | HsEmbTy HsType           -- (type Int)  (embed a type into an expression with `type`)
                  | ...
  
  * So (f @ty) is represented, just as you might expect:
      HsAppType f ty
  
  * But (f (type ty)) is represented by:
      HsApp f (HsEmbTy ty)
  
    Why the difference?  Because we /also/ need to express these /nested/ uses of `type`:
  
        g (Maybe (type Int))               -- valid for g :: forall (a :: Type) -> t
        g (Either (type Int) (type Bool))  -- valid for g :: forall (a :: Type) -> t
  
    This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
    switches namespace, and is subject to the term-to-type transformation.
  
  Syntax of abstractions in Pat
  -----------------------------
  * Type patterns are represented in Pat roughly like this
       data Pat = ConPat   ConLike [Pat]  -- (Con @tp1 @tp2 p1 p2)  (constructor pattern)
                | EmbTyPat HsTyPat        -- (type tp)              (embed a type into a pattern with `type`)
                | InvisPat HsTyPat        -- (@tp)                  (invisible type pattern)
                | ...
       data HsTyPat = HsTP LHsType
    (In ConPat, the type and term arguments are actually inside HsConPatDetails.)
  
    * Similar to HsAppType in HsExpr, InvisPat in ConPat is used for @ty arguments
    * Similar to HsEmbTy   in HsExpr, EmbTyPat lets you embed a type in a pattern
  
  * Examples:
        \ (MkT @a  (x :: a)) -> rhs    -- ConPat (c.o. Pat) and InvisPat (c.o. Pat)
        \ (type a) (x :: a)  -> rhs    -- EmbTyPat (c.o. Pat)
        \ a        (x :: a)  -> rhs    -- VarPat (c.o. Pat)
        \ @a       (x :: a)  -> rhs    -- InvisPat (c.o. Pat)
  
  * A HsTyPat is not necessarily a plain variable. At the very least,
    we support kind signatures and wildcards:
        \ (type _)           -> rhs
        \ (type (b :: Bool)) -> rhs
        \ (type (_ :: Bool)) -> rhs
    But in constructor patterns we also support full-on types
        \ (P @(a -> Either b c)) -> rhs
    All these forms are represented with HsTP (c.o. HsTyPat).
  
  Renaming type applications
  --------------------------
  rnExpr delegates renaming of type arguments to rnHsWcType if possible:
      f @t        -- HsAppType,         t is renamed with rnHsWcType
      f (type t)  -- HsApp and HsEmbTy, t is renamed with rnHsWcType
  
  But what about:
      f t         -- HsApp, no HsEmbTy
  We simply rename `t` as a term using a recursive call to rnExpr; in particular,
  the type of `f` does not affect name resolution (Lexical Scoping Principle).
  We will later convert `t` from a `HsExpr` to a `Type`, see "Typechecking type
  applications" later in this Note. The details are spelled out in the "Resolved
  Syntax Tree" and "T2T-Mapping" sections of GHC Proposal #281.
  
  Renaming type abstractions
  --------------------------
  rnPat delegates renaming of type arguments to rnHsTyPat if possible:
    f (P @t)   = rhs  -- ConPat,   t is renamed with rnHsTyPat
    f (type t) = rhs  -- EmbTyPat, t is renamed with rnHsTyPat
  
  But what about:
    f t = rhs   -- VarPat
  The solution is as before (see previous section), mutatis mutandis.
  Rename `t` as a pattern using a recursive call to `rnPat`, convert it
  to a type pattern later.
  
  One particularly prickly issue is that of implicit quantification. Consider:
  
    f :: forall a -> ...
    f t = ...   -- binding site of `t`
      where
        g :: t -> t   -- use site of `t` or a fresh variable?
        g = ...
  
  Does the signature of `g` refer to `t` bound in `f`, or is it a fresh,
  implicitly quantified variable? This is normally controlled by
  ScopedTypeVariables, but in this example the renamer can't tell `t` from a term
  variable.  Only later (in the type checker) will we find out that it stands for
  the forall-bound type variable `a`.  So when RequiredTypeArguments is in effect,
  we change implicit quantification to take term variables into account; that is,
  we do not implicitly quantify the signature of `g` to `g :: forall t. t->t`
  because of the term-level `t` that is in scope.
  See Note [Term variable capture and implicit quantification].
  
  Typechecking type applications
  ------------------------------
  Type applications are checked alongside ordinary function applications
  in tcInstFun.
  
  First of all, we assume that the function type is known (i.e. not a metavariable)
  and contains a `forall`. Consider:
    f :: forall a. a -> a
    f x = const x (f @Int 5)
  If the type signature is removed, the definition results in an error:
    Cannot apply expression of type ‘t1’
    to a visible type argument ‘Int’
  
  The same principle applies to required type arguments:
    f :: forall a -> a -> a
    f (type a) x = const x (f (type Int) 5)
  If the type signature is removed, the error is:
    Illegal type pattern.
    A type pattern must be checked against a visible forall.
  
  When the type of the function is known and contains a `forall`, all we need to
  do is instantiate the forall-bound variable with the supplied type argument.
  This is done by tcVTA (if Specified) and tcVDQ (if Required).
  
  tcVDQ unwraps the HsEmbTy and uses the type contained within it.  Crucially, in
  tcVDQ we know that we are expecting a type argument.  This means that we can
  support
      f (Maybe Int)   -- HsApp, no HsEmbTy
  The type argument (Maybe Int) is represented as an HsExpr, but tcVDQ can easily
  convert it to HsType.  This conversion is called the "T2T-Mapping" in GHC
  Proposal #281.
  
  Typechecking type abstractions
  ------------------------------
  Type abstractions are checked alongside ordinary patterns in GHC.Tc.Gen.Pat.tcMatchPats.
  One of its inputs is a list of ExpPatType that has two constructors
    * ExpFunPatTy    ...   -- the type A of a function A -> B
    * ExpForAllPatTy ...   -- the binder (a::A) of forall (a::A) -> B
  so when we are checking
    f :: forall a b -> a -> b -> ...
    f (type a) (type b) (x :: a) (y :: b) = ...
  our expected pattern types are
    [ ExpForAllPatTy ...      -- forall a ->
    , ExpForAllPatTy ...      -- forall b ->
    , ExpFunPatTy    ...      -- a ->
    , ExpFunPatTy    ...      -- b ->
    ]
  
  The [ExpPatType] is initially constructed by GHC.Tc.Utils.Unify.matchExpectedFunTys,
  by decomposing the type signature for `f` in our example.  If we are given a
  definition
     g (type a) = ...
  we never /infer/ a type g :: forall a -> blah.  We can only /check/
  explicit type abstractions in terms.
  
  The [ExpPatType] allows us to use different code paths for type abstractions
  and ordinary patterns:
    * tc_pat :: Scaled ExpSigmaTypeFRR -> Checker (Pat GhcRn) (Pat GhcTc)
    * tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
  
  tc_forall_pat unwraps the EmbTyPat and uses the type pattern contained
  within it. This is another spot where the "T2T-Mapping" can take place,
  allowing us to support
    f a (x :: a) = rhs    -- no EmbTyPat
  
  Type patterns in constructor patterns are handled in with tcConTyArg.
  Both tc_forall_pat and tcConTyArg delegate most of the work to tcHsTyPat.
  
  Note [VTA for out-of-scope functions]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Suppose 'wurble' is not in scope, and we have
     (wurble @Int @Bool True 'x')
  
  Then the renamer will make (HsHole (HsVar "wurble")) for 'wurble',
  and the typechecker will typecheck it with tcUnboundId, giving it
  a type 'alpha', and emitting a deferred Hole constraint, to
  be reported later.
  
  But then comes the visible type application. If we do nothing, we'll
  generate an immediate failure (in tc_app_err), saying that a function
  of type 'alpha' can't be applied to Bool.  That's insane!  And indeed
  users complain bitterly (#13834, #17150.)
  
  The right error is the Hole, which has /already/ been emitted by
  tcUnboundId.  It later reports 'wurble' as out of scope, and tries to
  give its type.
  
  Fortunately in tcInstFun we still have access to the function, so we
  can check if it is a HsHole.  We use this info to simply skip
  over any visible type arguments.  We'll /already/ have emitted a
  Hole constraint; failing preserves that constraint.
  
  We do /not/ want to fail altogether in this case (via failM) because
  that may abandon an entire instance decl, which (in the presence of
  -fdefer-type-errors) leads to leading to #17792.
  
  What about required type arguments?  Suppose we see
      f (type Int)
  where `f` is out of scope.  Then again we don't want to crash because f's
  type (which will be just a fresh unification variable) isn't a visible forall.
  Instead we just skip the `(type Int)` argument, as before.
  
  Downside: the typechecked term has lost its visible type arguments; we
  don't even kind-check them.  But let's jump that bridge if we come to
  it.  Meanwhile, let's not crash!
  
  Note [Type application substitution]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In `tc_inst_forall_arg`, suppose we are checking a visible type
  application `f @hs_ty`, where `f :: forall (a :: k). body`.  We will:
    * Compute `ty <- tcHsTypeApp hs_ty k`
    * Then substitute `a :-> ty` in `body`.
  Now, you might worry that `a` might not have the same kind as `ty`, so that the
  substitution isn't kind-preserving.  How can that happen?  The kinds will
  definitely be the same after zonking, and `ty` will be zonked (as this is
  a postcondition of `tcHsTypeApp`). But the function type `forall a. body`
  might not be fully zonked (hence the worry).
  
  But it's OK!  During type checking, we don't require types to be well-kinded (without
  zonking); we only require them to satsisfy the Purely Kinded Type Invariant (PKTI).
  See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType.
  
  In the case of a type application:
    * `forall a. body` satisfies the PKTI
    * `ty` is zonked
    * If we substitute a fully-zonked thing into an un-zonked Type that
      satisfies the PKTI, the result still satisfies the PKTI.
  
  This last statement isn't obvious, but read
  Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType.
  The tricky case is when `body` contains an application of the form `a b1 ... bn`,
  and we substitute `a :-> ty` where `ty` has fewer arrows in its kind than `a` does.
  That can't happen: the call `tcHsTypeApp hs_ty k` would have rejected the
  type application as ill-kinded.
  
  Historical remark: we used to require a stronger invariant than the PKTI,
  namely that all types are well-kinded prior to zonking. In that context, we did
  need to zonk `body` before performing the substitution above. See test case
  #14158, as well as the discussion in #23661.
  -}
  
  {- *********************************************************************
  *                                                                      *
                Quick Look
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [Quick Look at value arguments]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  The function quickLookArg implements the "QL argument" judgement of
  the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
  rather directly.  The key rule, implemented by `quickLookArg` is
  
     G |-h h:sg                         -- Find the type of the head
     G |-inst sg;pis ~> phis;rho_r      -- tcInstFun on the args
     (A) rho = T sgs  OR  (B) fiv(phis) = emptyset  -- can_do_ql
     -------------------------------------- APP-QL
     G |-ql h pis : rho ~> qlUnify( rho, rho_r )
  
  (The paper uses a lightning-bolt where we use "ql".)  The most straightforward
  way to implement this rule for a call (f e1 ... en) would be:
  
     1. Take a quick look at the argumets e1..en to guide instantiation
        of the function f.
     2. Then typecheck e1..en from scratch.
  
  That's wasteful, because in Step 1, the quick look at each argument, say (g
  h1..hm), involves instantiating `h` and taking a quick look at /its/
  arguments.  Then in Step 2 we typecheck (g h1..hm) and again take a quick look
  at its arguments.  This is quadratic in the nesting depth of the arguments.
  
  Instead, after the quick look, we /save/ the work we have done in an EValArgQL
  record, and /resume/ it later.  The way to think of it is this:
  
    * `tcApp` typechecks an application.  It uses `tcInstFun`, which in turn
      calls `quickLookArg` on each value argument.
  
    * `quickLookArg` (which takes a quick look at the argument)
  
        - Does the "initial" part of `tcApp`, especially `tcInstFun`
  
        - Captures the result in an EValArgQL record
  
        - Later, `tcValArg` starts from the EValArgQL record, and
          completes the job of typechecking the application
  
  This turned out to be more subtle than I expected.  Wrinkles:
  
  (QLA1) `quickLookArg` decides whether or not premises (A) and (B) of the
    quick-look-arg judgement APP-QL are satisfied; this is captured in
    `arg_influences_enclosing_call`.
  
  (QLA2) We avoid zonking, so the `arg_influences_enclosing_call` sees the
    argument type /before/ the QL substitution Theta is applied to it. So we
    achieve argument-order independence for free (see 5.7 in the paper).  See the
    `isGuardedTy orig_arg_rho` test in `quickLookArg`.
  
  (QLA3) Deciding whether the premises are satisfied involves calling `tcInstFun`
    (which takes quite some work becuase it calls quickLookArg on nested calls).
    That's why we want to capture the work done, in EValArgQL.
  
    Do we really have to call `tcInstFun` before deciding (B) of
    `arg_influences_enclosing_call`? Yes (#24686).
    Suppose ids :: [forall a. a->a], and consider
       (:) (reverse ids) blah
    `tcApp` on the outer call will instantiate (:) with `kappa`, and take a
    quick look at (reverse ids). Only after instantiating `reverse` with kappa2,
    quick-looking at `ids` can we discover that (kappa2:=forall a. a->a), which
    satisfies premise (B) of `arg_influence_enclosing_call`.
  
  (QLA4) When we resume typechecking an argument, in `tcValArg` on `EValArgQL`
  
    - Calling `tcInstFun` on the argument may have emitted some constraints, which
      we carefully captured in `quickLookArg` and stored in the EValArgQL.  We must
      now emit them with `emitConstraints`.  This must be done /under/ the skolemisation
      of the argument's type (see `tcSkolemise` in `tcValArg` for EValArgQL { ...}.
      Example:   f :: (forall b. Ord b => b -> b -> Bool) -> ...
         Call:   f (==)
      we must skolemise the argument type (forall b. Ord b => b -> b -> Bool)
      before emitting the [W] Eq alpha constraint arising from the call to (==).
      It will be solved from the Ord b!
  
    - quickLookArg may or may not have done `qlUnify` with the calling context.
      If not (eaql_encl = False) must do so now.  Example:  choose [] ids,
              where ids :: [forall a. a->a]
                    choose :: a -> a -> a
      We instantiate choose with `kappa` and discover from `ids` that
      (kappa = [forall a. a->a]).  Now we resume typechecking argument [], and
      we must take advantage of what we have now discovered about `kappa`,
      to typecheck   [] :: [forall a. a->a]
  
  (QLA5) In the quicklook pass, we don't scale multiplicities. Since arguments
      aren't typechecked yet, we don't know their free variable usages
      anyway. But, in a nested call, the head of an application chain is fully
      typechecked.
  
      In order for the multiplicities in the head to be properly scaled, we store
      the head's usage environment in the eaql_fun_ue field. Then, when we do the
      full-typechecking pass, we can emit the head's usage environment where we
      would have typechecked the head in a naive algorithm.
  
  (QLA6) `quickLookArg` is supposed to capture the result of partially typechecking
     the argument, so it can be resumed later.  "Capturing" should include all
     generated type-class/equality constraints and Linear-Haskell usage info. There
     are two calls in `quickLookArg1` that might generate such constraints:
  
       - `tcInferAppHead_maybe`.  This can generat Linear-Haskell usage info, via
         the call to `tcEmitBindingUsage` in `check_local_id`, which is called
         indirectly by `tcInferAppHead_maybe`.
  
         In contrast, `tcInferAppHead_maybe` does not generate any type-class or
         equality constraints, because it doesn't instantiate any functions.  [But
         see #25493 and #25494 for why this isn't quite true today.]
  
      - `tcInstFun` generates lots of type-class and equality constraints, as it
        instantiates the function.  But it generates no usage info, because that
        comes only from the call to `check_local_id`, whose usage info is captured
        in the call to `tcInferAppHead_maybe` in `quickLookArg1`.
  
    Conclusion: in quickLookArg1:
      - capture usage information (but not constraints)
          for the call to `tcInferAppHead_maybe`
      - capture constraints (but not usage information)
          for the call to `tcInstFun`
  
  -}
  
  quickLookArg :: QLFlag -> AppCtxt
               -> LHsExpr GhcRn          -- ^ Argument
               -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
               -> TcM (HsExprArg 'TcpInst)
  -- See Note [Quick Look at value arguments]
  quickLookArg NoQL ctxt larg orig_arg_ty
    = skipQuickLook ctxt larg orig_arg_ty
  quickLookArg DoQL 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
           else quickLookArg1 ctxt larg orig_arg_ty }
  
  skipQuickLook :: AppCtxt -> LHsExpr GhcRn -> Scaled TcRhoType
                -> TcM (HsExprArg 'TcpInst)
  skipQuickLook ctxt larg arg_ty
    = return (EValArg { ea_ctxt   = ctxt
                      , ea_arg    = larg
                      , ea_arg_ty = arg_ty })
  
  whenQL :: QLFlag -> ZonkM () -> TcM ()
  whenQL DoQL thing_inside = liftZonkM thing_inside
  whenQL NoQL _            = return ()
  
  tcIsDeepRho :: TcType -> TcM Bool
  -- This top-level zonk step, which is the reason we need a local 'go' loop,
  -- is subtle. See Section 9 of the QL paper
  
  tcIsDeepRho ty
    = do { ds_flag <- getDeepSubsumptionFlag
         ; go ds_flag ty }
    where
      go ds_flag ty
        | isSigmaTy ty = return False
  
        | Just kappa <- getTyVar_maybe ty
        , isQLInstTyVar kappa
        = do { info <- readMetaTyVar kappa
             ; case info of
                 Indirect arg_ty' -> go ds_flag arg_ty'
                 Flexi            -> return True }
  
        | Deep <- ds_flag
        , Just (_, res_ty) <- tcSplitFunTy_maybe ty
        = go ds_flag res_ty
  
        | otherwise = return True
  
  isGuardedTy :: TcType -> Bool
  isGuardedTy ty
    | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
    | Just {} <- tcSplitAppTy_maybe ty        = True
    | otherwise                               = False
  
  quickLookArg1 :: AppCtxt -> LHsExpr GhcRn
                -> Scaled TcRhoType  -- Deeply skolemised
                -> TcM (HsExprArg 'TcpInst)
  -- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
  quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    = addArgCtxt ctxt larg $ -- Context needed for constraints
                             -- generated by calls in arg
      do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
  
         -- Step 1: get the type of the head of the argument
         ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun
           -- tcCollectingUsage: the use of an Id at the head generates usage-info
           -- See the call to `tcEmitBindingUsage` in `check_local_id`.  So we must
           -- capture and save it in the `EValArgQL`.  See (QLA6) in
           -- Note [Quick Look at value arguments]
  
         ; traceTc "quickLookArg {" $
           vcat [ text "arg:" <+> ppr arg
                , text "orig_arg_rho:" <+> ppr orig_arg_rho
                , text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
                , text "args:" <+> ppr rn_args ]
  
         ; case mb_fun_ty of {
             Nothing -> skipQuickLook ctxt larg sc_arg_ty ;    -- fun is too complicated
             Just (tc_fun, fun_sigma) ->
  
         -- step 2: use |-inst to instantiate the head applied to the arguments
      do { let tc_head = (tc_fun, fun_ctxt)
         ; do_ql <- wantQuickLook rn_fun
         ; ((inst_args, app_res_rho), wanted)
               <- captureConstraints $
                  tcInstFun do_ql True tc_head fun_sigma rn_args
                  -- We must capture type-class and equality constraints here, but
                  -- not equality constraints.  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 ]
  
         -- Step 3: Check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
         --         Namely: (A) is orig_arg_rho is guarded
           --           or: (B) fiv(app_res_rho) = emptyset
         -- This tells us if the quick look at the argument yields information that
         -- influences the enclosing function call
         -- NB: guardedness is computed based on the original,
         -- unzonked orig_arg_rho, so that we deliberately do
         -- not exploit guardedness that emerges a result of QL on earlier args
         -- We must do the anyFreeKappa test /after/ tcInstFun; see (QLA3).
         ; arg_influences_enclosing_call
              <- if isGuardedTy orig_arg_rho
                 then return True
                 else not <$> anyFreeKappa app_res_rho  -- (B)
                      -- For (B) see Note [The fiv test in quickLookArg]
  
         -- Step 4: do quick-look unification if either (A) or (B) hold
         -- NB: orig_arg_rho may not be zonked, but that's ok
         ; when arg_influences_enclosing_call $
           qlUnify app_res_rho orig_arg_rho
  
         ; traceTc "quickLookArg done }" (ppr rn_fun)
  
         ; return (EValArgQL { eaql_ctxt    = ctxt
                             , 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
                             , eaql_encl    = arg_influences_enclosing_call
                             , eaql_res_rho = app_res_rho }) }}}
  
  {- *********************************************************************
  *                                                                      *
                   Folding over instantiation variables
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [Monomorphise instantiation variables]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When we are done with Quick Look on a call, we must turn any un-unified
  /instantiation/ variables into regular /unification/ variables.  This is the
  lower-case 'theta' (a mono-substitution) in the APP-DOWN rule of Fig 5 of the
  Quick Look paper.
  
  We so this by look at the arguments, left to right, monomorphising the free
  instantiation variables of the /type/ arguments of the call.  Those type
  arguments appear (only) in
    * the `WpTyApp` components of
    * the `HsWrapper` of
    * a `EWrap` argument
  See `qlMonoHsWrapper`.
  
  By going left to right, we are sure to monomorphise instantiation variables
  before we encounter them in an argument type (in `tcValArg`).
  
  All instantiation variables for a call will be reachable from the type(s)
  at which the function is instantiated -- i.e. those WpTyApps.  Even instantiation
  variables allocoated by tcInstFun itself, such as in the IRESULT rule, end up
  connected to the original type(s) at which the function is instantiated.
  
  To monomorphise the free QL instantiation variables of a type, we use
  `foldQLInstVars`.
  
  Wrinkles:
  
  (MIV1) When monomorphising an instantiation variable, don't forget to
     monomorphise its kind. It might have type (a :: TYPE k), where both
    `a` and `k` are instantiation variables.
  
  (MIV2) In `qlUnify`, `make_kinds_ok` may unify
      a :: k1  ~  b :: k2
    making a cast
      a := b |> (co :: k1 ~ k2)
    But now suppose k1 is an instantiation variable.  Then that coercion hole
    `co` is the only place that `k1` will show up in the traversal, and yet
    we want to monomrphise it.  Hence the do_hole in `foldQLInstTyVars`
  -}
  
  qlMonoHsWrapper :: HsWrapper -> ZonkM ()
  -- See Note [Monomorphise instantiation variables]
  qlMonoHsWrapper (WpCompose w1 w2) = qlMonoHsWrapper w1 >> qlMonoHsWrapper w2
  qlMonoHsWrapper (WpTyApp ty)      = qlMonoTcType ty
  qlMonoHsWrapper _                 = return ()
  
  qlMonoTcType :: TcType -> ZonkM ()
  -- See Note [Monomorphise instantiation variables]
  qlMonoTcType ty
    = do { traceZonk "monomorphiseQLInstVars {" (ppr ty)
         ; go_ty ty
         ; traceZonk "monomorphiseQLInstVars }" empty }
    where
      go_ty :: TcType -> ZonkM ()
      go_ty ty = unTcMUnit (foldQLInstVars go_tv ty)
  
      go_tv :: TcTyVar -> TcMUnit
      -- Precondition: tv is a QL instantiation variable
      -- If it is already unified, look through it and carry on
      -- If not, monomorphise it, by making a fresh unification variable,
      -- at the ambient level
      go_tv tv
        | MetaTv { mtv_ref = ref, mtv_tclvl = lvl, mtv_info = info } <- tcTyVarDetails tv
        = assertPpr (case lvl of QLInstVar -> True; _ -> False) (ppr tv) $
          TCMU $ do { traceZonk "qlMonoTcType" (ppr tv)
                    ; flex <- readTcRef ref
                    ; case flex of {
                        Indirect ty -> go_ty ty ;
                        Flexi       ->
                 do { let kind = tyVarKind tv
                    ; go_ty kind  -- See (MIV1) in Note [Monomorphise instantiation variables]
                    ; ref2  <- newTcRef Flexi
                    ; lvl2  <- getZonkTcLevel
                    ; let details = MetaTv { mtv_info  = info
                                           , mtv_ref   = ref2
                                           , mtv_tclvl = lvl2 }
                          tv2  = mkTcTyVar (tyVarName tv) kind details
                   ; writeTcRef ref (Indirect (mkTyVarTy tv2)) }}}
        | otherwise
        = pprPanic "qlMonoTcType" (ppr tv)
  
  newtype TcMUnit = TCMU { unTcMUnit :: ZonkM () }
  instance Semigroup TcMUnit where
    TCMU ml <> TCMU mr = TCMU (ml >> mr)
  instance Monoid TcMUnit where
    mempty = TCMU (return ())
  
  {- Note [The fiv test in quickLookArg]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
  for having no free instantiation variables.  We do this in Step 3 of quickLookArg1,
  using anyFreeKappa.  Example:
      Suppose       ids :: [forall a. a->a]
      and consider  Just (ids++ids)
  We will instantiate Just with kappa, say, and then call
      quickLookArg1 False {kappa} (ids ++ ids) kappa
  The call to tcInstFun will return with app_res_rho = [forall a. a->a]
  which has no free instantiation variables, so we can QL-unify
    kappa ~ [Forall a. a->a]
  -}
  
  anyFreeKappa :: TcType -> TcM Bool
  -- True if there is a free instantiation variable
  -- in the argument type, after zonking
  -- See Note [The fiv test in quickLookArg]
  anyFreeKappa ty = unTcMBool (foldQLInstVars go_tv ty)
    where
      go_tv tv = TCMB $ do { info <- readMetaTyVar tv
                           ; case info of
                               Indirect ty -> anyFreeKappa ty
                               Flexi       -> return True }
  
  newtype TcMBool = TCMB { unTcMBool :: TcM Bool }
  instance Semigroup TcMBool where
    TCMB ml <> TCMB mr = TCMB (do { l <- ml; if l then return True else mr })
  instance Monoid TcMBool where
    mempty = TCMB (return False)
  
  foldQLInstVars :: forall a. Monoid a => (TcTyVar -> a) -> TcType -> a
  {-# INLINE foldQLInstVars #-}
  foldQLInstVars check_tv ty
    = do_ty ty
    where
      (do_ty, _, _, _) = foldTyCo folder ()
  
      folder :: TyCoFolder () a
      folder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
                                               -- in GHC.Core.TyCo.FVs
                          , tcf_tyvar = do_tv, tcf_covar = mempty
                          , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
  
      do_bndr _ _ _ = ()
  
      do_hole _ hole = do_ty (coVarKind (coHoleCoVar hole))
                       -- See (MIV2) in Note [Monomorphise instantiation variables]
  
      do_tv :: () -> TcTyVar -> a
      do_tv _ tv | isQLInstTyVar tv = check_tv tv
                 | otherwise        = mempty
  
  {- *********************************************************************
  *                                                                      *
                   QuickLook unification
  *                                                                      *
  ********************************************************************* -}
  
  qlUnify :: TcType -> TcType -> TcM ()
  -- Unify ty1 with ty2:
  --   * It can unify both instantiation variables (possibly with polytypes),
  --     and ordinary unification variables (but only with monotypes)
  --   * It does not return a coercion (unlike unifyType); it is called
  --     for the sole purpose of unifying instantiation variables, although it
  --     may also (opportunistically) unify regular unification variables.
  --   * It never produces errors, even for mis-matched types
  --   * It may return without having made the argument types equal, of course;
  --     it just makes best efforts.
  qlUnify ty1 ty2
    = do { traceTc "qlUnify" (ppr ty1 $$ ppr ty2)
         ; go ty1 ty2 }
    where
      go :: TcType -> TcType
         -> TcM ()
      go (TyVarTy tv) ty2
        | isMetaTyVar tv = go_kappa tv ty2
      go ty1 (TyVarTy tv)
        | isMetaTyVar tv = go_kappa tv ty1
  
      go (CastTy ty1 _) ty2 = go ty1 ty2
      go ty1 (CastTy ty2 _) = go ty1 ty2
  
      go (TyConApp tc1 []) (TyConApp tc2 [])
        | tc1 == tc2 -- See GHC.Tc.Utils.Unify
        = return ()  -- Note [Expanding synonyms during unification]
  
      -- Now, and only now, expand synonyms
      go rho1 rho2
        | Just rho1 <- coreView rho1 = go rho1 rho2
        | Just rho2 <- coreView rho2 = go rho1 rho2
  
      go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
        | tc1 == tc2
        , not (isTypeFamilyTyCon tc1)
        , tys1 `equalLength` tys2
        = zipWithM_ go tys1 tys2
  
      -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
      -- and         (c1 => res1) ~   (c2 => res2)
      -- But for the latter we only learn instantiation info from res1~res2
      -- We look at the multiplicity too, although the chances of getting
      -- impredicative instantiation info from there seems...remote.
      go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
         (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
        | af1 == af2 -- Match the arrow TyCon
        = do { when (isVisibleFunArg af1) (go arg1 arg2)
             ; when (isFUNArg af1)        (go mult1 mult2)
             ; go res1 res2 }
  
      -- ToDo: c.f. Tc.Utils.unify.uType,
      -- which does not split FunTy here
      -- Also NB tcSplitAppTyNoView here, which does not split (c => t)
      go  (AppTy t1a t1b) ty2
        | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2
        = do { go t1a t2a; go t1b t2b }
  
      go ty1 (AppTy t2a t2b)
        | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1
        = do { go t1a t2a; go t1b t2b }
  
      go _ _ = return ()
         -- Don't look under foralls; see (UQL4) of Note [QuickLook unification]
  
      ----------------
      go_kappa kappa ty2
        = assertPpr (isMetaTyVar kappa) (ppr kappa) $
          do { info <- readMetaTyVar kappa
             ; case info of
                 Indirect ty1 -> go ty1 ty2
                 Flexi        -> do { ty2 <- liftZonkM $ zonkTcType ty2
                                    ; go_flexi kappa ty2 } }
  
      ----------------
      -- Swap (kappa1[conc] ~ kappa2[tau])
      -- otherwise we'll fail to unify and emit a coercion.
      -- Just an optimisation: emitting a coercion is fine
      go_flexi kappa (TyVarTy tv2)
        | lhsPriority tv2 > lhsPriority kappa
        = go_flexi1 tv2 (TyVarTy kappa)
      go_flexi kappa ty2
        = go_flexi1 kappa ty2
  
      go_flexi1 kappa ty2  -- ty2 is zonked
        = do { cur_lvl <- getTcLevel
                -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
                -- Here we are in the TcM monad, which does not track enclosing
                -- Given equalities; so for quick-look unification we conservatively
                -- treat /any/ level outside this one as untouchable. Hence cur_lvl.
             ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of
                SUC_CanUnify ->
                  do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
                             -- unifyKind: see (UQL2) in Note [QuickLook unification]
                             --            and (MIV2) in Note [Monomorphise instantiation variables]
                     ; let ty2' = mkCastTy ty2 co
                     ; traceTc "qlUnify:update" $
                       ppr kappa <+> text ":=" <+> ppr ty2
                     ; liftZonkM $ writeMetaTyVar kappa ty2' }
                _ -> return () -- e.g. occurs-check or forall-bound variable
             }
        where
          kappa_kind = tyVarKind kappa
          ty2_kind   = typeKind ty2
  
  {- Note [QuickLook unification]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
  That is the entire point of qlUnify!   Wrinkles:
  
  (UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
    the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`.
    For example that checks for
      * An occurs-check
      * Level mis-match
      * An attempt to unify a concrete type variable with a non-concrete type.
  
  (UQL2) What if kappa and ty have different kinds?  We simply call the
    ordinary unifier and use the coercion to connect the two.
  
    If that coercion is not Refl, it is all in vain: The whole point of
    qlUnify is to impredicatively unify (kappa := forall a. blah). It is
    no good to unify (kappa := (forall a.blah) |> co) because we can't
    use that casted polytype.
  
    BUT: unifyKind has emitted constraint(s) into the Tc monad, so we may as well
    use them.  (An alternative; use uType directly, if the result is not Refl,
    discard the constraints and the coercion, and do not update the instantiation
    variable.  But see "Sadly discarded design alternative" below.)
  
    See also (TCAPP2) in Note [tcApp: typechecking applications].
  
  (UQL3) Instantiation variables don't really have a settled level yet;
    they have level QLInstVar (see Note [The QLInstVar TcLevel] in GHC.Tc.Utils.TcType.
    You might worry that we might unify
        alpha[1] := Maybe kappa[qlinst]
    and later this kappa turns out to be a level-2 variable, and we have committed
    a skolem-escape error.
  
    But happily this can't happen: QL instantiation variables have level infinity,
    and we never unify a variable with a type from a deeper level.
  
  (UQL4) Should we look under foralls in qlUnify? The use-case would be
       (forall a.  beta[qlinst] -> a)  ~  (forall a. (forall b. b->b) -> a)
    where we might hope for
       beta := forall b. b
  
    But in fact we don't attempt this:
  
    * The normal on-the-fly unifier doesn't look under foralls, so why
      should qlUnify?
  
    * Looking under foralls means we'd have to track the bound variables on both
      sides.  Tiresome but not a show stopper.
  
    * We might call the *regular* unifier (via unifyKind) under foralls, and that
      doesn't know about those bound variables (it controls scope through level
      numbers) so it might go totally wrong.  At least we'd have to instantaite
      the forall-types with skolems (with level numbers).  Maybe more.
  
    It's just not worth the trouble, we think (for now at least).
  
  
  Sadly discarded design alternative
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  It is very tempting to use `unifyType` rather than `qlUnify`, killing off the
  latter.  (Extending `unifyType` slightly to allow it to unify an instantiation
  variable with a polytype is easy.).  But I could not see how to make it work:
  
   * `unifyType` makes the types /equal/, and returns a coercion, and it is hard to
     marry that up with DeepSubsumption.  Absent deep subsumption, this approach
     might just work.
  
   * I considered making a wrapper for `uType`, which simply discards any deferred
     equality constraints.  But we can't do that: in a heterogeneous equality we might
     have unified a unification variable (alpha := ty |> co), where `co` is only bound
     by those constraints.
  -}
  
  {- *********************************************************************
  *                                                                      *
                   tagToEnum#
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [tagToEnum#]
  ~~~~~~~~~~~~~~~~~~~~
  Nasty check to ensure that tagToEnum# is applied to a type that is an
  enumeration TyCon.  It's crude, because it relies on our
  knowing *now* that the type is ok, which in turn relies on the
  eager-unification part of the type checker pushing enough information
  here.  In theory the Right Thing to do is to have a new form of
  constraint but I definitely cannot face that!  And it works ok as-is.
  
  Here's are two cases that should fail
          f :: forall a. a
          f = tagToEnum# 0        -- Can't do tagToEnum# at a type variable
  
          g :: Int
          g = tagToEnum# 0        -- Int is not an enumeration
  
  When data type families are involved it's a bit more complicated.
       data family F a
       data instance F [Int] = A | B | C
  Then we want to generate something like
       tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
  Usually that coercion is hidden inside the wrappers for
  constructors of F [Int] but here we have to do it explicitly.
  
  It's all grotesquely complicated.
  -}
  
  isTagToEnum :: HsExpr GhcTc -> Bool
  isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
  isTagToEnum _ = False
  
  tcTagToEnum :: (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc]
              -> TcRhoType
              -> TcM (HsExpr GhcTc)
  -- tagToEnum# :: forall a. Int# -> a
  -- See Note [tagToEnum#]   Urgh!
  tcTagToEnum (tc_fun, fun_ctxt) tc_args res_ty
    | [val_arg] <- dropWhile (not . isHsValArg) tc_args
    = do { res_ty <- liftZonkM $ zonkTcType res_ty
  
         -- Check that the type is algebraic
         ; case tcSplitTyConApp_maybe res_ty of {
             Nothing -> do { addErrTc (TcRnTagToEnumUnspecifiedResTy res_ty)
                           ; vanilla_result } ;
             Just (tc, tc_args) ->
  
      do { -- Look through any type family
         ; fam_envs <- tcGetFamInstEnvs
         ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
             Nothing -> do { check_enumeration res_ty tc
                           ; vanilla_result } ;
             Just (rep_tc, rep_args, coi) ->
  
      do { -- coi :: tc tc_args ~R rep_tc rep_args
           check_enumeration res_ty rep_tc
         ; let rep_ty  = mkTyConApp rep_tc rep_args
               tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
               df_wrap = mkWpCastR (mkSymCo coi)
               tc_expr = rebuildHsApps (tc_fun', fun_ctxt) [val_arg]
         ; return (mkHsWrap df_wrap tc_expr) }}}}}
  
    | otherwise
    = failWithTc TcRnTagToEnumMissingValArg
  
    where
      vanilla_result = return (rebuildHsApps (tc_fun, fun_ctxt) tc_args)
  
      check_enumeration ty' tc
        | -- isTypeDataTyCon: see wrinkle (W1) in
          -- Note [Type data declarations] in GHC.Rename.Module
          isTypeDataTyCon tc    = addErrTc (TcRnTagToEnumResTyTypeData ty')
        | isEnumerationTyCon tc = return ()
        | otherwise             = addErrTc (TcRnTagToEnumResTyNotAnEnum ty')
  
  
  {- *********************************************************************
  *                                                                      *
             Horrible hack for rep-poly unlifted newtypes
  *                                                                      *
  ********************************************************************* -}
  
  {- Note [Eta-expanding rep-poly unlifted newtypes]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Any occurrence of a newtype constructor must appear at a known representation.
  If the newtype is applied to an argument, then we are done: by (I2) in
  Note [Representation polymorphism invariants], the argument has a known
  representation, and we are done. So we are left with the situation of an
  unapplied newtype constructor. For example:
  
    type N :: TYPE r -> TYPE r
    newtype N a = MkN a
  
    ok :: N Int# -> N Int#
    ok = MkN
  
    bad :: forall r (a :: TYPE r). N (# Int, r #) -> N (# Int, r #)
    bad = MkN
  
  The difficulty is that, unlike the situation described in
  Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete,
  it is not necessarily the case that we simply need to check the instantiation
  of a single variable. Consider for example:
  
    type RR :: Type -> Type -> RuntimeRep
    type family RR a b where ...
  
    type T :: forall a -> forall b -> TYPE (RR a b)
    type family T a b where ...
  
    type M :: forall a -> forall b -> TYPE (RR a b)
    newtype M a b = MkM (T a b)
  
  Now, suppose we instantiate MkM, say with two types X, Y from the environment:
  
    foo :: T X Y -> M X Y
    foo = MkM @X @Y
  
  we need to check that we can eta-expand MkM, for which we need to know the
  representation of its argument, which is "RR X Y".
  
  To do this, in "rejectRepPolyNewtypes", we perform a syntactic representation-
  polymorphism check on the instantiated argument of the newtype, and reject
  the definition if the representation isn't concrete (in the sense of Note [Concrete types]
  in GHC.Tc.Utils.Concrete).
  
  For example, we would accept "ok" above, as "IntRep" is a concrete RuntimeRep.
  However, we would reject "foo", because "RR X Y" is not a concrete RuntimeRep.
  If we wanted to accept "foo" (performing a PHASE 2 check (in the sense of
  Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete), we would have to
  significantly re-engineer unlifted newtypes in GHC. Currently, "MkM" has type:
  
    MkM :: forall a b. T a b %1 -> M a b
  
  However, we should only be able to use MkM when we know the representation of
  T a b (which is RR a b). This means that MkM should instead have type:
  
    MkM :: forall {must_be_conc} a b (co :: RR a b ~# must_be_conc)
        .  T a b |> GRefl Nominal (TYPE co) %1 -> M a b
  
  where "must_be_conc" is a skolem type variable that must be instantiated to a
  concrete type, just as in Note [Representation-polymorphism checking built-ins]
  in GHC.Tc.Utils.Concrete. This means that any instantiation of "MkM", such as
  "MkM @X @Y" from "foo", would create a fresh concrete metavariable "gamma[conc]"
  and emit a Wanted constraint
  
    [W] co :: RR X Y ~# gamma[conc]
  
  However, this all seems like a lot of work for a feature that no one is asking for,
  so we decided to keep the much simpler syntactic check. Note that one possible
  advantage of this approach is that we should be able to stop skipping
  representation-polymorphism checks in the output of the desugarer; see (C) in
  Wrinkle [Representation-polymorphic lambdas] in Note [Typechecking data constructors].
  -}
  
  -- | Reject any unsaturated use of an unlifted newtype constructor
  -- if the representation of its argument isn't known.
  --
  -- See Note [Eta-expanding rep-poly unlifted newtypes].
  rejectRepPolyNewtypes :: (HsExpr GhcTc, AppCtxt)
                        -> TcRhoType
                        -> TcM ()
  rejectRepPolyNewtypes (fun,_) app_res_rho = case fun of
  
    XExpr (ConLikeTc (RealDataCon con) _ _)
      -- Check that this is an unsaturated occurrence of a
      -- representation-polymorphic newtype constructor.
      | isNewDataCon con
      , not $ tcHasFixedRuntimeRep $ dataConTyCon con
      , Just (_rem_arg_af, _rem_arg_mult, rem_arg_ty, _nt_res_ty)
          <- splitFunTy_maybe app_res_rho
      -> do { let frr_ctxt = FRRRepPolyUnliftedNewtype con
            ; hasFixedRuntimeRep_syntactic frr_ctxt rem_arg_ty }
  
    _ -> return ()
  
  
  {- *********************************************************************
  *                                                                      *
               Pragmas on expressions
  *                                                                      *
  ********************************************************************* -}
  
  tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
  tcExprPrag (HsPragSCC x1 ann) = HsPragSCC x1 ann
  