The main job of this commit is to track more accurately the scope
of tyvars introduced by user-written foralls. For example, it would
be to have something like this:

  forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool

In that type, a's kind must be k, but k isn't in scope. We had a
terrible way of doing this before (not worth repeating or describing
here, but see the old tcImplicitTKBndrs and friends), but now
we have a principled approach: make an Implication when kind-checking
a forall. Doing so then hooks into the existing machinery for
preventing skolem-escape, performing floating, etc. This also means
that we bump the TcLevel whenever going into a forall.

The new behavior is done in TcHsType.scopeTyVars, but see also
TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
rewriting. There are several Notes near there to guide you. Of
particular interest there is that Implication constraints can now
have skolems that are out of order; th...