GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201023T15:11:08Zhttps://gitlab.haskell.org/ghc/ghc//issues/18855GHC 9.0+ regression in checking program with higherrank kinds20201023T15:11:08ZRyan ScottGHC 9.0+ regression in checking program with higherrank kindsGHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```GHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```9.0.1https://gitlab.haskell.org/ghc/ghc//issues/17841"No skolem info" panic with PolyKinds20201019T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_64## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2https://gitlab.haskell.org/ghc/ghc//issues/17566GHC 8.10 regression: Core Lint error when defining instance of CUSKless class20201019T09:14:39ZRyan ScottGHC 8.10 regression: Core Lint error when defining instance of CUSKless classHere are two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Lib where
import Data.Kind
class C (f :: k > Type) z where
type T (x :: f a) :: f a
```
```hs
 App.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module App where
import Data.Kind
import Data.Proxy
import Lib
type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
type T x = F x
```
Compiling this with GHC 8.8.1 passes Core Lint:
```
$ /opt/ghc/8.8.1/bin/ghc c Lib.hs && /opt/ghc/8.8.1/bin/ghc c App.hs dcorelint
```
But it does _not_ pass Core Lint on GHC 8.10.1alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc c Lib.hs && /opt/ghc/8.10.1/bin/ghc c App.hs dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
Core Lint error
<no location info>: warning:
The variable @ k1_aiz is out of scope
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
T
[TCvSubst
In scope: InScope {k1_aiz a_awk x_awl}
Type env: [aig :> x_awl, awg :> a_awk]
Co env: []]
[a_awk, x_awl]
[]
[k1_aiz, Proxy, a_awk, x_awl]
F x_awl
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst
```

Another curious thing is that if you load `Lib.hs` into GHCi, you'll observe something strange about the kind of `T`:
```
$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 > *) > k > Constraint
class C f z where
type T :: forall k2 (f :: k1 > *) (a :: k2). f a > f a
type family T x
 Defined at Lib.hs:11:3
```
Note that `T` has kind `forall k2 (f :: k1 > *) (a :: k2). f a > f a`, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.Here are two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Lib where
import Data.Kind
class C (f :: k > Type) z where
type T (x :: f a) :: f a
```
```hs
 App.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module App where
import Data.Kind
import Data.Proxy
import Lib
type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
type T x = F x
```
Compiling this with GHC 8.8.1 passes Core Lint:
```
$ /opt/ghc/8.8.1/bin/ghc c Lib.hs && /opt/ghc/8.8.1/bin/ghc c App.hs dcorelint
```
But it does _not_ pass Core Lint on GHC 8.10.1alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc c Lib.hs && /opt/ghc/8.10.1/bin/ghc c App.hs dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
Core Lint error
<no location info>: warning:
The variable @ k1_aiz is out of scope
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
T
[TCvSubst
In scope: InScope {k1_aiz a_awk x_awl}
Type env: [aig :> x_awl, awg :> a_awk]
Co env: []]
[a_awk, x_awl]
[]
[k1_aiz, Proxy, a_awk, x_awl]
F x_awl
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst
```

Another curious thing is that if you load `Lib.hs` into GHCi, you'll observe something strange about the kind of `T`:
```
$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 > *) > k > Constraint
class C f z where
type T :: forall k2 (f :: k1 > *) (a :: k2). f a > f a
type family T x
 Defined at Lib.hs:11:3
```
Note that `T` has kind `forall k2 (f :: k1 > *) (a :: k2). f a > f a`, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.8.10.2https://gitlab.haskell.org/ghc/ghc//issues/18831GHC requires PolyKinds in places without any kind polymorphism20201014T16:36:06ZRyan ScottGHC requires PolyKinds in places without any kind polymorphismI would expect the following to typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 > Type
```
Surprisingly, however, it doesn't.
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: 0
Did you mean to enable PolyKinds?

8  data T :: Proxy 0 > Type
 ^
```
I find it quite surprising that using a typelevel literal would require `PolyKinds`, as there's nothing inherently polykinded about it.
This isn't even the only example of strange `PolyKinds` requirements. The following programs are also rejected for similar reasons:
* Kindlevel uses of `=>`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: () => Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:11: error:
Illegal kind: () => Type
Did you mean to enable PolyKinds?

7  data T :: () => Type
 ^^^^^^^^^^
```
</details>
* Kindlevel uses of explicit annotations:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: (Type :: Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:12: error:
Illegal kind: Type :: Type
Did you mean to enable PolyKinds?

7  data T :: (Type :: Type) > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted lists:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '[Type,Type] > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '[Type, Type]
Did you mean to enable PolyKinds?

8  data T :: Proxy '[Type,Type] > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted tuples:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '(Type,Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '(Type, Type)
Did you mean to enable PolyKinds?

8  data T :: Proxy '(Type,Type) > Type
 ^^^^^^^^^^^^
```
</details>I would expect the following to typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 > Type
```
Surprisingly, however, it doesn't.
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: 0
Did you mean to enable PolyKinds?

8  data T :: Proxy 0 > Type
 ^
```
I find it quite surprising that using a typelevel literal would require `PolyKinds`, as there's nothing inherently polykinded about it.
This isn't even the only example of strange `PolyKinds` requirements. The following programs are also rejected for similar reasons:
* Kindlevel uses of `=>`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: () => Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:11: error:
Illegal kind: () => Type
Did you mean to enable PolyKinds?

