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

[Viktor Dukhovni]

On Sat, Jan 19, 2019 at 04:20:23PM -0500, Viktor Dukhovni wrote:

> in my complete program, the call to 'mkEnv' fails to compile, when
> called via:
> 
>         mkLockEnv :: IO Env
>         mkLockEnv = do
>             lock <- newMVar ()
>             let locker :: Locker
>                 locker = withMVar lock . const
>             ... (mkEnv locker)
> 
> But after inlining the "locker" binding, the code compiles:
> 
>         mkLockEnv :: IO Env
>         mkLockEnv = do
>             lock <- newMVar ()
>             ... (mkEnv (withMVar lock . const))
> 
> Given "let-bound polymorphism":
> 
>     https://kseo.github.io/posts/2016-12-27-higher-rank-polymorphism.html
> 
> I would not have expected the change to make a difference...

Well, it turns out that some of the difference between the simplified
and complete program is that my "Reader Env IO" monad gets some
additional constraints via:

   http://hackage.haskell.org/package/http-conduit-2.3.4/docs/Network-HTTP-Client-Conduit.html#v:withResponse

   withResponse :: ( MonadUnliftIO m, MonadIO n, MonadReader env m
                   , HasHttpManager env)
                => Request
		-> (Response (ConduitM i ByteString n ()) -> m a) -> m a

Removing the call to 'withResponse' allows a simplified program
compile without inlining the let-bind.  Inspired by that, I cobbled
together the below, 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)

And yet, adding a type declaration for the let-bind still is not
enough for the full program, only inlining "withMVar lock .  const"
makes GHC happy.  Don't yet know why...

        • Couldn't match type ‘a’ with ‘a0’
          ‘a’ is a rigid type variable bound by
            a type expected by the context:
              forall a. IO a -> IO a
            at Jname.hs:135:32-56
          Expected type: IO a -> IO a
            Actual type: IO a0 -> IO a0
        • In the second argument of ‘optsParser’, namely ‘locker’
          In the second argument of ‘(<*>)’, namely
            ‘optsParser manager locker’
          In the first argument of ‘O.info’, namely
            ‘(O.helper <*> optsParser manager locker)’
        • Relevant bindings include
            locker :: IO a0 -> IO a0 (bound at Jname.hs:132:9)
        |
    135 |         $ O.info (O.helper <*> optsParser manager locker)
        |                                                   ^^^^^^

-- 
	Viktor.