Note [Unification result]

See `UnifyResult` and `UnifyResultM`.  When unifying t1 ~ t2, we return
* Unifiable s, if s is a substitution such that s(t1) is syntactically the
  same as s(t2), modulo type-synonym expansion.
* SurelyApart, if there is no substitution s such that s(t1) = s(t2),
  where "=" includes type-family reductions.
* MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.

Examples
* [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify

* [(a,Int)] ~ [(Bool,b)]:  Unifiable

* [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool
                    (the unifier does not try this)

* a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart
    either; consider
       a := Loop
       where  type family Loop where Loop = Maybe Loop

Wrinkle (UR1): see `combineMAR`
   There is the possibility that two types are MaybeApart for *both* reasons:

   * (a, F Int) ~ (Maybe a, Bool)

   What reason should we use? The *only* consumer of the reason is described
   in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
   there is identify which instances might match a target later (but don't
   match now) -- except that we want to ignore the possibility of infinitary
   substitutions. So let's examine a concrete scenario:

     class C a b c
     instance C a (Maybe a) Bool
     other instances, including one that will actually match
     [W] C b b (F Int)

   Do we want the instance as a future possibility? No. The only way that
   instance can match is in the presence of an infinite type (infinitely nested
   Maybes). We thus say that `MARInfinite` takes precedence, so that InstEnv treats
   this case as an infinitary substitution case; the fact that a type family is
   involved is only incidental. We thus define `combineMAR` to prefer
   `MARInfinite`.