Maciej Piechotka wrote:

class (Monad m, Monad (IO' m)) => MonadIO m where type IO' m :: * -> * liftIO :: IO a -> IO' m a liftM :: m a -> IO' m a

The signature for liftIO betrays a problem. Since liftIO is a member of a type class, when liftIO is used in code, the type checker has to find the appropriate instance (i.e., resolve the overloading). Suppose we have this piece of code: tt :: FooIO () tt = liftIO (return () :: IO ()) How to find the appropriate instance of MonadIO and resolve the liftIO overloading? The argument type of liftIO does not mention the type class parameter m at all, and so it is of no guidance for overloading resolution. We know that the return type of liftIO in the tt code is FooIO (). Thus we have to find such instance of the MonadIO class that its associated type IO' m is equal to FooIO. In other words, we have to find m as a solution of the equation IO' m = FooIO Or, we have to invert the type function IO' m. Alas, type functions are not generally injective and hence not invertible. Indeed, nothing prevents the user from defining two instances of MonadIO, for types m1 and m2, such that IO' m1 = IO' m2 = FooIO.