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 pures and let

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: