GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:18:09Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14174GHC panic with TypeInType and type family2019-07-07T18:18:09ZDavid FeuerGHC panic with TypeInType and type familyThis rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y...This rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y
```
produces the following panic:
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
piResultTy
k_a1LK[tau:1]
p_a1Lz[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
```
This happens with both GHC 8.2.1 and something very close to HEAD.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"GHC panic with TypeInType and type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This rather simple type family,\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}\r\n\r\nmodule GenWhoops where\r\nimport GHC.Generics\r\n\r\ntype family GenComp k (x :: k) (y :: k) :: Ordering where\r\n GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y\r\n}}}\r\n\r\nproduces the following panic:\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n piResultTy\r\n k_a1LK[tau:1]\r\n p_a1Lz[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type\r\n}}}\r\n\r\nThis happens with both GHC 8.2.1 and something very close to HEAD.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/14175Panic repSplitTyConApp_maybe2019-07-07T18:18:08ZDavid FeuerPanic repSplitTyConApp_maybeThis definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3....This definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
repSplitTyConApp_maybe
j_aon[sk:1]
*
*
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type
```
If I make it a type synonym instead, I get a proper error as expected.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Panic repSplitTyConApp_maybe","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This definition panics!\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeInType #-}\r\n\r\nmodule Whoops where\r\nimport Data.Kind\r\n\r\ntype family PComp (k :: j -> Type) (x :: k) :: ()\r\n}}}\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n repSplitTyConApp_maybe\r\n j_aon[sk:1]\r\n *\r\n *\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type\r\n}}}\r\n\r\nIf I make it a type synonym instead, I get a proper error as expected.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14203GHC-inferred type signature doesn't actually typecheck2019-07-07T18:17:58ZRyan ScottGHC-inferred type signature doesn't actually typecheckThis code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * ->...This code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)
```
I was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:
```
λ> :i SMkSigma
data instance Sing z where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
x) (px :: Apply p x).
(Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)
```
I attempted to incorporate this newfound knowledge into the program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).
Sing sx -> Sing px -> Sing (MkSigma sx px)
```
But to my surprise, adding this inferred type signature causes the program to no longer typecheck!
```
GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:31: error:
• Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
• In the first argument of ‘Sing’, namely ‘px’
In the type ‘Sing px’
In the definition of data constructor ‘SMkSigma’
|
23 | Sing sx -> Sing px -> Sing (MkSigma sx px)
| ^^
```
I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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-inferred type signature doesn't actually typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nI was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:\r\n\r\n{{{\r\nλ> :i SMkSigma\r\ndata instance Sing z where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing\r\n x) (px :: Apply p x).\r\n (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)\r\n}}}\r\n\r\nI attempted to incorporate this newfound knowledge into the program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).\r\n Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nBut to my surprise, adding this inferred type signature causes the program to no longer typecheck!\r\n\r\n{{{\r\nGHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:31: error:\r\n • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’\r\n • In the first argument of ‘Sing’, namely ‘px’\r\n In the type ‘Sing px’\r\n In the definition of data constructor ‘SMkSigma’\r\n |\r\n23 | Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n | ^^\r\n}}}\r\n\r\nI'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14209GHC 8.2.1 regression involving telescoping kind signature2019-07-07T18:17:56ZRyan ScottGHC 8.2.1 regression involving telescoping kind signatureThe following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejecte...The following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejected:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘Foo’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
Type variables with inferred kinds:
(k :: *) (a :: k) (z :: MyProxy k a)
|
6 | data Foo (z :: MyProxy k (a :: k))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"GHC 8.2.1 regression involving telescoping kind signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata MyProxy k (a :: k) = MyProxy\r\ndata Foo (z :: MyProxy k (a :: k))\r\n}}}\r\n\r\nBut in GHC 8.2.1, it's rejected:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:6:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘Foo’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it explicitly somewhere?\r\n Type variables with inferred kinds:\r\n (k :: *) (a :: k) (z :: MyProxy k a)\r\n |\r\n6 | data Foo (z :: MyProxy k (a :: k))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://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/14238`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.12019-07-07T18:17:49ZRyan Scott`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it w...Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it what the kind of `Foo` is:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :k Foo
Foo :: k -> *
```
This is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.
A workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:
```
λ> :set -fprint-explicit-foralls
λ> :k Foo
Foo :: forall k -> k -> *
```
This is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> :k Foo
Foo :: forall k -> k -> Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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` suppresses visible dependent quantifiers by default in GHCi 8.2.1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this program into GHCi on 8.2.1 or later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (k :: Type) :: k -> Type where\r\n MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)\r\n}}}\r\n\r\nAnd ask it what the kind of `Foo` is:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :k Foo\r\nFoo :: k -> *\r\n}}}\r\n\r\nThis is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.\r\n\r\nA workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:\r\n\r\n{{{\r\nλ> :set -fprint-explicit-foralls \r\nλ> :k Foo\r\nFoo :: forall k -> k -> *\r\n}}}\r\n\r\nThis is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, modules loaded: Main.\r\nλ> :k Foo\r\nFoo :: forall k -> k -> Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14350Infinite loop when typechecking incorrect implementation (GHC HEAD only)2019-07-07T18:17:22ZRyan ScottInfinite loop when typechecking incorrect implementation (GHC HEAD only)On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ...On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data Proxy a = Proxy
data family Sing (a :: k)
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (x :: Proxy k) where
SProxy :: Sing 'Proxy
instance SingKind (Proxy k) where
type Demote (Proxy k) = Proxy k
fromSing SProxy = Proxy
toSing Proxy = SomeSing SProxy
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
toSing = undefined
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
Sing f
-> Sing g
-> Sing x
-> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
dcomp f g x = applySing f Proxy Proxy
```
This is a regression from GHC 8.2.1/8.2.2, where it gives a proper error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:59:15: error:
• Couldn't match expected type ‘Proxy a2
-> Apply (Apply (c x4) 'Proxy) (Apply (g x4) 'Proxy)’
with actual type ‘Sing (f x y @@ t0)’
• The function ‘applySing’ is applied to three arguments,
but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
has only two
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:59:27: error:
• Couldn't match expected type ‘Sing t0’
with actual type ‘Proxy a0’
• In the second argument of ‘applySing’, namely ‘Proxy’
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14352Higher-rank kind ascription oddities2019-07-07T18:17:21ZRyan ScottHigher-rank kind ascription odditiesGHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy...GHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)
g = Proxy
```
However, it does not accept this one, which (AFAICT) should be equivalent to the two above:
```hs
h :: forall x. Proxy (x :: forall b. b -> Int)
h = Proxy
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:23: error:
• Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely
‘(x :: forall b. b -> Int)’
In the type signature:
h :: forall x. Proxy (x :: forall b. b -> Int)
|
13 | h :: forall x. Proxy (x :: forall b. b -> Int)
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Higher-rank kind ascription oddities","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts these two definitions:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nf :: forall (x :: forall a. a -> Int). Proxy x\r\nf = Proxy\r\n\r\ng :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)\r\ng = Proxy\r\n}}}\r\n\r\nHowever, it does not accept this one, which (AFAICT) should be equivalent to the two above:\r\n\r\n{{{#!hs\r\nh :: forall x. Proxy (x :: forall b. b -> Int)\r\nh = Proxy\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:23: error:\r\n • Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘Proxy’, namely\r\n ‘(x :: forall b. b -> Int)’\r\n In the type signature:\r\n h :: forall x. Proxy (x :: forall b. b -> Int)\r\n |\r\n13 | h :: forall x. Proxy (x :: forall b. b -> Int)\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14366Type family equation refuses to unify wildcard type patterns2019-07-07T18:17:18ZRyan ScottType family equation refuses to unify wildcard type patternsThis typechecks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
Howe...This typechecks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
However, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast _ _ Refl x = x
```
Then GHC gets confused:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:9:12: error:
• Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’
• In the third argument of ‘Cast’, namely ‘Refl’
In the type family declaration for ‘Cast’
|
9 | Cast _ _ Refl x = x
| ^^^^
```
A workaround is to explicitly write out what should be inferred by the underscores:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast a a Refl x = x
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Type family equation refuses to unify wildcard type patterns","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (e :: a :~: b) (x :: a) :: b where\r\n Cast Refl x = x\r\n}}}\r\n\r\nHowever, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast _ _ Refl x = x\r\n}}}\r\n\r\nThen GHC gets confused:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:12: error:\r\n • Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’\r\n • In the third argument of ‘Cast’, namely ‘Refl’\r\n In the type family declaration for ‘Cast’\r\n |\r\n9 | Cast _ _ Refl x = x\r\n | ^^^^\r\n}}}\r\n\r\nA workaround is to explicitly write out what should be inferred by the underscores:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast a a Refl x = x\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/14394Inferred type for pattern synonym has redundant equality constraint2019-07-07T18:17:11ZRyan ScottInferred type for pattern synonym has redundant equality constraintLoad this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.o...Load this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
```
Notice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}
module Works where
import Data.Type.Equality
pattern Foo = HRefl
```
```
λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
(b :: k2) ~~ (a :: k1)) => a :~~: b
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Inferred type for pattern synonym has redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :i Foo\r\npattern Foo :: () => (* ~ *, b ~ a) => a :~~: b\r\n}}}\r\n\r\nNotice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Works where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\nλ> :i Foo\r\npattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,\r\n (b :: k2) ~~ (a :: k1)) => a :~~: b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14441GHC HEAD regression involving type families in kinds2019-07-07T18:17:02ZRyan ScottGHC HEAD regression involving type families in kindsIn GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k)...In GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
data Prox (a :: k) = P
type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
$(return [])
type instance DemoteX P = P
```
(Note that the `$(return [])` line is essential, as it works around #13790.)
However, on GHC HEAD, this now fails:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:27: error:
• Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’
• In the type ‘P’
In the type instance declaration for ‘DemoteX’
|
15 | type instance DemoteX P = P
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression involving type families in kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In GHC 8.2.1, this file typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\ndata Prox (a :: k) = P\r\n\r\ntype instance Demote (Prox (a :: k)) = Prox (DemoteX a)\r\n$(return [])\r\ntype instance DemoteX P = P\r\n}}}\r\n\r\n(Note that the `$(return [])` line is essential, as it works around #13790.)\r\n\r\nHowever, on GHC HEAD, this now fails:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:27: error:\r\n • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’\r\n • In the type ‘P’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n15 | type instance DemoteX P = P\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14450GHCi spins forever2019-07-07T18:16:59ZIcelandjackGHCi spins foreverThe following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import ...The following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type Cat ob = ob -> ob -> Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (->)
type Cod (IddSym0 :: Type ~> Type) = (->)
varpa :: (a -> a') -> (a -> a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (->)
```
it sends GHC for a spin.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type -> Type -> Type\r\n\r\ntype a ~> b = TyFun a b -> Type\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n type Cod (IddSym0 :: Type ~> Type) = (->)\r\n\r\n varpa :: (a -> a') -> (a -> a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14507Core Lint error with Type.Reflection and pattern synonyms2019-07-07T18:16:45ZIcelandjackCore Lint error with Type.Reflection and pattern synonyms```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
impor...```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
import Type.Reflection
import Prelude
import Data.Kind
data Dict c where
Dict :: c => Dict c
data N = O | S N
foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)
foo krep rep = do
HRefl <- eqTypeRep krep (typeRepKind rep)
pure (HRefl, rep)
pattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)
pattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))
where Bloop' HRefl rep = rep
type family
SING = (res :: k -> Type) | res -> k where
-- Core Lint error disappears with this line:
SING = (TypeRep :: N -> Type)
pattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)
pattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))
where RepN tr = tr
asTypeable :: TypeRep a -> Dict (Typeable a)
asTypeable rep =
withTypeable rep
Dict
pattern TypeRep :: () => Typeable a => TypeRep a
pattern TypeRep <- (asTypeable -> Dict)
where TypeRep = typeRep
-- error
pattern SO = RepN TypeRep
```
triggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Core Lint error with Type.Reflection and pattern synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}\r\n\r\nimport Type.Reflection\r\nimport Prelude\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata N = O | S N\r\n\r\nfoo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)\r\nfoo krep rep = do\r\n HRefl <- eqTypeRep krep (typeRepKind rep)\r\n pure (HRefl, rep)\r\n\r\npattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)\r\npattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))\r\n where Bloop' HRefl rep = rep\r\n\r\ntype family \r\n SING = (res :: k -> Type) | res -> k where\r\n -- Core Lint error disappears with this line:\r\n SING = (TypeRep :: N -> Type)\r\n\r\npattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)\r\npattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))\r\n where RepN tr = tr\r\n\r\nasTypeable :: TypeRep a -> Dict (Typeable a)\r\nasTypeable rep =\r\n withTypeable rep\r\n Dict\r\n\r\npattern TypeRep :: () => Typeable a => TypeRep a\r\npattern TypeRep <- (asTypeable -> Dict)\r\n where TypeRep = typeRep\r\n\r\n-- error \r\npattern SO = RepN TypeRep\r\n}}}\r\n\r\ntriggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14515"Same" higher-rank kind synonyms behave differently2019-07-07T18:16:43ZIcelandjack"Same" higher-rank kind synonyms behave differentlyAs you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL ...As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL a a
```
Let us capture `forall k2. k2 -> ..` with a kind synonym
```hs
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: forall k. k -> HRank2 Type where
HREFL :: HREFL a a
```
Works fine. Phew. Let's do the same for `forall k1. k1 -> ..`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: HRank1 (HRank2 Type) where
HREFL :: HREFL a a
```
Works fine. Phew.
“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!
```hs
data HREFL :: HRank1 (HRank1 Type) -- FAILS
data HREFL :: HRank1 (HRank2 Type) -- OK
data HREFL :: HRank2 (HRank1 Type) -- OK
data HREFL :: HRank2 (HRank2 Type) -- FAILS
```
```
$ ghci -ignore-dot-ghci /tmp/Weird.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )
/tmp/Weird.hs:8:1: error:
• These kind and type variables: (b :: k2) k2 (d :: k2)
are out of dependency order. Perhaps try this ordering:
k2 (b :: k2) (d :: k2)
• In the data type declaration for ‘HREFL’
|
8 | data HREFL :: HRank2 (HRank2 Type)
| ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude>
```
Same happens defining `HRank2` in terms of `HRank1`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = HRank1 ty
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"\"Same\" higher-rank kind synonyms behave differently","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind\r\n\r\n{{{#!hs\r\n-- Different from\r\n-- HREFL :: forall k1 k2. k1 -> k2 -> Type\r\n-- \r\ndata HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nLet us capture `forall k2. k2 -> ..` with a kind synonym\r\n\r\n{{{#!hs\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: forall k. k -> HRank2 Type where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nWorks fine. Phew. Let's do the same for `forall k1. k1 -> ..`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: HRank1 (HRank2 Type) where\r\n HREFL :: HREFL a a \r\n}}}\r\n\r\nWorks fine. Phew. \r\n\r\n“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!\r\n\r\n{{{#!hs\r\ndata HREFL :: HRank1 (HRank1 Type) -- FAILS\r\ndata HREFL :: HRank1 (HRank2 Type) -- OK\r\ndata HREFL :: HRank2 (HRank1 Type) -- OK \r\ndata HREFL :: HRank2 (HRank2 Type) -- FAILS\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/Weird.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )\r\n\r\n/tmp/Weird.hs:8:1: error:\r\n • These kind and type variables: (b :: k2) k2 (d :: k2)\r\n are out of dependency order. Perhaps try this ordering:\r\n k2 (b :: k2) (d :: k2)\r\n • In the data type declaration for ‘HREFL’\r\n |\r\n8 | data HREFL :: HRank2 (HRank2 Type) \r\n | ^^^^^^^^^^\r\nFailed, 0 modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nSame happens defining `HRank2` in terms of `HRank1`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = HRank1 ty\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14520GHC panic (TypeInType)2019-07-07T18:16:41ZIcelandjackGHC panic (TypeInType)```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp:...```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp::kat·b·c -> kat·a·b -> kat·a·c
class SCategory kat where
sId :: Sing a -> Sing (Id::kat a a)
sComp :: Sing f -> Sing g -> Sing (Comp f g)
```
triggers a panic
```
$ ghci -ignore-dot-ghci Bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
piResultTy
k_a1KI[tau:1]
a_a1vb[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type
typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type
typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC panic (TypeInType)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language TypeInType, TypeFamilies, TypeOperators #-}\r\n\r\nimport Data.Kind\r\n\r\ntype a ~>> b = (a, b) -> Type\r\n\r\ndata family Sing (a::k)\r\n\r\ntype family\r\n (·) (f::a~>>b) (x::a)::b\r\n\r\nclass PCategory kat where\r\n type Id ::kat·a·a\r\n type Comp::kat·b·c -> kat·a·b -> kat·a·c\r\n\r\nclass SCategory kat where\r\n sId :: Sing a -> Sing (Id::kat a a)\r\n sComp :: Sing f -> Sing g -> Sing (Comp f g)\r\n}}}\r\n\r\ntriggers a panic\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci Bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a1KI[tau:1]\r\n a_a1vb[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type\r\n typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type\r\n typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14552GHC panic on pattern synonym2019-07-07T18:16:32ZIcelandjackGHC panic on pattern synonym```hs
{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
import Data.Kind
data family Sing a
type a --> b = (a, b) -> Type
type family (@@)...```hs
{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
import Data.Kind
data family Sing a
type a --> b = (a, b) -> Type
type family (@@) (f::a --> b) (x::a) :: b
data Proxy a = Proxy
newtype Limit' :: (k --> Type) -> Type where
Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f
data Exp :: [Type] -> Type -> Type where
TLam' :: Proxy f
-> (forall aa. Proxy aa -> Exp xs (f @@ aa))
-> Exp xs (Limit' f)
pattern FOO f <- TLam' Proxy (($ Proxy) -> f)
```
---\>
```
$ ghci -ignore-dot-ghci 119-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 119-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
ASSERT failed!
in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC}
tenv [a1MC :-> r_a1MC]
cenv []
tys [k_a1Mj[ssk:3]]
cos []
needInScope [a1Mj :-> k_a1Mj[ssk:3]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| 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":"GHC panic on pattern synonym","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["PatternSynonyms,","TypeInType,","ViewPatterns"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing a\r\n\r\ntype a --> b = (a, b) -> Type\r\n\r\ntype family (@@) (f::a --> b) (x::a) :: b\r\n\r\ndata Proxy a = Proxy\r\n\r\nnewtype Limit' :: (k --> Type) -> Type where\r\n Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f\r\n\r\ndata Exp :: [Type] -> Type -> Type where\r\n TLam' :: Proxy f\r\n -> (forall aa. Proxy aa -> Exp xs (f @@ aa))\r\n -> Exp xs (Limit' f)\r\n\r\npattern FOO f <- TLam' Proxy (($ Proxy) -> f)\r\n}}}\r\n\r\n--->\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 119-bug.hs \r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 119-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tASSERT failed!\r\n in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC}\r\n tenv [a1MC :-> r_a1MC]\r\n cenv []\r\n tys [k_a1Mj[ssk:3]]\r\n cos []\r\n needInScope [a1Mj :-> k_a1Mj[ssk:3]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep\r\n substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep\r\n substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep\r\n substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep\r\n substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14555GHC Panic with TypeInType / levity polymorphism2019-07-07T18:16:32ZIcelandjackGHC Panic with TypeInType / levity polymorphism```hs
{-# Language TypeInType #-}
{-# Language TypeOperators, DataKinds, PolyKinds #-}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] -> TYPE rep -> Type where
Lam :: Exp (a:xs) b -> Exp xs (a -> b)
```
gives
```
$...```hs
{-# Language TypeInType #-}
{-# Language TypeOperators, DataKinds, PolyKinds #-}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] -> TYPE rep -> Type where
Lam :: Exp (a:xs) b -> Exp xs (a -> b)
```
gives
```
$ ghci -ignore-dot-ghci hs/126-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
caused by `TypeInType`. Removing the first line, we get an error
```
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )
hs/126-bug.hs:7:19: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] -> TYPE rep -> Type’
|
7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where
| ^^^
hs/126-bug.hs:7:32: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] -> TYPE rep -> Type’
|
7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where
| ^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| 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":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language TypeInType #-}\r\n{-# Language TypeOperators, DataKinds, PolyKinds #-}\r\n\r\nimport Data.Kind\r\nimport GHC.Types (TYPE)\r\n\r\ndata Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n Lam :: Exp (a:xs) b -> Exp xs (a -> b)\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci hs/126-bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\ncaused by `TypeInType`. Removing the first line, we get an error\r\n\r\n{{{\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )\r\n\r\nhs/126-bug.hs:7:19: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] -> TYPE rep -> Type’\r\n |\r\n7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n | ^^^\r\n\r\nhs/126-bug.hs:7:32: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] -> TYPE rep -> Type’\r\n |\r\n7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n | ^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14556Core Lint error: Ill-kinded result in coercion2019-07-07T18:16:31ZIcelandjackCore Lint error: Ill-kinded result in coercion```hs
{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type ...```hs
{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type Type
type family
(@@) (f::Fn k k') (a::k)::k' where
IdSym @@ a = a
data KIND = X | FNARR KIND KIND
data TY :: KIND -> Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') -> TY k -> TY k'
data TyRep (kind::KIND) :: TY kind -> Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
-> TyRep k a
-> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = Fn (IK k) (IK k')
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a -> IT a
zero = undefined
```
which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-lint` (8.3.20171122) attached.
It compiles fine with
```hs
zero :: TyRep X a -> IT a
zero = zero
```
but fails with `zero = let x = x in x`. See #14554.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| 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":"Core Lint error: Ill-kinded result in coercion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata Fn a b where\r\n IdSym :: Fn Type Type\r\n\r\ntype family\r\n (@@) (f::Fn k k') (a::k)::k' where\r\n IdSym @@ a = a\r\n\r\ndata KIND = X | FNARR KIND KIND\r\n\r\ndata TY :: KIND -> Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') -> TY k -> TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind -> Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n -> TyRep k a\r\n -> TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = Fn (IK k) (IK k')\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a -> IT a\r\nzero = undefined \r\n}}}\r\n\r\nwhich gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-lint` (8.3.20171122) attached. \r\n\r\nIt compiles fine with\r\n\r\n{{{#!hs\r\nzero :: TyRep X a -> IT a\r\nzero = zero\r\n}}}\r\n\r\nbut fails with `zero = let x = x in x`. See #14554.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14563GHC Panic with TypeInType / levity polymorphism2019-07-07T18:16:30ZIcelandjackGHC Panic with TypeInType / levity polymorphismThis code is rightfully rejected.
```hs
-- {-# Language TypeInType #-}
{-# Language RankNTypes, KindSignatures, PolyKinds #-}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a w...This code is rightfully rejected.
```hs
-- {-# Language TypeInType #-}
{-# Language RankNTypes, KindSignatures, PolyKinds #-}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. (g xx -> a) -> h xx -> Lan g h a
```
But uncomment first line and it panics
```
$ ghci2 ~/hs/132-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/132-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
Maybe the same as #14555.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code is rightfully rejected.\r\n\r\n{{{#!hs\r\n-- {-# Language TypeInType #-}\r\n{-# Language RankNTypes, KindSignatures, PolyKinds #-}\r\n\r\nimport GHC.Types (TYPE)\r\nimport Data.Kind\r\n\r\ndata Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. (g xx -> a) -> h xx -> Lan g h a\r\n}}}\r\n\r\nBut uncomment first line and it panics\r\n\r\n{{{\r\n$ ghci2 ~/hs/132-bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/132-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}\r\n\r\nMaybe the same as #14555.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14580GHC panic (TypeInType) (the 'impossible' happened)2019-07-07T18:16:25ZIcelandjackGHC panic (TypeInType) (the 'impossible' happened)```
$ ghci -ignore-dot-ghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators
Prelude Data.Kind> type Cat ob = ob ...```
$ ghci -ignore-dot-ghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators
Prelude Data.Kind> type Cat ob = ob -> ob -> Type
Prelude Data.Kind> data ISO' :: Cat i -> i -> i -> Type
Prelude Data.Kind> type ISO cat a b = ISO' cat a b -> Type
Prelude Data.Kind> type (a <--> b) iso cat = ISO (iso :: cat a b)
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171208 for x86_64-unknown-linux):
piResultTy
k_a1x1[tau:1]
a_a1wU[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Prelude Data.Kind>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| 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":"GHC panic (TypeInType) (the 'impossible' happened)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n$ ghci -ignore-dot-ghci\r\nGHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators \r\nPrelude Data.Kind> type Cat ob = ob -> ob -> Type\r\nPrelude Data.Kind> data ISO' :: Cat i -> i -> i -> Type\r\nPrelude Data.Kind> type ISO cat a b = ISO' cat a b -> Type\r\nPrelude Data.Kind> type (a <--> b) iso cat = ISO (iso :: cat a b)\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171208 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a1x1[tau:1]\r\n a_a1wU[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\nPrelude Data.Kind> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->