[EMAIL PROTECTED] 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
