GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:29:09Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11672Poor error message2019-07-07T18:29:09ZAdam GundryPoor error message[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures ...[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) -> Int
f _ = f (Proxy :: Proxy (Int -> Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((->) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy
(Int -> Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int -> Bool))’
In the expression: f (Proxy :: Proxy (Int -> Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
```
or with `-fprint-explicit-kinds -fprint-explicit-coercions`:
```
• Expected kind ‘Proxy
Symbol
(((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
- It says `kind` when it should say `type`.
- `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).
- The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki, goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1-rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) -> Int\r\nf _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((->) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy\r\n (Int -> Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int -> Bool))’\r\n In the expression: f (Proxy :: Proxy (Int -> Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\nor with `-fprint-explicit-kinds -fprint-explicit-coercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} -->Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc/-/issues/11560panic: isInjectiveTyCon sees a TcTyCon2019-07-07T18:29:48Zrwbartonpanic: isInjectiveTyCon sees a TcTyConI typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160201: htt...I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeFamilies -XTypeInType
Prelude> :m +Data.Kind
Prelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160201 for x86_64-unknown-linux):
isInjectiveTyCon sees a TcTyCon T
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 | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"panic: isInjectiveTyCon sees a TcTyCon","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.\r\n{{{\r\nrwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XTypeFamilies -XTypeInType\r\nPrelude> :m +Data.Kind\r\nPrelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160201 for x86_64-unknown-linux):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11554Self quantification in GADT data declarations2020-09-19T20:01:19ZRafbillSelf quantification in GADT data declarationsGHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType...GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType #-}
import Data.Kind
data A :: Type where
B :: forall (a :: A). A
```
I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc2 |
| 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":"Self quantification in GADT data declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56) :\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeInType #-}\r\nimport Data.Kind\r\ndata A :: Type where\r\n B :: forall (a :: A). A\r\n}}}\r\n\r\nI guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11453Kinds in type synonym/data declarations can unexpectedly unify2019-07-07T18:30:21ZRyan ScottKinds in type synonym/data declarations can unexpectedly unifyWhile trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType ...While trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall (f :: k1 -> *). Either (f a) (f b)
-- Defined at <interactive>:2:1
```
This is pretty odd for two reasons. One, the kind `k1` was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:
```
λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall k2 (f :: k2 -> *). Either (f a) (f b)
-- Defined at <interactive>:4:1
```
We still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.
Note that this doesn't happen if you use explicit kind binders:
```
type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
<interactive>:6:74: error:
• Expected kind ‘k1’, but ‘a’ has kind ‘k2’
• In the first argument of ‘f’, namely ‘a’
In the first argument of ‘Either’, namely ‘f a’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
<interactive>:6:80: error:
• Expected kind ‘k1’, but ‘b’ has kind ‘k3’
• In the first argument of ‘f’, namely ‘b’
In the second argument of ‘Either’, namely ‘f b’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
```
only when the kinds are specified but not visible.
<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":"Kinds in type synonym/data declarations can unexpectedly unify","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":"While trying out ideas to fix [https://github.com/ekmett/lens/issues/626 this lens issue], I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators\r\nGHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/xnux/.ghci\r\nλ> import Data.Kind\r\nλ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall (f :: k1 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:2:1\r\n}}}\r\n\r\nThis is pretty odd for two reasons. One, the kind {{{k1}}} was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:\r\n\r\n{{{\r\nλ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall k2 (f :: k2 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:4:1\r\n}}}\r\n\r\nWe still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.\r\n\r\nNote that this doesn't happen if you use explicit kind binders:\r\n\r\n{{{\r\ntype Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\n\r\n<interactive>:6:74: error:\r\n • Expected kind ‘k1’, but ‘a’ has kind ‘k2’\r\n • In the first argument of ‘f’, namely ‘a’\r\n In the first argument of ‘Either’, namely ‘f a’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n\r\n<interactive>:6:80: error:\r\n • Expected kind ‘k1’, but ‘b’ has kind ‘k3’\r\n • In the first argument of ‘f’, namely ‘b’\r\n In the second argument of ‘Either’, namely ‘f b’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n}}}\r\n\r\nonly when the kinds are specified but not visible.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11410Quantification over unlifted type variable2019-07-07T18:30:32ZRichard Eisenbergrae@richarde.devQuantification over unlifted type variableThis silliness is accepted:
```
data X (a :: TYPE 'Unlifted) = X
```
I will fix.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version |...This silliness is accepted:
```
data X (a :: TYPE 'Unlifted) = X
```
I will fix.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Quantification over unlifted type variable","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This silliness is accepted:\r\n\r\n{{{\r\ndata X (a :: TYPE 'Unlifted) = X\r\n}}}\r\n\r\nI will fix.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev