Note [The Core unifier]

This module contains the (pure) unifier two types.  It is subtle in a number
of ways.  Here we summarise, but see Note [Specification of unification].

(CU1) It creates a substition only for "bindable" or "template" type variables.
  These are identified by a `um_bind_tv_fun` function passed down in the `UMEnv`
  environment.

(CU2) We want to match in the presence of foralls;
        e.g     (forall a. t1) ~ (forall b. t2)
   That is what the `um_rn_env :: RnEnv2` field of `UMEnv` is for; it does the
   alpha-renaming that makes it as if `a` and `b` were the same variable.
   Initialising the `RnEnv2`, so that it can generate a fresh binder when
   necessary, entails knowing the free variables of both types.

   Of course, we must be careful not to bind a template type variable to a
   locally bound variable.  E.g.
        (forall a. x) ~ (forall b. b)
   where `x` is the template type variable.  Then we do not want to
   bind `x` to a/b!  See `mentionsForAllBoundTyVarsL/R`.

(CU3) We want to take special care for type families.
  See the big Note [Apartness and type families]

(CU4) Rather than returning just "unifiable" or "not-unifiable" we do "fine-grained"
  unification (hence "fg" or "FG" in this module) returning three possiblities,
  captured in `UnifyResult`:
    - Unifiable subst : certainly unifiable with this type substitution
    - SurelyApart     : cannot be unifiable, regardless of how type familes reduce
    - MaybeApart      : neither of the above
  See Note [Unification result].

  Four reasons for MaybeApart (see `MaybeApartReason`).  The first two are the
  big ones!
    * MARTypeFamily:
         Family reduction might make the two types equal
             Maybe (F Int) ~ Maybe Bool
         See Note [Apartness and type families]
    * MARInfinite (occurs check):
         See Note [Infinitary substitutions]
    * MARTypeVsConstraint:
         See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
    * MARCast (obscure):
         See (KCU2) in Note [Kind coercions in Unify]

(CU5) We need to take care with kinds.  See Note [tcMatchTy vs tcMatchTyKi]

(CU6) The "unifier" can also do /matching/, governed by `um_unif :: AmIUnifying`.
   When matching, the LHS and RHS namespaces are unrelated. In particular, the
   bindable type variable can occur (unrelatedly) in the RHS.  E.g.
        match  (a,Maybe a) ~  ([a], Maybe [a])
   We get the substitution [a :-> [a]], without confusing the
   LHS `a` with the RHS `a`.  The substitition is "one-shot", and should not be
   iterated.