Note [Let-bound skolems]

If   * the inert set contains a canonical Given CEqCan (a ~ ty)
and  * 'a' is a skolem bound in this very implication,

then:
   a) The Given is pretty much a let-binding, like
         f :: (a ~ b->c) => a -> a
      Here the equality constraint is like saying
         let a = b->c in ...
      It is not adding any new, local equality  information,
      and hence can be ignored by has_given_eqs

   b) 'a' will have been completely substituted out in the inert set,
      so we can safely discard it.

For an example, see #9211.

The actual test is in `isLetBoundSkolemCt`

Wrinkles:

(LBS1) See GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
       that the correct variable is on the left of the equality when both are
       tyvars.

(LBS2) We also want this to work for
            forall a. [G] F b ~ a   (CEqCt with TyFamLHS)
   Here the Given will have a TyFamLHS, with the skolem-bound tyvar on the RHS.
   See tests T24938a, and LocalGivenEqs.

(LBS3) Happily (LBS2) also makes cycle-breakers work. Suppose we have
            forall a. [G] (F a) Int ~ a
  where F has arity 1, and `a` is the locally-bound skolem.  Then, as
  Note [Type equality cycles] explains, we split into
           [G] F a ~ cbv, [G] cbv Int ~ a
  where `cbv` is the cycle breaker variable.  But cbv has the same level
  as `a`, so `isOuterTyVar` (called in `isLetBoundSkolemCt`) will return False.

  This actually matters occasionally: see test LocalGivenEqs.

You might wonder whether the skolem really needs to be bound "in the
very same implication" as the equality constraint.
Consider this (c.f. #15009):

  data S a where
    MkS :: (a ~ Int) => S a

  g :: forall a. S a -> a -> blah
  g x y = let h = \z. ( z :: Int
                      , case x of
                           MkS -> [y,z])
          in ...

From the type signature for `g`, we get `y::a` .  Then when we
encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
body of the lambda we'll get

  [W] alpha[1] ~ Int                             -- From z::Int
  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]

Now, unify alpha := a.  Now we are stuck with an unsolved alpha~Int!
So we must treat alpha as untouchable under the forall[2] implication.

Possible future improvements.  The current test just looks to see whether one
side of an equality is a locally-bound skolem.  But actually we could, in
theory, do better: if one side (or both sides, actually) of an equality
ineluctably mentions a local skolem, then the equality cannot possibly impact
types outside of the implication (because doing to would cause those types to be
ill-scoped). The problem is the "ineluctably": this means that no expansion,
other solving, etc., could possibly get rid of the variable. This is hard,
perhaps impossible, to know for sure, especially when we think about type family
interactions. (And it's a user-visible property so we don't want it to be hard
to predict.) So we keep the existing check, looking for one lone variable,
because we're sure that variable isn't going anywhere.