Note [Combining equalities]

Suppose we have
   Inert:     g1 :: a ~ t
   Work item: g2 :: a ~ t

Then we can simply solve g2 from g1, thus g2 := g1.  Easy!
But it's not so simple:

(CE1) If t is a type variable, the equalties might be oriented differently:
      e.g. (g1 :: a~b) and (g2 :: b~a)
  So we look both ways round.  Hence the SwapFlag result to
  inertsCanDischarge.

(CE2) We can only do g2 := g1 if g1 can discharge g2; that depends on
  (a) the role and (b) the flavour.  E.g. a representational equality
  cannot discharge a nominal one; a Wanted cannot discharge a Given.
  The predicate is eqCanRewriteFR.

(CE3) Visibility. Suppose  S :: forall k. k -> Type, and consider unifying
      S @Type (a::Type)  ~   S @(Type->Type) (b::Type->Type)
  From the first argument we get (Type ~ Type->Type); from the second
  argument we get (a ~ b) which in turn gives (Type ~ Type->Type).
  See typecheck/should_fail/T16204c.

  That first argument is invisible in the source program (aside from
  visible type application), so we'd much prefer to get the error from
  the second. We track visibility in the uo_visible field of a TypeEqOrigin.
  We use this to prioritise visible errors (see GHC.Tc.Errors.tryReporters,
  the partition on isVisibleOrigin).

  So when combining two otherwise-identical equalites, we want to
  keep the visible one, and discharge the invisible one.  Hence the
  call to strictly_more_visible.

(CE4) Suppose we have this set up (#25440):
   Inert:     [W] g1: F a ~ a Int    (arising from (F a ~ a Int)
   Work item: [W] g2: F alpha ~ F a  (arising from (F alpha ~ F a)
   We rewrite g2 with g1, to give
              [W] g2{rw:g1} : F alpha ~ a Int
   Now if F is injective we can get [W] alpha~a, and hence alpha:=a, and
   we kick out g1. Now we have two constraints
       [W] g1        : F a ~ a Int  (arising from (F a ~ a Int)
       [W] g2{rw:g1} : F a ~ a Int  (arising from (F alpha ~ F a)
   If we end up with g2 in the inert set (not g1) we'll get a very confusing
   error message that we can solve (F a ~ a Int)
       arising from F a ~ F a

   TL;DR: Better to hang on to `g1` (with no rewriters), in preference
   to `g2` (which has a rewriter).

   See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.