GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-10-19T09:16:46Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17841"No skolem info" panic with PolyKinds2020-10-19T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kind-polymorphic 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...## Summary
Making a class with a kind-polymorphic 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 CUSK-less class2020-10-19T09:14:39ZRyan ScottGHC 8.10 regression: Core Lint error when defining instance of CUSK-less 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...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 -dcore-lint
```
But it does _not_ pass Core Lint on GHC 8.10.1-alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc -c Lib.hs && /opt/ghc/8.10.1/bin/ghc -c App.hs -dcore-lint
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.2