Note [Skolem escape and forall-types]

See also Note [Checking telescopes].

Consider
  f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()

The Proxy '[a,b] forces a and b to have the same kind.  But a's
kind must be bound outside the 'forall a', and hence escapes.
We discover this by building an implication constraint for
each forall.  So the inner implication constraint will look like
    forall kb (b::kb).  kb ~ ka
where ka is a's kind.  We can't unify these two, /even/ if ka is
unification variable, because it would be untouchable inside
this inner implication.

That's what the pushLevelAndCaptureConstraints, plus subsequent
buildTvImplication/emitImplication is all about, when kind-checking
HsForAllTy.

Note that

* We don't need to /simplify/ the constraints here
  because we aren't generalising. We just capture them.

* We can't use emitResidualTvConstraint, because that has a fast-path
  for empty constraints.  We can't take that fast path here, because
  we must do the bad-telescope check even if there are no inner wanted
  constraints. See Note [Checking telescopes] in
  GHC.Tc.Types.Constraint.  Lacking this check led to #16247.