Note [Wanteds rewrite Wanteds]

Should one Wanted constraint be allowed to rewrite another?

This example (along with #8450) suggests not:
   f :: a -> Bool
   f x = ( [x,'c'], [x,True] ) `seq` True
Here we get
  [W] a ~ Char
  [W] a ~ Bool
but we do not want to complain about Bool ~ Char!

This example suggests yes (indexed-types/should_fail/T4093a):
  type family Foo a
  f :: (Foo e ~ Maybe e) => Foo e
In the ambiguity check, we get
  [G] g1 :: Foo e ~ Maybe e
  [W] w1 :: Foo alpha ~ Foo e
  [W] w2 :: Foo alpha ~ Maybe alpha
w1 gets rewritten by the Given to become
  [W] w3 :: Foo alpha ~ Maybe e
Now, the only way to make progress is to allow Wanteds to rewrite Wanteds.
Rewriting w3 with w2 gives us
  [W] w4 :: Maybe alpha ~ Maybe e
which will soon get us to alpha := e and thence to victory.

TL;DR we want equality saturation.

We thus want Wanteds to rewrite Wanteds in order to accept more programs,
but we don't want Wanteds to rewrite Wanteds because doing so can create
inscrutable error messages. To solve this dilemma:

* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds
  it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters
  field of the CtWanted constructor of CtEvidence.  (Only Wanteds have
  RewriterSets.)

* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient
  because only equalities (evidenced by coercion holes) are used for rewriting;
  other (dictionary) constraints cannot ever rewrite.

* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet,
  consisting of the evidence (a CoercionHole) for any Wanted equalities used in
  rewriting.

* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence
  add this RewriterSet to the rewritten constraint's rewriter set.

* We prevent the unifier from unifying any equality with a non-empty rewriter set;
  unification effectively turns a Wanted into a Given, and we lose all tracking.
  See (REWRITERS) in Note [Unification preconditions] in GHC.Tc.Utils.Unify and
  Note [Unify only if the rewriter set is empty] in GHC.Solver.Equality.

* In error reporting, we simply suppress any errors that have been rewritten
  by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
  which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled
  coercion holes. The idea is that we wish to report the "root cause" -- the
  error that rewrote all the others.

* In `selectNextWorkItem`, priorities equalities with no rewiters.  See
  Note [Prioritise Wanteds with empty RewriterSet] in GHC.Tc.Types.Constraint
  wrinkle (PER1).

* In error reporting, we prioritise Wanteds that have an empty RewriterSet:
  see Note [Prioritise Wanteds with empty RewriterSet].

Let's continue our first example above:

  inert: [W] w1 :: a ~ Char
  work:  [W] w2 :: a ~ Bool

Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding

  inert: [W] w1 :: a ~ Char
         [W] w2 {w1}:: Char ~ Bool

The {w1} in the second line of output is the RewriterSet of w1.

Wrinkles:

(WRW1) When we find a constraint identical to one already in the inert set,
   we solve one from the other. Other things being equal, keep the one
   that has fewer (better still no) rewriters.
   See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality.

   To this accurately we should use `zonkRewriterSet` during canonicalisation,
   to eliminate rewriters that have now been solved.  Currently we only do so
   during error reporting; but perhaps we should change that.

(WRW2) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take
   the opportunity to zonk its `RewriterSet`, which eliminates solved ones.
   This doesn't guarantee that rewriter sets are always up to date -- see
   (WRW1) -- but it helps, and it de-clutters debug output.