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:
```hs
{-# 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) }’
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Monomoprhic code makes ImpredicativeTypes infer an existential type","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["<A.SerranoMena@uu.nl>","<simonpj@microsoft.com>","Alejandro","Jones","Mena","Peyton","Serrano","Simon"],"type":"Bug","description":"I realise that ImpredicativeTypes is a problematic extension, but I have\r\nfound something that looks like an outright bug -- no polymorphism involved:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n\r\nmodule Foo where\r\n\r\nfoo :: IO (Maybe Int)\r\nfoo = do\r\n pure $ case undefined :: Maybe String of\r\n Nothing\r\n -> Nothing\r\n Just _\r\n -> (undefined :: Maybe Int)\r\n}}}\r\n\r\nProduces the following errors:\r\n\r\n{{{\r\nfoo.hs:7:3: error:\r\n • Couldn't match type ‘forall a. Maybe a’ with ‘Maybe Int’\r\n Expected type: IO (Maybe Int)\r\n Actual type: IO (forall a. Maybe a)\r\n • In a stmt of a 'do' block:\r\n pure\r\n $ case undefined :: Maybe String of {\r\n Nothing -> Nothing\r\n Just _ -> (undefined :: Maybe Int) }\r\n In the expression:\r\n do { pure\r\n $ case undefined :: Maybe String of {\r\n Nothing -> Nothing\r\n Just _ -> (undefined :: Maybe Int) } }\r\n In an equation for ‘foo’:\r\n foo\r\n = do { pure\r\n $ case undefined :: Maybe String of {\r\n Nothing -> Nothing\r\n Just _ -> (undefined :: Maybe Int) } }\r\n\r\nfoo.hs:11:19: error:\r\n • Couldn't match type ‘a’ with ‘Int’\r\n ‘a’ is a rigid type variable bound by\r\n a type expected by the context:\r\n forall a. Maybe a\r\n at foo.hs:11:19\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe Int\r\n • In the expression: (undefined :: Maybe Int)\r\n In a case alternative: Just _ -> (undefined :: Maybe Int)\r\n In the second argument of ‘($)’, namely\r\n ‘case undefined :: Maybe String of {\r\n Nothing -> Nothing\r\n Just _ -> (undefined :: Maybe Int) }’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->
issue