Note [The Purely Kinded Type Invariant (PKTI)]

During type inference, we maintain this invariant

 (PKTI) It is legal to call 'typeKind' on any Type ty,
        on any sub-term of ty, /without/ zonking ty

        Moreover, any such returned kind
        will itself satisfy (PKTI)

By "legal to call typeKind" we mean "typeKind will not crash".
The way in which typeKind can crash is in applications
    (a t1 t2 .. tn)
if 'a' is a type variable whose kind doesn't have enough arrows
or foralls.  (The crash is in piResultTys.)

The loop in tcInferTyApps has to be very careful to maintain the (PKTI).
For example, suppose
    kappa is a unification variable
    We have already unified kappa := Type
      yielding    co :: Refl (Type -> Type)
    a :: kappa
then consider the type
    (a Int)
If we call typeKind on that, we'll crash, because the (un-zonked)
kind of 'a' is just kappa, not an arrow kind.  So we must zonk first.

So the type inference engine is very careful when building applications.
This happens in tcInferTyApps. Suppose we are kind-checking the type (a Int),
where (a :: kappa).  Then in tcInferApps we'll run out of binders on
a's kind, so we'll call matchExpectedFunKind, and unify
   kappa := kappa1 -> kappa2,  with evidence co :: kappa ~ (kappa1 ~ kappa2)
At this point we must zonk the function type to expose the arrrow, so
that (a Int) will satisfy (PKTI).

The absence of this caused #14174 and #14520.

The calls to mkAppTyM is the other place we are very careful; see Note [mkAppTyM].

Wrinkle around FunTy:
Note that the PKTI does *not* guarantee anything about the shape of FunTys.
Specifically, when we have (FunTy vis mult arg res), it should be the case
that arg :: TYPE rr1 and res :: TYPE rr2, for some rr1 and rr2. However, we
might not have this. Example: if the user writes (a -> b), then we might
invent a :: kappa1 and b :: kappa2. We soon will check whether kappa1 ~ TYPE rho1
(for some rho1), and that will lead to kappa1 := TYPE rho1 (ditto for kappa2).
However, when we build the FunTy, we might not have zonked `a`, and so the
FunTy will be built without being able to purely extract the RuntimeReps.

Because the PKTI does not guarantee that the RuntimeReps are available in a FunTy,
we must be aware of this when splitting: splitTyConApp and splitAppTy will *not*
split a FunTy if the RuntimeReps are not available. See also Note [Decomposing FunTy]
in GHC.Tc.Solver.Equality.