Note [Promotion and level-checking]

"Promotion" happens when we have this:

  [W] w1: alpha[2] ~ Maybe beta[4]

Here we must NOT unify alpha := Maybe beta, because beta may turn out
to stand for a type involving some inner skolem.  Yikes!
Skolem-escape.  So instead we /promote/ beta, like this:

  beta[4] := beta'[2]
  [W] w1: alpha[2] ~ Maybe beta'[2]

Now we can unify alpha := Maybe beta', which might unlock other
constraints.  But if some other constraint wants to unify beta with a
nested skolem, it'll get stuck with a skolem-escape error.

Now consider `w2` where a type family is involved (#22194):

  [W] w2: alpha[2] ~ Maybe (F gamma beta[4])

In `w2`, it may or may not be the case that `beta` is level 2; suppose
we later discover gamma := Int, and type instance F Int _ = Int.
So, instead, we promote the entire funcion call:

  [W] w2': alpha[2] ~ Maybe gamma[2]
  [W] w3:  gamma[2] ~ F gamma beta[4]

Now we can unify alpha := Maybe gamma, which is a Good Thng.

Wrinkle (W1)

There is an important wrinkle: /all this only applies when unifying/.
For example, suppose we have
 [G] a[2] ~ Maybe b[4]
where 'a' is a skolem.  This Given might arise from a GADT match, and
we can absolutely use it to rewrite locally. In fact we must do so:
that is how we exploit local knowledge about the outer skolem a[2].
This applies equally for a Wanted [W] a[2] ~ Maybe b[4]. Using it for
local rewriting is fine. (It's not clear to me that it is /useful/,
but it's fine anyway.)

So we only do the level-check in checkTyVar when /unifying/ not for
skolems (or untouchable unification variables).