Monomoprhic code makes ImpredicativeTypes infer an existential type
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) }’Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | A.SerranoMena@uu.nl, simonpj@microsoft.com, Alejandro, Jones, Mena, Peyton, Serrano, Simon |
| Operating system | |
| Architecture |