id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
5763,Confusing error message,simonpj,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.)
",bug,new,high,7.6.2,Compiler,7.2.2,,,dimitris@… hackage.haskell.org@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,indexed-types/should_fail/T5763,,,