Skip to content

ImpredicativeTypes vs. do notation

Summary

do notation doesn't work with ImpredicativeTypes even when its desugaring does.

Steps to reproduce

potato :: IO (forall a. a -> [a])
potato = readLn >>= \n -> pure (replicate n)

If I write

potato >>= \f -> pure (f 3, f 'a')

it works fine.

If I instead write

do
  f <- potato
  pure (f 3, f 'a')

I get

    • Couldn't match type: forall a. a -> [a]
                     with: Char -> b
      Expected: IO (Char -> b)
        Actual: IO (forall a. a -> [a])

Expected behavior

I expect do notation (without ApplicativeDo, etc.), to work (or not work) with impredicative types the same as its desugaring. I don't know enough about ImpredicativeTypes to know whether to expect both to succeed or both to fail, but the mismatch is jarring.

Environment

  • GHC version used: 9.2.1
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information