This looks very similar to https://ghc.haskell.org/trac/ghc/ticket/11319, but might be worth including as a separate example there. Note that it does compile if you swap the order of the case alternatives.

Regards,
Reid Barton


On Fri, Mar 4, 2016 at 8:43 AM, Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:
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,
Косырев Сергей
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs