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

[Martin Sulzmann]

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
others to follow our discussion.