Opened 4 years ago

Closed 3 years ago

#8240 closed bug (fixed)

Better error messages for type family constraints

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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

    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.

Change History (1)

comment:1 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed

This is a dup of #9318, which is fixed


Note: See TracTickets for help on using tickets.