oleg@pobox.com writes:
Let's consider the general case (which I didn't describe in my earlier email).
In case we have an n-ary type function T (or (n+1)-ary type class constraint T) the conditions says for each
type T t1 ... tn = t
(or rule T t1 ... tn x ==> t)
then rank(ti) > rank(t) for each i=1,..,n
I didn't know what condition you meant for the general form. But the condition above is not sufficient either, as a trivial modification of the example shows. The only modification is
instance E ((->) (m ())) (() -> ()) (m ()) where
and test = foo (undefined::((() -> ()) -> ()) -> ()) (\f -> (f ()) :: ())
Now we have t1 = ((->) (m ())) : two constructors, one variable t2 = () -> () : three constructors t = m () : one constructor, one variable
and yet GHC 6.4.1 loops in the typechecking phase as before.
rank (() ->()) > rank (m ()) does NOT hold. Sorry, I left out the precise definition of the rank function in my previous email. Here's the formal definition. rank(x) is some positive number for variable x rank(F t1 ... tn) = 1 + rank t1 + ... + rank tn where F is an n-ary type constructor. rank (f t) = rank f + rank t f is a functor variable Hence, rank (()->()) = 3 rank (m ()) = rank m + 1 We cannot verify that 3 > rank m + 1. So, I still claim my conjecture is correct. Martin P. S. Oleg, can you next time please provide more details why type inference does not terminate. This will help others to follow our discussion.