GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-10-14T16:36:06Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18831GHC requires PolyKinds in places without any kind polymorphism2020-10-14T16:36:06ZRyan ScottGHC requires PolyKinds in places without any kind polymorphismI would expect the following to typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 -> Type
```
Surprisingly, however, it doesn't.
```
$ /...I would expect the following to typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 -> Type
```
Surprisingly, however, it doesn't.
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: 0
Did you mean to enable PolyKinds?
|
8 | data T :: Proxy 0 -> Type
| ^
```
I find it quite surprising that using a type-level literal would require `PolyKinds`, as there's nothing inherently poly-kinded about it.
This isn't even the only example of strange `PolyKinds` requirements. The following programs are also rejected for similar reasons:
* Kind-level uses of `=>`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
data T :: () => Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:11: error:
Illegal kind: () => Type
Did you mean to enable PolyKinds?
|
7 | data T :: () => Type
| ^^^^^^^^^^
```
</details>
* Kind-level uses of explicit annotations:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
data T :: (Type :: Type) -> Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:12: error:
Illegal kind: Type :: Type
Did you mean to enable PolyKinds?
|
7 | data T :: (Type :: Type) -> Type
| ^^^^^^^^^^^^
```
</details>
* Kind-level uses of promoted lists:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '[Type,Type] -> Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '[Type, Type]
Did you mean to enable PolyKinds?
|
8 | data T :: Proxy '[Type,Type] -> Type
| ^^^^^^^^^^^^
```
</details>
* Kind-level uses of promoted tuples:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '(Type,Type) -> Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '(Type, Type)
Did you mean to enable PolyKinds?
|
8 | data T :: Proxy '(Type,Type) -> Type
| ^^^^^^^^^^^^
```
</details>https://gitlab.haskell.org/ghc/ghc/-/issues/18488DerivingVia: Kinding information isn't propagated2020-07-22T00: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
Co...## 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 stand-alone 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/18059Add warning for type aliases that monomorphise a PolyKinds-ed type2022-10-12T18:28:43ZlspitznerAdd warning for type aliases that monomorphise a PolyKinds-ed type## Motivation
module A has `-XPolyKinds` and defines some polykinded type `MyPoly :: Type -> k -> Type`
module B does not have `-XPolyKinds` and defines an alias `type MySpecialP = MyPoly Bool`
`MySpecialP` is monokinded, leading to c...## Motivation
module A has `-XPolyKinds` and defines some polykinded type `MyPoly :: Type -> k -> Type`
module B does not have `-XPolyKinds` and defines an alias `type MySpecialP = MyPoly Bool`
`MySpecialP` is monokinded, leading to confusing error messages down the line.
## Proposal
Does it make sense to have a warning ("-Wmonomorphizing-alias"?) for this? For any type alias, check if the RHS involves PolyKinds, check that it does not have an explicitly mono-kinded kind-signature and that PolyKinds is disabled. If so, raise the warning.
For the unlikely case that the mono-kinded alias is desired, allowing an explicit kind signature to silence the warning seems appropriate.
I have no idea how complex this is to implement. If checking the above condition is too complex or is hard to do without false positives, feel free to close this.
Thanks for your consideration.https://gitlab.haskell.org/ghc/ghc/-/issues/17838Unused type variable error misidentifies the name of the type variable2020-03-31T20: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 ::...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/17772CUSK-less class typechecks on 8.4, but not on 8.6+2021-03-31T17:39:10ZRyan ScottCUSK-less 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 (...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 UndecidableInstances2019-10-31T22:30:53ZMax HarmsAnnotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances## Summary
The error message provided when GHC infers the kind of an otherwise poly-kinded 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.
#...## Summary
The error message provided when GHC infers the kind of an otherwise poly-kinded 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 known-to-be-valid 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/16755Pattern signature subtyping for higher-rank types works differently in term-l...2019-06-06T09:28:04ZRyan ScottPattern signature subtyping for higher-rank types works differently in term-level type signatures and TLKSsGHC accepts the following program:
```hs
f :: (forall a. a -> a) -> b -> b
f (g :: b -> b) x = g x
```
But not this type-level counterpart:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables ...GHC accepts the following program:
```hs
f :: (forall a. a -> a) -> b -> b
f (g :: b -> b) x = g x
```
But not this type-level counterpart:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where
type F :: (forall a. a -> a) -> b -> b
type F (g :: b -> b) x = g x
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:1: error:
• Expected kind ‘b -> b’, but ‘g’ has kind ‘forall a. a -> a’
• In the type synonym declaration for ‘F’
|
8 | type F (g :: b -> b) x = g x
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/16726Data type can't be given return kind that is identical to its TLKS2019-09-26T20:32:36ZRyan ScottData type can't be given return kind that is identical to its TLKSI would have expected this to work, but it doesn't:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where
import Data.Kind
type D :: forall k. k -> Type
data D :...I would have expected this to work, but it doesn't:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where
import Data.Kind
type D :: forall k. k -> Type
data D :: forall k. k -> Type
```
```
[1 of 1] Compiling Bug ( ../Bug.hs, ../Bug.o )
../Bug.hs:9:1: error:
• Couldn't match expected kind ‘forall k1. k1 -> *’
with actual kind ‘k -> *’
• In the data type declaration for ‘D’
|
9 | data D :: forall k. k -> Type
| ^^^^^^
```
Note that this bug does not appear to apply to type families, as the following works without issue:
```hs
type T :: forall k. k -> Type
type family T :: forall k. k -> Type
```Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/16724Inconsistent treatment of type family arities in TLKSs2019-08-23T21:50:04ZRyan ScottInconsistent treatment of type family arities in TLKSsConsider this program:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
type T1 :: forall k (a :: k). Type
ty...Consider this program:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
type T1 :: forall k (a :: k). Type
type family T1
-- type T2 :: forall {k} (a :: k). Type
type T2 :: forall a. Type
type family T2
```
`T1` and `T2` look the same, but they actually get assigned very different arities, as GHCi reveals when `-fprint-explicit-kinds` is enabled:
```
λ> :set -fprint-explicit-kinds -fprint-explicit-foralls
λ> :info T1
type family T1 @k @(a :: k) :: * -- Defined at ../Bug.hs:10:1
λ> :info T2
type family T2 :: forall {k} (a :: k). *
-- Defined at ../Bug.hs:14:1
```
`T1` has arity two, whereas `T2` has arity zero! I find this rather surprising given that there are no syntactic differences in the declarations for `T1` and `T2`—the only differences lie in the visibility of the `k` in their kinds. I would expect `T1` and `T2` to have the same arity here.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/16722Lack of PolyKinds validity checking in TLKS kinds2019-05-31T17:31:59ZRyan ScottLack of PolyKinds validity checking in TLKS kindsThe following program is accepted:
```hs
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where
import Data.Kind
type D :: k -> Type
data D a
```
I would expect to have to enable `PolyKinds` in order for this to work.The following program is accepted:
```hs
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where
import Data.Kind
type D :: k -> Type
data D a
```
I would expect to have to enable `PolyKinds` in order for this to work.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/16276Feature request: Polymorphic kinds in Data.Functor.Classes2019-07-07T18:00:42ZLangston BarrettFeature request: Polymorphic kinds in Data.Functor.ClassesThe classes in Data.Functor.Classes have a somewhat restrictive kind signature:
```
*Data.Functor.Classes> :k Eq1
Eq1 :: (* -> *) ...The classes in Data.Functor.Classes have a somewhat restrictive kind signature:
```
*Data.Functor.Classes> :k Eq1
Eq1 :: (* -> *) -> Constraint
```
As a result, we redefine \[1\] many of them in the [parameterized-utils](https://hackage.haskell.org/package/parameterized-utils-1.0.1/docs/Data-Parameterized-Classes.html) library. It would be quite easy to make more polymorphic (have kind "(k -\> \*) -\> Constraint"). If everyone thinks this is a good idea, I'm happy to submit a pull request.
\[1\]: To be precise, there are actually a few axes along which the classes in parameterized-utils vary from those in base. Some, like OrdF, require more type-level evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.6.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Feature request: Polymorphic kinds in Data.Functor.Classes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["polykinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The classes in Data.Functor.Classes have a somewhat restrictive kind signature:\r\n{{{\r\n*Data.Functor.Classes> :k Eq1 \r\nEq1 :: (* -> *) -> Constraint \r\n}}}\r\n\r\nAs a result, we redefine [1] many of them in the [https://hackage.haskell.org/package/parameterized-utils-1.0.1/docs/Data-Parameterized-Classes.html parameterized-utils] library. It would be quite easy to make more polymorphic (have kind \"(k -> *) -> Constraint\"). If everyone thinks this is a good idea, I'm happy to submit a pull request. \r\n\r\n[1]: To be precise, there are actually a few axes along which the classes in parameterized-utils vary from those in base. Some, like OrdF, require more type-level evidence. Others, like EqF, don't require their type parameter to have the corresponding instance. There are a lot of points in the design space here. ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15120Default methods don't pass implicit kind parameters properly2019-07-07T18: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 -> ...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 `-fprint-explicit-kinds`):
```
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 `-fprint-explicit-kinds`):\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/14554Core Lint error mixing2019-07-07T18: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 r...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 `-dcore-lint` 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 -ignore-dot-ghci -dcore-lint ~/hs/123-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/123-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
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 `-dcore-lint` 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 -ignore-dot-ghci -dcore-lint ~/hs/123-bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/123-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\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/13992Error message, room for improvement (polykinds)2019-07-07T18:18:57ZIcelandjackError message, room for improvement (polykinds)Something like
```hs
-- • No instance for (Show (Compose Proxy Proxy a))
-- arising from the 'deriving' clause of a data type declaration
-- Possible fix:
-- use a standalone 'deriving instance' declaration,
-- ...Something like
```hs
-- • No instance for (Show (Compose Proxy Proxy a))
-- arising from the 'deriving' clause of a data type declaration
-- Possible fix:
-- use a standalone 'deriving instance' declaration,
-- so you can specify the instance context yourself
-- • When deriving the instance for (Show (FlipProxy a))
{-# Language DerivingStrategies, GeneralizedNewtypeDeriving, PolyKinds, KindSignatures #-}
import Data.Functor.Compose
import Data.Proxy
import Data.Kind
newtype FlipProxy a = FlipProxy_ (Compose Proxy Proxy a)
deriving newtype
Show
```
where the solution is to constrain the kind of `a` to `Type`, it would be nice if GHC could reference kind variables.https://gitlab.haskell.org/ghc/ghc/-/issues/13814Unable to resolve instance for polykinded superclass constraint on associated...2019-07-07T18:19:59ZisovectorUnable to resolve instance for polykinded superclass constraint on associated-type-family.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 FrontB...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 instance2019-07-07T18: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 #-}
modu...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_64-apple-darwin):
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_64-apple-darwin):\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/8913either bug or confusing error message mixing PolyKinds and TypeFamilies2019-07-07T18: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 stand-alone example:
```
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
module ...I found this when using GHC.Generics, but it has to do with TypeFamilies so here is a stand-alone 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:8-48
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.1-rc2 |
| 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.1-rc2","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 stand-alone 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:8-48\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/8031Template Haskell gets confused with kind variables introduced in separate for...2019-07-07T18: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 :: [...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 top-level `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 top-level 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 top-level `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 top-level 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 family2019-07-07T18: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: `...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":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7404Inconsistent treatment of overlap between type and kind variables in type fam...2019-07-07T18:49:53ZRichard Eisenbergrae@richarde.devInconsistent treatment of overlap between type and kind variables in type familiesThe following code compiles on 7.7.20121031:
```
type family Foo (x :: *) (y :: x)
type instance Foo Bool Int = Int
```
After some poking around, I discovered that GHC is treating the type variable `x` and the kind variable `x` as dist...The following code compiles on 7.7.20121031:
```
type family Foo (x :: *) (y :: x)
type instance Foo Bool Int = Int
```
After some poking around, I discovered that GHC is treating the type variable `x` and the kind variable `x` as distinct. In core, Foo has three arguments.
The following code does not compile:
```
type family Bar (x :: *) :: x
```
The error is
```
Type variable `x' used in a kind
In the kind `x'
```
I can see arguments in favor of either of the above treatments (separate namespaces for type and kind variables vs. unified namespace), but the current implementation seems inconsistent to me.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| 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":"Inconsistent treatment of overlap between type and kind variables in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles on 7.7.20121031:\r\n\r\n{{{\r\ntype family Foo (x :: *) (y :: x)\r\ntype instance Foo Bool Int = Int\r\n}}}\r\n\r\nAfter some poking around, I discovered that GHC is treating the type variable {{{x}}} and the kind variable {{{x}}} as distinct. In core, Foo has three arguments.\r\n\r\nThe following code does not compile:\r\n\r\n{{{\r\ntype family Bar (x :: *) :: x\r\n}}}\r\n\r\nThe error is\r\n\r\n{{{\r\n Type variable `x' used in a kind\r\n In the kind `x'\r\n}}}\r\n\r\nI can see arguments in favor of either of the above treatments (separate namespaces for type and kind variables vs. unified namespace), but the current implementation seems inconsistent to me.","type_of_failure":"OtherFailure","blocking":[]} -->