Note [Shortcomings of the apartness test]

Note [Apartness and type families] is very clever.

But it still has shortcomings (#26358).  Consider unifying
    [F a, F Int, Int]  ~  [Bool, Char, a]
Working left to right you might think we would build the mapping
  F a   :-> Bool
  F Int :-> Char
Now we discover that `a` unifies with `Int`. So really these two lists are Apart
because F Int can't be both Bool and Char.

Just the same applies when adding a type-family binding to um_fam_env:
  [F (G Float), F Int, G Float] ~ [Bool, Char, Iont]
Again these are Apart, because (G Float = Int),
and (F Int) can't be both Bool and Char

But achieving this is very tricky! Perhaps whenever we unify a type variable,
or a type family, we should run it over the domain and (maybe range) of the
type-family mapping too?  Sigh.

For now we make no such attempt.
* The um_fam_env has only /un-substituted/ types.
* We look up only /un-substituted/ types in um_fam_env

This may make us say MaybeApart when we could say SurelyApart, but it has no
effect on the correctness of unification: if we return Unifiable, it really is
Unifiable.

This is all quite subtle. suppose we have:
    um_tv_env:   c :-> b
    um_fam_env   F b :-> a
and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will
fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq,
getting:
    um_tv_env:   a :-> F c, c :-> b
    um_fam_env   F b :-> a

Does that loop, like this:
   a --> F c --> F b --> a?
No, because we do not substitute (F c) to (F b) and then look up in um_fam_env;
we look up only un-substituted types.