Better error messages for type family constraints
Consider this constraint
F Int ~ Bool -- Arising (say) on line 5 F Int ~ Char -- Arising (say) on line 10
At the moment we'll combine the two to
F Int ~ Bool -- Arising on line 5 Bool ~ Char -- Arising on line 10
The second of these errors is "insoluble" and is reported first. But it's totally misleading: nowhere in the program did we directly need
Another variant of this came up in Trac #8227 (closed). There we get the constraint
Scalar (V a) ~ t0 Scalar (V a) ~ t0 -> t0
which leads to
Scalar (V a) ~ t0 -> t0 t0 ~ t0 -> t0 -- Occurs check
which gives the confusing error
T8227.hs:16:44: Occurs check: cannot construct the infinite type: t0 ~ t0 -> t0 Expected type: Scalar (V (t0 -> t0)) Actual type: Scalar (V a)
I think the solution is
- Do not combine two Wanteds
[W] F tys ~ t1 [W] F tys ~ t2
unless t1 and t2 are both touchable unification variables.
- Instead (perhaps) generate a Derived constraint
[D] t1 ~ t2
to express the fact that t1 and t2 had better end up equal.
- To do this the inert set would need to contain many
CTyFunEqconstraints with the same LHS.
I'm not very sure about this, and no time now, so I'm just making this ticket to record the issue.