[Haskell] MTL violates coverage condition?

[Tom Schrijvers]

> Does 'MonadState s m => MonadState s (ReaderT r m)', found in
> Control.Monad.Reader violate the coverage condition as I believe it
> does?

Yes, it does.

> Can one write a function using this library to force the type
> inference engine to loop indefinitely?  If not, what mitigating
> conditions prevent it?  Can I write a similar declaration in my
> library and compile it with -fallow-undecidable-instances and without
> worry?

The coverage condition is a sufficient condition for termination of the 
type checker.

Another sufficient condition is the Terminating Weak Coverage condition 
(Definition 14). This condition is met by that instance, as well as yours.

If you want to get non-terminating, you must write a funny instance like:

 	MonadState s m => MonadState (MymonadT s) (MymonadT m)

and then set up a constraint

 	MonadState x (MymonadT x)

I did not try it, but GHC should run out of stack on this one or give up.

I'm currently working with Martin Sulzmann on a relaxed set of 
conditions for FDs and type functions.

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/