Note [Equalities with heterogeneous kinds]

What do we do when we have an equality

  (tv :: k1) ~ (rhs :: k2)

where k1 and k2 differ? Easy: we create a coercion that relates k1 and
k2 and use this to cast. To wit, from

  [X] co1 :: (tv :: k1) ~ (rhs :: k2)

(where [X] is [G] or [W]), we go to

  co1 = co2 ; sym (GRefl kco)
  [X] co2 :: (tv :: k1) ~ ((rhs |> sym kco) :: k1)
  [X] kco :: k1 ~ k2

Wrinkles:

(EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by
     the kind-level one. We thus include the kind-level wanted in the RewriterSet
     for the type-level one. See Note [Wanteds rewrite Wanteds] in
     GHC.Tc.Types.Constraint.  This is done in canEqCanLHSHetero.

(EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce
        [W] w (rewriters: {kw}) : a ~ (b |> kw)
        [W] kw                  : Type ~ (Type->Type)

     We track `w` as having `kw` in its rewriter set.  That will stop us unifying `w`
     (see Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality).

    But `w` is still /canonical/, and used for rewriting other constraints.
    See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. That's important
    in general. Consider:
        [W] kw : k  ~ Type
        [W] w  : a ~ F k t
     We can rewrite `w` with `kw` like this:
        [W] w' (rewriters: {kw}) : a ~ F Type (t |> kw)
     The cast on the second argument of `F` is necessary to keep the appliation well-kinded.
     There is nothing special here; no reason not treat w' as canonical, and use it for
     rewriting. Indeed test JuanLopez only typechecks if we do.

  So here is our implementation:
     * When doing the kind unification, any equality constraints we can't solve
       immediately get an origin that tells that the constraint arises from
       the kind of the parent type-equality.  See the calls to `mkKindEqLoc`
       in `canEqCanLHSHetero`.

     * We /also/ add these unsolved kind equalities to the `RewriterSet` of the
       parent constraint; see the call to `rewriteEqEvidence` in `finish` in
       `canEqCanLHSHetero`.

     * When filling a coercion hole we kick out any equality constraints whose
       rewriter set mentions this hole.  See `kickOutAfterFillingCoercionHole`

(EIK3) Suppose we have [W] co1 : (a :: k1) ~ (rhs :: k2). We duly follow the
     algorithm detailed here, producing [W] kco :: k1 ~ k2, and adding
     [W] co2 : (a :: k1) ~ ((rhs |> sym kco) :: k1) to the inert set.
     Some time later, we solve `kco`, and fill in kco's coercion hole.
     This kicks out the inert equality `co2`

     But now, during canonicalization, we see the cast and remove it, in
     `canEqCast`. By the time we get into `canEqCanLHS`, the equality is
     heterogeneous again, and the process repeats!

     To avoid this, we don't strip casts off a type if the other type in the
     equality is a CanEqLHS.  See the `CastTy` case of `can_eq_nc`.
     (The scenario above can happen with a type family, too.
      testcase: typecheck/should_compile/T13822).

     And this is an improvement regardless: because tyvars can, generally,
     unify with casted types, there's no reason to go through the work of
     stripping off the cast when the cast appears opposite a tyvar.

Historical note:

We used to do this via emitting a Derived kind equality and then parking
the heterogeneous equality as irreducible. But this new approach is much
more direct. And it doesn't produce duplicate Deriveds (as the old one did).