GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:29:26Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11624Cannot declare hs-boot declaration if there is already a value in scope2019-07-07T18:29:26ZEdward Z. YangCannot declare hs-boot declaration if there is already a value in scopeThis code no longer works:
```hs
-- A.hs-boot
module A where
concat :: Int -> Int -- overlaps with Prelude's concat
-- B.hs
module B where
import Prelude ()
import {-# SOURCE #-} A
x = concat 3
-- A.hs
module A where
import B
concat n = n + 2
```
Building `ghc --make A`, this crashes with:
```
[1 of 3] Compiling A[boot] ( A.hs-boot, A.o-boot )
[2 of 3] Compiling B ( B.hs, B.o )
B.hs:4:5: error:
• Can't find interface-file declaration for variable concat
Probable cause: bug in .hi-boot file, or inconsistent .hi file
Use -ddump-if-trace to get an idea of which file caused the error
• In the expression: concat 3
In an equation for ‘x’: x = concat 3
```
The trouble is that renaming has botched up the top-level declaration for boot:
```
ezyang@sabre:~$ ghc-8.0 -c A.hs-boot -ddump-rn -dppr-debug
A.hs-boot:1:1:
==================== Renamer ====================
{A.hs-boot:2:1-20}
base-4.9.0.0:Data.Foldable.concat{v r2S} ::
{A.hs-boot:2:11-20}
ghc-prim-0.5.0.0:GHC.Types.Int{(w) tc 3J}
-> ghc-prim-0.5.0.0:GHC.Types.Int{(w) tc 3J}
```
Is a regression from 7.10. The dodginess is proximal to `renameSig` but I haven't quite narrowed it down yet.This code no longer works:
```hs
-- A.hs-boot
module A where
concat :: Int -> Int -- overlaps with Prelude's concat
-- B.hs
module B where
import Prelude ()
import {-# SOURCE #-} A
x = concat 3
-- A.hs
module A where
import B
concat n = n + 2
```
Building `ghc --make A`, this crashes with:
```
[1 of 3] Compiling A[boot] ( A.hs-boot, A.o-boot )
[2 of 3] Compiling B ( B.hs, B.o )
B.hs:4:5: error:
• Can't find interface-file declaration for variable concat
Probable cause: bug in .hi-boot file, or inconsistent .hi file
Use -ddump-if-trace to get an idea of which file caused the error
• In the expression: concat 3
In an equation for ‘x’: x = concat 3
```
The trouble is that renaming has botched up the top-level declaration for boot:
```
ezyang@sabre:~$ ghc-8.0 -c A.hs-boot -ddump-rn -dppr-debug
A.hs-boot:1:1:
==================== Renamer ====================
{A.hs-boot:2:1-20}
base-4.9.0.0:Data.Foldable.concat{v r2S} ::
{A.hs-boot:2:11-20}
ghc-prim-0.5.0.0:GHC.Types.Int{(w) tc 3J}
-> ghc-prim-0.5.0.0:GHC.Types.Int{(w) tc 3J}
```
Is a regression from 7.10. The dodginess is proximal to `renameSig` but I haven't quite narrowed it down yet.8.0.1Edward Z. YangEdward Z. Yanghttps://gitlab.haskell.org/ghc/ghc/-/issues/11608Possible type-checker regression in GHC 8.0 when compiling `microlens`2019-07-07T18:29:37ZHerbert Valerio Riedelhvr@gnu.orgPossible type-checker regression in GHC 8.0 when compiling `microlens`I just updated the GHC 8.0 snapshot I was using from 8.0.0.20160214-g977fb8 to 8.0.0.20160218-g23baff7, and suddenly hackage:microlens-0.4.2.0 fails to build with
```
...
Preprocessing library microlens-0.4.2.0...
[1 of 4] Compiling Lens.Micro.Type ( src/Lens/Micro/Type.hs, dist/build/Lens/Micro/Type.o )
[2 of 4] Compiling Lens.Micro.Internal ( src/Lens/Micro/Internal.hs, dist/build/Lens/Micro/Internal.o )
src/Lens/Micro/Internal.hs:184:3: error:
• Couldn't match type ‘s’ with ‘g0 a’
‘s’ is untouchable
inside the constraints: (Traversable g,
s ~ g a,
t ~ g b,
Applicative f)
bound by the type signature for:
each :: (Traversable g, s ~ g a, t ~ g b, Applicative f) =>
(a -> f b) -> s -> f t
at src/Lens/Micro/Internal.hs:184:3-27
• In the ambiguity check for ‘each’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
each :: forall s t a b. Each s t a b => Traversal s t a b
In the class declaration for ‘Each’
```
1. ..is this a regression or a feature? :-)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0 when compiling `microlens`","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I just updated the GHC 8.0 snapshot I was using from 8.0.0.20160214-g977fb8 to 8.0.0.20160218-g23baff7, and suddenly hackage:microlens-0.4.2.0 fails to build with\r\n\r\n{{{\r\n...\r\nPreprocessing library microlens-0.4.2.0...\r\n[1 of 4] Compiling Lens.Micro.Type ( src/Lens/Micro/Type.hs, dist/build/Lens/Micro/Type.o )\r\n[2 of 4] Compiling Lens.Micro.Internal ( src/Lens/Micro/Internal.hs, dist/build/Lens/Micro/Internal.o )\r\n\r\nsrc/Lens/Micro/Internal.hs:184:3: error:\r\n • Couldn't match type ‘s’ with ‘g0 a’\r\n ‘s’ is untouchable\r\n inside the constraints: (Traversable g,\r\n s ~ g a,\r\n t ~ g b,\r\n Applicative f)\r\n bound by the type signature for:\r\n each :: (Traversable g, s ~ g a, t ~ g b, Applicative f) =>\r\n (a -> f b) -> s -> f t\r\n at src/Lens/Micro/Internal.hs:184:3-27\r\n • In the ambiguity check for ‘each’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the class method:\r\n each :: forall s t a b. Each s t a b => Traversal s t a b\r\n In the class declaration for ‘Each’\r\n}}}\r\n\r\n...is this a regression or a feature? :-)","type_of_failure":"OtherFailure","blocking":[]} -->I just updated the GHC 8.0 snapshot I was using from 8.0.0.20160214-g977fb8 to 8.0.0.20160218-g23baff7, and suddenly hackage:microlens-0.4.2.0 fails to build with
```
...
Preprocessing library microlens-0.4.2.0...
[1 of 4] Compiling Lens.Micro.Type ( src/Lens/Micro/Type.hs, dist/build/Lens/Micro/Type.o )
[2 of 4] Compiling Lens.Micro.Internal ( src/Lens/Micro/Internal.hs, dist/build/Lens/Micro/Internal.o )
src/Lens/Micro/Internal.hs:184:3: error:
• Couldn't match type ‘s’ with ‘g0 a’
‘s’ is untouchable
inside the constraints: (Traversable g,
s ~ g a,
t ~ g b,
Applicative f)
bound by the type signature for:
each :: (Traversable g, s ~ g a, t ~ g b, Applicative f) =>
(a -> f b) -> s -> f t
at src/Lens/Micro/Internal.hs:184:3-27
• In the ambiguity check for ‘each’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
each :: forall s t a b. Each s t a b => Traversal s t a b
In the class declaration for ‘Each’
```
1. ..is this a regression or a feature? :-)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0 when compiling `microlens`","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I just updated the GHC 8.0 snapshot I was using from 8.0.0.20160214-g977fb8 to 8.0.0.20160218-g23baff7, and suddenly hackage:microlens-0.4.2.0 fails to build with\r\n\r\n{{{\r\n...\r\nPreprocessing library microlens-0.4.2.0...\r\n[1 of 4] Compiling Lens.Micro.Type ( src/Lens/Micro/Type.hs, dist/build/Lens/Micro/Type.o )\r\n[2 of 4] Compiling Lens.Micro.Internal ( src/Lens/Micro/Internal.hs, dist/build/Lens/Micro/Internal.o )\r\n\r\nsrc/Lens/Micro/Internal.hs:184:3: error:\r\n • Couldn't match type ‘s’ with ‘g0 a’\r\n ‘s’ is untouchable\r\n inside the constraints: (Traversable g,\r\n s ~ g a,\r\n t ~ g b,\r\n Applicative f)\r\n bound by the type signature for:\r\n each :: (Traversable g, s ~ g a, t ~ g b, Applicative f) =>\r\n (a -> f b) -> s -> f t\r\n at src/Lens/Micro/Internal.hs:184:3-27\r\n • In the ambiguity check for ‘each’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the class method:\r\n each :: forall s t a b. Each s t a b => Traversal s t a b\r\n In the class declaration for ‘Each’\r\n}}}\r\n\r\n...is this a regression or a feature? :-)","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11520GHC falls into a hole if given incorrect kind signature2019-07-07T18:30:05ZBen GamariGHC falls into a hole if given incorrect kind signatureIf one provides an incorrect kind signature GHC throws up. For instance, this non-sense,
```hs
{-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-}
module Play where
import GHC.Types hiding (TyCon)
data TypeRep (a :: k)
class Typeable k => Typeable (a :: k) where
typeRep :: TypeRep a
data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a))
-- Note how the kind signature on g is incorrect
instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where
typeRep = undefined
```
fails with
```
λ> :load Bug.hs
[1 of 1] Compiling Play ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160122 for x86_64-unknown-linux):
fvProv falls into a hole {abet}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```If one provides an incorrect kind signature GHC throws up. For instance, this non-sense,
```hs
{-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-}
module Play where
import GHC.Types hiding (TyCon)
data TypeRep (a :: k)
class Typeable k => Typeable (a :: k) where
typeRep :: TypeRep a
data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a))
-- Note how the kind signature on g is incorrect
instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where
typeRep = undefined
```
fails with
```
λ> :load Bug.hs
[1 of 1] Compiling Play ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160122 for x86_64-unknown-linux):
fvProv falls into a hole {abet}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11458Terrible failure of type inference in visible type application2019-07-07T18:30:20ZSimon Peyton JonesTerrible failure of type inference in visible type applicationConsider
```
-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)
optIntArg f = (f Nothing, f (Just True))
```
This is rejected (by HEAD)
```
T11379a.hs:5:30: error:
* Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at T11379a.hs:5:30
Expected type: forall a. Maybe a
Actual type: Maybe Bool
* In the first argument of `f', namely `(Just True)'
In the expression: f (Just True)
In the expression: (f Nothing, f (Just True))
```
but if you put the tuple components the other way round, it works fine
```
optIntArg f = (f (Just True), f Nothing)
```
Adding the commented-out signature also makes it work fine.
I'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.
I suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Terrible failure of type inference in visible type application","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)\r\noptIntArg f = (f Nothing, f (Just True))\r\n}}}\r\nThis is rejected (by HEAD)\r\n{{{\r\nT11379a.hs:5:30: error:\r\n * Couldn't match type `a' with `Bool'\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 T11379a.hs:5:30\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe Bool\r\n * In the first argument of `f', namely `(Just True)'\r\n In the expression: f (Just True)\r\n In the expression: (f Nothing, f (Just True))\r\n}}}\r\nbut if you put the tuple components the other way round, it works fine\r\n{{{\r\noptIntArg f = (f (Just True), f Nothing)\r\n}}}\r\nAdding the commented-out signature also makes it work fine.\r\n\r\nI'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.\r\n\r\nI suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Consider
```
-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)
optIntArg f = (f Nothing, f (Just True))
```
This is rejected (by HEAD)
```
T11379a.hs:5:30: error:
* Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at T11379a.hs:5:30
Expected type: forall a. Maybe a
Actual type: Maybe Bool
* In the first argument of `f', namely `(Just True)'
In the expression: f (Just True)
In the expression: (f Nothing, f (Just True))
```
but if you put the tuple components the other way round, it works fine
```
optIntArg f = (f (Just True), f Nothing)
```
Adding the commented-out signature also makes it work fine.
I'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.
I suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Terrible failure of type inference in visible type application","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)\r\noptIntArg f = (f Nothing, f (Just True))\r\n}}}\r\nThis is rejected (by HEAD)\r\n{{{\r\nT11379a.hs:5:30: error:\r\n * Couldn't match type `a' with `Bool'\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 T11379a.hs:5:30\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe Bool\r\n * In the first argument of `f', namely `(Just True)'\r\n In the expression: f (Just True)\r\n In the expression: (f Nothing, f (Just True))\r\n}}}\r\nbut if you put the tuple components the other way round, it works fine\r\n{{{\r\noptIntArg f = (f (Just True), f Nothing)\r\n}}}\r\nAdding the commented-out signature also makes it work fine.\r\n\r\nI'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.\r\n\r\nI suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11407-XTypeInType uses up all memory when used in data family instance2019-07-07T18:30:33ZRyan Scott-XTypeInType uses up all memory when used in data family instanceCompiling this code with GHC 8.1 causes all my memory to be used very quickly:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data family UhOh (f :: k1) (a :: k2) (b :: k3)
data instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
On the other hand, this code compiles without issue:
```hs
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-XTypeInType uses up all memory when used in data family instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Compiling this code with GHC 8.1 causes all my memory to be used very quickly:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata family UhOh (f :: k1) (a :: k2) (b :: k3)\r\ndata instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}\r\n\r\nOn the other hand, this code compiles without issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Compiling this code with GHC 8.1 causes all my memory to be used very quickly:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data family UhOh (f :: k1) (a :: k2) (b :: k3)
data instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
On the other hand, this code compiles without issue:
```hs
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-XTypeInType uses up all memory when used in data family instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Compiling this code with GHC 8.1 causes all my memory to be used very quickly:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata family UhOh (f :: k1) (a :: k2) (b :: k3)\r\ndata instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}\r\n\r\nOn the other hand, this code compiles without issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11399Ill-kinded instance head involving -XTypeInType can invoke GHC panic2019-07-07T18:30:35ZRyan ScottIll-kinded instance head involving -XTypeInType can invoke GHC panicThis code:
```hs
{-# LANGUAGE FlexibleInstances, TypeInType #-}
module FvProvFallsIntoAHole where
import Data.Kind
newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)
instance Functor k => Functor (UhOh k) where
```
produces this GHC panic:
```
$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs
[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160108 for x86_64-unknown-linux):
fvProv falls into a hole {aq6}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Ill-kinded instance head involving -XTypeInType can invoke GHC panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances, TypeInType #-}\r\nmodule FvProvFallsIntoAHole where\r\n\r\nimport Data.Kind\r\n\r\nnewtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)\r\ninstance Functor k => Functor (UhOh k) where\r\n}}}\r\n\r\nproduces this GHC panic:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs\r\n[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160108 for x86_64-unknown-linux):\r\n fvProv falls into a hole {aq6}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->This code:
```hs
{-# LANGUAGE FlexibleInstances, TypeInType #-}
module FvProvFallsIntoAHole where
import Data.Kind
newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)
instance Functor k => Functor (UhOh k) where
```
produces this GHC panic:
```
$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs
[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160108 for x86_64-unknown-linux):
fvProv falls into a hole {aq6}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Ill-kinded instance head involving -XTypeInType can invoke GHC panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances, TypeInType #-}\r\nmodule FvProvFallsIntoAHole where\r\n\r\nimport Data.Kind\r\n\r\nnewtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)\r\ninstance Functor k => Functor (UhOh k) where\r\n}}}\r\n\r\nproduces this GHC panic:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs\r\n[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160108 for x86_64-unknown-linux):\r\n fvProv falls into a hole {aq6}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11397Type mismatch in local definitions in Haskell 98 code2019-07-07T18:30:36ZLemmingType mismatch in local definitions in Haskell 98 codeHere is the affected code with all package dependencies removes:
```
$ cat PairMismatch.hs
module PairMismatch (inverseFrequencyModulationChunk) where
newtype VectorLazy a = VectorLazy a
newtype Vector a = Vector a
newtype Pointer a = Pointer a
empty :: VectorLazy a
empty = undefined
cons :: Vector a -> Pointer a
cons = undefined
unfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)
unfoldrResult = undefined
switchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b
switchL = undefined
inverseFrequencyModulationChunk ::
(Num t, Ord t) =>
(s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))
inverseFrequencyModulationChunk nextC (phase,cst0) chunk =
let {-
switch ::
(Maybe (t, s) -> r) ->
((t, v) -> (s, Pointer v) -> r) ->
t ->
(s, Pointer v) -> r
-}
switch l r t (cp0,xp0) =
maybe
(l Nothing)
(\(c1,cp1) ->
switchL
(l (Just (t,cp0)))
(\x1 xp1 -> r (t+c1,x1) (cp1,xp1))
xp0)
(nextC cp0)
{-
go ::
(t,v) -> (s, Pointer v) ->
Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))
-}
go (c,x) cxp =
if c<1
then switch Left go c cxp
else Right (x, ((c-1,x),cxp))
in switch ((,) empty)
(curry $ unfoldrResult (uncurry go))
phase (cst0, cons chunk)
$ ghci-8.0.0.20160109 PairMismatch.hs
GHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )
PairMismatch.hs:35:24: error:
• Couldn't match type ‘a’ with ‘(t, s)’
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at PairMismatch.hs:35:24
Expected type: forall a. Maybe a
Actual type: Maybe (t, s)
• In the first argument of ‘l’, namely ‘(Just (t, cp0))’
In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’
In the expression:
switchL
(l (Just (t, cp0))) (\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0
• Relevant bindings include
cp1 :: s (bound at PairMismatch.hs:33:20)
c1 :: t (bound at PairMismatch.hs:33:17)
cp0 :: s (bound at PairMismatch.hs:30:22)
t :: t (bound at PairMismatch.hs:30:19)
r :: (t, t1) -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:17)
switch :: ((forall a. Maybe a) -> b)
-> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:8)
inverseFrequencyModulationChunk :: (s -> Maybe (t, s))
-> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))
(bound at PairMismatch.hs:22:1)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
Failed, modules loaded: none.
```
It works with GHC-7.10.3 and before.
I may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type mismatch in local definitions in Haskell 98 code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is the affected code with all package dependencies removes:\r\n{{{\r\n$ cat PairMismatch.hs\r\nmodule PairMismatch (inverseFrequencyModulationChunk) where\r\n\r\nnewtype VectorLazy a = VectorLazy a\r\nnewtype Vector a = Vector a\r\nnewtype Pointer a = Pointer a\r\n\r\nempty :: VectorLazy a\r\nempty = undefined\r\n\r\ncons :: Vector a -> Pointer a\r\ncons = undefined\r\n\r\nunfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)\r\nunfoldrResult = undefined\r\n\r\nswitchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b\r\nswitchL = undefined\r\n\r\ninverseFrequencyModulationChunk ::\r\n (Num t, Ord t) =>\r\n (s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))\r\ninverseFrequencyModulationChunk nextC (phase,cst0) chunk =\r\n let {-\r\n switch ::\r\n (Maybe (t, s) -> r) ->\r\n ((t, v) -> (s, Pointer v) -> r) ->\r\n t ->\r\n (s, Pointer v) -> r\r\n -}\r\n switch l r t (cp0,xp0) =\r\n maybe\r\n (l Nothing)\r\n (\\(c1,cp1) ->\r\n switchL\r\n (l (Just (t,cp0)))\r\n (\\x1 xp1 -> r (t+c1,x1) (cp1,xp1))\r\n xp0)\r\n (nextC cp0)\r\n\r\n {-\r\n go ::\r\n (t,v) -> (s, Pointer v) ->\r\n Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))\r\n -}\r\n go (c,x) cxp =\r\n if c<1\r\n then switch Left go c cxp\r\n else Right (x, ((c-1,x),cxp))\r\n\r\n in switch ((,) empty)\r\n (curry $ unfoldrResult (uncurry go))\r\n phase (cst0, cons chunk)\r\n\r\n$ ghci-8.0.0.20160109 PairMismatch.hs \r\nGHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )\r\n\r\nPairMismatch.hs:35:24: error:\r\n • Couldn't match type ‘a’ with ‘(t, s)’\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 PairMismatch.hs:35:24\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe (t, s)\r\n • In the first argument of ‘l’, namely ‘(Just (t, cp0))’\r\n In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’\r\n In the expression:\r\n switchL\r\n (l (Just (t, cp0))) (\\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0\r\n • Relevant bindings include\r\n cp1 :: s (bound at PairMismatch.hs:33:20)\r\n c1 :: t (bound at PairMismatch.hs:33:17)\r\n cp0 :: s (bound at PairMismatch.hs:30:22)\r\n t :: t (bound at PairMismatch.hs:30:19)\r\n r :: (t, t1) -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:17)\r\n switch :: ((forall a. Maybe a) -> b)\r\n -> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:8)\r\n inverseFrequencyModulationChunk :: (s -> Maybe (t, s))\r\n -> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))\r\n (bound at PairMismatch.hs:22:1)\r\n (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)\r\nFailed, modules loaded: none.\r\n}}}\r\nIt works with GHC-7.10.3 and before.\r\nI may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Here is the affected code with all package dependencies removes:
```
$ cat PairMismatch.hs
module PairMismatch (inverseFrequencyModulationChunk) where
newtype VectorLazy a = VectorLazy a
newtype Vector a = Vector a
newtype Pointer a = Pointer a
empty :: VectorLazy a
empty = undefined
cons :: Vector a -> Pointer a
cons = undefined
unfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)
unfoldrResult = undefined
switchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b
switchL = undefined
inverseFrequencyModulationChunk ::
(Num t, Ord t) =>
(s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))
inverseFrequencyModulationChunk nextC (phase,cst0) chunk =
let {-
switch ::
(Maybe (t, s) -> r) ->
((t, v) -> (s, Pointer v) -> r) ->
t ->
(s, Pointer v) -> r
-}
switch l r t (cp0,xp0) =
maybe
(l Nothing)
(\(c1,cp1) ->
switchL
(l (Just (t,cp0)))
(\x1 xp1 -> r (t+c1,x1) (cp1,xp1))
xp0)
(nextC cp0)
{-
go ::
(t,v) -> (s, Pointer v) ->
Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))
-}
go (c,x) cxp =
if c<1
then switch Left go c cxp
else Right (x, ((c-1,x),cxp))
in switch ((,) empty)
(curry $ unfoldrResult (uncurry go))
phase (cst0, cons chunk)
$ ghci-8.0.0.20160109 PairMismatch.hs
GHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )
PairMismatch.hs:35:24: error:
• Couldn't match type ‘a’ with ‘(t, s)’
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at PairMismatch.hs:35:24
Expected type: forall a. Maybe a
Actual type: Maybe (t, s)
• In the first argument of ‘l’, namely ‘(Just (t, cp0))’
In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’
In the expression:
switchL
(l (Just (t, cp0))) (\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0
• Relevant bindings include
cp1 :: s (bound at PairMismatch.hs:33:20)
c1 :: t (bound at PairMismatch.hs:33:17)
cp0 :: s (bound at PairMismatch.hs:30:22)
t :: t (bound at PairMismatch.hs:30:19)
r :: (t, t1) -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:17)
switch :: ((forall a. Maybe a) -> b)
-> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:8)
inverseFrequencyModulationChunk :: (s -> Maybe (t, s))
-> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))
(bound at PairMismatch.hs:22:1)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
Failed, modules loaded: none.
```
It works with GHC-7.10.3 and before.
I may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type mismatch in local definitions in Haskell 98 code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is the affected code with all package dependencies removes:\r\n{{{\r\n$ cat PairMismatch.hs\r\nmodule PairMismatch (inverseFrequencyModulationChunk) where\r\n\r\nnewtype VectorLazy a = VectorLazy a\r\nnewtype Vector a = Vector a\r\nnewtype Pointer a = Pointer a\r\n\r\nempty :: VectorLazy a\r\nempty = undefined\r\n\r\ncons :: Vector a -> Pointer a\r\ncons = undefined\r\n\r\nunfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)\r\nunfoldrResult = undefined\r\n\r\nswitchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b\r\nswitchL = undefined\r\n\r\ninverseFrequencyModulationChunk ::\r\n (Num t, Ord t) =>\r\n (s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))\r\ninverseFrequencyModulationChunk nextC (phase,cst0) chunk =\r\n let {-\r\n switch ::\r\n (Maybe (t, s) -> r) ->\r\n ((t, v) -> (s, Pointer v) -> r) ->\r\n t ->\r\n (s, Pointer v) -> r\r\n -}\r\n switch l r t (cp0,xp0) =\r\n maybe\r\n (l Nothing)\r\n (\\(c1,cp1) ->\r\n switchL\r\n (l (Just (t,cp0)))\r\n (\\x1 xp1 -> r (t+c1,x1) (cp1,xp1))\r\n xp0)\r\n (nextC cp0)\r\n\r\n {-\r\n go ::\r\n (t,v) -> (s, Pointer v) ->\r\n Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))\r\n -}\r\n go (c,x) cxp =\r\n if c<1\r\n then switch Left go c cxp\r\n else Right (x, ((c-1,x),cxp))\r\n\r\n in switch ((,) empty)\r\n (curry $ unfoldrResult (uncurry go))\r\n phase (cst0, cons chunk)\r\n\r\n$ ghci-8.0.0.20160109 PairMismatch.hs \r\nGHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )\r\n\r\nPairMismatch.hs:35:24: error:\r\n • Couldn't match type ‘a’ with ‘(t, s)’\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 PairMismatch.hs:35:24\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe (t, s)\r\n • In the first argument of ‘l’, namely ‘(Just (t, cp0))’\r\n In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’\r\n In the expression:\r\n switchL\r\n (l (Just (t, cp0))) (\\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0\r\n • Relevant bindings include\r\n cp1 :: s (bound at PairMismatch.hs:33:20)\r\n c1 :: t (bound at PairMismatch.hs:33:17)\r\n cp0 :: s (bound at PairMismatch.hs:30:22)\r\n t :: t (bound at PairMismatch.hs:30:19)\r\n r :: (t, t1) -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:17)\r\n switch :: ((forall a. Maybe a) -> b)\r\n -> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:8)\r\n inverseFrequencyModulationChunk :: (s -> Maybe (t, s))\r\n -> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))\r\n (bound at PairMismatch.hs:22:1)\r\n (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)\r\nFailed, modules loaded: none.\r\n}}}\r\nIt works with GHC-7.10.3 and before.\r\nI may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11364Possible type-checker regression in GHC 8.02019-07-07T18:30:44ZHerbert Valerio Riedelhvr@gnu.orgPossible type-checker regression in GHC 8.0The following code fragment works with GHCs prior to GHC 8.0 but not with GHC 8.0:
```hs
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE RankNTypes #-}
module Issue where
import Data.Coerce (coerce)
data Proxy a = Proxy
newtype Catch a = Catch a
class Throws e
type role Throws representational
instance Throws (Catch e)
newtype Wrap e a = Wrap { unWrap :: Throws e => a }
coerceWrap :: Wrap e a -> Wrap (Catch e) a
coerceWrap = coerce
unthrow :: proxy e -> (Throws e => a) -> a
unthrow _ = unWrap . coerceWrap . Wrap
{- this works in GHC 7.10.3, but fails in GHC 8.0 with
GHCi, version 8.0.0.20160105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Issue ( Issue.hs, interpreted )
Issue.hs:25:13: error:
• Could not deduce (Throws e)
from the context: Throws e0
bound by a type expected by the context:
Throws e0 => a
at Issue.hs:26:13-38
Possible fix:
add (Throws e) to the context of
the type signature for:
unthrow :: proxy e -> (Throws e => a) -> a
• In the expression: unWrap . coerceWrap . Wrap
In an equation for ‘unthrow’: unthrow _ = unWrap . coerceWrap . Wrap
Failed, modules loaded: none.
-}
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, goldfire, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","goldfire","simonpj"],"type":"Bug","description":"The following code fragment works with GHCs prior to GHC 8.0 but not with GHC 8.0:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RoleAnnotations #-}\r\n{-# LANGUAGE IncoherentInstances #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n\r\nmodule Issue where\r\n\r\nimport Data.Coerce (coerce)\r\n\r\ndata Proxy a = Proxy\r\n\r\nnewtype Catch a = Catch a\r\n\r\nclass Throws e\r\n\r\ntype role Throws representational\r\n\r\ninstance Throws (Catch e)\r\n\r\nnewtype Wrap e a = Wrap { unWrap :: Throws e => a }\r\n\r\ncoerceWrap :: Wrap e a -> Wrap (Catch e) a\r\ncoerceWrap = coerce\r\n\r\nunthrow :: proxy e -> (Throws e => a) -> a\r\nunthrow _ = unWrap . coerceWrap . Wrap\r\n\r\n{- this works in GHC 7.10.3, but fails in GHC 8.0 with\r\n\r\nGHCi, version 8.0.0.20160105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Issue ( Issue.hs, interpreted )\r\n\r\nIssue.hs:25:13: error:\r\n • Could not deduce (Throws e)\r\n from the context: Throws e0\r\n bound by a type expected by the context:\r\n Throws e0 => a\r\n at Issue.hs:26:13-38\r\n Possible fix:\r\n add (Throws e) to the context of\r\n the type signature for:\r\n unthrow :: proxy e -> (Throws e => a) -> a\r\n • In the expression: unWrap . coerceWrap . Wrap\r\n In an equation for ‘unthrow’: unthrow _ = unWrap . coerceWrap . Wrap\r\nFailed, modules loaded: none.\r\n-}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->The following code fragment works with GHCs prior to GHC 8.0 but not with GHC 8.0:
```hs
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE RankNTypes #-}
module Issue where
import Data.Coerce (coerce)
data Proxy a = Proxy
newtype Catch a = Catch a
class Throws e
type role Throws representational
instance Throws (Catch e)
newtype Wrap e a = Wrap { unWrap :: Throws e => a }
coerceWrap :: Wrap e a -> Wrap (Catch e) a
coerceWrap = coerce
unthrow :: proxy e -> (Throws e => a) -> a
unthrow _ = unWrap . coerceWrap . Wrap
{- this works in GHC 7.10.3, but fails in GHC 8.0 with
GHCi, version 8.0.0.20160105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Issue ( Issue.hs, interpreted )
Issue.hs:25:13: error:
• Could not deduce (Throws e)
from the context: Throws e0
bound by a type expected by the context:
Throws e0 => a
at Issue.hs:26:13-38
Possible fix:
add (Throws e) to the context of
the type signature for:
unthrow :: proxy e -> (Throws e => a) -> a
• In the expression: unWrap . coerceWrap . Wrap
In an equation for ‘unthrow’: unthrow _ = unWrap . coerceWrap . Wrap
Failed, modules loaded: none.
-}
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, goldfire, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","goldfire","simonpj"],"type":"Bug","description":"The following code fragment works with GHCs prior to GHC 8.0 but not with GHC 8.0:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RoleAnnotations #-}\r\n{-# LANGUAGE IncoherentInstances #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n\r\nmodule Issue where\r\n\r\nimport Data.Coerce (coerce)\r\n\r\ndata Proxy a = Proxy\r\n\r\nnewtype Catch a = Catch a\r\n\r\nclass Throws e\r\n\r\ntype role Throws representational\r\n\r\ninstance Throws (Catch e)\r\n\r\nnewtype Wrap e a = Wrap { unWrap :: Throws e => a }\r\n\r\ncoerceWrap :: Wrap e a -> Wrap (Catch e) a\r\ncoerceWrap = coerce\r\n\r\nunthrow :: proxy e -> (Throws e => a) -> a\r\nunthrow _ = unWrap . coerceWrap . Wrap\r\n\r\n{- this works in GHC 7.10.3, but fails in GHC 8.0 with\r\n\r\nGHCi, version 8.0.0.20160105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Issue ( Issue.hs, interpreted )\r\n\r\nIssue.hs:25:13: error:\r\n • Could not deduce (Throws e)\r\n from the context: Throws e0\r\n bound by a type expected by the context:\r\n Throws e0 => a\r\n at Issue.hs:26:13-38\r\n Possible fix:\r\n add (Throws e) to the context of\r\n the type signature for:\r\n unthrow :: proxy e -> (Throws e => a) -> a\r\n • In the expression: unWrap . coerceWrap . Wrap\r\n In an equation for ‘unthrow’: unthrow _ = unWrap . coerceWrap . Wrap\r\nFailed, modules loaded: none.\r\n-}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11339Possible type-checker regression in GHC 8.02019-07-07T18:30:52ZHerbert Valerio Riedelhvr@gnu.orgPossible type-checker regression in GHC 8.0The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but **not** on GHC 8.0/8.1:
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Failing where
import Control.Applicative ( Const(Const, getConst) )
import Data.Functor.Identity ( Identity(Identity) )
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
failing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
[] -> right afb s
_ -> t afb
where
-- t :: (a -> f b) -> f t
-- TYPECHECKS with GHC 7.10, but not with GHC 8.x:
Bazaar { getBazaar = t } = left sell s
-- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:
-- t = getBazaar (left sell s)
sell :: a -> Bazaar a b b
sell w = Bazaar ($ w)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]
pins f = getConst (f (\ra -> Const [Identity ra]))
newtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }
instance Functor (Bazaar a b) where
fmap f (Bazaar k) = Bazaar (fmap f . k)
instance Applicative (Bazaar a b) where
pure a = Bazaar $ \_ -> pure a
Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb
```
The following error is emitted on GHC 8.0:
```
failing.hs:13:11: error:
• Couldn't match type ‘f’ with ‘Const [Identity a]’
‘f’ is a rigid type variable bound by
the type signature for:
failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t
at failing.hs:11:1
Expected type: a -> Const [Identity a] b
Actual type: a -> f b
• In the first argument of ‘t’, namely ‘afb’
In the expression: t afb
In a case alternative: _ -> t afb
• Relevant bindings include
t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)
sell :: a -> Bazaar a b b (bound at failing.hs:24:5)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)
afb :: a -> f b (bound at failing.hs:11:20)
right :: Traversal s t a b (bound at failing.hs:11:14)
left :: Traversal s t a b (bound at failing.hs:11:9)
failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)
```
I don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","simonpj"],"type":"Bug","description":"The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but '''not''' on GHC 8.0/8.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}\r\n\r\nmodule Failing where\r\n\r\nimport Control.Applicative ( Const(Const, getConst) )\r\nimport Data.Functor.Identity ( Identity(Identity) )\r\n\r\ntype Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t\r\n\r\nfailing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b\r\nfailing left right afb s = case pins t of\r\n [] -> right afb s\r\n _ -> t afb\r\n where\r\n -- t :: (a -> f b) -> f t\r\n\r\n -- TYPECHECKS with GHC 7.10, but not with GHC 8.x:\r\n Bazaar { getBazaar = t } = left sell s\r\n\r\n -- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:\r\n -- t = getBazaar (left sell s)\r\n\r\n sell :: a -> Bazaar a b b\r\n sell w = Bazaar ($ w)\r\n\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]\r\n pins f = getConst (f (\\ra -> Const [Identity ra]))\r\n\r\nnewtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }\r\n\r\ninstance Functor (Bazaar a b) where\r\n fmap f (Bazaar k) = Bazaar (fmap f . k)\r\n\r\ninstance Applicative (Bazaar a b) where\r\n pure a = Bazaar $ \\_ -> pure a\r\n Bazaar mf <*> Bazaar ma = Bazaar $ \\afb -> mf afb <*> ma afb\r\n}}}\r\n\r\nThe following error is emitted on GHC 8.0:\r\n\r\n{{{\r\nfailing.hs:13:11: error:\r\n • Couldn't match type ‘f’ with ‘Const [Identity a]’\r\n ‘f’ is a rigid type variable bound by\r\n the type signature for:\r\n failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t\r\n at failing.hs:11:1\r\n Expected type: a -> Const [Identity a] b\r\n Actual type: a -> f b\r\n • In the first argument of ‘t’, namely ‘afb’\r\n In the expression: t afb\r\n In a case alternative: _ -> t afb\r\n • Relevant bindings include\r\n t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)\r\n sell :: a -> Bazaar a b b (bound at failing.hs:24:5)\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)\r\n afb :: a -> f b (bound at failing.hs:11:20)\r\n right :: Traversal s t a b (bound at failing.hs:11:14)\r\n left :: Traversal s t a b (bound at failing.hs:11:9)\r\n failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)\r\n}}}\r\n\r\n\r\nI don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...","type_of_failure":"OtherFailure","blocking":[]} -->The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but **not** on GHC 8.0/8.1:
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Failing where
import Control.Applicative ( Const(Const, getConst) )
import Data.Functor.Identity ( Identity(Identity) )
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
failing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
[] -> right afb s
_ -> t afb
where
-- t :: (a -> f b) -> f t
-- TYPECHECKS with GHC 7.10, but not with GHC 8.x:
Bazaar { getBazaar = t } = left sell s
-- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:
-- t = getBazaar (left sell s)
sell :: a -> Bazaar a b b
sell w = Bazaar ($ w)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]
pins f = getConst (f (\ra -> Const [Identity ra]))
newtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }
instance Functor (Bazaar a b) where
fmap f (Bazaar k) = Bazaar (fmap f . k)
instance Applicative (Bazaar a b) where
pure a = Bazaar $ \_ -> pure a
Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb
```
The following error is emitted on GHC 8.0:
```
failing.hs:13:11: error:
• Couldn't match type ‘f’ with ‘Const [Identity a]’
‘f’ is a rigid type variable bound by
the type signature for:
failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t
at failing.hs:11:1
Expected type: a -> Const [Identity a] b
Actual type: a -> f b
• In the first argument of ‘t’, namely ‘afb’
In the expression: t afb
In a case alternative: _ -> t afb
• Relevant bindings include
t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)
sell :: a -> Bazaar a b b (bound at failing.hs:24:5)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)
afb :: a -> f b (bound at failing.hs:11:20)
right :: Traversal s t a b (bound at failing.hs:11:14)
left :: Traversal s t a b (bound at failing.hs:11:9)
failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)
```
I don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","simonpj"],"type":"Bug","description":"The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but '''not''' on GHC 8.0/8.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}\r\n\r\nmodule Failing where\r\n\r\nimport Control.Applicative ( Const(Const, getConst) )\r\nimport Data.Functor.Identity ( Identity(Identity) )\r\n\r\ntype Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t\r\n\r\nfailing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b\r\nfailing left right afb s = case pins t of\r\n [] -> right afb s\r\n _ -> t afb\r\n where\r\n -- t :: (a -> f b) -> f t\r\n\r\n -- TYPECHECKS with GHC 7.10, but not with GHC 8.x:\r\n Bazaar { getBazaar = t } = left sell s\r\n\r\n -- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:\r\n -- t = getBazaar (left sell s)\r\n\r\n sell :: a -> Bazaar a b b\r\n sell w = Bazaar ($ w)\r\n\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]\r\n pins f = getConst (f (\\ra -> Const [Identity ra]))\r\n\r\nnewtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }\r\n\r\ninstance Functor (Bazaar a b) where\r\n fmap f (Bazaar k) = Bazaar (fmap f . k)\r\n\r\ninstance Applicative (Bazaar a b) where\r\n pure a = Bazaar $ \\_ -> pure a\r\n Bazaar mf <*> Bazaar ma = Bazaar $ \\afb -> mf afb <*> ma afb\r\n}}}\r\n\r\nThe following error is emitted on GHC 8.0:\r\n\r\n{{{\r\nfailing.hs:13:11: error:\r\n • Couldn't match type ‘f’ with ‘Const [Identity a]’\r\n ‘f’ is a rigid type variable bound by\r\n the type signature for:\r\n failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t\r\n at failing.hs:11:1\r\n Expected type: a -> Const [Identity a] b\r\n Actual type: a -> f b\r\n • In the first argument of ‘t’, namely ‘afb’\r\n In the expression: t afb\r\n In a case alternative: _ -> t afb\r\n • Relevant bindings include\r\n t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)\r\n sell :: a -> Bazaar a b b (bound at failing.hs:24:5)\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)\r\n afb :: a -> f b (bound at failing.hs:11:20)\r\n right :: Traversal s t a b (bound at failing.hs:11:14)\r\n left :: Traversal s t a b (bound at failing.hs:11:9)\r\n failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)\r\n}}}\r\n\r\n\r\nI don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11334GHC panic when calling typeOf on a promoted data constructor2019-07-07T18:30:53ZRyan ScottGHC panic when calling typeOf on a promoted data constructorHere's what I did in GHCi to trigger the panic:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help
λ> :set -XDataKinds
λ> :m Data.Typeable Data.Functor.Compose
λ> typeOf (Proxy :: Proxy 'Compose)
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160101 for x86_64-unknown-linux):
piResultTy
*
TYPE 'Lifted *
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Enabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:
```
λ> :set -XPolyKinds
λ> typeOf (Proxy :: Proxy 'Compose)
<interactive>:5:1: error:
• No instance for (Typeable a0) arising from a use of ‘typeOf’
• In the expression: typeOf (Proxy :: Proxy Compose)
In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic when calling typeOf on a promoted data constructor","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Here's what I did in GHCi to trigger the panic:\r\n\r\n{{{\r\n$ inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XDataKinds\r\nλ> :m Data.Typeable Data.Functor.Compose\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160101 for x86_64-unknown-linux):\r\n piResultTy\r\n *\r\n TYPE 'Lifted *\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nEnabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:\r\n\r\n{{{\r\nλ> :set -XPolyKinds\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\n\r\n<interactive>:5:1: error:\r\n • No instance for (Typeable a0) arising from a use of ‘typeOf’\r\n • In the expression: typeOf (Proxy :: Proxy Compose)\r\n In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Here's what I did in GHCi to trigger the panic:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help
λ> :set -XDataKinds
λ> :m Data.Typeable Data.Functor.Compose
λ> typeOf (Proxy :: Proxy 'Compose)
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160101 for x86_64-unknown-linux):
piResultTy
*
TYPE 'Lifted *
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Enabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:
```
λ> :set -XPolyKinds
λ> typeOf (Proxy :: Proxy 'Compose)
<interactive>:5:1: error:
• No instance for (Typeable a0) arising from a use of ‘typeOf’
• In the expression: typeOf (Proxy :: Proxy Compose)
In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic when calling typeOf on a promoted data constructor","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Here's what I did in GHCi to trigger the panic:\r\n\r\n{{{\r\n$ inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XDataKinds\r\nλ> :m Data.Typeable Data.Functor.Compose\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160101 for x86_64-unknown-linux):\r\n piResultTy\r\n *\r\n TYPE 'Lifted *\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nEnabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:\r\n\r\n{{{\r\nλ> :set -XPolyKinds\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\n\r\n<interactive>:5:1: error:\r\n • No instance for (Typeable a0) arising from a use of ‘typeOf’\r\n • In the expression: typeOf (Proxy :: Proxy Compose)\r\n In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11305Type checker regression introduced by visible type-application2019-07-07T18:31:01ZHerbert Valerio Riedelhvr@gnu.orgType checker regression introduced by visible type-applicationTODO: figure out better summary ;-)
The following snippet extracted from Edward's `profunctors` package compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Data.Profunctor.Strong where
import Control.Arrow
import Control.Category
import Data.Tuple
import Prelude hiding (id,(.))
infixr 0 :->
type p :-> q = forall a b. p a b -> q a b
class Profunctor p where
dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
class ProfunctorFunctor t where
promap :: Profunctor p => (p :-> q) -> t p :-> t q
class ProfunctorFunctor t => ProfunctorMonad t where
proreturn :: Profunctor p => p :-> t p
projoin :: Profunctor p => t (t p) :-> t p
class ProfunctorFunctor t => ProfunctorComonad t where
proextract :: Profunctor p => t p :-> p
produplicate :: Profunctor p => t p :-> t (t p)
class Profunctor p => Strong p where
first' :: p a b -> p (a, c) (b, c)
first' = dimap swap swap . second'
second' :: p a b -> p (c, a) (c, b)
second' = dimap swap swap . first'
----------------------------------------------------------------------------
newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
instance Profunctor p => Profunctor (Tambara p) where
dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
instance ProfunctorFunctor Tambara where
promap f (Tambara p) = Tambara (f p)
instance ProfunctorComonad Tambara where
proextract (Tambara p) = dimap (\a -> (a,())) fst p
produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
where
hither :: ((a, b), c) -> (a, (b, c))
hither ~(~(x,y),z) = (x,(y,z))
yon :: (a, (b, c)) -> ((a, b), c)
yon ~(x,~(y,z)) = ((x,y),z)
instance Profunctor p => Strong (Tambara p) where
first' = runTambara . produplicate
```
```
Strong.hs:57:12: error:
• Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1. Tambara p (a, c1) (b, c1)’
Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)
Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)
• In the first argument of ‘(.)’, namely ‘runTambara’
In the expression: runTambara . produplicate
In an equation for ‘first'’: first' = runTambara . produplicate
• Relevant bindings include first' :: Tambara p a b -> Tambara p (a, c) (b, c) (bound at Strong.hs:57:3)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | alanz |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TC Regression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["alanz"],"type":"Bug","description":"TODO: figure out better summary ;-)\r\n\r\nThe following snippet extracted from Edward's `profunctors` package compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Data.Profunctor.Strong where\r\n\r\nimport Control.Arrow\r\nimport Control.Category\r\nimport Data.Tuple\r\nimport Prelude hiding (id,(.))\r\n\r\ninfixr 0 :->\r\ntype p :-> q = forall a b. p a b -> q a b\r\n\r\nclass Profunctor p where\r\n dimap :: (a -> b) -> (c -> d) -> p b c -> p a d\r\n\r\nclass ProfunctorFunctor t where\r\n promap :: Profunctor p => (p :-> q) -> t p :-> t q\r\n\r\nclass ProfunctorFunctor t => ProfunctorMonad t where\r\n proreturn :: Profunctor p => p :-> t p\r\n projoin :: Profunctor p => t (t p) :-> t p\r\n\r\nclass ProfunctorFunctor t => ProfunctorComonad t where\r\n proextract :: Profunctor p => t p :-> p\r\n produplicate :: Profunctor p => t p :-> t (t p)\r\n\r\nclass Profunctor p => Strong p where\r\n first' :: p a b -> p (a, c) (b, c)\r\n first' = dimap swap swap . second'\r\n\r\n second' :: p a b -> p (c, a) (c, b)\r\n second' = dimap swap swap . first'\r\n\r\n----------------------------------------------------------------------------\r\n\r\nnewtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }\r\n\r\ninstance Profunctor p => Profunctor (Tambara p) where\r\n dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p\r\n\r\ninstance ProfunctorFunctor Tambara where\r\n promap f (Tambara p) = Tambara (f p)\r\n\r\ninstance ProfunctorComonad Tambara where\r\n proextract (Tambara p) = dimap (\\a -> (a,())) fst p\r\n\r\n produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)\r\n where\r\n hither :: ((a, b), c) -> (a, (b, c))\r\n hither ~(~(x,y),z) = (x,(y,z))\r\n\r\n yon :: (a, (b, c)) -> ((a, b), c)\r\n yon ~(x,~(y,z)) = ((x,y),z)\r\n\r\ninstance Profunctor p => Strong (Tambara p) where\r\n first' = runTambara . produplicate\r\n}}}\r\n\r\n{{{\r\nStrong.hs:57:12: error:\r\n • Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1. Tambara p (a, c1) (b, c1)’\r\n Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)\r\n Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)\r\n • In the first argument of ‘(.)’, namely ‘runTambara’\r\n In the expression: runTambara . produplicate\r\n In an equation for ‘first'’: first' = runTambara . produplicate\r\n • Relevant bindings include first' :: Tambara p a b -> Tambara p (a, c) (b, c) (bound at Strong.hs:57:3)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->TODO: figure out better summary ;-)
The following snippet extracted from Edward's `profunctors` package compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Data.Profunctor.Strong where
import Control.Arrow
import Control.Category
import Data.Tuple
import Prelude hiding (id,(.))
infixr 0 :->
type p :-> q = forall a b. p a b -> q a b
class Profunctor p where
dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
class ProfunctorFunctor t where
promap :: Profunctor p => (p :-> q) -> t p :-> t q
class ProfunctorFunctor t => ProfunctorMonad t where
proreturn :: Profunctor p => p :-> t p
projoin :: Profunctor p => t (t p) :-> t p
class ProfunctorFunctor t => ProfunctorComonad t where
proextract :: Profunctor p => t p :-> p
produplicate :: Profunctor p => t p :-> t (t p)
class Profunctor p => Strong p where
first' :: p a b -> p (a, c) (b, c)
first' = dimap swap swap . second'
second' :: p a b -> p (c, a) (c, b)
second' = dimap swap swap . first'
----------------------------------------------------------------------------
newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
instance Profunctor p => Profunctor (Tambara p) where
dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
instance ProfunctorFunctor Tambara where
promap f (Tambara p) = Tambara (f p)
instance ProfunctorComonad Tambara where
proextract (Tambara p) = dimap (\a -> (a,())) fst p
produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
where
hither :: ((a, b), c) -> (a, (b, c))
hither ~(~(x,y),z) = (x,(y,z))
yon :: (a, (b, c)) -> ((a, b), c)
yon ~(x,~(y,z)) = ((x,y),z)
instance Profunctor p => Strong (Tambara p) where
first' = runTambara . produplicate
```
```
Strong.hs:57:12: error:
• Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1. Tambara p (a, c1) (b, c1)’
Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)
Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)
• In the first argument of ‘(.)’, namely ‘runTambara’
In the expression: runTambara . produplicate
In an equation for ‘first'’: first' = runTambara . produplicate
• Relevant bindings include first' :: Tambara p a b -> Tambara p (a, c) (b, c) (bound at Strong.hs:57:3)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | alanz |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TC Regression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["alanz"],"type":"Bug","description":"TODO: figure out better summary ;-)\r\n\r\nThe following snippet extracted from Edward's `profunctors` package compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Data.Profunctor.Strong where\r\n\r\nimport Control.Arrow\r\nimport Control.Category\r\nimport Data.Tuple\r\nimport Prelude hiding (id,(.))\r\n\r\ninfixr 0 :->\r\ntype p :-> q = forall a b. p a b -> q a b\r\n\r\nclass Profunctor p where\r\n dimap :: (a -> b) -> (c -> d) -> p b c -> p a d\r\n\r\nclass ProfunctorFunctor t where\r\n promap :: Profunctor p => (p :-> q) -> t p :-> t q\r\n\r\nclass ProfunctorFunctor t => ProfunctorMonad t where\r\n proreturn :: Profunctor p => p :-> t p\r\n projoin :: Profunctor p => t (t p) :-> t p\r\n\r\nclass ProfunctorFunctor t => ProfunctorComonad t where\r\n proextract :: Profunctor p => t p :-> p\r\n produplicate :: Profunctor p => t p :-> t (t p)\r\n\r\nclass Profunctor p => Strong p where\r\n first' :: p a b -> p (a, c) (b, c)\r\n first' = dimap swap swap . second'\r\n\r\n second' :: p a b -> p (c, a) (c, b)\r\n second' = dimap swap swap . first'\r\n\r\n----------------------------------------------------------------------------\r\n\r\nnewtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }\r\n\r\ninstance Profunctor p => Profunctor (Tambara p) where\r\n dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p\r\n\r\ninstance ProfunctorFunctor Tambara where\r\n promap f (Tambara p) = Tambara (f p)\r\n\r\ninstance ProfunctorComonad Tambara where\r\n proextract (Tambara p) = dimap (\\a -> (a,())) fst p\r\n\r\n produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)\r\n where\r\n hither :: ((a, b), c) -> (a, (b, c))\r\n hither ~(~(x,y),z) = (x,(y,z))\r\n\r\n yon :: (a, (b, c)) -> ((a, b), c)\r\n yon ~(x,~(y,z)) = ((x,y),z)\r\n\r\ninstance Profunctor p => Strong (Tambara p) where\r\n first' = runTambara . produplicate\r\n}}}\r\n\r\n{{{\r\nStrong.hs:57:12: error:\r\n • Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1. Tambara p (a, c1) (b, c1)’\r\n Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)\r\n Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)\r\n • In the first argument of ‘(.)’, namely ‘runTambara’\r\n In the expression: runTambara . produplicate\r\n In an equation for ‘first'’: first' = runTambara . produplicate\r\n • Relevant bindings include first' :: Tambara p a b -> Tambara p (a, c) (b, c) (bound at Strong.hs:57:3)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11246Regression typechecking type synonym which includes `Any`.2019-07-07T18:31:17ZMatthew PickeringRegression typechecking type synonym which includes `Any`.```hs
module Foo where
import GHC.Exts
type Key a = Any
```
produces the error message on HEAD but compiles on 7.8.3 and 7.10.1 (thanks to Reid for testing).
```
unsafeany.hs:5:1: error:
• The type family ‘Any’ should have no arguments, but has been given none
• In the type synonym declaration for ‘Key’
Failed, modules loaded: none.
``````hs
module Foo where
import GHC.Exts
type Key a = Any
```
produces the error message on HEAD but compiles on 7.8.3 and 7.10.1 (thanks to Reid for testing).
```
unsafeany.hs:5:1: error:
• The type family ‘Any’ should have no arguments, but has been given none
• In the type synonym declaration for ‘Key’
Failed, modules loaded: none.
```8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/10635-fwarn-redundant-constraints should not be part of -Wall2019-07-07T18:34:56ZLemming-fwarn-redundant-constraints should not be part of -WallWhen I compile existing code with GHC-7.11.20150707 I get lot of "redundant constraints" warnings. Generally I think that this warning can be very useful for minimizing constraints, nonetheless there are good reasons not choose minimal constraints for a type signature.
E.g. if I have to implement `Data.Map.singleton` I do not need the `Ord k` constraint for the key type. However, I might add it anyway in order to be able to change the implementation in future such that it uses `Ord k` dictionary.
Thus I suggest to exclude `-fwarn-redundant-constraints` from `-Wall`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-fwarn-redundant-constraints should not be part of -Wall","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When I compile existing code with GHC-7.11.20150707 I get lot of \"redundant constraints\" warnings. Generally I think that this warning can be very useful for minimizing constraints, nonetheless there are good reasons not choose minimal constraints for a type signature.\r\nE.g. if I have to implement `Data.Map.singleton` I do not need the `Ord k` constraint for the key type. However, I might add it anyway in order to be able to change the implementation in future such that it uses `Ord k` dictionary.\r\n\r\nThus I suggest to exclude `-fwarn-redundant-constraints` from `-Wall`.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->When I compile existing code with GHC-7.11.20150707 I get lot of "redundant constraints" warnings. Generally I think that this warning can be very useful for minimizing constraints, nonetheless there are good reasons not choose minimal constraints for a type signature.
E.g. if I have to implement `Data.Map.singleton` I do not need the `Ord k` constraint for the key type. However, I might add it anyway in order to be able to change the implementation in future such that it uses `Ord k` dictionary.
Thus I suggest to exclude `-fwarn-redundant-constraints` from `-Wall`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-fwarn-redundant-constraints should not be part of -Wall","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When I compile existing code with GHC-7.11.20150707 I get lot of \"redundant constraints\" warnings. Generally I think that this warning can be very useful for minimizing constraints, nonetheless there are good reasons not choose minimal constraints for a type signature.\r\nE.g. if I have to implement `Data.Map.singleton` I do not need the `Ord k` constraint for the key type. However, I might add it anyway in order to be able to change the implementation in future such that it uses `Ord k` dictionary.\r\n\r\nThus I suggest to exclude `-fwarn-redundant-constraints` from `-Wall`.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/10443Regression in forall typechecking2019-07-07T18:35:54ZAlan ZimmermanRegression in forall typecheckingThe following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch
Ths code below, from
https://github.com/DanielG/ghc-mod/blob/b52c0a5d767282369f2748c5ec070b802ed8e23c/Language/Haskell/GhcMod/Monad/Types.hs\#L346
```hs
instance (MonadBaseControl IO m) => MonadBaseControl IO (GhcModT m) where
type StM (GhcModT m) a =
StM (StateT GhcModState
(ErrorT GhcModError
(JournalT GhcModLog
(ReaderT GhcModEnv m) ) ) ) a
liftBaseWith f = GhcModT . liftBaseWith $ \runInBase ->
f $ runInBase . unGhcModT
restoreM = GhcModT . restoreM
{-# INLINE liftBaseWith #-}
{-# INLINE restoreM #-}
```
Which compiles fine with GHC 7.10.1 now has the error
```
Language/Haskell/GhcMod/Monad/Types.hs:346:13:
Couldn't match expected type ‘StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a1
-> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’
with actual type ‘forall a2.
StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a2
-> IO
(StM
(StateT
GhcModState
(ErrorT
GhcModError
(JournalT GhcModLog (ReaderT GhcModEnv m))))
a2)’
Relevant bindings include
runInBase :: forall a.
StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a
-> IO
(StM
(StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))))
a)
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:48)
f :: RunInBase (GhcModT m) IO -> IO a
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:18)
liftBaseWith :: (RunInBase (GhcModT m) IO -> IO a) -> GhcModT m a
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:5)
In the first argument of ‘(.)’, namely ‘runInBase’
In the second argument of ‘($)’, namely ‘runInBase . unGhcModT’
```
A laborious git bisect tracked it down to
```
681d82c0d44f06f0b958b75778c30b0910df982b is the first bad commit
commit 681d82c0d44f06f0b958b75778c30b0910df982b
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Tue Apr 7 14:45:04 2015 +0100
Look inside synonyms for foralls when unifying
This fixes Trac #10194
(cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)
:040000 040000 1f0e62661ed1c48a9cbfab72ca3e38bb9e501412 ef6786fdb952d3446121b27b56f6103533d52356 M compiler
:040000 040000 d607f1bff94578b0677df9cba01371dad6b26a32 ac715cec4fd8d43a53ecee132eae2b4c0c65e31a M testsuite
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1 |
| 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":"Regression in forall typechecking","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch\r\n\r\nThs code below, from\r\nhttps://github.com/DanielG/ghc-mod/blob/b52c0a5d767282369f2748c5ec070b802ed8e23c/Language/Haskell/GhcMod/Monad/Types.hs#L346\r\n\r\n{{{#!hs\r\ninstance (MonadBaseControl IO m) => MonadBaseControl IO (GhcModT m) where\r\n type StM (GhcModT m) a =\r\n StM (StateT GhcModState\r\n (ErrorT GhcModError\r\n (JournalT GhcModLog\r\n (ReaderT GhcModEnv m) ) ) ) a\r\n liftBaseWith f = GhcModT . liftBaseWith $ \\runInBase ->\r\n f $ runInBase . unGhcModT\r\n\r\n restoreM = GhcModT . restoreM\r\n {-# INLINE liftBaseWith #-}\r\n {-# INLINE restoreM #-}\r\n}}}\r\n\r\nWhich compiles fine with GHC 7.10.1 now has the error\r\n\r\n{{{\r\nLanguage/Haskell/GhcMod/Monad/Types.hs:346:13:\r\n Couldn't match expected type ‘StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a1\r\n -> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’\r\n with actual type ‘forall a2.\r\n StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a2\r\n -> IO\r\n (StM\r\n (StateT\r\n GhcModState\r\n (ErrorT\r\n GhcModError\r\n (JournalT GhcModLog (ReaderT GhcModEnv m))))\r\n a2)’\r\n Relevant bindings include\r\n runInBase :: forall a.\r\n StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a\r\n -> IO\r\n (StM\r\n (StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))))\r\n a)\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:48)\r\n f :: RunInBase (GhcModT m) IO -> IO a\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:18)\r\n liftBaseWith :: (RunInBase (GhcModT m) IO -> IO a) -> GhcModT m a\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:5)\r\n In the first argument of ‘(.)’, namely ‘runInBase’\r\n In the second argument of ‘($)’, namely ‘runInBase . unGhcModT’\r\n}}}\r\n\r\nA laborious git bisect tracked it down to\r\n\r\n{{{\r\n681d82c0d44f06f0b958b75778c30b0910df982b is the first bad commit\r\ncommit 681d82c0d44f06f0b958b75778c30b0910df982b\r\nAuthor: Simon Peyton Jones <simonpj@microsoft.com>\r\nDate: Tue Apr 7 14:45:04 2015 +0100\r\n\r\n Look inside synonyms for foralls when unifying\r\n \r\n This fixes Trac #10194\r\n \r\n (cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)\r\n\r\n:040000 040000 1f0e62661ed1c48a9cbfab72ca3e38bb9e501412 ef6786fdb952d3446121b27b56f6103533d52356 M\tcompiler\r\n:040000 040000 d607f1bff94578b0677df9cba01371dad6b26a32 ac715cec4fd8d43a53ecee132eae2b4c0c65e31a M\ttestsuite\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->The following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch
Ths code below, from
https://github.com/DanielG/ghc-mod/blob/b52c0a5d767282369f2748c5ec070b802ed8e23c/Language/Haskell/GhcMod/Monad/Types.hs\#L346
```hs
instance (MonadBaseControl IO m) => MonadBaseControl IO (GhcModT m) where
type StM (GhcModT m) a =
StM (StateT GhcModState
(ErrorT GhcModError
(JournalT GhcModLog
(ReaderT GhcModEnv m) ) ) ) a
liftBaseWith f = GhcModT . liftBaseWith $ \runInBase ->
f $ runInBase . unGhcModT
restoreM = GhcModT . restoreM
{-# INLINE liftBaseWith #-}
{-# INLINE restoreM #-}
```
Which compiles fine with GHC 7.10.1 now has the error
```
Language/Haskell/GhcMod/Monad/Types.hs:346:13:
Couldn't match expected type ‘StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a1
-> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’
with actual type ‘forall a2.
StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a2
-> IO
(StM
(StateT
GhcModState
(ErrorT
GhcModError
(JournalT GhcModLog (ReaderT GhcModEnv m))))
a2)’
Relevant bindings include
runInBase :: forall a.
StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))
a
-> IO
(StM
(StateT
GhcModState
(ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))))
a)
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:48)
f :: RunInBase (GhcModT m) IO -> IO a
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:18)
liftBaseWith :: (RunInBase (GhcModT m) IO -> IO a) -> GhcModT m a
(bound at Language/Haskell/GhcMod/Monad/Types.hs:345:5)
In the first argument of ‘(.)’, namely ‘runInBase’
In the second argument of ‘($)’, namely ‘runInBase . unGhcModT’
```
A laborious git bisect tracked it down to
```
681d82c0d44f06f0b958b75778c30b0910df982b is the first bad commit
commit 681d82c0d44f06f0b958b75778c30b0910df982b
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Tue Apr 7 14:45:04 2015 +0100
Look inside synonyms for foralls when unifying
This fixes Trac #10194
(cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)
:040000 040000 1f0e62661ed1c48a9cbfab72ca3e38bb9e501412 ef6786fdb952d3446121b27b56f6103533d52356 M compiler
:040000 040000 d607f1bff94578b0677df9cba01371dad6b26a32 ac715cec4fd8d43a53ecee132eae2b4c0c65e31a M testsuite
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1 |
| 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":"Regression in forall typechecking","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following bug showed up when trying to install ghc-mod against the current ghc-7.10 branch\r\n\r\nThs code below, from\r\nhttps://github.com/DanielG/ghc-mod/blob/b52c0a5d767282369f2748c5ec070b802ed8e23c/Language/Haskell/GhcMod/Monad/Types.hs#L346\r\n\r\n{{{#!hs\r\ninstance (MonadBaseControl IO m) => MonadBaseControl IO (GhcModT m) where\r\n type StM (GhcModT m) a =\r\n StM (StateT GhcModState\r\n (ErrorT GhcModError\r\n (JournalT GhcModLog\r\n (ReaderT GhcModEnv m) ) ) ) a\r\n liftBaseWith f = GhcModT . liftBaseWith $ \\runInBase ->\r\n f $ runInBase . unGhcModT\r\n\r\n restoreM = GhcModT . restoreM\r\n {-# INLINE liftBaseWith #-}\r\n {-# INLINE restoreM #-}\r\n}}}\r\n\r\nWhich compiles fine with GHC 7.10.1 now has the error\r\n\r\n{{{\r\nLanguage/Haskell/GhcMod/Monad/Types.hs:346:13:\r\n Couldn't match expected type ‘StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a1\r\n -> IO (StM m (Either GhcModError (a1, GhcModState), GhcModLog))’\r\n with actual type ‘forall a2.\r\n StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a2\r\n -> IO\r\n (StM\r\n (StateT\r\n GhcModState\r\n (ErrorT\r\n GhcModError\r\n (JournalT GhcModLog (ReaderT GhcModEnv m))))\r\n a2)’\r\n Relevant bindings include\r\n runInBase :: forall a.\r\n StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m)))\r\n a\r\n -> IO\r\n (StM\r\n (StateT\r\n GhcModState\r\n (ErrorT GhcModError (JournalT GhcModLog (ReaderT GhcModEnv m))))\r\n a)\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:48)\r\n f :: RunInBase (GhcModT m) IO -> IO a\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:18)\r\n liftBaseWith :: (RunInBase (GhcModT m) IO -> IO a) -> GhcModT m a\r\n (bound at Language/Haskell/GhcMod/Monad/Types.hs:345:5)\r\n In the first argument of ‘(.)’, namely ‘runInBase’\r\n In the second argument of ‘($)’, namely ‘runInBase . unGhcModT’\r\n}}}\r\n\r\nA laborious git bisect tracked it down to\r\n\r\n{{{\r\n681d82c0d44f06f0b958b75778c30b0910df982b is the first bad commit\r\ncommit 681d82c0d44f06f0b958b75778c30b0910df982b\r\nAuthor: Simon Peyton Jones <simonpj@microsoft.com>\r\nDate: Tue Apr 7 14:45:04 2015 +0100\r\n\r\n Look inside synonyms for foralls when unifying\r\n \r\n This fixes Trac #10194\r\n \r\n (cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)\r\n\r\n:040000 040000 1f0e62661ed1c48a9cbfab72ca3e38bb9e501412 ef6786fdb952d3446121b27b56f6103533d52356 M\tcompiler\r\n:040000 040000 d607f1bff94578b0677df9cba01371dad6b26a32 ac715cec4fd8d43a53ecee132eae2b4c0c65e31a M\ttestsuite\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.10.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/10348HEAD: `KnownNat` does not imply `Typeable` any more2019-07-07T18:36:27ZGabor GreifHEAD: `KnownNat` does not imply `Typeable` any moreAs Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:
```hs
{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}
import GHC.TypeLits
import Data.Typeable
data Foo (n :: Nat) where
Hey :: KnownNat n => Foo n
deriving instance Show (Foo n)
data T t where
T :: (Show t, Typeable t) => t -> T t
deriving instance Show (T n)
```
With ghci-7.11.20150407 I now see more constraints
```
*Main> :t T Hey
T Hey :: (Typeable n, KnownNat n) => T (Foo n)
```
OTOH ghci-7.11.20150215 only wanted `KnownNat`:
```
*Main> :t T Hey
T Hey :: KnownNat n => T (Foo n)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"HEAD: `KnownNat` does not imply `Typeable` any more","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:\r\n\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Typeable\r\n\r\ndata Foo (n :: Nat) where\r\n Hey :: KnownNat n => Foo n\r\n\r\nderiving instance Show (Foo n)\r\n\r\ndata T t where\r\n T :: (Show t, Typeable t) => t -> T t\r\n\r\nderiving instance Show (T n)\r\n}}}\r\nWith ghci-7.11.20150407 I now see more constraints\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: (Typeable n, KnownNat n) => T (Foo n)\r\n}}}\r\n\r\nOTOH ghci-7.11.20150215 only wanted `KnownNat`:\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: KnownNat n => T (Foo n)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:
```hs
{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}
import GHC.TypeLits
import Data.Typeable
data Foo (n :: Nat) where
Hey :: KnownNat n => Foo n
deriving instance Show (Foo n)
data T t where
T :: (Show t, Typeable t) => t -> T t
deriving instance Show (T n)
```
With ghci-7.11.20150407 I now see more constraints
```
*Main> :t T Hey
T Hey :: (Typeable n, KnownNat n) => T (Foo n)
```
OTOH ghci-7.11.20150215 only wanted `KnownNat`:
```
*Main> :t T Hey
T Hey :: KnownNat n => T (Foo n)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"HEAD: `KnownNat` does not imply `Typeable` any more","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As Iavor confirmed (https://mail.haskell.org/pipermail/ghc-devs/2015-April/008885.html) there is a regression on HEAD relative to `ghc-7.11.20150215`. Here is a reproduction snippet:\r\n\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures, StandaloneDeriving #-}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Typeable\r\n\r\ndata Foo (n :: Nat) where\r\n Hey :: KnownNat n => Foo n\r\n\r\nderiving instance Show (Foo n)\r\n\r\ndata T t where\r\n T :: (Show t, Typeable t) => t -> T t\r\n\r\nderiving instance Show (T n)\r\n}}}\r\nWith ghci-7.11.20150407 I now see more constraints\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: (Typeable n, KnownNat n) => T (Foo n)\r\n}}}\r\n\r\nOTOH ghci-7.11.20150215 only wanted `KnownNat`:\r\n{{{\r\n*Main> :t T Hey\r\nT Hey :: KnownNat n => T (Foo n)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/10321GHC.TypeLits.Nat types no longer fully simplified.2019-07-07T18:36:35ZdarchonGHC.TypeLits.Nat types no longer fully simplified.The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
infixr 5 :>
```
when loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:
```
$ ghci example/vec.hs
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a
```
while in GHCi 7.10.1 it gives:
```
$ ghci example/vec.hs
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
That is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.
The same still happens in HEAD (20150417)
```
$ ghci example/vec.hs
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC.TypeLits.Nat types no longer fully simplified.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["TypeLits"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata Vec :: Nat -> * -> * where\r\n Nil :: Vec 0 a\r\n (:>) :: a -> Vec n a -> Vec (n + 1) a\r\n\r\ninfixr 5 :>\r\n}}}\r\n\r\nwhen loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec 3 a\r\n}}}\r\n\r\nwhile in GHCi 7.10.1 it gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nThat is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.\r\n\r\nThe same still happens in HEAD (20150417)\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nI strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.","type_of_failure":"OtherFailure","blocking":[]} -->The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
infixr 5 :>
```
when loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:
```
$ ghci example/vec.hs
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a
```
while in GHCi 7.10.1 it gives:
```
$ ghci example/vec.hs
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
That is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.
The same still happens in HEAD (20150417)
```
$ ghci example/vec.hs
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC.TypeLits.Nat types no longer fully simplified.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["TypeLits"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata Vec :: Nat -> * -> * where\r\n Nil :: Vec 0 a\r\n (:>) :: a -> Vec n a -> Vec (n + 1) a\r\n\r\ninfixr 5 :>\r\n}}}\r\n\r\nwhen loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec 3 a\r\n}}}\r\n\r\nwhile in GHCi 7.10.1 it gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nThat is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.\r\n\r\nThe same still happens in HEAD (20150417)\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nI strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/10194Shouldn't this require ImpredicativeTypes?2019-07-07T18:37:08ZAndres LöhShouldn't this require ImpredicativeTypes?The following program compiles:
```
{-# LANGUAGE RankNTypes #-}
module TestRN1 where
type X = forall a . a
comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)
```
But this one fails:
```
{-# LANGUAGE RankNTypes #-}
module TestRN2 where
comp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)
comp = (.)
```
Error:
```
Cannot instantiate unification variable ‘b0’
with a type involving foralls: forall a1. a1
Perhaps you want ImpredicativeTypes
In the expression: (.)
In an equation for ‘comp’: comp = (.)
```
I would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Shouldn't this require ImpredicativeTypes?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule TestRN1 where\r\n\r\ntype X = forall a . a\r\n\r\ncomp :: (X -> c) -> (a -> X) -> (a -> c)\r\ncomp = (.)\r\n}}}\r\n\r\nBut this one fails:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule TestRN2 where\r\n\r\ncomp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)\r\ncomp = (.)\r\n}}}\r\n\r\nError:\r\n\r\n{{{\r\n Cannot instantiate unification variable ‘b0’\r\n with a type involving foralls: forall a1. a1\r\n Perhaps you want ImpredicativeTypes\r\n In the expression: (.)\r\n In an equation for ‘comp’: comp = (.)\r\n}}}\r\n\r\nI would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->The following program compiles:
```
{-# LANGUAGE RankNTypes #-}
module TestRN1 where
type X = forall a . a
comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)
```
But this one fails:
```
{-# LANGUAGE RankNTypes #-}
module TestRN2 where
comp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)
comp = (.)
```
Error:
```
Cannot instantiate unification variable ‘b0’
with a type involving foralls: forall a1. a1
Perhaps you want ImpredicativeTypes
In the expression: (.)
In an equation for ‘comp’: comp = (.)
```
I would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Shouldn't this require ImpredicativeTypes?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule TestRN1 where\r\n\r\ntype X = forall a . a\r\n\r\ncomp :: (X -> c) -> (a -> X) -> (a -> c)\r\ncomp = (.)\r\n}}}\r\n\r\nBut this one fails:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule TestRN2 where\r\n\r\ncomp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)\r\ncomp = (.)\r\n}}}\r\n\r\nError:\r\n\r\n{{{\r\n Cannot instantiate unification variable ‘b0’\r\n with a type involving foralls: forall a1. a1\r\n Perhaps you want ImpredicativeTypes\r\n In the expression: (.)\r\n In an equation for ‘comp’: comp = (.)\r\n}}}\r\n\r\nI would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/10177Typeable solver regression2019-07-07T18:37:13ZglguyTypeable solver regressionThis bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost.
This code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master.
The relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve `Typeable` solver.
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
module Bug where
import Data.Typeable
newtype V n a = V [a]
class Typeable a => C a
instance (Typeable (V n), Typeable a) => C (V n a)
-- Bug.hs:13:10:
-- Could not deduce (Typeable (V n a))
-- arising from the superclasses of an instance declaration
-- from the context (Typeable (V n), Typeable a)
-- bound by the instance declaration at Bug.hs:13:10-50
-- In the instance declaration for ‘C (V n a)’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1-rc3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typeable solver regression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["diatchki"],"type":"Bug","description":"This bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost.\r\n\r\nThis code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master.\r\n\r\nThe relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve `Typeable` solver.\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\nmodule Bug where\r\n\r\nimport Data.Typeable\r\n\r\nnewtype V n a = V [a]\r\n\r\nclass Typeable a => C a\r\ninstance (Typeable (V n), Typeable a) => C (V n a)\r\n\r\n-- Bug.hs:13:10:\r\n-- Could not deduce (Typeable (V n a))\r\n-- arising from the superclasses of an instance declaration\r\n-- from the context (Typeable (V n), Typeable a)\r\n-- bound by the instance declaration at Bug.hs:13:10-50\r\n-- In the instance declaration for ‘C (V n a)’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->This bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost.
This code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master.
The relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve `Typeable` solver.
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
module Bug where
import Data.Typeable
newtype V n a = V [a]
class Typeable a => C a
instance (Typeable (V n), Typeable a) => C (V n a)
-- Bug.hs:13:10:
-- Could not deduce (Typeable (V n a))
-- arising from the superclasses of an instance declaration
-- from the context (Typeable (V n), Typeable a)
-- bound by the instance declaration at Bug.hs:13:10-50
-- In the instance declaration for ‘C (V n a)’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1-rc3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typeable solver regression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["diatchki"],"type":"Bug","description":"This bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost.\r\n\r\nThis code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master.\r\n\r\nThe relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve `Typeable` solver.\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\nmodule Bug where\r\n\r\nimport Data.Typeable\r\n\r\nnewtype V n a = V [a]\r\n\r\nclass Typeable a => C a\r\ninstance (Typeable (V n), Typeable a) => C (V n a)\r\n\r\n-- Bug.hs:13:10:\r\n-- Could not deduce (Typeable (V n a))\r\n-- arising from the superclasses of an instance declaration\r\n-- from the context (Typeable (V n), Typeable a)\r\n-- bound by the instance declaration at Bug.hs:13:10-50\r\n-- In the instance declaration for ‘C (V n a)’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/10009type inference regression when faking injective type families2019-07-07T18:37:56Zaavogttype inference regression when faking injective type familiesghc-7.10.0.20141222 does not accept the program unless I uncomment the
type signature (a :: a). ghc-7.8 accepts it as-is.
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
class (UnF (F a) ~ a, Show a) => C a where
type F a
f :: F a -> a
type family UnF a
g :: forall a. C a => a -> String
g _ = show a
where a = f (undefined :: F a) -- :: a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.1-rc1 |
| 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":"type inference regression when faking injective type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"ghc-7.10.0.20141222 does not accept the program unless I uncomment the\r\ntype signature (a :: a). ghc-7.8 accepts it as-is.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\nclass (UnF (F a) ~ a, Show a) => C a where\r\n type F a\r\n f :: F a -> a\r\n\r\ntype family UnF a\r\n\r\ng :: forall a. C a => a -> String\r\ng _ = show a\r\n where a = f (undefined :: F a) -- :: a\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->ghc-7.10.0.20141222 does not accept the program unless I uncomment the
type signature (a :: a). ghc-7.8 accepts it as-is.
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
class (UnF (F a) ~ a, Show a) => C a where
type F a
f :: F a -> a
type family UnF a
g :: forall a. C a => a -> String
g _ = show a
where a = f (undefined :: F a) -- :: a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.1-rc1 |
| 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":"type inference regression when faking injective type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"ghc-7.10.0.20141222 does not accept the program unless I uncomment the\r\ntype signature (a :: a). ghc-7.8 accepts it as-is.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\nclass (UnF (F a) ~ a, Show a) => C a where\r\n type F a\r\n f :: F a -> a\r\n\r\ntype family UnF a\r\n\r\ng :: forall a. C a => a -> String\r\ng _ = show a\r\n where a = f (undefined :: F a) -- :: a\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/8268Local annotations ignored in ambiguity check2019-07-07T18:45:47ZmaxsLocal annotations ignored in ambiguity checkThe following program type checks correctly in GHC 7.6.3 but fails in 7.7 (2013 09 04).
```
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, OverlappingInstances, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
module Test where
newtype Exp t = Exp (Exp t)
type family EltRepr a :: *
type instance EltRepr () = ()
data TupleType a where
UnitTuple :: TupleType ()
class (Show a)
=> Elt a where
eltType :: {-dummy-} a -> TupleType (EltRepr a)
instance Elt () where
eltType _ = UnitTuple
instance (Lift Exp a, Lift Exp b, Elt (Plain a), Elt (Plain b)) => Lift Exp (a, b) where
type Plain (a, b) = (Plain a, Plain b)
lift (x, y) = tup2 (lift x, lift y)
tup2 :: (Elt a, Elt b) => (Exp a, Exp b) -> Exp (a, b)
tup2 (x1, x2) = undefined -- Exp $ Tuple (NilTup `SnocTup` x1 `SnocTup` x2)
class Lift c e where
type Plain e
lift :: e -> c (Plain e)
class Lift c e => Unlift c e where
unlift :: c (Plain e) -> e
fst :: forall f a b. Unlift f (f a, f b) => f (Plain (f a), Plain (f b)) -> f a
fst e = let (x, _:: f b) = unlift e in x
```
The error
```
Test.hs:34:8:
Could not deduce (Plain (f b0) ~ Plain (f b))
from the context (Unlift f (f a, f b))
bound by the type signature for
Test.fst :: Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
at Test.hs:34:8-79
NB: ‛Plain’ is a type function, and may not be injective
The type variable ‛b0’ is ambiguous
Expected type: f (Plain (f a), Plain (f b)) -> f a
Actual type: f (Plain (f a), Plain (f b0)) -> f a
In the ambiguity check for:
forall (f :: * -> *) a b.
Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
In the type signature for ‛Test.fst’:
Test.fst :: forall f a b. Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
```
GHC 7.7 reports:
```
Actual type: f (Plain (f a), Plain (f b0)) -> f a
```
which is incorrect due to the type annotation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Local annotations ignored in ambiguity check","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program type checks correctly in GHC 7.6.3 but fails in 7.7 (2013 09 04).\r\n\r\n{{{\r\n{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, OverlappingInstances, ScopedTypeVariables, TypeFamilies, TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nnewtype Exp t = Exp (Exp t)\r\n\r\ntype family EltRepr a :: *\r\ntype instance EltRepr () = ()\r\n\r\ndata TupleType a where\r\n UnitTuple :: TupleType ()\r\n\r\nclass (Show a)\r\n => Elt a where\r\n eltType :: {-dummy-} a -> TupleType (EltRepr a)\r\n\r\ninstance Elt () where\r\n eltType _ = UnitTuple\r\n\r\ninstance (Lift Exp a, Lift Exp b, Elt (Plain a), Elt (Plain b)) => Lift Exp (a, b) where\r\n type Plain (a, b) = (Plain a, Plain b)\r\n lift (x, y) = tup2 (lift x, lift y)\r\n\r\ntup2 :: (Elt a, Elt b) => (Exp a, Exp b) -> Exp (a, b)\r\ntup2 (x1, x2) = undefined -- Exp $ Tuple (NilTup `SnocTup` x1 `SnocTup` x2)\r\n\r\nclass Lift c e where\r\n type Plain e\r\n lift :: e -> c (Plain e)\r\n\r\nclass Lift c e => Unlift c e where\r\n unlift :: c (Plain e) -> e\r\n\r\nfst :: forall f a b. Unlift f (f a, f b) => f (Plain (f a), Plain (f b)) -> f a\r\nfst e = let (x, _:: f b) = unlift e in x\r\n}}}\r\n\r\nThe error\r\n\r\n\r\n{{{\r\nTest.hs:34:8:\r\n Could not deduce (Plain (f b0) ~ Plain (f b))\r\n from the context (Unlift f (f a, f b))\r\n bound by the type signature for\r\n Test.fst :: Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n at Test.hs:34:8-79\r\n NB: ‛Plain’ is a type function, and may not be injective\r\n The type variable ‛b0’ is ambiguous\r\n Expected type: f (Plain (f a), Plain (f b)) -> f a\r\n Actual type: f (Plain (f a), Plain (f b0)) -> f a\r\n In the ambiguity check for:\r\n forall (f :: * -> *) a b.\r\n Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n In the type signature for ‛Test.fst’:\r\n Test.fst :: forall f a b. Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n\r\n}}}\r\n\r\nGHC 7.7 reports:\r\n{{{\r\n Actual type: f (Plain (f a), Plain (f b0)) -> f a\r\n}}}\r\nwhich is incorrect due to the type annotation.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->The following program type checks correctly in GHC 7.6.3 but fails in 7.7 (2013 09 04).
```
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, OverlappingInstances, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
module Test where
newtype Exp t = Exp (Exp t)
type family EltRepr a :: *
type instance EltRepr () = ()
data TupleType a where
UnitTuple :: TupleType ()
class (Show a)
=> Elt a where
eltType :: {-dummy-} a -> TupleType (EltRepr a)
instance Elt () where
eltType _ = UnitTuple
instance (Lift Exp a, Lift Exp b, Elt (Plain a), Elt (Plain b)) => Lift Exp (a, b) where
type Plain (a, b) = (Plain a, Plain b)
lift (x, y) = tup2 (lift x, lift y)
tup2 :: (Elt a, Elt b) => (Exp a, Exp b) -> Exp (a, b)
tup2 (x1, x2) = undefined -- Exp $ Tuple (NilTup `SnocTup` x1 `SnocTup` x2)
class Lift c e where
type Plain e
lift :: e -> c (Plain e)
class Lift c e => Unlift c e where
unlift :: c (Plain e) -> e
fst :: forall f a b. Unlift f (f a, f b) => f (Plain (f a), Plain (f b)) -> f a
fst e = let (x, _:: f b) = unlift e in x
```
The error
```
Test.hs:34:8:
Could not deduce (Plain (f b0) ~ Plain (f b))
from the context (Unlift f (f a, f b))
bound by the type signature for
Test.fst :: Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
at Test.hs:34:8-79
NB: ‛Plain’ is a type function, and may not be injective
The type variable ‛b0’ is ambiguous
Expected type: f (Plain (f a), Plain (f b)) -> f a
Actual type: f (Plain (f a), Plain (f b0)) -> f a
In the ambiguity check for:
forall (f :: * -> *) a b.
Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
In the type signature for ‛Test.fst’:
Test.fst :: forall f a b. Unlift f (f a, f b) =>
f (Plain (f a), Plain (f b)) -> f a
```
GHC 7.7 reports:
```
Actual type: f (Plain (f a), Plain (f b0)) -> f a
```
which is incorrect due to the type annotation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Local annotations ignored in ambiguity check","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program type checks correctly in GHC 7.6.3 but fails in 7.7 (2013 09 04).\r\n\r\n{{{\r\n{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, OverlappingInstances, ScopedTypeVariables, TypeFamilies, TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nnewtype Exp t = Exp (Exp t)\r\n\r\ntype family EltRepr a :: *\r\ntype instance EltRepr () = ()\r\n\r\ndata TupleType a where\r\n UnitTuple :: TupleType ()\r\n\r\nclass (Show a)\r\n => Elt a where\r\n eltType :: {-dummy-} a -> TupleType (EltRepr a)\r\n\r\ninstance Elt () where\r\n eltType _ = UnitTuple\r\n\r\ninstance (Lift Exp a, Lift Exp b, Elt (Plain a), Elt (Plain b)) => Lift Exp (a, b) where\r\n type Plain (a, b) = (Plain a, Plain b)\r\n lift (x, y) = tup2 (lift x, lift y)\r\n\r\ntup2 :: (Elt a, Elt b) => (Exp a, Exp b) -> Exp (a, b)\r\ntup2 (x1, x2) = undefined -- Exp $ Tuple (NilTup `SnocTup` x1 `SnocTup` x2)\r\n\r\nclass Lift c e where\r\n type Plain e\r\n lift :: e -> c (Plain e)\r\n\r\nclass Lift c e => Unlift c e where\r\n unlift :: c (Plain e) -> e\r\n\r\nfst :: forall f a b. Unlift f (f a, f b) => f (Plain (f a), Plain (f b)) -> f a\r\nfst e = let (x, _:: f b) = unlift e in x\r\n}}}\r\n\r\nThe error\r\n\r\n\r\n{{{\r\nTest.hs:34:8:\r\n Could not deduce (Plain (f b0) ~ Plain (f b))\r\n from the context (Unlift f (f a, f b))\r\n bound by the type signature for\r\n Test.fst :: Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n at Test.hs:34:8-79\r\n NB: ‛Plain’ is a type function, and may not be injective\r\n The type variable ‛b0’ is ambiguous\r\n Expected type: f (Plain (f a), Plain (f b)) -> f a\r\n Actual type: f (Plain (f a), Plain (f b0)) -> f a\r\n In the ambiguity check for:\r\n forall (f :: * -> *) a b.\r\n Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n In the type signature for ‛Test.fst’:\r\n Test.fst :: forall f a b. Unlift f (f a, f b) =>\r\n f (Plain (f a), Plain (f b)) -> f a\r\n\r\n}}}\r\n\r\nGHC 7.7 reports:\r\n{{{\r\n Actual type: f (Plain (f a), Plain (f b0)) -> f a\r\n}}}\r\nwhich is incorrect due to the type annotation.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->