Note [RULE quantification over equalities]

At the moment a RULE never quantifies over an equality; see `rule_quant_ct`
in `getRuleQuantCts`.  Why not?

 * It's not clear why we would want to do so (see Historical Note
   below)

 * We do not want to quantify over insoluble equalities (Int ~ Bool)
    (a) because we prefer to report a LHS type error
    (b) because if such things end up in 'givens' we get a bogus
        "inaccessible code" error

 * Matching on coercions is Deeply Suspicious.  We don't want to generate a
   RULE like
         forall a (co :: F a ~ Int).
                foo (x |> Sym co) = ...co...
   because matching on that template, to bind `co`, would require us to
   match on the /structure/ of a coercion, which we must never do.
   See GHC.Core.Rules Note [Casts in the template]

 * Equality constraints are unboxed, and that leads to complications
   For example equality constraints from the LHS will emit coercion hole
   Wanteds.  These don't have a name, so we can't quantify over them directly.
   Instead, in `getRuleQuantCts`, we'd have to invent a new EvVar for the
   coercion, fill the hole with the invented EvVar, and then quantify over the
   EvVar. Here is old code from `mk_one`
         do { ev_id <- newEvVar pred
            ; fillCoercionHole hole (mkCoVarCo ev_id)
            ; return ev_id }
    But that led to new complications becuase of the side effect on the coercion
    hole. Much easier just to side-step the issue entirely by not quantifying over
    equalities.

Historical Note:
  Back in 2012 (5aa1ae24567) we started quantifying over some equality
  constraints, saying
   * But we do want to quantify over things like (a ~ F b),
     where F is a type function.
  It is not clear /why/ we did so, and we don't do so any longer.
End of historical note.