Fragile GHC rank-2 type inference?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

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@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.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

Locker.hs (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: 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.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> */
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Fragile GHC rank-2 type inference?

Viktor Dukhovni
> On Jan 19, 2019, at 9:09 PM, 宮里 洸司 <[hidden email]> wrote:
>
> 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).

Thanks, that makes sense.  And indeed I only did that while
trying to understand how the use of "withResponse" plays into
the story, but just adding the type annotation is not enough,
so the real problem is elsewhere...

> 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.

Nice example, thanks!  Indeed that seems to be much closer to
the heart of 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.

Yes, removing ApplicativeDo and rewriting the option parser as:

        Env locker <$> f1 <*> f2 <*> ... <*> fN

solves the problem, but results in IMHO harder to maintain code,
because of the required positional correspondence between the
Env constructor fields and the placement of the field parsers.

It is certainly surprising that ApplicativeDo affects the
type inference of "locker" in:

        type Locker = forall a. IO a -> IO a
        data Env = Env { locker :: Locker, f1 :: T1, ... , fN :: TN }

        f locker = do
                f1 <- parser1
                f2 <- parser2
                ...
                fN <- parserN
                pure Env{..}

in a way that breaks:

        lock <- newMVar ()
        let locker :: Locker
            locker = withMVar lock . const
        f locker

but does not break:

        lock <- newMVar ()
        f (mkLocker lock)
      where
        mkLocker :: MVar () -> Locker
        mkLocker lock = withMVar lock . const

Would it be appropriate to file a bug report?  Your
example seems suitably succinct.

--
        Viktor.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Fragile GHC rank-2 type inference?

宮里 洸司
> Would it be appropriate to file a bug report?

Found that there's a related bug report:
https://ghc.haskell.org/trac/ghc/ticket/11982
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Fragile GHC rank-2 type inference?

Viktor Dukhovni


> On Jan 20, 2019, at 2:09 AM, 宮里 洸司 <[hidden email]> wrote:
>
>> Would it be appropriate to file a bug report?
>
> Found that there's a related bug report:
> https://ghc.haskell.org/trac/ghc/ticket/11982

Yes, that looks close.  I think that your example could be added
to the bug report, making a more compelling case for fixing it.

I've tidied it up a bit more below my signature.  Would you like
to add this to that ticket, or should I?

--
        Viktor.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ApplicativeDo #-}
module Main where
import Control.Concurrent.MVar

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

main :: IO ()
main = do
     line <- getLine
     lock <- newMVar ()
     let locker :: Locker
         locker = withMVar lock . const
     f line locker

f :: String -> Locker -> IO ()
f line locker = locker $ putStrLn line

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Fragile GHC rank-2 type inference?

Viktor Dukhovni
> On Jan 20, 2019, at 2:24 AM, Viktor Dukhovni <[hidden email]> wrote:
>
> I've tidied it up a bit more below my signature.  Would you like
> to add this to that ticket, or should I?

I went ahead and updated the ticket.  I hope you don't mind...

--
        Viktor.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Fragile GHC rank-2 type inference?

宮里 洸司
No problem! I rather thank you for taking your time to report the example.

--
/* Koji Miyazato <[hidden email]> */
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.