Impredicative types in 8.0, again

[Reid Barton]

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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160304/1e7964b3/attachment-0001.html>