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

[Viktor Dukhovni]

[ I am seeing somewhat subtle, and to me surprising, type-inference
  obstacles.  I am presently using GHC 8.6.3.  I don't know whether
  what I'm seeing is a feature or a bug. ]

Given a function 'mkEnv' (a command-line option parser built using
optparse-applicative) that returns a rank-2 type (via ApplicativeDo):

        {-# LANGUAGE ApplicativeDo #-}
        {-# LANGUAGE RankNTypes #-}
        {-# LANGUAGE RecordWildCards #-}

        type Locker = forall a. IO a -> IO a
        data Env = Env { envLocker :: Locker, ... }

        mkEnv :: Locker -> Env
        mkEnv envLocker = do
            ...
            pure Env{..}

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)

      -- Error message:

        * Couldn't match type ‘a’ with ‘a0’
          ‘a’ is a rigid type variable bound by
            a type expected by the context:
              Locker
            at ... 132
          Expected type: IO a -> IO a
            Actual type: IO a0 -> IO a0
        * In the second argument of ‘mkEnv’, namely ‘locker’
        * Relevant bindings include
            locker :: IO a0 -> IO a0 (bound at ...)
        |
    132 |             ... (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...

In trying to simplify the code (attached) to understand the source
of the problem, surprisingly, the simplified program compiles in
either form.  It is not apparent what facet of the larger program
has a bearing on the construction of the rank-2 environment.

The background is that some of my Haskell applications employ a
shared lock to serialize writes to stdout from concurrent forkIO
"threads".  The lock is the usual:

        type Lock = MVar ()

        withLock :: Lock -> IO a -> IO a
        withLock lock = withMVar lock . const

I am however tempted to abstract away the concrete lock type, leaving
just a polymorphic closure, which results in 'Env' having a rank-2
type:

        {-# LANGUAGE RankNTypes #-}

        data Env = Env { envLocker :: Locker, ... }
        type Locker = forall a. IO a -> IO a
        type EnvReader a = ReaderT Env IO a

        runLocked :: forall a. EnvReader a -> EnvReader a
        runLocked action = ask >>= \env at Env{..} ->
            liftIO $ envLocker $ runReaderT action env

and this works in the attached sample program which builds
and runs:

    $ echo "The answer to life the universe and everything is:" |
          ./locker --answer 42
    The answer to life the universe and everything is:
    42

but a larger program where a "runLocked" call is located deeper in
the call chain, fails to compile except as described at the top of
the message.

-- 
        Viktor.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Locker.hs
Type: text/x-haskell
Size: 1617 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190119/41b3767a/attachment.hs>