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 Int~Char.

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 CTyFunEq constraints 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.

Trac metadata

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