GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200315T18:51:16Zhttps://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/17566GHC 8.10 regression: Core Lint error when defining instance of CUSKless class20200818T15:57:02ZRyan 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/16728GHC HEADonly panic with PartialTypeSignatures20190707T18:00:04ZRyan ScottGHC HEADonly panic with PartialTypeSignaturesThe following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.The following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.8.10.1Richard Eisenbergrae@richarde.devRyan ScottRichard Eisenbergrae@richarde.devhttps://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/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/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/15120Default methods don't pass implicit kind parameters properly20190707T18:14:11ZmbieleckDefault methods don't pass implicit kind parameters properlyWhen compiling the following module:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE DefaultSignatures #}
module TestCase where
import Data.Proxy
class Describe a where
describe :: Proxy a > String
default describe :: Proxy a > String
describe _ = ""
data Foo = Foo
instance Describe Foo
```
I get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):
```
TestCase.hs:15:10: error:
• Couldn't match type ‘*’ with ‘Foo’
Expected type: Proxy * Foo > String
Actual type: Proxy Foo Foo > String
• In the expression: TestCase.$dmdescribe @Foo
In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo
In the instance declaration for ‘Describe * Foo’

15  instance Describe Foo
 ^^^^^^^^^^^^
```
The Core generated for `$dmdescribe` has the following type signature:
```
TestCase.$dmdescribe
:: forall k (a :: k). Describe k a => Proxy k a > String
```
I believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.
Seems related to #13998 .
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Default methods don't pass implicit kind parameters properly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DefaultSignatures","PolyKinds,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling the following module:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\nmodule TestCase where\r\n\r\nimport Data.Proxy\r\n\r\nclass Describe a where\r\n describe :: Proxy a > String\r\n\r\n default describe :: Proxy a > String\r\n describe _ = \"\"\r\n\r\ndata Foo = Foo\r\n\r\ninstance Describe Foo\r\n}}}\r\n\r\nI get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):\r\n\r\n{{{\r\nTestCase.hs:15:10: error:\r\n • Couldn't match type ‘*’ with ‘Foo’\r\n Expected type: Proxy * Foo > String\r\n Actual type: Proxy Foo Foo > String\r\n • In the expression: TestCase.$dmdescribe @Foo\r\n In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo\r\n In the instance declaration for ‘Describe * Foo’\r\n \r\n15  instance Describe Foo\r\n  ^^^^^^^^^^^^\r\n}}}\r\n\r\nThe Core generated for `$dmdescribe` has the following type signature:\r\n\r\n{{{\r\nTestCase.$dmdescribe\r\n :: forall k (a :: k). Describe k a => Proxy k a > String\r\n}}}\r\n\r\nI believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.\r\n\r\nSeems related to https://ghc.haskell.org/trac/ghc/ticket/13998 .","type_of_failure":"OtherFailure","blocking":[]} >When compiling the following module:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE DefaultSignatures #}
module TestCase where
import Data.Proxy
class Describe a where
describe :: Proxy a > String
default describe :: Proxy a > String
describe _ = ""
data Foo = Foo
instance Describe Foo
```
I get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):
```
TestCase.hs:15:10: error:
• Couldn't match type ‘*’ with ‘Foo’
Expected type: Proxy * Foo > String
Actual type: Proxy Foo Foo > String
• In the expression: TestCase.$dmdescribe @Foo
In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo
In the instance declaration for ‘Describe * Foo’

15  instance Describe Foo
 ^^^^^^^^^^^^
```
The Core generated for `$dmdescribe` has the following type signature:
```
TestCase.$dmdescribe
:: forall k (a :: k). Describe k a => Proxy k a > String
```
I believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.
Seems related to #13998 .
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Default methods don't pass implicit kind parameters properly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DefaultSignatures","PolyKinds,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling the following module:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\nmodule TestCase where\r\n\r\nimport Data.Proxy\r\n\r\nclass Describe a where\r\n describe :: Proxy a > String\r\n\r\n default describe :: Proxy a > String\r\n describe _ = \"\"\r\n\r\ndata Foo = Foo\r\n\r\ninstance Describe Foo\r\n}}}\r\n\r\nI get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):\r\n\r\n{{{\r\nTestCase.hs:15:10: error:\r\n • Couldn't match type ‘*’ with ‘Foo’\r\n Expected type: Proxy * Foo > String\r\n Actual type: Proxy Foo Foo > String\r\n • In the expression: TestCase.$dmdescribe @Foo\r\n In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo\r\n In the instance declaration for ‘Describe * Foo’\r\n \r\n15  instance Describe Foo\r\n  ^^^^^^^^^^^^\r\n}}}\r\n\r\nThe Core generated for `$dmdescribe` has the following type signature:\r\n\r\n{{{\r\nTestCase.$dmdescribe\r\n :: forall k (a :: k). Describe k a => Proxy k a > String\r\n}}}\r\n\r\nI believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.\r\n\r\nSeems related to https://ghc.haskell.org/trac/ghc/ticket/13998 .","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14710GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds20190707T18:15:55ZRyan ScottGHC 8.4.1alpha allows the use of kind polymorphism without PolyKindsThis program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# OPTIONS_GHC ddumpderiv #}
module Bug where
import Data.Coerce
import Data.Proxy
class C a b where
c :: Proxy (x :: a) > b
newtype I a = MkI a
instance C x a => C x (Bug.I a) where
c = coerce @(forall (z :: x). Proxy z > a)
@(forall (z :: x). Proxy z > I a)
c
```
is rightfully rejected by GHC 8.2.2:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

20  c = coerce @(forall (z :: x). Proxy z > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:21:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

21  @(forall (z :: x). Proxy z > I a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But GHC 8.4.1alpha2 actually //accepts// this program!
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
```
This is almost certainly bogus.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug where\r\n\r\nimport Data.Coerce\r\nimport Data.Proxy\r\n\r\nclass C a b where\r\n c :: Proxy (x :: a) > b\r\n\r\nnewtype I a = MkI a\r\n\r\ninstance C x a => C x (Bug.I a) where\r\n c = coerce @(forall (z :: x). Proxy z > a)\r\n @(forall (z :: x). Proxy z > I a)\r\n c\r\n}}}\r\n\r\nis rightfully rejected by GHC 8.2.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n20  c = coerce @(forall (z :: x). Proxy z > a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:21:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n21  @(forall (z :: x). Proxy z > I a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 actually //accepts// this program!\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs\r\nGHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\n}}}\r\n\r\nThis is almost certainly bogus.","type_of_failure":"OtherFailure","blocking":[]} >This program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# OPTIONS_GHC ddumpderiv #}
module Bug where
import Data.Coerce
import Data.Proxy
class C a b where
c :: Proxy (x :: a) > b
newtype I a = MkI a
instance C x a => C x (Bug.I a) where
c = coerce @(forall (z :: x). Proxy z > a)
@(forall (z :: x). Proxy z > I a)
c
```
is rightfully rejected by GHC 8.2.2:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

20  c = coerce @(forall (z :: x). Proxy z > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:21:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

21  @(forall (z :: x). Proxy z > I a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But GHC 8.4.1alpha2 actually //accepts// this program!
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
```
This is almost certainly bogus.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug where\r\n\r\nimport Data.Coerce\r\nimport Data.Proxy\r\n\r\nclass C a b where\r\n c :: Proxy (x :: a) > b\r\n\r\nnewtype I a = MkI a\r\n\r\ninstance C x a => C x (Bug.I a) where\r\n c = coerce @(forall (z :: x). Proxy z > a)\r\n @(forall (z :: x). Proxy z > I a)\r\n c\r\n}}}\r\n\r\nis rightfully rejected by GHC 8.2.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n20  c = coerce @(forall (z :: x). Proxy z > a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:21:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n21  @(forall (z :: x). Proxy z > I a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 actually //accepts// this program!\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs\r\nGHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\n}}}\r\n\r\nThis is almost certainly bogus.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14554Core Lint error mixing20190707T18:16:32ZIcelandjackCore Lint error mixingWhile trying to deeply embed *Singletons*style defunctionalization symbol application using the code from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs), I ran into the following `dcorelint` error:
```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type a ~> b = (a, b) > Type
type family (@@) (f::k ~> k') (a::k)::k'
data IdSym0 :: Type ~> Type
type instance IdSym0 @@ a = a
data KIND = X  FNARR KIND KIND
data TY :: KIND > Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') > TY k > TY k'
data TyRep (kind::KIND) :: TY kind > Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
> TyRep k a
> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = IK k ~> IK k'
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym0
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = \case
TFnApp TID a > undefined
```
```
$ ghci ignoredotghci dcorelint ~/hs/123bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
ASSERT failed!
Bad coercion hole {a2UN}: (IT
(a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
nominal
<(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N
IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)
IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)
nominal
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"Core Lint error mixing","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to deeply embed ''Singletons''style defunctionalization symbol application using the code from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality], I ran into the following `dcorelint` error:\r\n\r\n{{{#!hs\r\n{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ntype a ~> b = (a, b) > Type\r\n\r\ntype family (@@) (f::k ~> k') (a::k)::k'\r\n\r\ndata IdSym0 :: Type ~> Type\r\n\r\ntype instance IdSym0 @@ a = a\r\n\r\ndata KIND = X  FNARR KIND KIND\r\n\r\ndata TY :: KIND > Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') > TY k > TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind > Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n > TyRep k a\r\n > TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = IK k ~> IK k'\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym0\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = \\case\r\n TFnApp TID a > undefined \r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci dcorelint ~/hs/123bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tASSERT failed!\r\n Bad coercion hole {a2UN}: (IT\r\n (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n (IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n nominal\r\n <(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N\r\n IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)\r\n IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)\r\n nominal\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >While trying to deeply embed *Singletons*style defunctionalization symbol application using the code from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs), I ran into the following `dcorelint` error:
```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type a ~> b = (a, b) > Type
type family (@@) (f::k ~> k') (a::k)::k'
data IdSym0 :: Type ~> Type
type instance IdSym0 @@ a = a
data KIND = X  FNARR KIND KIND
data TY :: KIND > Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') > TY k > TY k'
data TyRep (kind::KIND) :: TY kind > Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
> TyRep k a
> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = IK k ~> IK k'
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym0
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = \case
TFnApp TID a > undefined
```
```
$ ghci ignoredotghci dcorelint ~/hs/123bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
ASSERT failed!
Bad coercion hole {a2UN}: (IT
(a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
nominal
<(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N
IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)
IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)
nominal
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"Core Lint error mixing","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to deeply embed ''Singletons''style defunctionalization symbol application using the code from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality], I ran into the following `dcorelint` error:\r\n\r\n{{{#!hs\r\n{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ntype a ~> b = (a, b) > Type\r\n\r\ntype family (@@) (f::k ~> k') (a::k)::k'\r\n\r\ndata IdSym0 :: Type ~> Type\r\n\r\ntype instance IdSym0 @@ a = a\r\n\r\ndata KIND = X  FNARR KIND KIND\r\n\r\ndata TY :: KIND > Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') > TY k > TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind > Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n > TyRep k a\r\n > TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = IK k ~> IK k'\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym0\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = \\case\r\n TFnApp TID a > undefined \r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci dcorelint ~/hs/123bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tASSERT failed!\r\n Bad coercion hole {a2UN}: (IT\r\n (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n (IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n nominal\r\n <(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N\r\n IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)\r\n IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)\r\n nominal\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14450GHCi spins forever20190707T18:16:59ZIcelandjackGHCi spins foreverThe following code compiles just fine (8.3.20170920)
```hs
{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
type Cat ob = ob > ob > Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (>)
type Cod (IddSym0 :: Type ~> Type) = (>)
varpa :: (a > a') > (a > a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (>)
```
it sends GHC for a spin.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type > Type > Type\r\n\r\ntype a ~> b = TyFun a b > Type\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n type Cod (IddSym0 :: Type ~> Type) = (>)\r\n\r\n varpa :: (a > a') > (a > a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} >The following code compiles just fine (8.3.20170920)
```hs
{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
type Cat ob = ob > ob > Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (>)
type Cod (IddSym0 :: Type ~> Type) = (>)
varpa :: (a > a') > (a > a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (>)
```
it sends GHC for a spin.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type > Type > Type\r\n\r\ntype a ~> b = TyFun a b > Type\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n type Cod (IddSym0 :: Type ~> Type) = (>)\r\n\r\n varpa :: (a > a') > (a > a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://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.https://gitlab.haskell.org/ghc/ghc//issues/12638GHC panic when resolving Show instance20190707T18:25:44ZMichaelKGHC panic when resolving Show instanceI'm playing around with rolling my own type defaulting and found a panic. Note: adding a stub `Show (W a)` instance resolves this (i.e. `show _ = "test"`).
```
{ Test.hs }
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Test where
import Data.Proxy
data W (a :: k) = Wk  W (MkStar a)
type family MkStar (a :: k) :: *
main = print (W Proxy :: W (Proxy (~)))
```
```
$ ghc Test.hs o test
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:13:8: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.1 for x86_64appledarwin):
print_equality ~
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
If `x = W Proxy :: W (Proxy (~))` is only defined, there is no issue. It seems to occur exactly when resolving a `Show` instance for `W (Proxy (~))` and one does not exist.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"GHC panic when resolving Show instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PolyKinds,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm playing around with rolling my own type defaulting and found a panic. Note: adding a stub `Show (W a)` instance resolves this (i.e. `show _ = \"test\"`). \r\n\r\n{{{\r\n{ Test.hs }\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nmodule Test where\r\n\r\nimport Data.Proxy\r\n\r\ndata W (a :: k) = Wk  W (MkStar a)\r\n\r\ntype family MkStar (a :: k) :: *\r\n\r\nmain = print (W Proxy :: W (Proxy (~)))\r\n}}}\r\n\r\n{{{\r\n$ ghc Test.hs o test \r\n[1 of 1] Compiling Test ( Test.hs, Test.o )\r\n\r\nTest.hs:13:8: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.1 for x86_64appledarwin):\r\n\tprint_equality ~\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIf `x = W Proxy :: W (Proxy (~))` is only defined, there is no issue. It seems to occur exactly when resolving a `Show` instance for `W (Proxy (~))` and one does not exist.\r\n","type_of_failure":"OtherFailure","blocking":[]} >I'm playing around with rolling my own type defaulting and found a panic. Note: adding a stub `Show (W a)` instance resolves this (i.e. `show _ = "test"`).
```
{ Test.hs }
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Test where
import Data.Proxy
data W (a :: k) = Wk  W (MkStar a)
type family MkStar (a :: k) :: *
main = print (W Proxy :: W (Proxy (~)))
```
```
$ ghc Test.hs o test
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:13:8: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.1 for x86_64appledarwin):
print_equality ~
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
If `x = W Proxy :: W (Proxy (~))` is only defined, there is no issue. It seems to occur exactly when resolving a `Show` instance for `W (Proxy (~))` and one does not exist.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 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":"GHC panic when resolving Show instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PolyKinds,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm playing around with rolling my own type defaulting and found a panic. Note: adding a stub `Show (W a)` instance resolves this (i.e. `show _ = \"test\"`). \r\n\r\n{{{\r\n{ Test.hs }\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nmodule Test where\r\n\r\nimport Data.Proxy\r\n\r\ndata W (a :: k) = Wk  W (MkStar a)\r\n\r\ntype family MkStar (a :: k) :: *\r\n\r\nmain = print (W Proxy :: W (Proxy (~)))\r\n}}}\r\n\r\n{{{\r\n$ ghc Test.hs o test \r\n[1 of 1] Compiling Test ( Test.hs, Test.o )\r\n\r\nTest.hs:13:8: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.1 for x86_64appledarwin):\r\n\tprint_equality ~\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIf `x = W Proxy :: W (Proxy (~))` is only defined, there is no issue. It seems to occur exactly when resolving a `Show` instance for `W (Proxy (~))` and one does not exist.\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/11480UndecidableSuperClasses causes the compiler to spin with UndecidableInstances20190707T18:30:14ZEdward KmettUndecidableSuperClasses causes the compiler to spin with UndecidableInstancesLooks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:
```hs
{# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances,
FunctionalDependencies, UndecidableSuperClasses #}
import GHC.Types (Constraint)
import qualified Prelude
data Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)
class Functor p (Nat p (>)) p => Category (p :: i > i > *)
class (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)
instance Category (>)
instance Functor (>) (>) ((>) e)
instance Functor (>) (Nat (>) (>)) (>)
```
Sorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.
One potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.
Also, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the "real" version of the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 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":"UndecidableSuperClasses causes the compiler to spin with UndecidableInstances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["PolyKinds,","UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.\r\n\r\nI took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:\r\n\r\n{{{#!hs\r\n{# language KindSignatures, PolyKinds, TypeFamilies, \r\n NoImplicitPrelude, FlexibleContexts,\r\n MultiParamTypeClasses, GADTs, \r\n ConstraintKinds, FlexibleInstances, \r\n FunctionalDependencies, UndecidableSuperClasses #}\r\n\r\nimport GHC.Types (Constraint)\r\nimport qualified Prelude\r\n\r\ndata Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)\r\n\r\nclass Functor p (Nat p (>)) p => Category (p :: i > i > *)\r\nclass (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod\r\n\r\ninstance (Category c, Category d) => Category (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)\r\n\r\ninstance Category (>)\r\ninstance Functor (>) (>) ((>) e)\r\ninstance Functor (>) (Nat (>) (>)) (>)\r\n}}}\r\n\r\nSorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.\r\n\r\nOne potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.\r\n\r\nAlso, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the \"real\" version of the problem.","type_of_failure":"OtherFailure","blocking":[]} >Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:
```hs
{# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances,
FunctionalDependencies, UndecidableSuperClasses #}
import GHC.Types (Constraint)
import qualified Prelude
data Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)
class Functor p (Nat p (>)) p => Category (p :: i > i > *)
class (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)
instance Category (>)
instance Functor (>) (>) ((>) e)
instance Functor (>) (Nat (>) (>)) (>)
```
Sorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.
One potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.
Also, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the "real" version of the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 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":"UndecidableSuperClasses causes the compiler to spin with UndecidableInstances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["PolyKinds,","UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.\r\n\r\nI took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:\r\n\r\n{{{#!hs\r\n{# language KindSignatures, PolyKinds, TypeFamilies, \r\n NoImplicitPrelude, FlexibleContexts,\r\n MultiParamTypeClasses, GADTs, \r\n ConstraintKinds, FlexibleInstances, \r\n FunctionalDependencies, UndecidableSuperClasses #}\r\n\r\nimport GHC.Types (Constraint)\r\nimport qualified Prelude\r\n\r\ndata Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)\r\n\r\nclass Functor p (Nat p (>)) p => Category (p :: i > i > *)\r\nclass (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod\r\n\r\ninstance (Category c, Category d) => Category (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)\r\n\r\ninstance Category (>)\r\ninstance Functor (>) (>) ((>) e)\r\ninstance Functor (>) (Nat (>) (>)) (>)\r\n}}}\r\n\r\nSorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.\r\n\r\nOne potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.\r\n\r\nAlso, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the \"real\" version of the problem.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1https://gitlab.haskell.org/ghc/ghc//issues/9633PolyKinds in 7.8.2 vs 7.8.320190707T18:39:44ZEric CrockettPolyKinds in 7.8.2 vs 7.8.3The following code **compiles** with GHC 7.8.2.
This code has been distilled down from a larger example where I needed `XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify` function is supposed to modify a mutable `Data.Vector`, hence the inner `go` function has the intended type of `Int > m ()`, though strictly speaking it could return any value since everything is discarded by the `forM_`.
```
 {# LANGUAGE PolyKinds #}
module Foo where
import Control.Monad (forM_)
import Bar
 Vector signatures
unsafeRead :: (Monad m) => v (PrimState m) a > Int > m a
unsafeRead = error "type only"
unsafeWrite :: (Monad m) => v (PrimState m) a > Int > a > m ()
unsafeWrite = error "type only"
modify :: Int > Bar v r
modify p = Bar (p1) $ \y > do
let go i = do
a < unsafeRead y i
unsafeWrite y i a
return a
forM_ [0..(p1)] go
```
```
{# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #}
module Bar where
type family PrimState (m :: * > *) :: *
data Bar v r = Bar Int (forall s . (Monad s) => v (PrimState s) r > s ())
```
In 7.8.3, this above code results in the error (with `fprintexplicitkinds`)
```
Foo.hs:19:23:
Couldn't match type ‘a0’ with ‘r’
‘a0’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘r’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Couldn't match type ‘v1’ with ‘v’
‘v1’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘v’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
...
Failed, modules loaded: Bar.
```
After much digging, I found that enabling `XPolyKinds` in Foo.hs gives a more meaningful error:
```
Foo.hs:19:23:
Could not deduce ((~) (* > k > *) v v0)
...
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Could not deduce ((~) (* > k > *) v v1)
...
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
In a stmt of a 'do' block: unsafeWrite y i a
Failed, modules loaded: Bar.
```
Adding `PolyKinds` to Foo.hs *and* uncommenting `return a` results in the error:
```
Foo.hs:17:12:
Couldn't match kind ‘k’ with ‘k1’
because type variable ‘k1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for modify :: Int > Bar k1 v r
at Foo.hs:16:1124
Expected type: Bar k1 v r
Actual type: Bar k v0 r0
...
In the expression:
Bar (p  1)
$ \ y
> do { let ...;
forM_ [0 .. (p  1)] go }
...
Foo.hs:18:7:
Kind incompatibility when matching types:
v0 :: * > k > *
v1 :: * > * > *
...
When checking that ‘go’
has the inferred type ‘forall (k :: BOX)
(m :: * > *)
b
(v :: * > * > *)
(v1 :: * > * > *).
((~) (* > k > *) v0 v, (~) k r0 b, (~) (* > k > *) v0 v1,
Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m b’
Probable cause: the inferred type is ambiguous
In the expression:
do { let go i = ...;
forM_ [0 .. (p  1)] go }
...
Failed, modules loaded: Bar.
```
These errors can be resolved by modifying the original code above in any of the following ways:
1. Remove `XPolyKinds` from Bar.hs
1. Add an explicit kind signature to the `v :: * > * > *` parameter of type `Bar`
1. With `PolyKinds` in Bar but \*not\* Foo, uncommenting `return a` make GHC 7.8.3. compile
What I'm trying to understand is
1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't seem to be anything addressing `PolyKinds` in the [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release783.html) .
1. In the event the above code should not compile with 7.8.3, there error message could be much clearer. The first error message above didn't help me understand that `PolyKinds` was to blame, while the second error did a better job, and the third was very clearly a `PolyKinds` issue (i.e. `kind mismatch`)
1. For the third resolution option above, I can't see any reason that adding `return a` to the inner `go` function should make the code compile while leaving it out makes the code somehow ambiguous. This, if nothing else, seems like a bug.The following code **compiles** with GHC 7.8.2.
This code has been distilled down from a larger example where I needed `XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify` function is supposed to modify a mutable `Data.Vector`, hence the inner `go` function has the intended type of `Int > m ()`, though strictly speaking it could return any value since everything is discarded by the `forM_`.
```
 {# LANGUAGE PolyKinds #}
module Foo where
import Control.Monad (forM_)
import Bar
 Vector signatures
unsafeRead :: (Monad m) => v (PrimState m) a > Int > m a
unsafeRead = error "type only"
unsafeWrite :: (Monad m) => v (PrimState m) a > Int > a > m ()
unsafeWrite = error "type only"
modify :: Int > Bar v r
modify p = Bar (p1) $ \y > do
let go i = do
a < unsafeRead y i
unsafeWrite y i a
return a
forM_ [0..(p1)] go
```
```
{# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #}
module Bar where
type family PrimState (m :: * > *) :: *
data Bar v r = Bar Int (forall s . (Monad s) => v (PrimState s) r > s ())
```
In 7.8.3, this above code results in the error (with `fprintexplicitkinds`)
```
Foo.hs:19:23:
Couldn't match type ‘a0’ with ‘r’
‘a0’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘r’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Couldn't match type ‘v1’ with ‘v’
‘v1’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘v’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
...
Failed, modules loaded: Bar.
```
After much digging, I found that enabling `XPolyKinds` in Foo.hs gives a more meaningful error:
```
Foo.hs:19:23:
Could not deduce ((~) (* > k > *) v v0)
...
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Could not deduce ((~) (* > k > *) v v1)
...
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
In a stmt of a 'do' block: unsafeWrite y i a
Failed, modules loaded: Bar.
```
Adding `PolyKinds` to Foo.hs *and* uncommenting `return a` results in the error:
```
Foo.hs:17:12:
Couldn't match kind ‘k’ with ‘k1’
because type variable ‘k1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for modify :: Int > Bar k1 v r
at Foo.hs:16:1124
Expected type: Bar k1 v r
Actual type: Bar k v0 r0
...
In the expression:
Bar (p  1)
$ \ y
> do { let ...;
forM_ [0 .. (p  1)] go }
...
Foo.hs:18:7:
Kind incompatibility when matching types:
v0 :: * > k > *
v1 :: * > * > *
...
When checking that ‘go’
has the inferred type ‘forall (k :: BOX)
(m :: * > *)
b
(v :: * > * > *)
(v1 :: * > * > *).
((~) (* > k > *) v0 v, (~) k r0 b, (~) (* > k > *) v0 v1,
Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m b’
Probable cause: the inferred type is ambiguous
In the expression:
do { let go i = ...;
forM_ [0 .. (p  1)] go }
...
Failed, modules loaded: Bar.
```
These errors can be resolved by modifying the original code above in any of the following ways:
1. Remove `XPolyKinds` from Bar.hs
1. Add an explicit kind signature to the `v :: * > * > *` parameter of type `Bar`
1. With `PolyKinds` in Bar but \*not\* Foo, uncommenting `return a` make GHC 7.8.3. compile
What I'm trying to understand is
1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't seem to be anything addressing `PolyKinds` in the [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release783.html) .
1. In the event the above code should not compile with 7.8.3, there error message could be much clearer. The first error message above didn't help me understand that `PolyKinds` was to blame, while the second error did a better job, and the third was very clearly a `PolyKinds` issue (i.e. `kind mismatch`)
1. For the third resolution option above, I can't see any reason that adding `return a` to the inner `go` function should make the code compile while leaving it out makes the code somehow ambiguous. This, if nothing else, seems like a bug.7.10.1https://gitlab.haskell.org/ghc/ghc//issues/8913either bug or confusing error message mixing PolyKinds and TypeFamilies20190707T18:42:50Zghorneither bug or confusing error message mixing PolyKinds and TypeFamiliesI found this when using GHC.Generics, but it has to do with TypeFamilies so here is a standalone example:
```
{# OPTIONS_GHC Wall #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
module Test where
class GCat f where
gcat :: f p > Int
cat :: (GCat (MyRep a), MyGeneric a) => a > Int
cat x = gcat (from x)
class MyGeneric a where
type MyRep a :: * > *
from :: a > (MyRep a) p
```
This code gives the error message
```
src/Dyno/Test.hs:12:9:
Could not deduce (GCat (MyRep a)) arising from a use of ‘gcat’
from the context (GCat (MyRep a), MyGeneric a)
bound by the type signature for
cat :: (GCat (MyRep a), MyGeneric a) => a > Int
at src/Dyno/Test.hs:11:848
In the expression: gcat (from x)
In an equation for ‘cat’: cat x = gcat (from x)
Failed, modules loaded: none.
```
If this is not a bug then error message is pretty confusing because it's saying "Can't deduce (C a) from (C a)", where the message I'm used to is "Can't derive (C a) from (C a0)" or something that indicates the mismatch.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  gregmainland@gmail.com 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"either bug or confusing error message mixing PolyKinds and TypeFamilies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["gregmainland@gmail.com"],"type":"Bug","description":"I found this when using GHC.Generics, but it has to do with TypeFamilies so here is a standalone example:\r\n\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Test where\r\n\r\nclass GCat f where\r\n gcat :: f p > Int\r\n\r\ncat :: (GCat (MyRep a), MyGeneric a) => a > Int\r\ncat x = gcat (from x)\r\n\r\nclass MyGeneric a where\r\n type MyRep a :: * > *\r\n from :: a > (MyRep a) p\r\n}}}\r\n\r\nThis code gives the error message\r\n{{{\r\nsrc/Dyno/Test.hs:12:9:\r\n Could not deduce (GCat (MyRep a)) arising from a use of ‘gcat’\r\n from the context (GCat (MyRep a), MyGeneric a)\r\n bound by the type signature for\r\n cat :: (GCat (MyRep a), MyGeneric a) => a > Int\r\n at src/Dyno/Test.hs:11:848\r\n In the expression: gcat (from x)\r\n In an equation for ‘cat’: cat x = gcat (from x)\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nIf this is not a bug then error message is pretty confusing because it's saying \"Can't deduce (C a) from (C a)\", where the message I'm used to is \"Can't derive (C a) from (C a0)\" or something that indicates the mismatch.","type_of_failure":"OtherFailure","blocking":[]} >I found this when using GHC.Generics, but it has to do with TypeFamilies so here is a standalone example:
```
{# OPTIONS_GHC Wall #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
module Test where
class GCat f where
gcat :: f p > Int
cat :: (GCat (MyRep a), MyGeneric a) => a > Int
cat x = gcat (from x)
class MyGeneric a where
type MyRep a :: * > *
from :: a > (MyRep a) p
```
This code gives the error message
```
src/Dyno/Test.hs:12:9:
Could not deduce (GCat (MyRep a)) arising from a use of ‘gcat’
from the context (GCat (MyRep a), MyGeneric a)
bound by the type signature for
cat :: (GCat (MyRep a), MyGeneric a) => a > Int
at src/Dyno/Test.hs:11:848
In the expression: gcat (from x)
In an equation for ‘cat’: cat x = gcat (from x)
Failed, modules loaded: none.
```
If this is not a bug then error message is pretty confusing because it's saying "Can't deduce (C a) from (C a)", where the message I'm used to is "Can't derive (C a) from (C a0)" or something that indicates the mismatch.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  gregmainland@gmail.com 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"either bug or confusing error message mixing PolyKinds and TypeFamilies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["gregmainland@gmail.com"],"type":"Bug","description":"I found this when using GHC.Generics, but it has to do with TypeFamilies so here is a standalone example:\r\n\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE PolyKinds #}\r\n\r\nmodule Test where\r\n\r\nclass GCat f where\r\n gcat :: f p > Int\r\n\r\ncat :: (GCat (MyRep a), MyGeneric a) => a > Int\r\ncat x = gcat (from x)\r\n\r\nclass MyGeneric a where\r\n type MyRep a :: * > *\r\n from :: a > (MyRep a) p\r\n}}}\r\n\r\nThis code gives the error message\r\n{{{\r\nsrc/Dyno/Test.hs:12:9:\r\n Could not deduce (GCat (MyRep a)) arising from a use of ‘gcat’\r\n from the context (GCat (MyRep a), MyGeneric a)\r\n bound by the type signature for\r\n cat :: (GCat (MyRep a), MyGeneric a) => a > Int\r\n at src/Dyno/Test.hs:11:848\r\n In the expression: gcat (from x)\r\n In an equation for ‘cat’: cat x = gcat (from x)\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nIf this is not a bug then error message is pretty confusing because it's saying \"Can't deduce (C a) from (C a)\", where the message I'm used to is \"Can't derive (C a) from (C a0)\" or something that indicates the mismatch.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/8893XPolyKinds causes "*** Exception: Prelude.(!!): index too large"20190707T18:42:55ZghornXPolyKinds causes "*** Exception: Prelude.(!!): index too large"The following program will compile fine:
```
{# OPTIONS_GHC Wall #}
{# Language DeriveFunctor #}
{# Language PolyKinds #}
module Bug where
data V a = V [a] deriving Functor
data C x a = C (V (P x a)) deriving Functor
data P x a = P (x a) deriving Functor
```
But when PolyKinds is enabled, GHC crashes with
```
$ ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:37:ghc: panic! (the 'impossible' happened)
(GHC version 7.8.0.20140228 for x86_64unknownlinux):
Prelude.(!!): index too large
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 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":"XPolyKinds causes \"*** Exception: Prelude.(!!): index too large\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will compile fine:\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# Language DeriveFunctor #}\r\n{# Language PolyKinds #}\r\n\r\nmodule Bug where\r\n\r\ndata V a = V [a] deriving Functor\r\n\r\ndata C x a = C (V (P x a)) deriving Functor\r\n\r\ndata P x a = P (x a) deriving Functor\r\n}}}\r\n\r\nBut when PolyKinds is enabled, GHC crashes with\r\n\r\n{{{\r\n$ ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:37:ghc: panic! (the 'impossible' happened)\r\n (GHC version 7.8.0.20140228 for x86_64unknownlinux):\r\n\tPrelude.(!!): index too large\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program will compile fine:
```
{# OPTIONS_GHC Wall #}
{# Language DeriveFunctor #}
{# Language PolyKinds #}
module Bug where
data V a = V [a] deriving Functor
data C x a = C (V (P x a)) deriving Functor
data P x a = P (x a) deriving Functor
```
But when PolyKinds is enabled, GHC crashes with
```
$ ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:37:ghc: panic! (the 'impossible' happened)
(GHC version 7.8.0.20140228 for x86_64unknownlinux):
Prelude.(!!): index too large
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 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":"XPolyKinds causes \"*** Exception: Prelude.(!!): index too large\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will compile fine:\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# Language DeriveFunctor #}\r\n{# Language PolyKinds #}\r\n\r\nmodule Bug where\r\n\r\ndata V a = V [a] deriving Functor\r\n\r\ndata C x a = C (V (P x a)) deriving Functor\r\n\r\ndata P x a = P (x a) deriving Functor\r\n}}}\r\n\r\nBut when PolyKinds is enabled, GHC crashes with\r\n\r\n{{{\r\n$ ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:37:ghc: panic! (the 'impossible' happened)\r\n (GHC version 7.8.0.20140228 for x86_64unknownlinux):\r\n\tPrelude.(!!): index too large\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >7.8.1https://gitlab.haskell.org/ghc/ghc//issues/8031Template Haskell gets confused with kind variables introduced in separate for...20190707T18:46:46ZRichard Eisenbergrae@richarde.devTemplate Haskell gets confused with kind variables introduced in separate forallsThe following file compiles without complaint:
```
{# LANGUAGE TemplateHaskell, RankNTypes, PolyKinds, DataKinds, TypeOperators,
GADTs #}
module S2 where
import Language.Haskell.TH
data Proxy a = Proxy
data SList :: [k] > * where
SCons :: Proxy h > Proxy t > SList (h ': t)
dec :: Q [Dec]
dec = [d foo :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)
foo a b = SCons a b ]
foo' :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)
foo' a b = SCons a b
```
Note that `foo` and `foo'` are identical, just at different compilation stages. However, the following module does not compile:
```
{# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, RankNTypes #}
module S3 where
import S2
$(dec)
```
The error is
```
S3.hs:7:3:
Couldn't match kind ‛k’ with ‛k1’
‛k’ is a rigid type variable bound by
the type signature for
foo :: Proxy k a0
> forall (k1 :: BOX) (b0 :: [k1]).
Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)
at S3.hs:7:3
‛k1’ is a rigid type variable bound by
the type signature for
foo :: Proxy k a0 > Proxy [k1] b > SList k1 ((':) k1 a0 b)
at S3.hs:7:3
Expected type: SList k1 ((':) k1 a0 b)
Actual type: SList k ((':) k a0 b)
Relevant bindings include
foo :: Proxy k a0
> forall (k1 :: BOX) (b0 :: [k1]).
Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)
(bound at S3.hs:7:3)
a_aTCB :: Proxy k a0 (bound at S3.hs:7:3)
b_aTCC :: Proxy [k1] b (bound at S3.hs:7:3)
In the expression: SCons a_aTCB b_aTCC
In an equation for ‛foo’: foo a_aTCB b_aTCC = SCons a_aTCB b_aTCC
```
If I change the nested `forall`s in the definition of `foo` to be just one toplevel `forall`, the problem goes away.
This may seem terribly esoteric, but it's easier to generate nested `forall`s than to float them all to the toplevel after processing a type. I received an email requesting that I get the `singletons` library to compile with HEAD, and this seems to be why it doesn't.
This is a regression error: the code compiles fine with 7.6.3 but not with HEAD.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"Template Haskell gets confused with kind variables introduced in separate foralls","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["PolyKinds","TemplateHaskell"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following file compiles without complaint:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell, RankNTypes, PolyKinds, DataKinds, TypeOperators,\r\n GADTs #}\r\n\r\nmodule S2 where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata Proxy a = Proxy\r\n\r\ndata SList :: [k] > * where\r\n SCons :: Proxy h > Proxy t > SList (h ': t)\r\n\r\ndec :: Q [Dec]\r\ndec = [d foo :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)\r\n foo a b = SCons a b ]\r\n\r\nfoo' :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)\r\nfoo' a b = SCons a b\r\n}}}\r\n\r\nNote that `foo` and `foo'` are identical, just at different compilation stages. However, the following module does not compile:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, RankNTypes #}\r\n\r\nmodule S3 where\r\n\r\nimport S2\r\n\r\n$(dec)\r\n}}}\r\n\r\nThe error is\r\n{{{\r\nS3.hs:7:3:\r\n Couldn't match kind ‛k’ with ‛k1’\r\n ‛k’ is a rigid type variable bound by\r\n the type signature for\r\n foo :: Proxy k a0\r\n > forall (k1 :: BOX) (b0 :: [k1]).\r\n Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)\r\n at S3.hs:7:3\r\n ‛k1’ is a rigid type variable bound by\r\n the type signature for\r\n foo :: Proxy k a0 > Proxy [k1] b > SList k1 ((':) k1 a0 b)\r\n at S3.hs:7:3\r\n Expected type: SList k1 ((':) k1 a0 b)\r\n Actual type: SList k ((':) k a0 b)\r\n Relevant bindings include\r\n foo :: Proxy k a0\r\n > forall (k1 :: BOX) (b0 :: [k1]).\r\n Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)\r\n (bound at S3.hs:7:3)\r\n a_aTCB :: Proxy k a0 (bound at S3.hs:7:3)\r\n b_aTCC :: Proxy [k1] b (bound at S3.hs:7:3)\r\n In the expression: SCons a_aTCB b_aTCC\r\n In an equation for ‛foo’: foo a_aTCB b_aTCC = SCons a_aTCB b_aTCC\r\n}}}\r\n\r\nIf I change the nested `forall`s in the definition of `foo` to be just one toplevel `forall`, the problem goes away.\r\n\r\nThis may seem terribly esoteric, but it's easier to generate nested `forall`s than to float them all to the toplevel after processing a type. I received an email requesting that I get the `singletons` library to compile with HEAD, and this seems to be why it doesn't.\r\n\r\nThis is a regression error: the code compiles fine with 7.6.3 but not with HEAD.","type_of_failure":"OtherFailure","blocking":[]} >The following file compiles without complaint:
```
{# LANGUAGE TemplateHaskell, RankNTypes, PolyKinds, DataKinds, TypeOperators,
GADTs #}
module S2 where
import Language.Haskell.TH
data Proxy a = Proxy
data SList :: [k] > * where
SCons :: Proxy h > Proxy t > SList (h ': t)
dec :: Q [Dec]
dec = [d foo :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)
foo a b = SCons a b ]
foo' :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)
foo' a b = SCons a b
```
Note that `foo` and `foo'` are identical, just at different compilation stages. However, the following module does not compile:
```
{# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, RankNTypes #}
module S3 where
import S2
$(dec)
```
The error is
```
S3.hs:7:3:
Couldn't match kind ‛k’ with ‛k1’
‛k’ is a rigid type variable bound by
the type signature for
foo :: Proxy k a0
> forall (k1 :: BOX) (b0 :: [k1]).
Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)
at S3.hs:7:3
‛k1’ is a rigid type variable bound by
the type signature for
foo :: Proxy k a0 > Proxy [k1] b > SList k1 ((':) k1 a0 b)
at S3.hs:7:3
Expected type: SList k1 ((':) k1 a0 b)
Actual type: SList k ((':) k a0 b)
Relevant bindings include
foo :: Proxy k a0
> forall (k1 :: BOX) (b0 :: [k1]).
Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)
(bound at S3.hs:7:3)
a_aTCB :: Proxy k a0 (bound at S3.hs:7:3)
b_aTCC :: Proxy [k1] b (bound at S3.hs:7:3)
In the expression: SCons a_aTCB b_aTCC
In an equation for ‛foo’: foo a_aTCB b_aTCC = SCons a_aTCB b_aTCC
```
If I change the nested `forall`s in the definition of `foo` to be just one toplevel `forall`, the problem goes away.
This may seem terribly esoteric, but it's easier to generate nested `forall`s than to float them all to the toplevel after processing a type. I received an email requesting that I get the `singletons` library to compile with HEAD, and this seems to be why it doesn't.
This is a regression error: the code compiles fine with 7.6.3 but not with HEAD.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"Template Haskell gets confused with kind variables introduced in separate foralls","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["PolyKinds","TemplateHaskell"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following file compiles without complaint:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell, RankNTypes, PolyKinds, DataKinds, TypeOperators,\r\n GADTs #}\r\n\r\nmodule S2 where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata Proxy a = Proxy\r\n\r\ndata SList :: [k] > * where\r\n SCons :: Proxy h > Proxy t > SList (h ': t)\r\n\r\ndec :: Q [Dec]\r\ndec = [d foo :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)\r\n foo a b = SCons a b ]\r\n\r\nfoo' :: forall (a :: k). Proxy a > forall (b :: [k]). Proxy b > SList (a ': b)\r\nfoo' a b = SCons a b\r\n}}}\r\n\r\nNote that `foo` and `foo'` are identical, just at different compilation stages. However, the following module does not compile:\r\n\r\n{{{\r\n{# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, RankNTypes #}\r\n\r\nmodule S3 where\r\n\r\nimport S2\r\n\r\n$(dec)\r\n}}}\r\n\r\nThe error is\r\n{{{\r\nS3.hs:7:3:\r\n Couldn't match kind ‛k’ with ‛k1’\r\n ‛k’ is a rigid type variable bound by\r\n the type signature for\r\n foo :: Proxy k a0\r\n > forall (k1 :: BOX) (b0 :: [k1]).\r\n Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)\r\n at S3.hs:7:3\r\n ‛k1’ is a rigid type variable bound by\r\n the type signature for\r\n foo :: Proxy k a0 > Proxy [k1] b > SList k1 ((':) k1 a0 b)\r\n at S3.hs:7:3\r\n Expected type: SList k1 ((':) k1 a0 b)\r\n Actual type: SList k ((':) k a0 b)\r\n Relevant bindings include\r\n foo :: Proxy k a0\r\n > forall (k1 :: BOX) (b0 :: [k1]).\r\n Proxy [k1] b0 > SList k1 ((':) k1 a0 b0)\r\n (bound at S3.hs:7:3)\r\n a_aTCB :: Proxy k a0 (bound at S3.hs:7:3)\r\n b_aTCC :: Proxy [k1] b (bound at S3.hs:7:3)\r\n In the expression: SCons a_aTCB b_aTCC\r\n In an equation for ‛foo’: foo a_aTCB b_aTCC = SCons a_aTCB b_aTCC\r\n}}}\r\n\r\nIf I change the nested `forall`s in the definition of `foo` to be just one toplevel `forall`, the problem goes away.\r\n\r\nThis may seem terribly esoteric, but it's easier to generate nested `forall`s than to float them all to the toplevel after processing a type. I received an email requesting that I get the `singletons` library to compile with HEAD, and this seems to be why it doesn't.\r\n\r\nThis is a regression error: the code compiles fine with 7.6.3 but not with HEAD.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/7601Internal error with kind annotation on associated type family20190707T18:49:02ZdreixelInternal error with kind annotation on associated type familyThe following module:
```
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Bug where
class C (a :: k) where
type F (a :: k)
```
Makes GHC raise an internal error:
```
GHC internal error: `k' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [(reB,
AThing forall (k :: BOX). k > Constraint),
(reC, AThing forall (k :: BOX) (k :: BOX). k > k)]
In the kind `k'
In the class declaration for `C'
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"Internal error with kind annotation on associated type family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["polykinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following module:\r\n{{{\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nmodule Bug where\r\n\r\nclass C (a :: k) where\r\n type F (a :: k)\r\n}}}\r\n\r\nMakes GHC raise an internal error:\r\n{{{\r\n GHC internal error: `k' is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [(reB,\r\n AThing forall (k :: BOX). k > Constraint),\r\n (reC, AThing forall (k :: BOX) (k :: BOX). k > k)]\r\n In the kind `k'\r\n In the class declaration for `C'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following module:
```
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Bug where
class C (a :: k) where
type F (a :: k)
```
Makes GHC raise an internal error:
```
GHC internal error: `k' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [(reB,
AThing forall (k :: BOX). k > Constraint),
(reC, AThing forall (k :: BOX) (k :: BOX). k > k)]
In the kind `k'
In the class declaration for `C'
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"Internal error with kind annotation on associated type family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["polykinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following module:\r\n{{{\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\nmodule Bug where\r\n\r\nclass C (a :: k) where\r\n type F (a :: k)\r\n}}}\r\n\r\nMakes GHC raise an internal error:\r\n{{{\r\n GHC internal error: `k' is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [(reB,\r\n AThing forall (k :: BOX). k > Constraint),\r\n (reC, AThing forall (k :: BOX) (k :: BOX). k > k)]\r\n In the kind `k'\r\n In the class declaration for `C'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >