TypeInType error message regressions

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.

Trac metadata

Trac field	Value
Version	7.11
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture