Note [Weird typing rule for ForAllTy]

Here is the (truncated) typing rule for the dependent ForAllTy:

  inner : TYPE r
  tyvar is not free in r
  
  ForAllTy (Bndr tyvar vis) inner : TYPE r

Note that the kind of `inner` is the kind of the overall ForAllTy. This is
necessary because every ForAllTy over a type variable is erased at runtime.
Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in
the kind) must be the same as the representation of the body. We must check
for skolem-escape, though. The skolem-escape would prevent a definition like

  undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a

because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real
type of undefined is

  undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a

and that HasCallStack constraint neatly sidesteps the potential skolem-escape
problem.

If the bound variable is a coercion variable:

  inner : TYPE r
  covar is free in inner
  
  ForAllTy (Bndr covar vis) inner : Type

Here, the kind of the ForAllTy is just Type, because coercion abstractions
are *not* erased. The "covar is free in inner" premise is solely to maintain
the representation invariant documented in
Note [Unused coercion variable in ForAllTy]. Though there is surface similarity
between this free-var check and the one in the tyvar rule, these two restrictions
are truly unrelated.