GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:01:01Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16188GHC HEAD-only panic (buildKindCoercion)2019-07-07T18:01:01ZRyan ScottGHC HEAD-only panic (buildKindCoercion)The following program compiles without issue on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators ...The following program compiles without issue on GHC 8.6.3:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Type.Bool (type (&&))
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type
data instance Sing :: Bool -> Type where
SFalse :: Sing False
STrue :: Sing True
(%&&) :: forall (x :: Bool) (y :: Bool).
Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue %&& a = a
data RegExp :: Type -> Type where
App :: RegExp t -> RegExp t -> RegExp t
data instance Sing :: forall t. RegExp t -> Type where
SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r
type family ReNotEmpty (r :: RegExp t) :: Bool where
ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
sReNotEmpty :: forall t (r :: RegExp t).
Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
blah :: forall (t :: Type) (re :: RegExp t).
Sing re -> ()
blah (SApp sre1 sre2)
= case (sReNotEmpty sre1, sReNotEmpty sre2) of
(STrue, STrue) -> ()
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20190114 for x86_64-unknown-linux):
buildKindCoercion
Any
ReNotEmpty re2_a1hm
Bool
t_a1hg
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"GHC HEAD-only panic (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles without issue on GHC 8.6.3:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Bool (type (&&))\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: a ~> b) (x :: a) :: b\r\ndata family Sing :: forall k. k -> Type\r\n\r\ndata instance Sing :: Bool -> Type where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\n\r\n(%&&) :: forall (x :: Bool) (y :: Bool).\r\n Sing x -> Sing y -> Sing (x && y)\r\nSFalse %&& _ = SFalse\r\nSTrue %&& a = a\r\n\r\ndata RegExp :: Type -> Type where\r\n App :: RegExp t -> RegExp t -> RegExp t\r\n\r\ndata instance Sing :: forall t. RegExp t -> Type where\r\n SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)\r\n\r\ndata ReNotEmptySym0 :: forall t. RegExp t ~> Bool\r\ntype instance Apply ReNotEmptySym0 r = ReNotEmpty r\r\n\r\ntype family ReNotEmpty (r :: RegExp t) :: Bool where\r\n ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2\r\n\r\nsReNotEmpty :: forall t (r :: RegExp t).\r\n Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)\r\nsReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2\r\n\r\nblah :: forall (t :: Type) (re :: RegExp t).\r\n Sing re -> ()\r\nblah (SApp sre1 sre2)\r\n = case (sReNotEmpty sre1, sReNotEmpty sre2) of\r\n (STrue, STrue) -> ()\r\n}}}\r\n\r\nHowever, it panics on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20190114 for x86_64-unknown-linux):\r\n buildKindCoercion\r\n Any\r\n ReNotEmpty re2_a1hm\r\n Bool\r\n t_a1hg\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14230Gruesome kind mismatch errors for associated data family instances2019-07-07T18:17:51ZRyan ScottGruesome kind mismatch errors for associated data family instancesSpun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
...Spun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C k where
data CD :: k -> k -> *
instance C (Maybe a) where
data CD :: (k -> *) -> (k -> *) -> *
```
Gives a heinous error message:
```
Bug.hs:11:3: error:
• Expected kind ‘(k -> *) -> (k -> *) -> *’,
but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
-> Maybe a -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
11 | data CD :: (k -> *) -> (k -> *) -> *
| ^^^^^^^
```
- We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.
- The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.
Another program in a similar vein:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C a where
data CD k (a :: k) :: k -> *
instance C (Maybe a) where
data CD k (a :: k -> *) :: (k -> *) -> *
```
```
Bug.hs:13:3: error:
• Expected kind ‘(k -> *) -> *’,
but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
13 | data CD k (a :: k -> *) :: (k -> *) -> *
| ^^^^^^^^^^^^^^^^^^^^^^^
```
This error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| 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":"Gruesome kind mismatch errors for associated data family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nclass C k where\r\n data CD :: k -> k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD :: (k -> *) -> (k -> *) -> *\r\n}}}\r\n\r\nGives a heinous error message:\r\n\r\n{{{\r\nBug.hs:11:3: error:\r\n • Expected kind ‘(k -> *) -> (k -> *) -> *’,\r\n but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a\r\n -> Maybe a -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n11 | data CD :: (k -> *) -> (k -> *) -> *\r\n | ^^^^^^^\r\n}}}\r\n\r\n* We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.\r\n* The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.\r\n\r\nAnother program in a similar vein:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C a where\r\n data CD k (a :: k) :: k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD k (a :: k -> *) :: (k -> *) -> *\r\n}}}\r\n{{{\r\nBug.hs:13:3: error:\r\n • Expected kind ‘(k -> *) -> *’,\r\n but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n13 | data CD k (a :: k -> *) :: (k -> *) -> *\r\n | ^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14887Explicitly quantifying a kind variable causes a telescope to fail to kind-check2019-07-07T18:15:11ZRyan ScottExplicitly quantifying a kind variable causes a telescope to fail to kind-checkConsider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type...Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
Foo1 (e :: a :~: a) = a :~: a
type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
Foo2 k (e :: a :~: a) = a :~: a
```
`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:10: error:
• Couldn't match kind ‘k’ with ‘k1’
When matching the kind of ‘a’
Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
• In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
In the type family declaration for ‘Foo2’
|
13 | Foo2 k (e :: a :~: a) = a :~: a
| ^^^^^^^^^^^^^^
```
(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Explicitly quantifying a kind variable causes a type family to fail to typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# OPTIONS_GHC -fprint-explicit-kinds #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo1 (e :: a :~: a) = a :~: a\r\n\r\ntype family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo2 k (e :: a :~: a) = a :~: a\r\n}}}\r\n\r\n`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:10: error:\r\n • Couldn't match kind ‘k’ with ‘k1’\r\n When matching the kind of ‘a’\r\n Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’\r\n • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’\r\n In the type family declaration for ‘Foo2’\r\n |\r\n13 | Foo2 k (e :: a :~: a) = a :~: a\r\n | ^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11549Add -fshow-runtime-rep2019-07-07T18:29:53ZRichard Eisenbergrae@richarde.devAdd -fshow-runtime-repAs discussed in several interwoven threads ([original](https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html), [café](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html)), it has been suggested to a...As discussed in several interwoven threads ([original](https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html), [café](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html)), it has been suggested to add a flag `-fshow-runtime-rep`. Without this flag enabled, the pretty printer will instantiate any `RuntimeRep` type parameters to `PtrRep Lifted`. This has the effect of changing
```
($) :: forall (r :: RuntimeRep) (a :: *) (b :: TYPE r). (a -> b) -> a -> b
```
to
```
($) :: (a -> b) -> a -> b
```
under the default GHCi settings.
Note that `Levity` becomes `RuntimeRep` after #11471 is complete.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Add -fshow-runtime-rep","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As discussed in several interwoven threads ([https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html original], [https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html café]), it has been suggested to add a flag `-fshow-runtime-rep`. Without this flag enabled, the pretty printer will instantiate any `RuntimeRep` type parameters to `PtrRep Lifted`. This has the effect of changing\r\n\r\n{{{\r\n($) :: forall (r :: RuntimeRep) (a :: *) (b :: TYPE r). (a -> b) -> a -> b\r\n}}}\r\n\r\nto\r\n\r\n{{{\r\n($) :: (a -> b) -> a -> b\r\n}}}\r\n\r\nunder the default GHCi settings.\r\n\r\nNote that `Levity` becomes `RuntimeRep` after #11471 is complete.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/9123Emit quantified Coercible constraints in GeneralizedNewtypeDeriving2024-01-11T02:06:42ZSimon Peyton JonesEmit quantified Coercible constraints in GeneralizedNewtypeDerivingThis [thread](http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html) on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread
```
class C m where
ret :: a -> m a
bind :: m...This [thread](http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html) on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread
```
class C m where
ret :: a -> m a
bind :: m a -> (a -> m b) -> m b
join :: m (m a) -> m a
newtype T m a = MkT (m a) deriving( C )
```
The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added.
```
T9123.hs:10:37:
Could not coerce from `m (m a)' to `m (T m a)'
because `m (m a)'
and `m (T m a)'
are different types.
arising from the coercion of the method `join'
from type `forall a. m (m a) -> m a'
to type `forall a. T m (T m a) -> T m a'
```
Note that the AMP proposal adds `join` to class `Monad`!
In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used.
This deficiency is noted in the [Safe Coercions paper](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/), but this seems to be the first occasion on which it has bitten us badly.
Edward [made a suggestion](http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html) on the thread.8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev