Confusing error message
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
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.)