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 |