GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:27Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11428ImpredicativeTypes causes GHC panic with 8.0.1-rc12019-07-07T18:30:27ZRyan ScottImpredicativeTypes causes GHC panic with 8.0.1-rc1I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [Data.Conduit.Internal.Pipe](https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs) module). This (greatly si...I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [Data.Conduit.Internal.Pipe](https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs) module). This (greatly simplified) code, which compiles without issue on GHC 7.10.3:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
module Data.Conduit.Internal.Pipe where
data Pipe o r =
HaveOutput (Pipe o r) o
mapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r
mapOutputMaybe f (HaveOutput p o) =
maybe id (\o' p' -> HaveOutput p' o') (f o) (mapOutputMaybe f p)
```
emits a GHC panic with GHC 8.0.1-rc1:
```
[1 of 1] Compiling Data.Conduit.Internal.Pipe ( Wat.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160111 for x86_64-unknown-linux):
matchExpectedFunTys
<>
a_a15Z[tau:5] -> b_a15Y[tau:5]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Note that this code does not require `-XImpredicativeTypes`, and removing the pragma makes the code compile again.
Marking as high since it's a regression, but not highest because `-XImpredicativeTypes` has long been broken (see also #11319). Still, this currently happens on code in the wild, and perhaps it would be worth turning this into a more sensible error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ImpredicativeTypes causes GHC panic with 8.0.1-rc1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["ImpredicativeTypes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs Data.Conduit.Internal.Pipe] module). This (greatly simplified) code, which compiles without issue on GHC 7.10.3:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\nmodule Data.Conduit.Internal.Pipe where\r\n\r\ndata Pipe o r =\r\n HaveOutput (Pipe o r) o\r\n\r\nmapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r\r\nmapOutputMaybe f (HaveOutput p o) =\r\n maybe id (\\o' p' -> HaveOutput p' o') (f o) (mapOutputMaybe f p)\r\n}}}\r\n\r\nemits a GHC panic with GHC 8.0.1-rc1:\r\n\r\n{{{\r\n[1 of 1] Compiling Data.Conduit.Internal.Pipe ( Wat.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160111 for x86_64-unknown-linux):\r\n\tmatchExpectedFunTys\r\n <>\r\n a_a15Z[tau:5] -> b_a15Y[tau:5]\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nNote that this code does not require `-XImpredicativeTypes`, and removing the pragma makes the code compile again.\r\n\r\nMarking as high since it's a regression, but not highest because `-XImpredicativeTypes` has long been broken (see also #11319). Still, this currently happens on code in the wild, and perhaps it would be worth turning this into a more sensible error.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/10619Order matters when type-checking2019-07-07T18:35:00ZRichard Eisenbergrae@richarde.devOrder matters when type-checkingWhen I say
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo True = (\x -> x) :: (forall a. a -> a) -> forall b. b -> b
foo False = \y -> y
```
the module compiles. But when I say
```
{-# LANGUAGE RankNTypes #-}
module Bug wher...When I say
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo True = (\x -> x) :: (forall a. a -> a) -> forall b. b -> b
foo False = \y -> y
```
the module compiles. But when I say
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo False = \y -> y
foo True = (\x -> x) :: (forall a. a -> a) -> forall b. b -> b
```
it doesn't, failing with
```
Bug.hs:6:13:
Couldn't match type ‘b0 -> b0’ with ‘forall a. a -> a’
Expected type: (forall a. a -> a) -> forall a. a -> a
Actual type: (forall a. a -> a) -> b0 -> b0
In the expression:
(\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
In an equation for ‘foo’:
foo True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
```
I believe this behavior stems from the special case in `tcMonoBinds`, for non-recursive functions without a type signature. I believe the bug would be fixed if that function also checks to make sure that there is precisely one clause to the function. Do you agree?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Order matters when type-checking","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\n\r\nmodule Bug where\r\n\r\nfoo True = (\\x -> x) :: (forall a. a -> a) -> forall b. b -> b\r\nfoo False = \\y -> y\r\n}}}\r\n\r\nthe module compiles. But when I say\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\n\r\nmodule Bug where\r\n\r\nfoo False = \\y -> y\r\nfoo True = (\\x -> x) :: (forall a. a -> a) -> forall b. b -> b\r\n}}}\r\n\r\nit doesn't, failing with\r\n\r\n{{{\r\nBug.hs:6:13:\r\n Couldn't match type ‘b0 -> b0’ with ‘forall a. a -> a’\r\n Expected type: (forall a. a -> a) -> forall a. a -> a\r\n Actual type: (forall a. a -> a) -> b0 -> b0\r\n In the expression:\r\n (\\ x -> x) :: (forall a. a -> a) -> forall b. b -> b\r\n In an equation for ‘foo’:\r\n foo True = (\\ x -> x) :: (forall a. a -> a) -> forall b. b -> b\r\n}}}\r\n\r\nI believe this behavior stems from the special case in `tcMonoBinds`, for non-recursive functions without a type signature. I believe the bug would be fixed if that function also checks to make sure that there is precisely one clause to the function. Do you agree?","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/4295Review higher-rank and impredicative types2020-09-24T18:44:09ZSimon Peyton JonesReview higher-rank and impredicative typesThe ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as `expect_broken` on this ticket, although I think many of them re...The ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as `expect_broken` on this ticket, although I think many of them really should fail.
- tc150
- tc194
- tcfail198
- tcfail174
- tcfail165
- tcfail145
- tcfail104
- tc211
- indexed-types/should_compile/T4120
- simpl017
- Many tests in `boxy/` (see also #1330 for Church2)
- #2193
- #2846
- #4347
- [Lennart's blog post](http://augustss.blogspot.com/2011/07/impredicative-polymorphism-use-case-in.html) has an interesting use case of impredicative polymorphism; it worked in 7.0, but alas not in the new typechecker.8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4281Make impredicativity work properly2020-07-16T17:06:20ZSimon Peyton JonesMake impredicativity work properlyThis ticket is a placeholder for work on impredicativity. In fact, with the new typechecker we have most of the story for impredicativity in place, in the style of QML. Still missing are:
- Rigid type signatures
- Notation for type appl...This ticket is a placeholder for work on impredicativity. In fact, with the new typechecker we have most of the story for impredicativity in place, in the style of QML. Still missing are:
- Rigid type signatures
- Notation for type application
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 6.12.3 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Make impredicativity work properly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"6.12.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"This ticket is a placeholder for work on impredicativity. In fact, with the new typechecker we have most of the story for impredicativity in place, in the style of QML. Still missing are:\r\n * Rigid type signatures\r\n * Notation for type application\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/1330Impredicativity bug: Church2 test gives a rather confusing error with the HEAD2020-09-24T18:35:20ZIan Lynagh <igloo@earth.li>Impredicativity bug: Church2 test gives a rather confusing error with the HEADThe Church2 test gives a rather confusing error with the HEAD:
```
Church2.hs:27:14:
Couldn't match expected type `CNat'
against inferred type `(a -> a) -> a -> a'
Expected type: CNat -> CNat
Inferred type: CN...The Church2 test gives a rather confusing error with the HEAD:
```
Church2.hs:27:14:
Couldn't match expected type `CNat'
against inferred type `(a -> a) -> a -> a'
Expected type: CNat -> CNat
Inferred type: CNat -> CNat
In the first argument of `n', namely `(mul m)'
In the expression: n (mul m) n1
```
In particular the lines
```
Expected type: CNat -> CNat
Inferred type: CNat -> CNat
```
are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Church2 test gives a rather confusing error with the HEAD","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"6.8 branch","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"The Church2 test gives a rather confusing error with the HEAD:\r\n{{{\r\nChurch2.hs:27:14:\r\n Couldn't match expected type `CNat'\r\n against inferred type `(a -> a) -> a -> a'\r\n Expected type: CNat -> CNat\r\n Inferred type: CNat -> CNat\r\n In the first argument of `n', namely `(mul m)'\r\n In the expression: n (mul m) n1\r\n}}}\r\nIn particular the lines\r\n{{{\r\n Expected type: CNat -> CNat\r\n Inferred type: CNat -> CNat\r\n}}}\r\nare confusing, and I'm not sure why it's giving two expected/inferred pairs of types.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Simon Peyton JonesSimon Peyton Jones