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