Note [Generalising in tcTyFamInstEqnGuts]

Suppose we have something like
  type instance forall (a::k) b. F (Proxy t1) _ = rhs

Then  imp_vars = [k], exp_bndrs = [a::k, b]

We want to quantify over all the free vars of the LHS including
  * any invisible kind variables arising from instantiating tycons,
    such as Proxy
  * wildcards such as '_' above

The wildcards are particularly awkward: they may need to be quantified
  - before the explicit variables k,a,b
  - after them
  - or even interleaved with them
  c.f. Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType

So, we use bindOuterFamEqnTKBndrs (which does not create an implication for
the telescope), and generalise over /all/ the variables in the LHS,
without treating the explicitly-quantified ones specially. Wrinkles:

 - When generalising, include the explicit user-specified forall'd
   variables, so that we get an error from Validity.checkFamPatBinders
   if a forall'd variable is not bound on the LHS

 - We still want to complain about a bad telescope among the user-specified
   variables.  So in checkFamTelescope we emit an implication constraint
   quantifying only over them, purely so that we get a good telescope error.

  - Note that, unlike a type signature like
       f :: forall (a::k). blah
    we do /not/ care about the Inferred/Specified designation or order for
    the final quantified tyvars.  Type-family instances are not invoked
    directly in Haskell source code, so visible type application etc plays
    no role.

See also Note [Re-quantify type variables in rules] in
GHC.Tc.Gen.Sig, which explains a /very/ similar design when
generalising over the type of a rewrite rule.