Infelicities in pure unifier

During code review on !852 (closed), Simon and I discovered a few infelicities in the pure unifier.

1. Many functions (ex: unify_ty, uVar) take a coercion between the kinds of the types being unified. It should be clarified what we are trying to say. To wit:

   A. If matching: kco :: subst(typeKind ty1) ~N typeKind ty2

   B. If unifying: subst(kco) :: subst(ty1) ~N subst(typeKind ty2)

2. All substitutions throughout GHC are kind preserving. Specifically, if we have a subst S containing a mapping a :: k to t, then it is always the case that t :: S(k). This can be checked.

3. There is no FunTy case for unify_ty because it is handled by the tycon case. This should be commented. Specifically, we must make sure to unify the RuntimeReps in the FunTy. This is indeed OK, but it should be made more clear.

4. ty_co_match is rather involved and may not be paying its way. Experiment what happens if it is removed.

5. The ty_co_match function is missing a case for FunCo. This is not actually a bug, because ty_co_match is a "best effort" function.

6. The FunTy case for ty_co_match incorrectly drops the RuntimeReps.

7. We do not unify the kinds of type variables because the relationship between the kinds is passed in. See point (1).

8. We appear to be making fix-points of substitutions even when doing one-way matching. As originally reported in #16512 (comment 221617).

The only real bug here is (6), but it can only happen when performing coercion optimization on programs involving type families that twiddle RuntimeReps in functions. I'm not going to try to find a test case.