Note [Solving equality classes]

Consider (~), which behaves as if it was defined like this:
  class a ~# b => a ~ b
  instance a ~# b => a ~ b
There are two more similar "equality classes" like this.  The full list is
  * (~)         eqTyCon
  * (~~)        heqTyCon
  * Coercible   coercibleTyCon
(See Note [The equality types story] in GHC.Builtin.Types.Prim.)

(EQC1) For Givens, when expanding the superclasses of a equality class,
  we can /replace/ the constraint with its superclasses (which, remember, are
  equally powerful) rather than /adding/ them. This can make a huge difference.
  Consider T17836, which has a constraint like
      forall b,c. a ~ (b,c) =>
        forall d,e. c ~ (d,e) =>
          ...etc...
  If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put
  [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c).  That will
  kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does
  no good to anyone.  When the implication is deeply nested, this has
  quadratic cost, and no benefit.  Just replace!

  (This can have a /big/ effect: test T17836 involves deeply-nested GADT
  pattern matching. Its compile-time allocation decreased by 40% when
  I added the "replace" rather than "add" semantics.)

  We achieve this by
   (a) not expanding superclasses for equality classes at all;
       see the `isEqualityClass` test in `mk_strict_superclasses`
   (b) special logic to solve (t1 ~ t2) in `solveEqualityDict`.

(EQC2) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,
  without worrying about Note [Instance and Given overlap].  Why?  Because
  if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and
  so the reduction of the [W] constraint does not risk losing any solutions.

  On the other hand, it can be fatal to /fail/ to reduce such equalities
  on the grounds of Note [Instance and Given overlap], because many good
  things flow from [W] t1 ~# t2.

Conclusion: we have a special solver pipeline for equality-class constraints,
`solveEqualityDict`.  It aggressively decomposes the boxed equality constraint
into an unboxed coercion, both for Givens and Wanteds, and /replaces/ the
boxed equality constraint with the unboxed one, so that the inert set never
contains the boxed one.