Note [Avoiding rewriting cycles]

Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet describes
the can-rewrite relation among CtFlavour/Role pairs, saying which constraints
can rewrite which other constraints. It puts forth (R2):
  (R2) If f1 >= f, and f2 >= f,
       then either f1 >= f2 or f2 >= f1
The naive can-rewrite relation says that (Given, Representational) can rewrite
(Wanted, Representational) and that (Wanted, Nominal) can rewrite
(Wanted, Representational), but neither of (Given, Representational) and
(Wanted, Nominal) can rewrite the other. This would violate (R2). See also
Note [Why R2?] in GHC.Tc.Solver.InertSet.

To keep R2, we do not allow (Wanted, Nominal) to rewrite (Wanted, Representational).
This can, in theory, bite, in this scenario:

  type family F a
  data T a
  type role T nominal

  [G] F a ~N T a
  [W] F alpha ~N T alpha
  [W] F alpha ~R T a

As written, this makes no progress, and GHC errors. But, if we
allowed W/N to rewrite W/R, the first W could rewrite the second:

  [G] F a ~N T a
  [W] F alpha ~N T alpha
  [W] T alpha ~R T a

Now we decompose the second W to get

  [W] alpha ~N a

noting the role annotation on T. This causes (alpha := a), and then
everything else unlocks.

What to do? We could "decompose" nominal equalities into nominal-only
("NO") equalities and representational ones, where a NO equality rewrites
only nominals. That is, when considering whether [W] F alpha ~N T alpha
should rewrite [W] F alpha ~R T a, we could require splitting the first W
into [W] F alpha ~NO T alpha, [W] F alpha ~R T alpha. Then, we use the R
half of the split to rewrite the second W, and off we go. This splitting
would allow the split-off R equality to be rewritten by other equalities,
thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.InertSet.

However, note that I said that this bites in theory. That's because no
known program actually gives rise to this scenario. A direct encoding
ends up starting with

  [G] F a ~ T a
  [W] F alpha ~ T alpha
  [W] Coercible (F alpha) (T a)

where ~ and Coercible denote lifted class constraints. The ~s quickly
reduce to ~N: good. But the Coercible constraint gets rewritten to

  [W] Coercible (T alpha) (T a)

by the first Wanted. This is because Coercible is a class, and arguments
in class constraints use *nominal* rewriting, not the representational
rewriting that is restricted due to (R2). Note that reordering the code
doesn't help, because equalities (including lifted ones) are prioritized
over Coercible. Thus, I (Richard E.) see no way to write a program that
is rejected because of this infelicity. I have not proved it impossible,
exactly, but my usual tricks have not yielded results.

In the olden days, when we had Derived constraints, this Note was all
about G/R and D/N both rewriting D/R. Back then, the code in
typecheck/should_compile/T19665 really did get rejected. But now,
according to the rewriting of the Coercible constraint, the program
is accepted.