Note [Infinitary substitution in lookup]

Consider

  class C a b
  instance C c c
  instance C d (Maybe d)
  [W] C e (Maybe e)

You would think we could just use the second instance, because the first doesn't
unify. But that's just ever so slightly wrong. The reason we check for unifiers
along with matchers is that we don't want the possibility that a type variable
instantiation could cause an instance choice to change. Yet if we have
  type family M = Maybe M
and choose (e |-> M), then both instances match. This is absurd, but we cannot
rule it out. Yet, worrying about this case is awfully inconvenient to users,
and so we pretend the problem doesn't exist, by considering a lookup that runs into
this occurs-check issue to indicate that an instance surely does not apply (i.e.
is like the SurelyApart case). In the brief time that we didn't treat infinitary
substitutions specially, two tickets were filed: #19044 and #19052, both trying
to do Real Work.

Why don't we just exclude any instances that are MaybeApart? Because we might
have a [W] C e (F e), where F is a type family. The second instance above does
not match, but it should be included as a future possibility. Unification will
return MaybeApart MARTypeFamily in this case.

What can go wrong with this design choice? We might get incoherence -- but not
loss of type safety. In particular, if we have [W] C M M (for the M type family
above), then GHC might arbitrarily choose either instance, depending on how
M reduces (or doesn't).

For type families, we can't just ignore the problem (as we essentially do here),
because doing so would give us a hole in the type safety proof (as explored in
Section 6 of "Closed Type Families with Overlapping Equations", POPL'14). This
possibility of an infinitary substitution manifests as closed type families that
look like they should reduce, but don't. Users complain: #9082 and #17311. For
open type families, we actually can have unsoundness if we don't take infinitary
substitutions into account: #8162. But, luckily, for class instances, we just
risk coherence -- not great, but it seems better to give users what they likely
want. (Also, note that this problem existed for the entire decade of 201x without
anyone noticing, so it's manifestly not ruining anyone's day.)