GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200427T10:26:56Zhttps://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/17841"No skolem info" panic with PolyKinds20200726T19:06:01ZJakob 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/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/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/16276Feature request: Polymorphic kinds in Data.Functor.Classes20190707T18:00:42ZLangston BarrettFeature request: Polymorphic kinds in Data.Functor.ClassesThe classes in Data.Functor.Classes have a somewhat restrictive kind signature:
```
*Data.Functor.Classes> :k Eq1
Eq1 :: (* > *) > Constraint
```
As a result, we redefine \[1\] many of them in the [parameterizedutils](https://hackage.haskell.org/package/parameterizedutils1.0.1/docs/DataParameterizedClasses.html) library. It would be quite easy to make more polymorphic (have kind "(k \> \*) \> Constraint"). If everyone thinks this is a good idea, I'm happy to submit a pull request.
\[1\]: To be precise, there are actually a few axes along which the classes in parameterizedutils vary from those in base. Some, like OrdF, require more typelevel evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Feature request: Polymorphic kinds in Data.Functor.Classes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["polykinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The classes in Data.Functor.Classes have a somewhat restrictive kind signature:\r\n{{{\r\n*Data.Functor.Classes> :k Eq1 \r\nEq1 :: (* > *) > Constraint \r\n}}}\r\n\r\nAs a result, we redefine [1] many of them in the [https://hackage.haskell.org/package/parameterizedutils1.0.1/docs/DataParameterizedClasses.html parameterizedutils] library. It would be quite easy to make more polymorphic (have kind \"(k > *) > Constraint\"). If everyone thinks this is a good idea, I'm happy to submit a pull request. \r\n\r\n[1]: To be precise, there are actually a few axes along which the classes in parameterizedutils vary from those in base. Some, like OrdF, require more typelevel evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here. ","type_of_failure":"OtherFailure","blocking":[]} >The classes in Data.Functor.Classes have a somewhat restrictive kind signature:
```
*Data.Functor.Classes> :k Eq1
Eq1 :: (* > *) > Constraint
```
As a result, we redefine \[1\] many of them in the [parameterizedutils](https://hackage.haskell.org/package/parameterizedutils1.0.1/docs/DataParameterizedClasses.html) library. It would be quite easy to make more polymorphic (have kind "(k \> \*) \> Constraint"). If everyone thinks this is a good idea, I'm happy to submit a pull request.
\[1\]: To be precise, there are actually a few axes along which the classes in parameterizedutils vary from those in base. Some, like OrdF, require more typelevel evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Feature request: Polymorphic kinds in Data.Functor.Classes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["polykinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The classes in Data.Functor.Classes have a somewhat restrictive kind signature:\r\n{{{\r\n*Data.Functor.Classes> :k Eq1 \r\nEq1 :: (* > *) > Constraint \r\n}}}\r\n\r\nAs a result, we redefine [1] many of them in the [https://hackage.haskell.org/package/parameterizedutils1.0.1/docs/DataParameterizedClasses.html parameterizedutils] library. It would be quite easy to make more polymorphic (have kind \"(k > *) > Constraint\"). If everyone thinks this is a good idea, I'm happy to submit a pull request. \r\n\r\n[1]: To be precise, there are actually a few axes along which the classes in parameterizedutils vary from those in base. Some, like OrdF, require more typelevel evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here. ","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13992Error message, room for improvement (polykinds)20190707T18:18:57ZIcelandjackError message, room for improvement (polykinds)Something like
```hs
 • No instance for (Show (Compose Proxy Proxy a))
 arising from the 'deriving' clause of a data type declaration
 Possible fix:
 use a standalone 'deriving instance' declaration,
 so you can specify the instance context yourself
 • When deriving the instance for (Show (FlipProxy a))
{# Language DerivingStrategies, GeneralizedNewtypeDeriving, PolyKinds, KindSignatures #}
import Data.Functor.Compose
import Data.Proxy
import Data.Kind
newtype FlipProxy a = FlipProxy_ (Compose Proxy Proxy a)
deriving newtype
Show
```
where the solution is to constrain the kind of `a` to `Type`, it would be nice if GHC could reference kind variables.Something like
```hs
 • No instance for (Show (Compose Proxy Proxy a))
 arising from the 'deriving' clause of a data type declaration
 Possible fix:
 use a standalone 'deriving instance' declaration,
 so you can specify the instance context yourself
 • When deriving the instance for (Show (FlipProxy a))
{# Language DerivingStrategies, GeneralizedNewtypeDeriving, PolyKinds, KindSignatures #}
import Data.Functor.Compose
import Data.Proxy
import Data.Kind
newtype FlipProxy a = FlipProxy_ (Compose Proxy Proxy a)
deriving newtype
Show
```
where the solution is to constrain the kind of `a` to `Type`, it would be nice if GHC could reference kind variables.https://gitlab.haskell.org/ghc/ghc//issues/13814Unable to resolve instance for polykinded superclass constraint on associated...20190707T18:19:59ZisovectorUnable to resolve instance for polykinded superclass constraint on associatedtypefamily.The following program doesn't compile:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Test where
class Back t
class Back (FrontBack t) => Front t where
type FrontBack t :: k
instance Back Bool
instance Front Int where
type FrontBack Int = Bool
```
with the error message:
```
• No instance for (Back (FrontBack Int))
arising from the superclasses of an instance declaration
• In the instance declaration for ‘Front Int’
```
The example successfully compiles if the kind annotation on FrontBack is removed.The following program doesn't compile:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Test where
class Back t
class Back (FrontBack t) => Front t where
type FrontBack t :: k
instance Back Bool
instance Front Int where
type FrontBack Int = Bool
```
with the error message:
```
• No instance for (Back (FrontBack Int))
arising from the superclasses of an instance declaration
• In the instance declaration for ‘Front Int’
```
The example successfully compiles if the kind annotation on FrontBack is removed.