Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information