MTL violates coverage condition?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

MTL violates coverage condition?

Mike Haskel
Hi,

A bit of a detailed technical question.


I'm writing a library which makes heavy use of the MTL (Monad.State,
etc) and monad transformers.  I have a monad transformer, MymonadT,
which I want to inherit relevant type classes from the monads it
transforms, i.e.

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

The MTL itself uses such instance declarations, such as

MonadState s m => MonadState s (ReaderT r m).


When I compile my library however (using ghc-6.6.1 and
-fglasgow-exts) I get an illegal instance declaration error:
  "The Coverage Condition fails for one of the functional dependencies;
   Use -fallow-undecidable-instances to permit this."
The code compiles with -fallow-undecidable-instances.


As a reminder, MonadState is declared as

class Monad m => MonadState s m | m -> s


The coverage condition is described in
http://research.microsoft.com/~simonpj/papers/fd-chr/jfp06.pdf on page
12.  My own analysis suggests that the declaration of MonadState for
ReaderT violates this condition as well.

The coverage condition exists, this paper claims, to prevent infinite
loops in type inference---someone could use some instance declarations
violating this condition to write a function whose type is
undecidable.


Does 'MonadState s m => MonadState s (ReaderT r m)', found in
Control.Monad.Reader violate the coverage condition as I believe 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?

Thanks,
Mike
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: MTL violates coverage condition?

Tom Schrijvers-2
> 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: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell