Impredicative types and do-notation
This ticket is about the interaction of Quick Look impredicativity and do-notation.
Consider these definitions
t :: IO (forall a. a -> a)
t = return id
p :: (forall a. a -> a) -> (Bool, Int)
p f = (f True, f 3)
-- This typechecks (with QL)
foo1 = t >>= \x -> return (p x)
-- But this does *not* type check:
foo2 = do { x <- t ; return (p x) }
Remember (>>=) :: forall m a b. Monad m => m a -> (a -> m b) -> m b
. Now, foo1
works because Quick Look can work out how to instantiate m
and a
from the first argument t
. Easy.
We just need to do the same for do-notation, foo2
. When #17582 finally lands (work in progress is !2960 (closed)), this will happen automatically.