[Haskell-cafe] (Un)termination of overloading resolution

[oleg at pobox.com]

> 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.