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 kcoThis 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 |