GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:50:48Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/7220Confusing error message in type checking related to type family, fundep, and ...2019-07-07T18:50:48ZtsuyoshiConfusing error message in type checking related to type family, fundep, and higher-rank type(This is related to, but different from, the message which I posted to glasgow-haskell-users mailing list: http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html.)
GHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows...(This is related to, but different from, the message which I posted to glasgow-haskell-users mailing list: http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html.)
GHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows) rejects the attached code (Test2.hs) with the following error message:
```
Test2.hs:24:52:
Couldn't match expected type `Y'
with actual type `TF (forall b. (C A b, TF b ~ Y) => b)'
In the first argument of `f ::
(forall b. (C A b, TF b ~ Y) => b) -> X', namely
`u'
In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
In an equation for `v':
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
```
I am not sure whether the code is supposed to be accepted or rejected, but even if it is correct to reject the code, this error message does not look right to me. If I am not mistaken, the error message is saying that the type checker expects the argument of `(f :: (forall b. (C A b, TF b ~ Y) => b) -> X)` to have type `Y`, but I cannot think of any reason why it should relate the type `(forall b. (C A b, TF b ~ Y) => b)` with `Y`.
The same code is available also at https://gist.github.com/3606856.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.6.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":"Confusing error message in type checking related to type family, fundep, and higher-rank type","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(This is related to, but different from, the message which I posted to glasgow-haskell-users mailing list: http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html.)\r\n\r\nGHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows) rejects the attached code (Test2.hs) with the following error message:\r\n\r\n{{{\r\nTest2.hs:24:52:\r\n Couldn't match expected type `Y'\r\n with actual type `TF (forall b. (C A b, TF b ~ Y) => b)'\r\n In the first argument of `f ::\r\n (forall b. (C A b, TF b ~ Y) => b) -> X', namely\r\n `u'\r\n In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u\r\n In an equation for `v':\r\n v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u\r\n}}}\r\n\r\nI am not sure whether the code is supposed to be accepted or rejected, but even if it is correct to reject the code, this error message does not look right to me. If I am not mistaken, the error message is saying that the type checker expects the argument of `(f :: (forall b. (C A b, TF b ~ Y) => b) -> X)` to have type `Y`, but I cannot think of any reason why it should relate the type `(forall b. (C A b, TF b ~ Y) => b)` with `Y`.\r\n\r\nThe same code is available also at https://gist.github.com/3606856.","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/7186problems with typelits and typenats2019-07-07T18:50:57ZCarter Schonwaldproblems with typelits and typenatsin this test case
https://gist.github.com/3445419
in this case, the type errors seem to indicate SingI has two parameters,
but the documentation and the error free usage both point to one parameter
likewise in
https://gist.github.com/34...in this test case
https://gist.github.com/3445419
in this case, the type errors seem to indicate SingI has two parameters,
but the documentation and the error free usage both point to one parameter
likewise in
https://gist.github.com/3445456
the type checker can't seem to deduce that 1\<=2
which should be "trivial" :)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.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":"problems with typelits and typenats","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"in this test case\r\nhttps://gist.github.com/3445419\r\nin this case, the type errors seem to indicate SingI has two parameters,\r\nbut the documentation and the error free usage both point to one parameter\r\n\r\n\r\nlikewise in \r\nhttps://gist.github.com/3445456\r\nthe type checker can't seem to deduce that 1<=2\r\nwhich should be \"trivial\" :)\r\n\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/7171erroneous overlapping instances reported with FunDeps2019-07-07T18:51:01Zjwlatoerroneous overlapping instances reported with FunDepsWhen a superclass constraint has functional dependencies, in certain cases GHC-7.6 erroneously reports that duplicate instances are found.
file Foo.hs
```
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
modu...When a superclass constraint has functional dependencies, in certain cases GHC-7.6 erroneously reports that duplicate instances are found.
file Foo.hs
```
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
module Foo where
import Data.ByteString as B
import Data.Word
class Foo a b | a -> b
class (Foo a b) => Bar a b | a -> b
instance Foo [a] a
instance Bar [a] a
instance Foo ByteString Word8
instance Bar ByteString Word8
test :: Bar full item => full -> full
test inp = inp
-- this works
-- _test_x :: ByteString -> ByteString
-- _test_x = test
```
file Main.hs
```
module Main where
import Foo
import Data.ByteString
-- this works
-- test1 :: [Int] -> [Int]
-- test1 = test
-- this fails
test2 :: ByteString -> ByteString
test2 = test
```
ghc reports
```
Main.hs:12:9:
Overlapping instances for Foo ByteString GHC.Word.Word8
arising from a use of `test'
Matching instances:
instance Foo ByteString GHC.Word.Word8 -- Defined at Foo.hs:20:10
There exists a (perhaps superclass) match:
(The choice depends on the instantiation of `'
To pick the first instance above, use -XIncoherentInstances
when compiling the other instance declarations)
In the expression: test
In an equation for `test2': test2 = test
```
For this to manifest, I think that at least the following must be true:
> - a function with class constraints must be called from a separate module
> - the type class instance must be monomorphic in the fundep-to parameter
This example works in ghc-7.4.2.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.6.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | jwlato@gmail.com |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"erroneous overlapping instances reported with FunDeps","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1-rc1","keywords":["classes,","fundeps","type"],"differentials":[],"test_case":"","architecture":"","cc":["jwlato@gmail.com"],"type":"Bug","description":"When a superclass constraint has functional dependencies, in certain cases GHC-7.6 erroneously reports that duplicate instances are found.\r\n\r\nfile Foo.hs\r\n{{{\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\n\r\nmodule Foo where\r\n\r\nimport Data.ByteString as B\r\nimport Data.Word\r\n\r\nclass Foo a b | a -> b\r\n\r\nclass (Foo a b) => Bar a b | a -> b\r\n\r\ninstance Foo [a] a\r\ninstance Bar [a] a\r\ninstance Foo ByteString Word8\r\ninstance Bar ByteString Word8\r\n\r\ntest :: Bar full item => full -> full\r\ntest inp = inp\r\n\r\n-- this works\r\n-- _test_x :: ByteString -> ByteString\r\n-- _test_x = test\r\n\r\n\r\n}}}\r\n\r\nfile Main.hs\r\n{{{\r\nmodule Main where\r\n\r\nimport Foo\r\nimport Data.ByteString\r\n\r\n-- this works\r\n-- test1 :: [Int] -> [Int]\r\n-- test1 = test\r\n\r\n-- this fails\r\ntest2 :: ByteString -> ByteString\r\ntest2 = test\r\n\r\n}}}\r\n\r\nghc reports\r\n\r\n{{{\r\nMain.hs:12:9:\r\n Overlapping instances for Foo ByteString GHC.Word.Word8\r\n arising from a use of `test'\r\n Matching instances:\r\n instance Foo ByteString GHC.Word.Word8 -- Defined at Foo.hs:20:10\r\n There exists a (perhaps superclass) match:\r\n (The choice depends on the instantiation of `'\r\n To pick the first instance above, use -XIncoherentInstances\r\n when compiling the other instance declarations)\r\n In the expression: test\r\n In an equation for `test2': test2 = test\r\n}}}\r\n\r\nFor this to manifest, I think that at least the following must be true:\r\n - a function with class constraints must be called from a separate module\r\n - the type class instance must be monomorphic in the fundep-to parameter\r\n\r\nThis example works in ghc-7.4.2.","type_of_failure":"OtherFailure","blocking":[]} -->7.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/7156"Pattern match on GADT" error for non-GADT2019-07-07T18:51:05Zryani"Pattern match on GADT" error for non-GADTIt's widely known that GADTs are just generalizations of type equality and existentials. And you can declare them that way!
```
{-# LANGUAGE TypeFamilies, ExistentialQuantification #-}
module NonGADT where
data T a = (a ~ ()) -> T
```
...It's widely known that GADTs are just generalizations of type equality and existentials. And you can declare them that way!
```
{-# LANGUAGE TypeFamilies, ExistentialQuantification #-}
module NonGADT where
data T a = (a ~ ()) -> T
```
But pattern matching on this gives a nasty error!
```
f :: T a -> a
f T = ()
```
```
{-
NonGADT.hs:7:3:
A pattern match on a GADT requires -XGADTs
In the pattern: T
In an equation for `f': f T = ()
-}
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.0.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":"\"Pattern match on GADT\" error for non-GADT","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.0.4","keywords":["ExistentialQuantification","GADTs,","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"It's widely known that GADTs are just generalizations of type equality and existentials. And you can declare them that way!\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies, ExistentialQuantification #-}\r\nmodule NonGADT where\r\ndata T a = (a ~ ()) -> T\r\n}}}\r\n\r\nBut pattern matching on this gives a nasty error!\r\n\r\n{{{\r\nf :: T a -> a\r\nf T = ()\r\n}}}\r\n\r\n{{{\r\n{-\r\nNonGADT.hs:7:3:\r\n A pattern match on a GADT requires -XGADTs\r\n In the pattern: T\r\n In an equation for `f': f T = ()\r\n -}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7148generalized newtype and type families is unsound2019-07-07T18:51:07ZCarter Schonwaldgeneralized newtype and type families is unsoundthe code from
http://joyoftypes.blogspot.com/2012/08/generalizednewtypederiving-is.html
type checks in the release candidate
also see discussion here http://www.reddit.com/r/haskell/comments/y8kca/generalizednewtypederiving_is_very_very...the code from
http://joyoftypes.blogspot.com/2012/08/generalizednewtypederiving-is.html
type checks in the release candidate
also see discussion here http://www.reddit.com/r/haskell/comments/y8kca/generalizednewtypederiving_is_very_very_unsafe/
(punch line: the generalized newtype deriving + type families or gadts allows users to write unsafeCoerce etc)
perhaps a simple near term solution is to have any module using generalized new type deriving be inferred to be unsafe by default?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.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":"generalized newtype and type families is unsound","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"the code from \r\nhttp://joyoftypes.blogspot.com/2012/08/generalizednewtypederiving-is.html\r\ntype checks in the release candidate\r\n\r\nalso see discussion here http://www.reddit.com/r/haskell/comments/y8kca/generalizednewtypederiving_is_very_very_unsafe/\r\n\r\n(punch line: the generalized newtype deriving + type families or gadts allows users to write unsafeCoerce etc)\r\n\r\nperhaps a simple near term solution is to have any module using generalized new type deriving be inferred to be unsafe by default? ","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/7140Allow type signature in export list2019-07-07T18:51:09ZDan BurtonAllow type signature in export listIn response to the new InstanceSigs extension in the 7.6.1 RC1, waterlight on Reddit suggested the following:
"While we're at it, why not also allow type signatures in export lists? People tend to add them anyway as comments, just becau...In response to the new InstanceSigs extension in the 7.6.1 RC1, waterlight on Reddit suggested the following:
"While we're at it, why not also allow type signatures in export lists? People tend to add them anyway as comments, just because it's useful documentation. Checking for consistency would be nice."
The desired syntax, therefore, is something like this:
```
{-# LANGUAGE ExportSigs #-}
module Foo
( foo :: Bar -> Baz
, Blah ( Blip :: a -> Blah a
, Bloop :: Blah Int )
, Quux ( quux :: Quux q => a -> q a
, qux :: Quux q => q (q ()) )
) where
...
```
where all of the type annotations here are optional, and can be **no less restrictive** than the corresponding type signatures provided at the definition site, if provided (whether that be in that file's own code, or imported from another file).
This would have non-trivial interaction with -fno-warn-missing-signatures, and consequently, with #2526.
There may also be non-trivial interaction with GADTs, if we allow exported constructors to be annotated with a type signature.
This idea was vaguely referenced by #1404, to which igloo responded:
"Type sigs in export lists might be nice, as some people seem to like giving them as comments which then get out of sync with the actual types."
If we are to consider this sort of thing for Haskell', we should try it out as a GHC extension first.8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/7082Default type family instances2019-07-07T18:51:27ZguestDefault type family instancesThe following code does not compile in GHC 7.4, unless line (2) is uncommented. I thought line (1) would remove need for (2). If it does not, probably declaration (1) should cause an error.
```
{-# LANGUAGE TypeFamilies #-}
class R m wh...The following code does not compile in GHC 7.4, unless line (2) is uncommented. I thought line (1) would remove need for (2). If it does not, probably declaration (1) should cause an error.
```
{-# LANGUAGE TypeFamilies #-}
class R m where
type D m a :: *
type D m a = () -- (1)
f :: m a -> D m a -> ()
instance R Maybe where
-- type D Maybe a = () -- (2)
f = undefined
x = f (Nothing :: Maybe Int) ()
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Default type family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code does not compile in GHC 7.4, unless line (2) is uncommented. I thought line (1) would remove need for (2). If it does not, probably declaration (1) should cause an error.\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\nclass R m where\r\n type D m a :: *\r\n type D m a = () -- (1)\r\n f :: m a -> D m a -> ()\r\n\r\ninstance R Maybe where\r\n -- type D Maybe a = () -- (2)\r\n f = undefined\r\n\r\nx = f (Nothing :: Maybe Int) ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7073Kind variable problem when declaring associated type family2019-07-07T18:51:31ZRichard Eisenbergrae@richarde.devKind variable problem when declaring associated type familyThe following code fails to compile:
```
{-# LANGUAGE PolyKinds, TypeFamilies #-}
class Foo a where
type Bar a
type Bar a = Int
```
The error I get is
```
Type indexes must match class instance head
Found `k' but expected...The following code fails to compile:
```
{-# LANGUAGE PolyKinds, TypeFamilies #-}
class Foo a where
type Bar a
type Bar a = Int
```
The error I get is
```
Type indexes must match class instance head
Found `k' but expected `k'
In the type synonym instance default declaration for `Bar'
In the class declaration for `Foo'
```
When I remove `-XPolyKinds`, the code compiles without a hiccup.
This was tested on 7.5.2012.0710
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| 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":"Kind variable problem when declaring associated type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds, TypeFamilies #-}\r\n\r\nclass Foo a where\r\n type Bar a\r\n type Bar a = Int\r\n}}}\r\n\r\nThe error I get is\r\n\r\n{{{\r\n Type indexes must match class instance head\r\n Found `k' but expected `k'\r\n In the type synonym instance default declaration for `Bar'\r\n In the class declaration for `Foo'\r\n}}}\r\n\r\nWhen I remove {{{-XPolyKinds}}}, the code compiles without a hiccup.\r\n\r\nThis was tested on 7.5.2012.0710","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7026Impredicative implicit parameters2020-09-24T18:34:19ZAshley YakeleyImpredicative implicit parametersThere doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:
```
{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
module Bug where
f1 :: Maybe ((?a :: Bool) => Char)
f1 = Just 'C'
f2 :: Maybe ...There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:
```
{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
module Bug where
f1 :: Maybe ((?a :: Bool) => Char)
f1 = Just 'C'
f2 :: Maybe ((?a :: Bool) => Bool)
f2 = Just ?a
```
```
$ ghc -c Bug.hs
Bug.hs:5:15:
Couldn't match expected type `(?a::Bool) => Char'
with actual type `Char'
In the first argument of `Just', namely 'C'
In the expression: Just 'C'
In an equation for `f1': f1 = Just 'C'
Bug.hs:8:15:
Unbound implicit parameter (?a::(?a::Bool) => Bool)
arising from a use of implicit parameter `?a'
In the first argument of `Just', namely `?a'
In the expression: Just ?a
In an equation for `f2': f2 = Just ?a
```
I believe this used to work?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.2 |
| 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":"Impredicative implicit parameters","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:\r\n\r\n{{{\r\n{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}\r\nmodule Bug where\r\n\r\n f1 :: Maybe ((?a :: Bool) => Char)\r\n f1 = Just 'C'\r\n\r\n f2 :: Maybe ((?a :: Bool) => Bool)\r\n f2 = Just ?a\r\n}}}\r\n\r\n\r\n{{{\r\n$ ghc -c Bug.hs \r\n\r\nBug.hs:5:15:\r\n Couldn't match expected type `(?a::Bool) => Char'\r\n with actual type `Char'\r\n In the first argument of `Just', namely 'C'\r\n In the expression: Just 'C'\r\n In an equation for `f1': f1 = Just 'C'\r\n\r\nBug.hs:8:15:\r\n Unbound implicit parameter (?a::(?a::Bool) => Bool)\r\n arising from a use of implicit parameter `?a'\r\n In the first argument of `Just', namely `?a'\r\n In the expression: Just ?a\r\n In an equation for `f2': f2 = Just ?a\r\n}}}\r\n\r\nI believe this used to work?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6147GeneralizedNewtypeDeriving should fail with data families2019-07-07T18:51:57Zrl@cse.unsw.edu.auGeneralizedNewtypeDeriving should fail with data familiesHere is an example:
```
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}
module Foo where
data family T a
data instance T Int = T_Int Int
class C a where
foo :: a -> T a
instance C Int where
foo = T_Int
newtype Foo = Fo...Here is an example:
```
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}
module Foo where
data family T a
data instance T Int = T_Int Int
class C a where
foo :: a -> T a
instance C Int where
foo = T_Int
newtype Foo = Foo Int deriving(C)
```
The `deriving(C)` clause on `Foo` should fail but instead it derives an instance which can't possible be correct since there is no corresponding `data instance T Foo`. This is closely related to #2721 (where newtype deriving was disabled in the presence of associated types) but much more difficult to test for. Probably also related to #1496.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GeneralizedNewtypeDeriving should fail with data families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is an example:\r\n\r\n{{{\r\n{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}\r\nmodule Foo where\r\n\r\ndata family T a\r\ndata instance T Int = T_Int Int\r\n\r\nclass C a where\r\n foo :: a -> T a\r\n\r\ninstance C Int where\r\n foo = T_Int\r\n\r\nnewtype Foo = Foo Int deriving(C)\r\n}}}\r\n\r\nThe `deriving(C)` clause on `Foo` should fail but instead it derives an instance which can't possible be correct since there is no corresponding `data instance T Foo`. This is closely related to #2721 (where newtype deriving was disabled in the presence of associated types) but much more difficult to test for. Probably also related to #1496.","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/6137Different behaviour between a GADT and a data family with regards to kind uni...2019-07-07T18:51:59ZdreixelDifferent behaviour between a GADT and a data family with regards to kind unificationWe have discussed this before, but I don't remember if this was classified as a bug or as a "known feature" of GADTs. Given the following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-...We have discussed this before, but I don't remember if this was classified as a bug or as a "known feature" of GADTs. Given the following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
data Sum a b = L a | R b
data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
LL :: a i -> Sum1 a b (L i)
RR :: b i -> Sum1 a b (R i)
data Code i o = F (Code (Sum i o) o)
```
An interpretation for `Code` using a data family works:
```
data family In (f :: Code i o) :: (i -> *) -> (o -> *)
data instance In (F f) r o where
In :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
```
However, if we try to use a GADT instead...
```
data In' (f :: Code i o) :: (i -> *) -> (o -> *) where
In' :: In' f (Sum1 r (In' (F f) r)) o -> In' (F f) r o
```
1. .. GHC complains:
```
Kind mis-match
The first argument of `F' should have kind `Code (Sum k0 k1) k1',
but `f' has kind `Code i o'
In the type `In' f (Sum1 r (In' (F f) r)) o'
In the definition of data constructor In'
In the data declaration for In'
```
Is there a good reason for the difference in behaviour? If so, is this something we should document?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| 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":"Different behaviour between a GADT and a data family with regards to kind unification","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"We have discussed this before, but I don't remember if this was classified as a bug or as a \"known feature\" of GADTs. Given the following code:\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE GADTs #-}\r\n\r\ndata Sum a b = L a | R b\r\n\r\ndata Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where\r\n LL :: a i -> Sum1 a b (L i)\r\n RR :: b i -> Sum1 a b (R i)\r\n\r\ndata Code i o = F (Code (Sum i o) o)\r\n}}}\r\n\r\nAn interpretation for `Code` using a data family works:\r\n{{{\r\ndata family In (f :: Code i o) :: (i -> *) -> (o -> *)\r\n\r\ndata instance In (F f) r o where\r\n In :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o\r\n}}}\r\n\r\nHowever, if we try to use a GADT instead...\r\n{{{\r\ndata In' (f :: Code i o) :: (i -> *) -> (o -> *) where\r\n In' :: In' f (Sum1 r (In' (F f) r)) o -> In' (F f) r o\r\n}}}\r\n\r\n... GHC complains:\r\n{{{\r\n Kind mis-match\r\n The first argument of `F' should have kind `Code (Sum k0 k1) k1',\r\n but `f' has kind `Code i o'\r\n In the type `In' f (Sum1 r (In' (F f) r)) o'\r\n In the definition of data constructor In'\r\n In the data declaration for In'\r\n}}}\r\n\r\nIs there a good reason for the difference in behaviour? If so, is this something we should document?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6134Incorrect ambiguity error with functional dependencies2019-07-07T18:52:00ZIavor S. DiatchkiIncorrect ambiguity error with functional dependenciesGHC reject a program as ambiguous when it is not. Consider the following example:
```
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
class C a b | a -> b where
f :: a -> b
test :: (Show a, C Int a) ...GHC reject a program as ambiguous when it is not. Consider the following example:
```
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
class C a b | a -> b where
f :: a -> b
test :: (Show a, C Int a) => Bool
test = show (f (1 :: Int)) == "1"
```
GHC rejects the program with the following error:
```
Ambiguous constraint `C Int a'
At least one of the forall'd type variables mentioned by the constraint
must be reachable from the type after the '=>'
In the type signature for `test': test :: (Show a, C Int a) => Bool
```
The only variable, `a`, is fully determined by the type `Int` via the functional dependency on class `C` so there is no ambiguity.
These sort of errors crop up when we desugar implicit parameters into uses of the `IP` class (which has a functional dependency).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Incorrect ambiguity error with functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC reject a program as ambiguous when it is not. Consider the following example:\r\n{{{\r\n{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}\r\n\r\nclass C a b | a -> b where\r\n f :: a -> b\r\n\r\ntest :: (Show a, C Int a) => Bool\r\ntest = show (f (1 :: Int)) == \"1\"\r\n}}}\r\nGHC rejects the program with the following error:\r\n{{{\r\n Ambiguous constraint `C Int a'\r\n At least one of the forall'd type variables mentioned by the constraint\r\n must be reachable from the type after the '=>'\r\n In the type signature for `test': test :: (Show a, C Int a) => Bool\r\n}}}\r\n\r\nThe only variable, {{{a}}}, is fully determined by the type `Int` via the functional dependency on class `C` so there is no ambiguity.\r\n\r\nThese sort of errors crop up when we desugar implicit parameters into uses of the `IP` class (which has a functional dependency). ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6124Spurious non-exhaustive warning with GADT and newtypes2019-09-30T21:37:27ZjoeyadamsSpurious non-exhaustive warning with GADT and newtypesThis may be related to #3927 or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:
```
newtype A = MkA Int
newtype B = M...This may be related to #3927 or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:
```
newtype A = MkA Int
newtype B = MkB Char
data T a where
A :: T A
B :: T B
f :: T A -> A
f A = undefined
```
This produces the following warning:
```
Warning: Pattern match(es) are non-exhaustive
In an equation for `f': Patterns not matched: B
```
It is impossible to write a pattern for `B` because `B :: T B` does not match `T A`.
If I replace `newtype` with `data` for both `A` and `B`, the warning goes away. If I replace only one instance of either `newtype`, it will still produce the warning.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Spurious non-exhaustive warning with GADT and newtypes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be related to #3927 or similar, but here's another case where the compiler produces a \"Pattern match(es) are non-exhaustive\" warning for patterns on a GADT that are impossible to implement:\r\n\r\n{{{\r\nnewtype A = MkA Int\r\nnewtype B = MkB Char\r\n\r\ndata T a where\r\n A :: T A\r\n B :: T B\r\n\r\nf :: T A -> A\r\nf A = undefined\r\n}}}\r\n\r\nThis produces the following warning:\r\n\r\n{{{\r\n Warning: Pattern match(es) are non-exhaustive\r\n In an equation for `f': Patterns not matched: B\r\n}}}\r\n\r\nIt is impossible to write a pattern for {{{B}}} because {{{B :: T B}}} does not match {{{T A}}}.\r\n\r\nIf I replace {{{newtype}}} with {{{data}}} for both {{{A}}} and {{{B}}}, the warning goes away. If I replace only one instance of either {{{newtype}}}, it will still produce the warning.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/6123occurs check should not apply to type families2019-07-07T18:52:04Zdmwitoccurs check should not apply to type familiesThis code:
```
{-# LANGUAGE TypeFamilies #-}
type family Id a
cid :: a ~ Id a => a -> a
cid x = x
cundefined = cid undefined
```
gives this error:
```
test.hs:5:14:
Occurs check: cannot construct the infinite type: a0 = Id a0
...This code:
```
{-# LANGUAGE TypeFamilies #-}
type family Id a
cid :: a ~ Id a => a -> a
cid x = x
cundefined = cid undefined
```
gives this error:
```
test.hs:5:14:
Occurs check: cannot construct the infinite type: a0 = Id a0
In the expression: cid undefined
In an equation for `cundefined': cundefined = cid undefined
```
whereas I think it should be possible to infer the type cundefined :: a \~ Id a =\> a. Equations with a variable on one side and a type family at the head of the other side should become constraints rather than being subject to the occurs check.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"occurs check should not apply to type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code:\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\ntype family Id a\r\ncid :: a ~ Id a => a -> a\r\ncid x = x\r\ncundefined = cid undefined\r\n}}}\r\ngives this error:\r\n{{{\r\ntest.hs:5:14:\r\n Occurs check: cannot construct the infinite type: a0 = Id a0\r\n In the expression: cid undefined\r\n In an equation for `cundefined': cundefined = cid undefined\r\n}}}\r\nwhereas I think it should be possible to infer the type cundefined :: a ~ Id a => a. Equations with a variable on one side and a type family at the head of the other side should become constraints rather than being subject to the occurs check.","type_of_failure":"OtherFailure","blocking":[]} -->Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/6117Cyclic Type Class Hierarchy Produces <<loop>>2019-07-07T18:52:05Zjun0Cyclic Type Class Hierarchy Produces <<loop>>If there is a cyclic class hierarchy like
```
class B a => Semigroup a where ...[[BR]]
class Semigroup (Additive a) => Ring a where ...[[BR]]
instance Ring a => Semigroup (Additive a) where ...[[BR]]
```
...If there is a cyclic class hierarchy like
```
class B a => Semigroup a where ...[[BR]]
class Semigroup (Additive a) => Ring a where ...[[BR]]
instance Ring a => Semigroup (Additive a) where ...[[BR]]
```
then uses of B's methods on `(Additive a)` in the method implementations of the
third declaration `instance Ring a => Semigroup (Additive a)` will:
1. be accepted by the compiler even in cases where `B (Additive a)` is not derivable.
1. result in \<\<loop\>\>.
The attached program prints \<\<loop\>\> when compiled with GHC-7.2.1 or newer but prints 1234567890 when compiled with GHC-7.0.4 or older. I haven't had time to try out any revisions in between those two, but I did check that HEAD produces \<\<loop\>\> as well.7.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/6093Kind polymorphism fails with recursive type definition using different kind2019-07-07T18:52:14ZAshley YakeleyKind polymorphism fails with recursive type definition using different kind```
{-# LANGUAGE GADTs, PolyKinds #-}
module Bug where
data R t where
MkR :: R f -> R (f ())
```
results in
```
Bug.hs:4:26:
Kind mis-match
The first argument of `R' should have kind `* -> k0',
but `f ()' has ki...```
{-# LANGUAGE GADTs, PolyKinds #-}
module Bug where
data R t where
MkR :: R f -> R (f ())
```
results in
```
Bug.hs:4:26:
Kind mis-match
The first argument of `R' should have kind `* -> k0',
but `f ()' has kind `k0'
In the type `R (f ())'
In the definition of data constructor `MkR'
In the data type declaration for `R'
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Kind polymorphism fails with recursive type definition using different kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE GADTs, PolyKinds #-}\r\nmodule Bug where\r\n data R t where\r\n MkR :: R f -> R (f ())\r\n}}}\r\nresults in\r\n{{{\r\nBug.hs:4:26:\r\n Kind mis-match\r\n The first argument of `R' should have kind `* -> k0',\r\n but `f ()' has kind `k0'\r\n In the type `R (f ())'\r\n In the definition of data constructor `MkR'\r\n In the data type declaration for `R'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6088GeneralizedNewtypeDeriving + TypeFamilies + Equality constraints2019-07-07T18:52:15ZLemmingGeneralizedNewtypeDeriving + TypeFamilies + Equality constraintsI have the following module that uses generalized newtype deriving:
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
class C a
newtype A n = A Int
class Pos n
instance (Pos n) => C (A n)
newtype B n = ...I have the following module that uses generalized newtype deriving:
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
class C a
newtype A n = A Int
class Pos n
instance (Pos n) => C (A n)
newtype B n = B (A n)
deriving (C)
```
This module can be compiled, and GHCi shows me what generalized newtype deriving generated for B:
```
*Main> :info B
newtype B n = B (A n) -- Defined at NewtypeSuperclass.hs:13:9
instance Pos n => C (B n) -- Defined at NewtypeSuperclass.hs:14:14
```
This is what I expected.
Now I want to translate the Pos type class to an equality constraint on a type function value:
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE EmptyDataDecls #-}
class C a
newtype A n = A Int
type family Pos n
data True
instance (Pos n ~ True) => C (A n)
newtype B n = B (A n)
deriving (C)
```
Now I get the compiler error:
```
Couldn't match type `Pos n' with `True'
arising from the 'deriving' clause of a data type declaration
When deriving the instance for (C (B n))
```
It seems that the equality constraint disallows generalized newtype deriving.
Is this an implementation issue or is there a deep theoretic problem?
I would certainly prefer to obtain something like:
```
*Main> :info B
newtype B n = B (A n)
instance (Pos n ~ True) => C (B n)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.1 |
| 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":"GeneralizedNewtypeDeriving + TypeFamilies + Equality constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I have the following module that uses generalized newtype deriving:\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n\r\nclass C a\r\n\r\n\r\nnewtype A n = A Int\r\n\r\nclass Pos n\r\ninstance (Pos n) => C (A n)\r\n\r\n\r\nnewtype B n = B (A n)\r\n deriving (C)\r\n}}}\r\nThis module can be compiled, and GHCi shows me what generalized newtype deriving generated for B:\r\n{{{\r\n*Main> :info B\r\nnewtype B n = B (A n) -- Defined at NewtypeSuperclass.hs:13:9\r\ninstance Pos n => C (B n) -- Defined at NewtypeSuperclass.hs:14:14\r\n}}}\r\nThis is what I expected.\r\n\r\nNow I want to translate the Pos type class to an equality constraint on a type function value:\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n{-# LANGUAGE EmptyDataDecls #-}\r\n\r\nclass C a\r\n\r\n\r\nnewtype A n = A Int\r\n\r\ntype family Pos n\r\ndata True\r\n\r\ninstance (Pos n ~ True) => C (A n)\r\n\r\n\r\nnewtype B n = B (A n)\r\n deriving (C)\r\n}}}\r\nNow I get the compiler error:\r\n{{{\r\n Couldn't match type `Pos n' with `True'\r\n arising from the 'deriving' clause of a data type declaration\r\n When deriving the instance for (C (B n))\r\n}}}\r\nIt seems that the equality constraint disallows generalized newtype deriving.\r\nIs this an implementation issue or is there a deep theoretic problem?\r\nI would certainly prefer to obtain something like:\r\n{{{\r\n*Main> :info B\r\nnewtype B n = B (A n)\r\ninstance (Pos n ~ True) => C (B n)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6081Kind variables not allowed in class instance declarations2019-07-07T18:52:17ZRichard Eisenbergrae@richarde.devKind variables not allowed in class instance declarationsConsider the following code:
```
{-# LANGUAGE KindSignatures, PolyKinds, DataKinds, RankNTypes #-}
data KProxy (a :: *) = KP
class KindClass (kp :: KProxy k)
instance KindClass (KP :: KProxy [k])
```
The last line fails to compile, p...Consider the following code:
```
{-# LANGUAGE KindSignatures, PolyKinds, DataKinds, RankNTypes #-}
data KProxy (a :: *) = KP
class KindClass (kp :: KProxy k)
instance KindClass (KP :: KProxy [k])
```
The last line fails to compile, producing the following error message:
```
Not in scope: type variable `k'
```
However, there is a workaround. When I change the last line to
```
instance forall (a :: k). KindClass (KP :: KProxy [k])
```
all is good. Unfortunately, this last line requires the declaration of an unused type variable `a`, which is a little messy.
This was tested on 7.5.20120426.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #6064 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind variables not allowed in class instance declarations","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[6064],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{\r\n{-# LANGUAGE KindSignatures, PolyKinds, DataKinds, RankNTypes #-}\r\n\r\ndata KProxy (a :: *) = KP\r\n\r\nclass KindClass (kp :: KProxy k)\r\ninstance KindClass (KP :: KProxy [k])\r\n}}}\r\n\r\nThe last line fails to compile, producing the following error message:\r\n\r\n{{{\r\n Not in scope: type variable `k'\r\n}}}\r\n\r\nHowever, there is a workaround. When I change the last line to\r\n\r\n{{{\r\ninstance forall (a :: k). KindClass (KP :: KProxy [k])\r\n}}}\r\n\r\nall is good. Unfortunately, this last line requires the declaration of an unused type variable {{{a}}}, which is a little messy.\r\n\r\nThis was tested on 7.5.20120426.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6074Instance inference failure with GADTs2019-07-07T18:52:18ZRichard Eisenbergrae@richarde.devInstance inference failure with GADTsConsider the following code:
```
{-# LANGUAGE GADTs, FlexibleInstances #-}
class Stringable a where
toString :: a -> String
data GADT a where
GInt :: GADT Int
GBool :: GADT Bool
instance Stringable (GADT Int) where
toString _...Consider the following code:
```
{-# LANGUAGE GADTs, FlexibleInstances #-}
class Stringable a where
toString :: a -> String
data GADT a where
GInt :: GADT Int
GBool :: GADT Bool
instance Stringable (GADT Int) where
toString _ = "constructor GInt"
instance Stringable (GADT Bool) where
toString _ = "constructor GBool"
mkString :: GADT a -> String
mkString g = toString g
mkString' :: GADT a -> String
mkString' g = case g of
GInt -> toString g
GBool -> toString g
```
The function `mkString` does not compile, while the function `mkString'` does. The problem seems to be that there is no instance declaration for `GADT a`, although there are instances for all the possible instantiations of `a`. It seems that requiring a `case` statement where all patterns are accounted for and all branches contain the same expression should be unnecessary.
This was tested on 7.5.20120426.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.5 |
| 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":"Instance inference failure with GADTs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, FlexibleInstances #-}\r\n\r\nclass Stringable a where\r\n toString :: a -> String\r\n\r\ndata GADT a where\r\n GInt :: GADT Int\r\n GBool :: GADT Bool\r\n\r\ninstance Stringable (GADT Int) where\r\n toString _ = \"constructor GInt\"\r\ninstance Stringable (GADT Bool) where\r\n toString _ = \"constructor GBool\"\r\n\r\nmkString :: GADT a -> String\r\nmkString g = toString g\r\n\r\nmkString' :: GADT a -> String\r\nmkString' g = case g of\r\n GInt -> toString g\r\n GBool -> toString g\r\n}}}\r\n\r\nThe function {{{mkString}}} does not compile, while the function {{{mkString'}}} does. The problem seems to be that there is no instance declaration for {{{GADT a}}}, although there are instances for all the possible instantiations of {{{a}}}. It seems that requiring a {{{case}}} statement where all patterns are accounted for and all branches contain the same expression should be unnecessary.\r\n\r\nThis was tested on 7.5.20120426.","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/6065Suggested type signature causes a type error (even though it appears correct)2019-07-07T18:52:21ZtvynrSuggested type signature causes a type error (even though it appears correct)The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast ...The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------------------- |
| Version | 7.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | zep_haskell_trac@bahj.com |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suggested type signature causes a type error (even though it appears correct)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["forall","instance","signature","type","typeclass"],"differentials":[],"test_case":"","architecture":"","cc":["zep_haskell_trac@bahj.com"],"type":"Bug","description":"The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.","type_of_failure":"OtherFailure","blocking":[]} -->