Note [Tracking Given equalities]

For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
Note [Unification preconditions], we can't unify
   alpha[2] ~ Int
under a level-4 implication if there are any Given equalities
bound by the implications at level 3 of 4.  To that end, the
InertCans tracks

  inert_given_eq_lvl :: TcLevel
     The TcLevel of the innermost implication that has a Given
     equality of the sort that make a unification variable untouchable
     (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).

We update inert_given_eq_lvl whenever we add a Given to the
inert set, in updGivenEqs.

Then a unification variable alpha[n] is untouchable iff
    n < inert_given_eq_lvl
that is, if the unification variable was born outside an
enclosing Given equality.

Exactly which constraints should trigger (UNTOUCHABLE), and hence
should update inert_given_eq_lvl?

(TGE1) We do /not/ need to worry about let-bound skolems, such as
     forall[2] a. a ~ [b] => blah
  See Note [Let-bound skolems] and the isOuterTyVar tests in `updGivenEqs`

(TGE2) However, solely to support better error messages (see Note [HasGivenEqs] in
   GHC.Tc.Types.Constraint) we also track these "local" equalities in the
   boolean inert_given_eqs field.  This field is used only subsequntly (see
   `getHasGivenEqs`), to set the ic_given_eqs field to LocalGivenEqs.

(TGE3) Consider an implication
      forall[2]. beta[1] => alpha[1] ~ Int
  where beta is a unification variable that has already been unified
  to () in an outer scope.  Then alpha[1] is perfectly touchable and
  we can unify alpha := Int. So when deciding whether the givens contain
  an equality, we should canonicalise first, rather than just looking at
  the /original/ givens (#8644).

(TGE4) However, we must take account of *potential* equalities. Consider the
   same example again, but this time we have /not/ yet unified beta:
      forall[2] beta[1] => ...blah...

   Because beta might turn into an equality, updGivenEqs conservatively
   treats it as a potential equality, and updates inert_give_eq_lvl

(TGE5) We should not look at the equality relation involved (nominal vs
   representational), because representational equalities can still
   imply nominal ones. For example, if (G a ~R G b) and G's argument's
   role is nominal, then we can deduce a ~N b.

(TGE6) A subtle point is this: when initialising the solver, giving it
   an empty InertSet, we must conservatively initialise `inert_given_lvl`
   to the /current/ TcLevel.  This matters when doing let-generalisation.
   Consider #26004:
      f w e = case e of
                  T1 -> let y = not w in False   -- T1 is a GADT
                  T2 -> True
   When let-generalising `y`, we will have (w :: alpha[1]) in the type
   envt; and we are under GADT pattern match.  So when we solve the
   constraints from y's RHS, in simplifyInfer, we must NOT unify
       alpha[1] := Bool
   Since we don't know what enclosing equalities there are, we just
   conservatively assume that there are some.

   This initialisation in done in `runTcSWithEvBinds`, which passes
   the current TcLevel to `emptyInertSet`.

Historical note: prior to #24938 we also ignored Given equalities that
did not mention an "outer" type variable.  But that is wrong, as #24938
showed. Another example is immortalised in test LocalGivenEqs2
   data T where
      MkT :: F a ~ G b => a -> b -> T
   f (MkT _ _) = True
We should not infer the type for `f`; let-bound-skolems does not apply.