What part of the type system is getting in the way, when I try to pass IO action via reader monad transformer instead of via function argument?

Question

Look at this answer from an older question about Testing functions in Haskell that do IO.

It proposes, as a solution, to pass IO actions as arguments to a function that doesn't hardcode IO, but just the requirement that a generic m that takes the place of IO, is a Monad:

numCharactersInFile' :: Monad m => (FilePath -> m String) -> FilePath -> m Int
numCharactersInFile' f filePath = do
    contents <- f filePath
    return (length contents)

A possible usage of that would be like this:

module Main where

import MTLPrelude

main :: IO ()
main = do
  -- usage in production
  n <- numCharactersInFile' readFile "/home/enrico/fibs.hs"
  print n
  -- usage in testing
  print $ 18 == (runIdentity .  numCharactersInFile' mockFileSystem "path")

mockFileSystem :: FilePath -> Identity String
mockFileSystem _ = return "mock file contents"

Now I was wondering: what if I want to pass readFile not through a function argument, but through a ReaderT layer?

This would allow running code inside of `runReaderT` readFile, thus having access to that action via ask, only in functions that need it, and right where it's needed, instead of having to pass it around as an argument.

I thought I could change the above numCharactersInFile to this:

numCharactersInFile'' :: (MonadIO m, MonadReader (FilePath -> m String) m) => FilePath -> m Int
numCharactersInFile'' filePath = do
  f <- ask
  contents <- f filePath
  return (length contents)

where the "input" (FilePath -> m String) has been moved from function arguments to the read-only state of the ReaderT layer, and correspondingly f <- ask is used to retrieve that read-only state.

I would think I could use that like this:

main :: IO ()
main = do  -- usage in production
  i <- numCharactersInFile'' "/home/enrico/fibs.hs" `runReaderT` readFile
  print i
  -- usage in testing
  j <- numCharactersInFile'' "path" `runReaderT` mockFileSystem

  print $ 18 == j

but this doesn't even typecheck, with the following error:

 • Couldn't match type: IO String
                  with: ReaderT (FilePath -> IO String) IO String
     arising from a functional dependency between:
       constraint ‘MonadReader
                     (FilePath -> ReaderT (FilePath -> IO String) IO String)
                     (ReaderT (FilePath -> IO String) IO)’
         arising from a use of ‘numCharactersInFile''’
       instance ‘MonadReader r (ReaderT r m)’ at <no location info>
 • In the first argument of ‘runReaderT’, namely
     ‘numCharactersInFile'' "/home/enrico/fibs.hs"’
   In a stmt of a 'do' block:
     i <- numCharactersInFile'' "/home/enrico/fibs.hs"
            `runReaderT` readFile
   In the expression:
     do n <- numCharactersInFile' readFile $ "/home/enrico/fibs.hs"
        print n
        print
          $ 18
              == (runIdentity . numCharactersInFile' mockFileSystem $ "path")
        i <- numCharactersInFile'' "/home/enrico/fibs.hs"
               `runReaderT` readFile
        .... [-Wdeferred-type-errors]

On one hand I'm bugged by my idea not working, but on the other hand I have the feeling that what I'm expecting to work doesn't work for a very good reason, but I can't quite grasp it now.

Any help in understanding this matter is appreciated.

Answer 1

To satisfy the constraint MonadReader (FilePath -> m String) m we would need something like m = ReaderT (FilePath -> m String) IO but that's forbidden since it would make m a into an "infinite type".

In Haskell, as in many programming languages, types must be representable using finitely many symbols. This greatly helps in type checking and inference. Consequently, we can't have a = (a, Int) for any type a, for instance.

Now, there is a way around it: Haskell type system is nominal, and allows recursion. So one could write

newtype M a = M {unM :: ReaderT (FilePath -> M String) IO a}

Then, we could define (or derive, I guess?) the instance MonadReader (FilePath -> M String) M we need. Its definition should involve carefully wrapping / removing the constructor M (or perhaps using safe coercions).