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, Косырев Сергей
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@haskell.org] On Behalf Of | Kosyrev Serge | Sent: 04 March 2016 13:43 | To: ghc-devs@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@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
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
participants (3)
-
Kosyrev Serge -
Reid Barton -
Simon Peyton Jones