Note [Kind coercions in Unify]

We wish to match/unify while ignoring casts. But, we can't just ignore
them completely, or we'll end up with ill-kinded substitutions. For example,
say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
return [a |-> ty], but `a` and `ty` might have different kinds. We can't
just match/unify their kinds, either, because this might gratuitously
fail. After all, `co` is the witness that the kinds are the same -- they
may look nothing alike.

So, we pass a kind coercion `kco` to the main `unify_ty`. This coercion witnesses
the equality between the substed kind of the left-hand type and the substed
kind of the right-hand type. Note that we do not unify kinds at the leaves
(as we did previously).

Hence: (UKINV) Unification Kind Invariant
* In the call
     unify_ty ty1 ty2 kco
  it must be that
     subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2))
  where `subst` is the ambient substitution in the UM monad
* In the call
     unify_tys tys1 tys2
  (which has no kco), after we unify any prefix of tys1,tys2, the kinds of the
  head of the remaining tys1,tys2 are identical after substitution.  This
  implies, for example, that the kinds of the head of tys1,tys2 are identical
  after substitution.

Preserving (UKINV) takes a bit of work, governed by the `match_kis` flag in
`tc_unify_tys`:

* When we're working with type applications (either TyConApp or AppTy) we
  need to worry about establishing (UKINV), as the kinds of the function
  & arguments aren't (necessarily) included in the kind of the result.
  When unifying two TyConApps, this is easy, because the two TyCons are
  the same. Their kinds are thus the same. As long as we unify left-to-right,
  we'll be sure to unify types' kinds before the types themselves. (For example,
  think about Proxy :: forall k. k -> *. Unifying the first args matches up
  the kinds of the second args.)

* For AppTy, we must unify the kinds of the functions, but once these are
  unified, we can continue unifying arguments without worrying further about
  kinds.

* The interface to this module includes both "...Ty" functions and
  "...TyKi" functions. The former assume that (UKINV) is already
  established, either because the kinds are the same or because the
  list of types being passed in are the well-typed arguments to some
  type constructor (see two paragraphs above). The latter take a separate
  pre-pass over the kinds to establish (UKINV). Sometimes, it's important
  not to take the second pass, as it caused #12442.

Wrinkles

(KCU1) We ensure that the `kco` argument never mentions variables in the
  domain of either RnEnvL or RnEnvR.  Why?

  * `kco` is used only to build the final well-kinded substitution
         a :-> ty |> kco
    The range of the substitution never mentions forall-bound variables,
    so `kco` cannot either.

  * `kco` mixes up types from both left and right arguments of
    `unify_ty`, which have different renamings in the RnEnv2.

  The easiest thing is to insist that `kco` does not need renaming with
  the RnEnv2; it mentions no forall-bound variables.

  To achieve this we do a `mentionsForAllBoundTyVars` test in the
  `CastTy` cases of `unify_ty`.

(KCU2) Suppose we are unifying
            (forall a. x |> (...F a b...) ~ (forall a. y)
  We can't bind y :-> x |> (...F a b...), becuase of that free `a`.

  But if we later learn that b=Int, and F a Int = Bool,
  that free `a` might disappear, so we could unify with
      y :-> x |> (...Bool...)

  Conclusion: if there is a free forall-bound variable in a cast,
  return MaybeApart, with a MaybeApartReason of MARCast.

(KCU3) We thought, at one point, that this was all unnecessary: why should
    casts be in types in the first place? But they are sometimes. In
    dependent/should_compile/KindEqualities2, we see, for example the
    constraint Num (Int |> (blah ; sym blah)).  We naturally want to find
    a dictionary for that constraint, which requires dealing with
    coercions in this manner.