GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20200326T15:39:16Zhttps://gitlab.haskell.org/ghc/ghc/issues/17841"No skolem info" panic with PolyKinds20200326T15:39:16ZJakob 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+20200331T13:01:51ZRyan 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/17566GHC 8.10 regression: Core Lint error when defining instance of CUSKless class20200201T19:06:31ZRyan 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/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.