Note [Checking telescopes]

When kind-checking a /user-written/ type, we might have a "bad telescope"
like this one:
  data SameKind :: forall k. k -> k -> Type
  type Foo :: forall a k (b :: k). SameKind a b -> Type

The kind of 'a' mentions 'k' which is bound after 'a'.  Oops.

One approach to doing this would be to bring each of a, k, and b into
scope, one at a time, creating a separate implication constraint for
each one, and bumping the TcLevel. This would work, because the kind
of, say, a would be untouchable when k is in scope (and the constraint
couldn't float out because k blocks it). However, it leads to terrible
error messages, complaining about skolem escape. While it is indeed a
problem of skolem escape, we can do better.

Instead, our approach is to bring the block of variables into scope
all at once, creating one implication constraint for the lot:

* We make a single implication constraint when kind-checking
  the 'forall' in Foo's kind, something like
      forall a k (b::k). { wanted constraints }

* Having solved {wanted}, before discarding the now-solved implication,
  the constraint solver checks the dependency order of the skolem
  variables (ic_skols).  This is done in setImplicationStatus.

* This check is only necessary if the implication was born from a
  'forall' in a user-written signature (the HsForAllTy case in
  GHC.Tc.Gen.HsType.  If, say, it comes from checking a pattern match
  that binds existentials, where the type of the data constructor is
  known to be valid (it in tcConPat), no need for the check.

  So the check is done /if and only if/ ic_info is ForAllSkol.

* If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the
  original, user-written type variables.

* Be careful /NOT/ to discard an implication with a ForAllSkol
  ic_info, even if ic_wanted is empty.  We must give the
  constraint solver a chance to make that bad-telescope test!  Hence
  the extra guard in emitResidualTvConstraint; see #16247

* Don't mix up inferred and explicit variables in the same implication
  constraint.  E.g.
      foo :: forall a kx (b :: kx). SameKind a b
  We want an implication
      Implic { ic_skol = [(a::kx), kx, (b::kx)], ... }
  but GHC will attempt to quantify over kx, since it is free in (a::kx),
  and it's hopelessly confusing to report an error about quantified
  variables   kx (a::kx) kx (b::kx).
  Instead, the outer quantification over kx should be in a separate
  implication. TL;DR: an explicit forall should generate an implication
  quantified only over those explicitly quantified variables.