ApplicativeDo breaks compilation with polymorphic bindings
Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when ApplicativeDo
is enabled.
Steps to reproduce
{-# LANGUAGE ApplicativeDo, Rank2Types #-}
module Test where
type M = forall m. Monad m => m () -> m ()
runM :: M -> IO ()
runM m = m $ pure ()
q :: IO ()
q = do
() <- pure ()
let
m :: M
m = id
() <- pure ()
runM m
-- pure ()
Note that the example is very fragile. It will start to compile if you either:
- Remove
ApplicativeDo
- Uncomment the last
pure
- Remove one of the
pure
- Reorder the
pure
s andlet
The error is:
foo.hs:14:3-4: error:
• Ambiguous type variable ‘m0’ arising from a use of ‘m’
prevents the constraint ‘(Monad m0)’ from being solved.
<...>
• In the first argument of ‘return’, namely ‘m’
In the expression:
do () <- pure ()
let m :: M
m = id
() <- pure ()
runM m
In an equation for ‘q’:
q = do () <- pure ()
let m :: M
....
() <- pure ()
runM m
|
14 | () <- pure ()
| ^^
foo.hs:19:8: error:
• Couldn't match type ‘m’ with ‘m0’
‘m’ is a rigid type variable bound by
a type expected by the context:
M
at foo.hs:19:3-8
Expected type: m () -> m ()
Actual type: m0 () -> m0 ()
• In the first argument of ‘runM’, namely ‘m’
In a stmt of a 'do' block: runM m
In the expression:
do () <- pure ()
let m :: M
m = id
() <- pure ()
runM m
• Relevant bindings include
m :: m0 () -> m0 () (bound at foo.hs:17:5)
|
19 | runM m
The renamer outputs:
= do join (m_aXe <- do () <- pure ()
let m_aXe :: Test.M
m_aXe = id
return m_aXe |
() <- pure ())
Test.runM m_aXe
which I couldn’t make sense of, but it looks like it is getting deshugared to something like:
q2 :: IO ()
q2 = let {m :: M; m = id} in return m >>= runM
which doesn’t compile indeed.
Expected behavior
Code that compiles without ApplicativeDo
should compile with ApplicativeDo
.
Environment
- GHC version used: 8.6.5, 8.8.2
Optional:
- Operating System:
- System Architecture: