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.