7  data T :: () => Type
 ^^^^^^^^^^
```
</details>
* Kindlevel uses of explicit annotations:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: (Type :: Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:12: error:
Illegal kind: Type :: Type
Did you mean to enable PolyKinds?

7  data T :: (Type :: Type) > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted lists:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '[Type,Type] > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '[Type, Type]
Did you mean to enable PolyKinds?

8  data T :: Proxy '[Type,Type] > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted tuples:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '(Type,Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '(Type, Type)
Did you mean to enable PolyKinds?

8  data T :: Proxy '(Type,Type) > Type
 ^^^^^^^^^^^^
```
</details>https://gitlab.haskell.org/ghc/ghc//issues/18488DerivingVia: Kinding information isn't propagated20200722T00:36:30ZGeshDerivingVia: Kinding information isn't propagated## Summary
Using `DerivingVia` unexpectedly restricts the flow of kinding information. This is problematic in modules with `PolyKinds` enabled, since it limits what sources of kinding information are available
## Steps to reproduce
Consider the following snippet.
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE StandaloneDeriving #}
class C t
newtype Tag t a = T a
newtype Tag' t a = T' a
instance (C t, Eq t) => Eq (Tag t a)
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
```
Clearly, from the context `Eq t`, we infer `t :: Type`. GHC disagrees:
```
• Expected a type, but ‘t’ has kind ‘k’
• In the first argument of ‘Eq’, namely ‘t’
In the standalone deriving instance for
‘(C t, Eq t) => Eq (Tag' t a)’
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
^
```
OK, fine. Maybe GHC doesn't take the context into consideration. Let's try monomorphising other indeces involved. Surprise, both writing `class C (t :: *)` and `newtype Tag' (t :: *) a` fail to give enough kinding information to satisfy GHC.
However, writing `newtype Tag (t :: *) a` unexpectedly works. This leads me to the hypothesis that `DerivingVia` only uses kinding information of the via type, even with `StandaloneDeriving` providing extra context.
## Expected behavior
`DerivingVia` should use all the kinding information available in the declaration. If this is too much, at least have it do so for standalone derivations.
## Environment
* GHC version used: 8.8.1## Summary
Using `DerivingVia` unexpectedly restricts the flow of kinding information. This is problematic in modules with `PolyKinds` enabled, since it limits what sources of kinding information are available
## Steps to reproduce
Consider the following snippet.
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE StandaloneDeriving #}
class C t
newtype Tag t a = T a
newtype Tag' t a = T' a
instance (C t, Eq t) => Eq (Tag t a)
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
```
Clearly, from the context `Eq t`, we infer `t :: Type`. GHC disagrees:
```
• Expected a type, but ‘t’ has kind ‘k’
• In the first argument of ‘Eq’, namely ‘t’
In the standalone deriving instance for
‘(C t, Eq t) => Eq (Tag' t a)’
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
^
```
OK, fine. Maybe GHC doesn't take the context into consideration. Let's try monomorphising other indeces involved. Surprise, both writing `class C (t :: *)` and `newtype Tag' (t :: *) a` fail to give enough kinding information to satisfy GHC.
However, writing `newtype Tag (t :: *) a` unexpectedly works. This leads me to the hypothesis that `DerivingVia` only uses kinding information of the via type, even with `StandaloneDeriving` providing extra context.
## Expected behavior
`DerivingVia` should use all the kinding information available in the declaration. If this is too much, at least have it do so for standalone derivations.
## Environment
* GHC version used: 8.8.1https://gitlab.haskell.org/ghc/ghc//issues/17772CUSKless class typechecks on 8.4, but not on 8.6+20200608T10:56:41ZRyan ScottCUSKless class typechecks on 8.4, but not on 8.6+This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```https://gitlab.haskell.org/ghc/ghc//issues/18059Add warning for type aliases that monomorphise a PolyKindsed type20200427T10:26:56ZlspitznerAdd warning for type aliases that monomorphise a PolyKindsed type## Motivation
module A has `XPolyKinds` and defines some polykinded type `MyPoly :: Type > k > Type`
module B does not have `XPolyKinds` and defines an alias `type MySpecialP = MyPoly Bool`
`MySpecialP` is monokinded, leading to confusing error messages down the line.
## Proposal
Does it make sense to have a warning ("Wmonomorphizingalias"?) for this? For any type alias, check if the RHS involves PolyKinds, check that it does not have an explicitly monokinded kindsignature and that PolyKinds is disabled. If so, raise the warning.
For the unlikely case that the monokinded alias is desired, allowing an explicit kind signature to silence the warning seems appropriate.
I have no idea how complex this is to implement. If checking the above condition is too complex or is hard to do without false positives, feel free to close this.
Thanks for your consideration.## Motivation
module A has `XPolyKinds` and defines some polykinded type `MyPoly :: Type > k > Type`
module B does not have `XPolyKinds` and defines an alias `type MySpecialP = MyPoly Bool`
`MySpecialP` is monokinded, leading to confusing error messages down the line.
## Proposal
Does it make sense to have a warning ("Wmonomorphizingalias"?) for this? For any type alias, check if the RHS involves PolyKinds, check that it does not have an explicitly monokinded kindsignature and that PolyKinds is disabled. If so, raise the warning.
For the unlikely case that the monokinded alias is desired, allowing an explicit kind signature to silence the warning seems appropriate.
I have no idea how complex this is to implement. If checking the above condition is too complex or is hard to do without false positives, feel free to close this.
Thanks for your consideration.https://gitlab.haskell.org/ghc/ghc//issues/17838Unused type variable error misidentifies the name of the type variable20200331T20:55:29ZRyan ScottUnused type variable error misidentifies the name of the type variableIf you compile the following (erroneous) program on GHC 8.8.2 or later:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F (x :: a) :: Type where
forall a x. F x = Const Int a
```
You'll get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a2’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```
This points to the type variable `a` in the source code, but names it `a2` in the error message! This appears to be the result of having a kind variable named `a` in the type family header, since renaming that kind variable to something else makes the issue go away. For example, this variant of the program above:
```hs
type family F (x :: b) :: Type where
forall a x. F x = Const Int a
```
Gives a sensible error message:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```If you compile the following (erroneous) program on GHC 8.8.2 or later:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F (x :: a) :: Type where
forall a x. F x = Const Int a
```
You'll get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a2’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```
This points to the type variable `a` in the source code, but names it `a2` in the error message! This appears to be the result of having a kind variable named `a` in the type family header, since renaming that kind variable to something else makes the issue go away. For example, this variant of the program above:
```hs
type family F (x :: b) :: Type where
forall a x. F x = Const Int a
```
Gives a sensible error message:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```https://gitlab.haskell.org/ghc/ghc//issues/17710Polykinded rewrite rule fails to typecheck (HEAD only)20200315T18:51:16ZRyan ScottPolykinded rewrite rule fails to typecheck (HEAD only)I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.9.0.1https://gitlab.haskell.org/ghc/ghc//issues/17397Annotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances20191031T22:30:53ZMax HarmsAnnotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances## Summary
The error message provided when GHC infers the kind of an otherwise polykinded structure is unhelpful. I recognize that this might not be the highest priority, but I do think Haskell's error messages here could be better.
## Steps to reproduce
Let's say I have a little program like
```
{# LANGUAGE PolyKinds #}
class Foo a
data Bar (f :: * > *)
instance (Foo (f Bool)) => Foo (Bar f)
main :: IO ()
main = pure ()
```
Everything compiles and is happy and fun.
(This is stripped down for clarity; imagine lots of irrelevant methods and constructors and other spinning parts in the case where I actually hit this.)
Now let's say you foolishly add a method to `Foo` like so:
```
class Foo a where
foo :: Int > [a]
```
GHC errors, saying:
```
• The constraint ‘Foo (f Bool)’
is no smaller than the instance head ‘Foo (Bar f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Foo (Bar f)’
```
What happened here was that by mentioning `[a]` we've pinned down the kind of `a`. A similar effect can be produced simply by annotating the kind of `a` like so:
```
class Foo (a :: *)
```
Before this kind was specified, the decidability checker on the instance was satisfied, but afterwards it chokes and demands `UndecidableInstances`. My guess of why it's doing this is that there's an implicit kind showing up in the context afterwards, and so it no longer knows that the context is smaller than the head. *\*shrug\**
## Expected behavior
I would hope that annotating the kind of a class would not affect knowntobevalid instances of that class elsewhere. At the very least I'd hope that the decidability checker would report in its error that it only failed because of an inferred kind when PolyKinds is active. Best of all would be if the decidability checker could handle having kinds specified in cases like this.
## Environment
Tested on GHC 8.6 and 8.8.## Summary
The error message provided when GHC infers the kind of an otherwise polykinded structure is unhelpful. I recognize that this might not be the highest priority, but I do think Haskell's error messages here could be better.
## Steps to reproduce
Let's say I have a little program like
```
{# LANGUAGE PolyKinds #}
class Foo a
data Bar (f :: * > *)
instance (Foo (f Bool)) => Foo (Bar f)
main :: IO ()
main = pure ()
```
Everything compiles and is happy and fun.
(This is stripped down for clarity; imagine lots of irrelevant methods and constructors and other spinning parts in the case where I actually hit this.)
Now let's say you foolishly add a method to `Foo` like so:
```
class Foo a where
foo :: Int > [a]
```
GHC errors, saying:
```
• The constraint ‘Foo (f Bool)’
is no smaller than the instance head ‘Foo (Bar f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Foo (Bar f)’
```
What happened here was that by mentioning `[a]` we've pinned down the kind of `a`. A similar effect can be produced simply by annotating the kind of `a` like so:
```
class Foo (a :: *)
```
Before this kind was specified, the decidability checker on the instance was satisfied, but afterwards it chokes and demands `UndecidableInstances`. My guess of why it's doing this is that there's an implicit kind showing up in the context afterwards, and so it no longer knows that the context is smaller than the head. *\*shrug\**
## Expected behavior
I would hope that annotating the kind of a class would not affect knowntobevalid instances of that class elsewhere. At the very least I'd hope that the decidability checker would report in its error that it only failed because of an inferred kind when PolyKinds is active. Best of all would be if the decidability checker could handle having kinds specified in cases like this.
## Environment
Tested on GHC 8.6 and 8.8.https://gitlab.haskell.org/ghc/ghc//issues/16726Data type can't be given return kind that is identical to its TLKS20190926T20:32:36ZRyan ScottData type can't be given return kind that is identical to its TLKSI would have expected this to work, but it doesn't:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
type D :: forall k. k > Type
data D :: forall k. k > Type
```
```
[1 of 1] Compiling Bug ( ../Bug.hs, ../Bug.o )
../Bug.hs:9:1: error:
• Couldn't match expected kind ‘forall k1. k1 > *’
with actual kind ‘k > *’
• In the data type declaration for ‘D’

9  data D :: forall k. k > Type
 ^^^^^^
```
Note that this bug does not appear to apply to type families, as the following works without issue:
```hs
type T :: forall k. k > Type
type family T :: forall k. k > Type
```I would have expected this to work, but it doesn't:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
type D :: forall k. k > Type
data D :: forall k. k > Type
```
```
[1 of 1] Compiling Bug ( ../Bug.hs, ../Bug.o )
../Bug.hs:9:1: error:
• Couldn't match expected kind ‘forall k1. k1 > *’
with actual kind ‘k > *’
• In the data type declaration for ‘D’

9  data D :: forall k. k > Type
 ^^^^^^
```
Note that this bug does not appear to apply to type families, as the following works without issue:
```hs
type T :: forall k. k > Type
type family T :: forall k. k > Type
```Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/16731GHC internal error when combining TLKSs and deriving20190925T18:06:24ZRyan ScottGHC internal error when combining TLKSs and derivingGHC freaks out when given this code:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
class C (a :: Type) (b :: Type)
type T :: a > Type
data T (x :: z) deriving (C z)
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:29: error:
• GHC internal error: ‘z’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [as1 :> Type variable ‘a’ = a :: *,
aWI :> Type variable ‘x’ = x :: a]
• In the first argument of ‘C’, namely ‘z’
In the data declaration for ‘T’

12  data T (x :: z) deriving (C z)
 ^
```
The code works as written if the TLKS is omitted.GHC freaks out when given this code:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
class C (a :: Type) (b :: Type)
type T :: a > Type
data T (x :: z) deriving (C z)
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:29: error:
• GHC internal error: ‘z’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [as1 :> Type variable ‘a’ = a :: *,
aWI :> Type variable ‘x’ = x :: a]
• In the first argument of ‘C’, namely ‘z’
In the data declaration for ‘T’

12  data T (x :: z) deriving (C z)
 ^
```
The code works as written if the TLKS is omitted.8.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/16724Inconsistent treatment of type family arities in TLKSs20190823T21:50:04ZRyan ScottInconsistent treatment of type family arities in TLKSsConsider this program:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TopLevelKindSignatures #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type T1 :: forall k (a :: k). Type
type family T1
 type T2 :: forall {k} (a :: k). Type
type T2 :: forall a. Type
type family T2
```
`T1` and `T2` look the same, but they actually get assigned very different arities, as GHCi reveals when `fprintexplicitkinds` is enabled:
```
λ> :set fprintexplicitkinds fprintexplicitforalls
λ> :info T1
type family T1 @k @(a :: k) :: *  Defined at ../Bug.hs:10:1
λ> :info T2
type family T2 :: forall {k} (a :: k). *
 Defined at ../Bug.hs:14:1
```
`T1` has arity two, whereas `T2` has arity zero! I find this rather surprising given that there are no syntactic differences in the declarations for `T1` and `T2`—the only differences lie in the visibility of the `k` in their kinds. I would expect `T1` and `T2` to have the same arity here.Consider this program:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TopLevelKindSignatures #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type T1 :: forall k (a :: k). Type
type family T1
 type T2 :: forall {k} (a :: k). Type
type T2 :: forall a. Type
type family T2
```
`T1` and `T2` look the same, but they actually get assigned very different arities, as GHCi reveals when `fprintexplicitkinds` is enabled:
```
λ> :set fprintexplicitkinds fprintexplicitforalls
λ> :info T1
type family T1 @k @(a :: k) :: *  Defined at ../Bug.hs:10:1
λ> :info T2
type family T2 :: forall {k} (a :: k). *
 Defined at ../Bug.hs:14:1
```
`T1` has arity two, whereas `T2` has arity zero! I find this rather surprising given that there are no syntactic differences in the declarations for `T1` and `T2`—the only differences lie in the visibility of the `k` in their kinds. I would expect `T1` and `T2` to have the same arity here.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/5682Properly parse promoted data constructor operators20190707T18:54:04ZlunarisProperly parse promoted data constructor operators```
% ghci XPolyKinds XTypeOperators
GHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help
Loading package ghcprim ... linking ... done.
Loading package integergmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :k (:)
<interactive>:1:2: parse error on input `:'
Prelude> :k '(:)
<interactive>:1:3: parse error on input `:'
Prelude> :k (':)
<interactive>:1:3: parse error on input `:'
Prelude> :k (Int ': '[Bool])
(Int ': '[Bool]) :: [*]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Cannot parse (:) in a KindSignature with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"dreixel"},"version":"7.3","keywords":["PolyKinds,","ghckinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n% ghci XPolyKinds XTypeOperators\r\nGHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghcprim ... linking ... done.\r\nLoading package integergmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nPrelude> :k (:)\r\n\r\n<interactive>:1:2: parse error on input `:'\r\nPrelude> :k '(:)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (':)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (Int ': '[Bool])\r\n(Int ': '[Bool]) :: [*]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```
% ghci XPolyKinds XTypeOperators
GHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help
Loading package ghcprim ... linking ... done.
Loading package integergmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :k (:)
<interactive>:1:2: parse error on input `:'
Prelude> :k '(:)
<interactive>:1:3: parse error on input `:'
Prelude> :k (':)
<interactive>:1:3: parse error on input `:'
Prelude> :k (Int ': '[Bool])
(Int ': '[Bool]) :: [*]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Cannot parse (:) in a KindSignature with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"dreixel"},"version":"7.3","keywords":["PolyKinds,","ghckinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n% ghci XPolyKinds XTypeOperators\r\nGHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghcprim ... linking ... done.\r\nLoading package integergmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nPrelude> :k (:)\r\n\r\n<interactive>:1:2: parse error on input `:'\r\nPrelude> :k '(:)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (':)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (Int ': '[Bool])\r\n(Int ': '[Bool]) :: [*]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >7.8.1https://gitlab.haskell.org/ghc/ghc//issues/5716Failure when using promoted data family instances20190707T18:53:55ZdreixelFailure when using promoted data family instancesThe following code should fail (since we don't promote data families), but it should do so gracefully:
```
{# LANGUAGE GADTs #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PolyKinds #}
module Bug1 where
data family DF a
data instance DF Int = DFInt
data U = U1 (DF Int)
data I :: U > * where I1 :: I (U1 DFInt)
{
GHC internal error: `DFInt' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [(r9P, AThing U > *), (r9Q, ANothing)]
In the type `I (U1 DFInt)'
In the definition of data constructor `I1'
In the data type declaration for `I'
}
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  jpm@cs.uu.nl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Failure when using promoted data family instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["jpm@cs.uu.nl"],"type":"Bug","description":"The following code should fail (since we don't promote data families), but it should do so gracefully:\r\n{{{\r\n\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Bug1 where\r\n\r\n\r\ndata family DF a \r\ndata instance DF Int = DFInt\r\n\r\ndata U = U1 (DF Int)\r\n\r\ndata I :: U > * where I1 :: I (U1 DFInt)\r\n\r\n{\r\n GHC internal error: `DFInt' is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [(r9P, AThing U > *), (r9Q, ANothing)]\r\n In the type `I (U1 DFInt)'\r\n In the definition of data constructor `I1'\r\n In the data type declaration for `I'\r\n}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following code should fail (since we don't promote data families), but it should do so gracefully:
```
{# LANGUAGE GADTs #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE PolyKinds #}
module Bug1 where
data family DF a
data instance DF Int = DFInt
data U = U1 (DF Int)
data I :: U > * where I1 :: I (U1 DFInt)
{
GHC internal error: `DFInt' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [(r9P, AThing U > *), (r9Q, ANothing)]
In the type `I (U1 DFInt)'
In the definition of data constructor `I1'
In the data type declaration for `I'
}
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  jpm@cs.uu.nl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Failure when using promoted data family instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["jpm@cs.uu.nl"],"type":"Bug","description":"The following code should fail (since we don't promote data families), but it should do so gracefully:\r\n{{{\r\n\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Bug1 where\r\n\r\n\r\ndata family DF a \r\ndata instance DF Int = DFInt\r\n\r\ndata U = U1 (DF Int)\r\n\r\ndata I :: U > * where I1 :: I (U1 DFInt)\r\n\r\n{\r\n GHC internal error: `DFInt' is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [(r9P, AThing U > *), (r9Q, ANothing)]\r\n In the type `I (U1 DFInt)'\r\n In the definition of data constructor `I1'\r\n In the data type declaration for `I'\r\n}\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >7.4.2https://gitlab.haskell.org/ghc/ghc//issues/5717ScopedTypeVariables and PolyKinds20190707T18:53:54ZdreixelScopedTypeVariables and PolyKindsThe following code panics:
```
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE PolyKinds #}
module Bug2 where
data TypeRep = TypeRep
data Proxy t = Proxy
typeRep :: Proxy a > TypeRep
typeRep Proxy = TypeRep
 This one works fine:
typeOf :: forall a. a > TypeRep
typeOf _ = typeRep (Proxy :: Proxy a)
 But this one panics!
typeOf1 :: forall t a. t a > TypeRep
typeOf1 _ = typeRep (Proxy :: Proxy t)
{
panic! (the 'impossible' happened)
(GHC version 7.5.20111216 for x86_64unknownlinux):
tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}
}
```
I believe the problem is an interaction between !ScopedTypeVariables and !PolyKinds.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  jpm@cs.uu.nl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"ScopedTypeVariables and PolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["jpm@cs.uu.nl"],"type":"Bug","description":"The following code panics:\r\n{{{\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Bug2 where\r\n\r\n\r\ndata TypeRep = TypeRep\r\n\r\ndata Proxy t = Proxy\r\n\r\ntypeRep :: Proxy a > TypeRep\r\ntypeRep Proxy = TypeRep\r\n\r\n This one works fine:\r\ntypeOf :: forall a. a > TypeRep\r\ntypeOf _ = typeRep (Proxy :: Proxy a)\r\n\r\n But this one panics!\r\ntypeOf1 :: forall t a. t a > TypeRep\r\ntypeOf1 _ = typeRep (Proxy :: Proxy t)\r\n\r\n{\r\npanic! (the 'impossible' happened)\r\n (GHC version 7.5.20111216 for x86_64unknownlinux):\r\n tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}\r\n}\r\n}}}\r\nI believe the problem is an interaction between !ScopedTypeVariables and !PolyKinds.","type_of_failure":"OtherFailure","blocking":[]} >The following code panics:
```
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE PolyKinds #}
module Bug2 where
data TypeRep = TypeRep
data Proxy t = Proxy
typeRep :: Proxy a > TypeRep
typeRep Proxy = TypeRep
 This one works fine:
typeOf :: forall a. a > TypeRep
typeOf _ = typeRep (Proxy :: Proxy a)
 But this one panics!
typeOf1 :: forall t a. t a > TypeRep
typeOf1 _ = typeRep (Proxy :: Proxy t)
{
panic! (the 'impossible' happened)
(GHC version 7.5.20111216 for x86_64unknownlinux):
tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}
}
```
I believe the problem is an interaction between !ScopedTypeVariables and !PolyKinds.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  jpm@cs.uu.nl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"ScopedTypeVariables and PolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["jpm@cs.uu.nl"],"type":"Bug","description":"The following code panics:\r\n{{{\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Bug2 where\r\n\r\n\r\ndata TypeRep = TypeRep\r\n\r\ndata Proxy t = Proxy\r\n\r\ntypeRep :: Proxy a > TypeRep\r\ntypeRep Proxy = TypeRep\r\n\r\n This one works fine:\r\ntypeOf :: forall a. a > TypeRep\r\ntypeOf _ = typeRep (Proxy :: Proxy a)\r\n\r\n But this one panics!\r\ntypeOf1 :: forall t a. t a > TypeRep\r\ntypeOf1 _ = typeRep (Proxy :: Proxy t)\r\n\r\n{\r\npanic! (the 'impossible' happened)\r\n (GHC version 7.5.20111216 for x86_64unknownlinux):\r\n tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}\r\n}\r\n}}}\r\nI believe the problem is an interaction between !ScopedTypeVariables and !PolyKinds.","type_of_failure":"OtherFailure","blocking":[]} >7.6.1https://gitlab.haskell.org/ghc/ghc//issues/5768GHC Panic compiling type family with XPolyKinds20190707T18:53:41ZRichard Eisenbergrae@richarde.devGHC Panic compiling type family with XPolyKindsI received the following error message:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.4.0.20111219 for x86_64unknownlinux):
tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}
```
I was compiling the following code:
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
bar :: forall a b. b > (Foo a)
bar f = (convert f :: (Foo a))
```
Interestingly, the output is different when changing the order in the forall (forall b a produces a different error). The same result happened on Linux/x86_64 and MacOS 10.7.2/x86_64appledarwin,
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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 compiling type family with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I received the following error message:\r\n\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 7.4.0.20111219 for x86_64unknownlinux):\r\n tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}\r\n}}}\r\n\r\n\r\nI was compiling the following code:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a\r\n\r\nbar :: forall a b. b > (Foo a)\r\nbar f = (convert f :: (Foo a))\r\n}}}\r\n\r\n\r\nInterestingly, the output is different when changing the order in the forall (forall b a produces a different error). The same result happened on Linux/x86_64 and MacOS 10.7.2/x86_64appledarwin,","type_of_failure":"OtherFailure","blocking":[]} >I received the following error message:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.4.0.20111219 for x86_64unknownlinux):
tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}
```
I was compiling the following code:
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
bar :: forall a b. b > (Foo a)
bar f = (convert f :: (Foo a))
```
Interestingly, the output is different when changing the order in the forall (forall b a produces a different error). The same result happened on Linux/x86_64 and MacOS 10.7.2/x86_64appledarwin,
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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 compiling type family with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I received the following error message:\r\n\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 7.4.0.20111219 for x86_64unknownlinux):\r\n tyConKind ghcprim:GHC.Prim.BOX{(w) tc 347}\r\n}}}\r\n\r\n\r\nI was compiling the following code:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a\r\n\r\nbar :: forall a b. b > (Foo a)\r\nbar f = (convert f :: (Foo a))\r\n}}}\r\n\r\n\r\nInterestingly, the output is different when changing the order in the forall (forall b a produces a different error). The same result happened on Linux/x86_64 and MacOS 10.7.2/x86_64appledarwin,","type_of_failure":"OtherFailure","blocking":[]} >7.6.1dreixeldreixelhttps://gitlab.haskell.org/ghc/ghc//issues/5769Incorrect error message when compiling with PolyKinds and a type family20190707T18:53:41ZRichard Eisenbergrae@richarde.devIncorrect error message when compiling with PolyKinds and a type familyWhen trying to compile
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
bar :: forall b a. b > (Foo a)
bar f = (convert f :: (Foo a))
```
I get the following error message:
```
Sandbox.hs:12:10:
Couldn't match type `Foo k a' with `Foo * b'
NB: `Foo' is a type function, and may not be injective
In the expression: (convert f :: Foo a)
In an equation for `bar': bar f = (convert f :: Foo a)
```
However, this compiles just fine without `PolyKinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Incorrect error message when compiling with PolyKinds and a type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to compile\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a\r\n\r\nbar :: forall b a. b > (Foo a)\r\nbar f = (convert f :: (Foo a))\r\n}}}\r\n\r\nI get the following error message:\r\n{{{\r\nSandbox.hs:12:10:\r\n Couldn't match type `Foo k a' with `Foo * b'\r\n NB: `Foo' is a type function, and may not be injective\r\n In the expression: (convert f :: Foo a)\r\n In an equation for `bar': bar f = (convert f :: Foo a)\r\n}}}\r\n\r\nHowever, this compiles just fine without {{{PolyKinds}}}.","type_of_failure":"OtherFailure","blocking":[]} >When trying to compile
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
bar :: forall b a. b > (Foo a)
bar f = (convert f :: (Foo a))
```
I get the following error message:
```
Sandbox.hs:12:10:
Couldn't match type `Foo k a' with `Foo * b'
NB: `Foo' is a type function, and may not be injective
In the expression: (convert f :: Foo a)
In an equation for `bar': bar f = (convert f :: Foo a)
```
However, this compiles just fine without `PolyKinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Incorrect error message when compiling with PolyKinds and a type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to compile\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a\r\n\r\nbar :: forall b a. b > (Foo a)\r\nbar f = (convert f :: (Foo a))\r\n}}}\r\n\r\nI get the following error message:\r\n{{{\r\nSandbox.hs:12:10:\r\n Couldn't match type `Foo k a' with `Foo * b'\r\n NB: `Foo' is a type function, and may not be injective\r\n In the expression: (convert f :: Foo a)\r\n In an equation for `bar': bar f = (convert f :: Foo a)\r\n}}}\r\n\r\nHowever, this compiles just fine without {{{PolyKinds}}}.","type_of_failure":"OtherFailure","blocking":[]} >7.6.1dreixeldreixelhttps://gitlab.haskell.org/ghc/ghc//issues/5770Nonsensical error message when compiling with PolyKinds and a type family20190707T18:53:40ZRichard Eisenbergrae@richarde.devNonsensical error message when compiling with PolyKinds and a type familyWhen I compile the following code:
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
type instance Foo Int = Bool
bar :: forall a b c dummya. (b > c) > ((Foo a) > c)
bar f = (convert f :: (Foo a) > c)
```
I get the following error message:
```
Sandbox.hs:13:34:
Kind mismatch
Expected kind `OpenKind', but `c' has kind `b'
In an expression type signature: (Foo a) > c
In the expression: (convert f :: (Foo a) > c)
In an equation for `bar': bar f = (convert f :: (Foo a) > c)
```
This error message does not make sense, for 'b' isn't a kind. It is interesting to note that removing `dummya` from the list of declared type variables changes the error to a GHC panic.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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":"Nonsensical error message when compiling with PolyKinds and a type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I compile the following code:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a \r\ntype instance Foo Int = Bool\r\n\r\nbar :: forall a b c dummya. (b > c) > ((Foo a) > c)\r\nbar f = (convert f :: (Foo a) > c)\r\n}}}\r\n\r\nI get the following error message:\r\n\r\n{{{\r\nSandbox.hs:13:34:\r\n Kind mismatch\r\n Expected kind `OpenKind', but `c' has kind `b'\r\n In an expression type signature: (Foo a) > c\r\n In the expression: (convert f :: (Foo a) > c)\r\n In an equation for `bar': bar f = (convert f :: (Foo a) > c)\r\n}}}\r\n\r\nThis error message does not make sense, for 'b' isn't a kind. It is interesting to note that removing {{{dummya}}} from the list of declared type variables changes the error to a GHC panic.","type_of_failure":"OtherFailure","blocking":[]} >When I compile the following code:
```
{# LANGUAGE TypeFamilies,
PolyKinds,
ScopedTypeVariables
#}
convert :: a > b
convert = undefined
type family Foo a
type instance Foo Int = Bool
bar :: forall a b c dummya. (b > c) > ((Foo a) > c)
bar f = (convert f :: (Foo a) > c)
```
I get the following error message:
```
Sandbox.hs:13:34:
Kind mismatch
Expected kind `OpenKind', but `c' has kind `b'
In an expression type signature: (Foo a) > c
In the expression: (convert f :: (Foo a) > c)
In an equation for `bar': bar f = (convert f :: (Foo a) > c)
```
This error message does not make sense, for 'b' isn't a kind. It is interesting to note that removing `dummya` from the list of declared type variables changes the error to a GHC panic.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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":"Nonsensical error message when compiling with PolyKinds and a type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I compile the following code:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds,\r\n ScopedTypeVariables\r\n #}\r\n\r\nconvert :: a > b\r\nconvert = undefined\r\n\r\ntype family Foo a \r\ntype instance Foo Int = Bool\r\n\r\nbar :: forall a b c dummya. (b > c) > ((Foo a) > c)\r\nbar f = (convert f :: (Foo a) > c)\r\n}}}\r\n\r\nI get the following error message:\r\n\r\n{{{\r\nSandbox.hs:13:34:\r\n Kind mismatch\r\n Expected kind `OpenKind', but `c' has kind `b'\r\n In an expression type signature: (Foo a) > c\r\n In the expression: (convert f :: (Foo a) > c)\r\n In an equation for `bar': bar f = (convert f :: (Foo a) > c)\r\n}}}\r\n\r\nThis error message does not make sense, for 'b' isn't a kind. It is interesting to note that removing {{{dummya}}} from the list of declared type variables changes the error to a GHC panic.","type_of_failure":"OtherFailure","blocking":[]} >7.6.1dreixeldreixelhttps://gitlab.haskell.org/ghc/ghc//issues/5771Confusing printout with PolyKinds20190707T18:53:40ZRichard Eisenbergrae@richarde.devConfusing printout with PolyKindsIf I load the following into ghci:
```
{# LANGUAGE TypeFamilies,
PolyKinds
#}
type family Foo a
```
and then get the info on `Foo`, I get the following printout:
```
type family Foo k a :: *
```
It seems that ghc is inserting the kind variable `k` into the name of the type function `Foo`. Perhaps this was intended, but it seems counterintuitive. A kind of `*` is also sometimes printed in different situations when compiling with `PolyKinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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":"Confusing printout with PolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I load the following into ghci:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds\r\n #}\r\n\r\ntype family Foo a\r\n}}}\r\n\r\nand then get the info on {{{Foo}}}, I get the following printout:\r\n\r\n{{{\r\ntype family Foo k a :: *\r\n}}}\r\n\r\nIt seems that ghc is inserting the kind variable {{{k}}} into the name of the type function {{{Foo}}}. Perhaps this was intended, but it seems counterintuitive. A kind of {{{*}}} is also sometimes printed in different situations when compiling with {{{PolyKinds}}}.","type_of_failure":"OtherFailure","blocking":[]} >If I load the following into ghci:
```
{# LANGUAGE TypeFamilies,
PolyKinds
#}
type family Foo a
```
and then get the info on `Foo`, I get the following printout:
```
type family Foo k a :: *
```
It seems that ghc is inserting the kind variable `k` into the name of the type function `Foo`. Perhaps this was intended, but it seems counterintuitive. A kind of `*` is also sometimes printed in different situations when compiling with `PolyKinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.4.1rc1 
 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":"Confusing printout with PolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I load the following into ghci:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies,\r\n PolyKinds\r\n #}\r\n\r\ntype family Foo a\r\n}}}\r\n\r\nand then get the info on {{{Foo}}}, I get the following printout:\r\n\r\n{{{\r\ntype family Foo k a :: *\r\n}}}\r\n\r\nIt seems that ghc is inserting the kind variable {{{k}}} into the name of the type function {{{Foo}}}. Perhaps this was intended, but it seems counterintuitive. A kind of {{{*}}} is also sometimes printed in different situations when compiling with {{{PolyKinds}}}.","type_of_failure":"OtherFailure","blocking":[]} >7.6.1