Unify wastes effort on casts

In GHC.Core.Unify the main unify_ty function has signature

unify_ty :: UMEnv
         -> Type -> Type  -- Types to be unified and a co
         -> CoercionN     -- A coercion between their kinds
                          -- See Note [Kind coercions in Unify]
         -> UM ()

That CoercionN, called kco in code, is derived from the idea in eqType that we are comparing types ignoring casts.

The point of this ticket is we do not know a single example where carrying kco makes unification succeed, where it would otherwise fail.

The simpler alternative is to have

unify_ty :: UMEnv
         -> Type -> Type
         -> UM ()

and code like

unify_ty env (CastTy ty1' co1) (CastTy ty2 co2)
  | isReflexiveCo (co1 `mkTransCo` sym co2)
  = = unify_ty env ty1' ty2' (co1 `mkTransCo` kco `mkTransCo` mkSymCo co2)
unify_ty env (Cast {}) ty2 = surelyApart
unify_ty env ty1 (Cast {}) = surelyApart

You might think this would not work on something like

f :: t1 -> t2
x :: t1

f x  ~   ((f |> co1) (x |> co2)) |> co3

where
  co1 :: t1 -> t2   ~   t3 -> t4
  co2 :: t1         ~   t3
  co3 :: t4         ~   t2

But that's ruled out by invariant (EQ1) in Note [Respecting definitional equality] in GHC.Core.TyCo.Rep. Similarly

(forall a. t1 |> co)  ~ (forall a. t2) |> co2

is ruled out by (EQ4).