-> TcType -> TcType   -- xi2

                   -> TcKind             -- ki2

                   -> TcS (StopOrContinue (Either IrredCt EqCt))

 -- See Note [Equalities with incompatible kinds]

 -- See Note [Kind Equality Orientation]

               -- Otherwise we might put something in the inert set that isn't inert

          then startAgainWith (mkNonCanonical ev)

          else

     do { let lhs_redn = mkReflRedn role ps_xi1

              rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co

              mb_sym_kind_co = case swapped of

             ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])

        ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn

   where

     mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool)

 where k1 and k2 differ? Easy: we create a coercion that relates k1 and

 k2 and use this to cast. To wit, from

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

 Wrinkles:

 (EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce

         [W] w  : a ~ (b |> kw)

      Instead, it lands in the inert_irreds in the inert set, awaiting solution of

      that `kw`.

      solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out

      all equalities whose RHS mentions the filled-in coercion hole.  Note that

      it looks for type family equalities, too, because of the use of unifyTest

      which records that `w` has been rewritten by `kw`.

      See (WRW3) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.

      main way is like this. Assume F :: forall k. k -> Type

         [W] kw : k  ~ Type

         [W] w  : a ~ F k t

      rewriting. Indeed tests JuanLopez only typechecks if we do.  So we'd like to treat

      this kind of equality as canonical.

      * An equality constraint is non-canonical if it mentions a hetero-kind

 (EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the

      algorithm detailed here, producing [W] co :: k1 ~ k2, and adding

        ; return n_kicked }

 kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()

 -- It's possible that this could just go ahead and unify, but could there be occurs-check

 -- problems? Seems simpler just to kick out.

 kickOutAfterFillingCoercionHole hole

   = do { ics <- getInertCans

        ; let (kicked_out, ics') = kick_out ics

              n_kicked           = lengthBag kicked_out

       where

         (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds

       | IrredCt { ir_ev = ev, ir_reason = reason } <- ct

       , CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev

       , NonCanonicalReason ctyeq <- reason

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 An EqCt is a canonical equality constraint, one that can live in the inert set,

 and that can be used to rewrite other constraints. It satisfies these invariants:

   * (TyEq:OC) lhs does not occur in rhs (occurs check)

               Note [EqCt occurs check]

   * (TyEq:F) rhs has no foralls

       (this avoids substituting a forall for the tyvar in other types)

   * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant]

   * (TyEq:N) If the equality is representational, rhs is not headed by a saturated

     application of a newtype TyCon. See GHC.Tc.Solver.Equality

     Note [No top-level newtypes on RHS of representational equalities].

     (Applies only when constructor of newtype is in scope.)

   * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we

     will not form an EqCt (a ~ ty).

   * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up

     a hetero-kinded equality.  See Note [Equalities with incompatible kinds] in

     GHC.Tc.Solver.Equality, wrinkle (EIK2)

    -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs

    -- See also Note [Insoluble mis-match] in GHC.Tc.Errors

 cteConcrete        = CTEP (bit 5)   -- Type variable that can't be made concrete

                                     --    e.g. alpha[conc] ~ Maybe beta[tv]

 cteSkolemEscape    = CTEP (bit 6)   -- Skolem escape e.g.  alpha[2] ~ b[sk,4]

 cteProblem :: CheckTyEqProblem -> CheckTyEqResult

 newCoercionHoleO _ pty                 = new_coercion_hole False pty

 new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole

 new_coercion_hole hetero_kind pred_ty

   = do { co_var <- newEvVar pred_ty

        ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty)

   = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev)

        ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') }

 zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet

 zonkRewriterSet (RewriterSet set)

   = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set

      -- monadic action is to read, and the combining function is

      -- commutative

   where

     go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc

     check_hole :: CoercionHole -> ZonkM RewriterSet

     check_ty :: Type -> UnfilledCoercionHoleMonoid

     check_co :: Coercion -> UnfilledCoercionHoleMonoid