TypeInType error message regressions
TypeInType causes error messages around certain kind errors to degrade.
Here is the case:
[W] (alpha :: k) ~ (Int :: *)
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
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.