Note [ApproximateWC]

approximateWC takes a constraint, typically arising from the RHS of a
let-binding whose type we are *inferring*, and extracts from it some *simple*
constraints that we might plausibly abstract over.  Of course the top-level
simple constraints are plausible, but we also float constraints out from inside,
if they are not captured by skolems.

The same function is used when doing type-class defaulting (see the call
to applyDefaultingRules) to extract constraints that might be defaulted.

We proceed by classifying the constraint:
  * ClassPred:
    * Never pick a CallStack constraint.
      See Note [Overview of implicit CallStacks]
    * Always pick an implicit-parameter constraint.
      Note [Inheriting implicit parameters]
    See wrinkle (W2)

  * EqPred: see Note [Quantifying over equality constraints]

  * IrredPred: we allow anything.

  * ForAllPred: never quantify over these

Wrinkle (W1)
  When inferring most-general types (in simplifyInfer), we
  do *not* quantify over equality constraint if the implication binds
  equality constraints, because that defeats the OutsideIn story.
  Consider data T a where { TInt :: T Int; MkT :: T a }
         f TInt = 3::Int
  We get the implication (a ~ Int => res ~ Int), where so far we've decided
     f :: T a -> res
  We don't want to float (res~Int) out because then we'll infer
     f :: T a -> Int
  which is only on of the possible types. (GHC 7.6 accidentally *did*
  float out of such implications, which meant it would happily infer
  non-principal types.)

Wrinkle (W2)
  We do allow /class/ constraints to float, even if the implication binds
  equalities.  This is a subtle point: see #23224.  In principle, a class
  constraint might ultimately be satisfiable from a constraint bound by an
  implication (see #19106 for an example of this kind), but it's extremely
  obscure and I was unable to construct a concrete example.  In any case, in
  super-subtle cases where this might make a difference, you would be much
  better advised to simply write a type signature.

Wrinkle (W3)
  In findDefaultableGroups we are not worried about the most-general type; and
  we /do/ want to float out of equalities (#12797).  Hence we just union the two
  returned lists.

Wrinkle (W4)
  In #26376 we had constraints
    [W] d1 : Functor f[tau:1]
    [W] d2 : Functor p[tau:1]
    [W] d3 : forall a. Functor (p[tau:1]) a   -- A quantified constraint
  We certainly don't want to /quantify/ over d3; but we /do/ want to
  quantify over `p`, so it would be a mistake to make the function monomorphic
  in `p` just because `p` is mentioned in this quantified constraint.

  Happily this problem cannot happen any more.  That quantified constraint `d3`
  dates from a time when we flirted with an all-or-nothing strategy for
  quantified constraints Nowadays we'll never see this: we'll have simplified
  that quantified constraint into a implication constraint.  (Exception:
  SPECIALISE pragmas: see (WFA4) in Note [Solving a Wanted forall-constraint].
  But there we don't use approximateWC.)

Historical note -----------
There used to be a second caveat, driven by #8155

   2. We do not float out an inner constraint that shares a type variable
      (transitively) with one that is trapped by a skolem.  Eg
          forall a.  F a ~ beta, Integral beta
      We don't want to float out (Integral beta).  Doing so would be bad
      when defaulting, because then we'll default beta:=Integer, and that
      makes the error message much worse; we'd get
          Can't solve  F a ~ Integer
      rather than
          Can't solve  Integral (F a)

      Moreover, floating out these "contaminated" constraints doesn't help
      when generalising either. If we generalise over (Integral b), we still
      can't solve the retained implication (forall a. F a ~ b).  Indeed,
      arguably that too would be a harder error to understand.

But this transitive closure stuff gives rise to a complex rule for
when defaulting actually happens, and one that was never documented.
Moreover (#12923), the more complex rule is sometimes NOT what
you want.  So I simply removed the extra code to implement the
contamination stuff.  There was zero effect on the testsuite (not even #8155).
End of historical note -----------