Impredicative types in 8.0, again

[Kosyrev Serge]

Good day!

I realise that ImpredicativeTypes is a problematic extension, but I have
found something that looks like an outright bug -- no polymorphism involved:

,----
| {-# LANGUAGE ImpredicativeTypes #-}
|
| module Foo where
| 
| foo :: IO (Maybe Int)
| foo = do
|   pure $ case undefined :: Maybe String of
|             Nothing
|               -> Nothing
|             Just _
|               -> (undefined :: Maybe Int)
`----

produces the following errors:

,----
| foo.hs:7:3: error:
|     • Couldn't match type ‘forall a. Maybe a’ with ‘Maybe Int’
|       Expected type: IO (Maybe Int)
|         Actual type: IO (forall a. Maybe a)
|     • In a stmt of a 'do' block:
|         pure
|         $ case undefined :: Maybe String of {
|             Nothing -> Nothing
|             Just _ -> (undefined :: Maybe Int) }
|       In the expression:
|         do { pure
|              $ case undefined :: Maybe String of {
|                  Nothing -> Nothing
|                  Just _ -> (undefined :: Maybe Int) } }
|       In an equation for ‘foo’:
|           foo
|             = do { pure
|                    $ case undefined :: Maybe String of {
|                        Nothing -> Nothing
|                        Just _ -> (undefined :: Maybe Int) } }
| 
| foo.hs:11:19: error:
|     • Couldn't match type ‘a’ with ‘Int’
|       ‘a’ is a rigid type variable bound by
|         a type expected by the context:
|           forall a. Maybe a
|         at foo.hs:11:19
|       Expected type: forall a. Maybe a
|         Actual type: Maybe Int
|     • In the expression: (undefined :: Maybe Int)
|       In a case alternative: Just _ -> (undefined :: Maybe Int)
|       In the second argument of ‘($)’, namely
|         ‘case undefined :: Maybe String of {
|            Nothing -> Nothing
|            Just _ -> (undefined :: Maybe Int) }’
`----

-- 
с уважениeм / respectfully,
Косырев Сергей