TypeInType causes error messages around certain kind errors to degrade.

Here is the case:

[W] (alpha :: k) ~ (Int :: *)

where alpha is a unification variable, k is a skolem, and there is no witness that k ~ *. The solver will simplify to

[W] kco :: k ~ *
[W] (alpha :: k) ~ (Int |> sym kco)

and then the latter, now homogeneous equality is solved by unification

alpha := Int |> sym kco

This is all sound. But when reporting a kind error around k not equalling *, GHC likes to report the type error that the kind error came from. But, after zonking, the type error looks like Int ~ Int, when we drop coercions (as we tend to do in error messages).

That's unfortunate. It affects test cases

• T9196
• T8262
• T8603
• tcfail122

Simon has proposed a rule that should avoid this: never, ever use a wanted as a kind cast. That might work, but an attempt at implementing caused a loop when kind families were involved. I will keep pushing on this.