Martin Sulzmann sulzmann at comp.nus.edu.sg
Wed Feb 22 00:24:03 EST 2006

```oleg at 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