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/17563Validity check quantified constraints2021-11-17T21:20:04ZRichard Eisenbergrae@richarde.devValidity check quantified constraintsThis module is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
module Bug2 where
blah :: (forall a. a b ~ a c) => b -> c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.This module is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
module Bug2 where
blah :: (forall a. a b ~ a c) => b -> c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.8.10.2