Confusing error message

[simonpj]

For test indexed-types/should_fail/T4272 we get this type error

T4272.hs:11:16:
    Occurs check: cannot construct the infinite type:
      x0 = TermFamily x0 x0
    Expected type: TermFamily x0 x0
      Actual type: TermFamily a a
    In the first argument of `prune', namely `t'
    In the expression: prune t (terms (undefined :: TermFamily a a))
    In an equation for `laws':
        laws t = prune t (terms (undefined :: TermFamily a a))

It's not at all obvious why unifying (TermFamily x0 x0) with (TermFamily a a) should yield an occurs check. Especially as TermFamily is a type function with arity 1, and x0 is a unification variable. So the natural way to solve this constraint would be to unify x0 with a, and then the constraint is satisfied.

What goes wrong is that there is another insolube constraint (which is also reported):

T4272.hs:11:19:
    Could not deduce (a ~ TermFamily x0 x0)
    from the context (TermLike a)
      bound by the type signature for
                 laws :: TermLike a => TermFamily a a -> b
      at T4272.hs:11:1-54
      `a' is a rigid type variable bound by
          the type signature for laws :: TermLike a => TermFamily a a -> b
          at T4272.hs:11:1
    In the return type of a call of `terms'
    In the second argument of `prune', namely
      `(terms (undefined :: TermFamily a a))'
    In the expression: prune t (terms (undefined :: TermFamily a a))

The constraint solver finds this latter constraint, can't solve it, but still uses it to simplify the first one, by substituting (TermFamily x0 x0) for a; and that is what gives the occurs check error.

I don't think that we should use insoluble constraints to rewrite unsolved constraints. But it's delicate, so I am not trying to fiddle right now. Hence making this ticket.

(Incidentally, it's not a regression; it's been like this forever.)

[simonpj]

I'll make it high priority to make sure I look at it for 7.6. But it's not really that serious.