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.