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

[oleg at pobox.com]

Martin Sulzmann wrote:

> 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

...

> 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

Yes, I was wondering what rank means exactly. But now I do
have a problem with the criterion itself. The following simple and
quite common code 

> newtype MyIOState a = MyIOState (Int -> IO (a,Int))
>
> instance Monad MyIOState where
>     return x = MyIOState (\s -> return (x,s))
>
> instance MonadState Int MyIOState where
>     put x = MyIOState (\s -> return ((),x))


becomes illegal then? Indeed, the class |MonadState s m| has a
functional dependency |m -> s|. In our case, 
	m = MyIOState, rank MyIOState = 1
	s = Int	       rank Int = 1
and so rank(m) > rank(s) is violated, right?


BTW, the above definition of the rank is still incomplete: it doesn't say
what rank(F t1 ... tm) is where F is an n-ary type constructor and 
m < n. Hopefully, the rank of an incomplete type application is bounded
(otherwise, I have a non-termination example in mind). If the rank is
bounded, then the problem with defining an instance of MonadState
persists. For example, I may wish for a more complex state (which is
realistic):

> newtype MyIOState a = MyIOState (Int -> IO (a,(Int,String,Bool)))
> instance MonadState (Int,String,Bool) MyIOState 

Now, the rank of the state is 4...