Note [GivenInv]

Invariant (GivenInv) is not essential, but it is easy to guarantee, and
it is a useful extra piece of structure.  It ensures that the Givens of
an implication don't change because of unifications /at the same level/
caused by Wanteds.  (Wanteds can also cause unifications at an outer
level, but that will iterate the entire implication; see GHC.Tc.Solver.Monad
Note [The Unification Level Flag].)

Givens can certainly contain meta-tyvars from /outer/ levels.  E.g.
   data T a where
     MkT :: Eq a => a -> MkT a

   f x = case x of MkT y -> y && True

Then we'll infer (x :: T alpha[1]).  The Givens from the implication
arising from the pattern match will look like this:

   forall[2] . Eq alpha[1] => (alpha[1] ~ Bool)

But if we unify alpha (which in this case we will), we'll iterate
the entire implication via Note [The Unification Level Flag] in
GHC.Tc.Solver.Monad.  That isn't true of unifications at the /ambient/
level.

It would be entirely possible to weaken (GivenInv), to LESS THAN OR
EQUAL TO, but we'd need to think carefully about
  - kick-out for Givens
  - GHC.Tc.Solver.Monad.isOuterTyVar
But in fact (GivenInv) is automatically true, so we're adhering to
it for now.  See #18929.

* If a tyvar tv has level n, then the levels of all variables free
  in tv's kind are <= n. Consequence: if tv is untouchable, so are
  all variables in tv's kind.