Impredicative types in 8.0, again

[Simon Peyton Jones]

ImpredicativeTypes is indeed problematic.  Perhaps you can add your example as another Trac ticket?   It's not really going to get fixed until someone pays sustained attention to it.

Alejandro (cc'd) is working on this.  We are working on a paper for ICFP... wait a couple of weeks!

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Kosyrev Serge
|  Sent: 04 March 2016 13:43
|  To: ghc-devs at haskell.org
|  Subject: Impredicative types in 8.0, again
|  
|  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 at haskell.org
|  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.ha
|  skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
|  devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c3150fd5e547f4
|  294afb408d34432eadb%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=9dlTzi
|  vbVZydfO5zN6i8CEHGoThCN7wR6cQavKkj1ZU%3d