Note [Quantifying over equality constraints]

Should we quantify over an equality constraint (s ~ t)
in pickQuantifiablePreds?

* It is always /sound/ to quantify over a constraint -- those
  quantified constraints will need to be proved at each call site.

* We definitely don't want to quantify over (Maybe a ~ Bool), to get
     f :: forall a. (Maybe a ~ Bool) => blah
  That simply postpones a type error from the function definition site to
  its call site.  Fortunately we have already filtered out insoluble
  constraints: see `definite_error` in `simplifyInfer`.

* What about (a ~ T alpha b), where we are about to quantify alpha, `a` and
  `b` are in-scope skolems, and `T` is a data type.  It's pretty unlikely
  that this will be soluble at a call site, so we don't quantify over it.

* What about `(F beta ~ Int)` where we are going to quantify `beta`?
  Should we quantify over the (F beta ~ Int), to get
     f :: forall b. (F b ~ Int) => blah
  Aha!  Perhaps yes, because at the call site we will instantiate `b`, and
  perhaps we have `instance F Bool = Int`. So we *do* quantify over a
  type-family equality where the arguments mention the quantified variables.

This is all a bit ad-hoc.


************************************************************************
*                                                                      *
            Invariant checking (debug only)
*                                                                      *
************************************************************************