[Haskell-cafe] Fragile GHC rank-2 type inference?

[宮里 洸司]

The error in the simplified program can be explained.

> ... which fails to compile unless one either
> uncomments the explicit type declaration for the let-bind, or else
> inlines the value:
>
>     {-# LANGUAGE RankNTypes #-}
>     {-# LANGUAGE TypeFamilies #-}
>     module Main (main) where
>     import Control.Monad.IO.Unlift (MonadUnliftIO, withRunInIO)
>     import Control.Concurrent.MVar (newMVar, withMVar)
>     import Control.Monad.IO.Class (liftIO)
>     import Control.Monad.Reader (MonadReader, ReaderT, runReaderT, asks)
>
>     data Env = Env { envLocker :: !Locker, envString :: String }
>     type Locker = forall a. IO a -> IO a
>
>     runLocked :: (env ~ Env, MonadReader env m, MonadUnliftIO m)
>               => forall a. m a -> m a
>     runLocked action = asks envLocker >>= \locker ->
>         withRunInIO $ \run -> locker $ run action
>
>     -- XXX: To compile, uncomment let-bind type, or else inline!
>     mkEnv :: IO Env
>     mkEnv = newMVar () >>= \lock ->
>         let -- locker :: Locker
>             locker = withMVar lock . const
>          in go locker "Hello World!"
>       where
>         go :: Locker -> String -> IO Env
>         go envLocker envString = Env{..}
>
>     main :: IO ()
>     main = mkEnv >>= runReaderT (runLocked $ asks envString >>= liftIO . putStrLn)

You enabled TypeFamilies extension, which subsumes MonoLocalBinds.
MonoLocalBinds
disables automatic let-generalization. Unless you attach type
annotation, the type of locker
is not (forall a. IO a -> IO a).

This is a pure guess, but I think your error in the actual code is
caused by ApplicativeDo.
The following code fails to compile but disabling ApplicativeDo solves
the problem.

  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ApplicativeDo #-}
  module Main where

  import Control.Concurrent.MVar

  type Locker = forall a. IO a -> IO a

  main :: IO ()
  main =
    do lock1 <- newMVar ()
       let locker1 :: Locker
           locker1 = withMVar lock1 . const
       lock2 <- newMVar ()
       let locker2 :: Locker
           locker2 = withMVar lock2 . const
       f locker1 locker2

  f :: Locker -> Locker -> IO ()
  f _ _ = putStrLn "dummy"

I think this is ApplicativeDo-side bug, not type checking bug.

--
/* Koji Miyazato <viercc at gmail.com> */