Note [Apartness and type families]

Consider this:

  type family F a b where
    F Int Bool = Char
    F a   b    = Double
  type family G a         -- open, no instances

How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't
match immediately while the second equation does. But, before reducing, we must
make sure that the target can never become (F Int Bool). Well, no matter what G
Float becomes, it certainly won't become *both* Int and Bool, so indeed we're
safe reducing (F (G Float) (G Float)) to Double.

So we must say that the argument list
     (G Float) (G Float)   is SurelyApart from   Int Bool

This is necessary not only to get more reductions (which we might be willing to
give up on), but for /substitutivity/. If we have (F x x), we can see that (F x x)
can reduce to Double. So, it had better be the case that (F blah blah) can
reduce to Double, no matter what (blah) is!

To achieve this, `go` in `uVarOrFam` does this;

* We maintain /two/ substitutions, not just one:
     * um_tv_env: the regular substitution, mapping TyVar :-> Type
     * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application
  In effect, these constitute one substitution mapping
     CanEqLHS :-> Types

* When we attempt to unify (G Float) ~ Int, we return MaybeApart..
  but we /also/ add a "family substitution" [G Float :-> Int],
  to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.

* When we later encounter (G Float) ~ Bool, we apply the family substitution,
  very much as we apply the conventional [tyvar :-> type] substitution
  when we encounter a type variable.  See the `lookupFamEnv` in `go` in
  `uVarOrFam`.

  So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart.  Bingo.


Wrinkles

(ATF0) Once we encounter a type-family application, we only ever return
             MaybeApart   or   SurelyApart
  but never `Unifiable`.  Accordingly, we only return a TyCoVar substitution
  from `tcUnifyTys` and friends; we don't return a type-family substitution as
  well.  (We could imagine doing so, though.)

(ATF1) Exactly the same mechanism is used in class-instance checking.
    If we have
        instance C (Maybe b)
        instance {-# OVERLAPPING #