GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-07-20T19:25:05Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23543Promoted empty list fails to kind-check with arity 02023-07-20T19:25:05ZRyan ScottPromoted empty list fails to kind-check with arity 0Data constructors that are promoted to the kind level can be partially applied, just like any other type constructor. For instance, this kind-checks:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-...Data constructors that are promoted to the kind level can be partially applied, just like any other type constructor. For instance, this kind-checks:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
type N :: forall a. Maybe a
type N = ('Nothing :: forall a. Maybe a)
```
Note that I've given `'Nothing` an explicit `forall a. Maybe a` kind signature to ensure that `N` has arity 0. That is, `N` does not require any arguments in order to partially apply it.
While most promoted data constructors (e.g., `'Nothing`) can be partially applied this way, there is a strange exception to this rule: the promoted empty list. If you try to write this:
```hs
type L :: forall a. [a]
type L = ('[] :: forall a. [a])
```
Then it will fail to kind-check:
```
$ ghc-9.6.2 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:12:11: error: [GHC-83865]
• Expected kind ‘forall a. [a]’, but ‘'[]’ has kind ‘[k0]’
• In the type ‘('[] :: forall a. [a])’
In the type declaration for ‘L’
|
12 | type L = ('[] :: forall a. [a])
| ^^^
```
I think this should kind-check, as `'[]` is a promoted data constructor just like `'Nothing` is. My suspicion is that GHC is special-casing `'[]` applications somewhere in the typechecker, and the special code path is likely mishandling things in some way.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/22793Type checker crash with some polykinded junk2023-03-04T07:32:24ZDavid FeuerType checker crash with some polykinded junk## Summary
I was doing something kind of impractical with quantified constraints
and such, and crashed the type checker. Fortunately (?) I was able to
reproduce the crash with a greatly stripped down example.
## Steps to reproduce
```...## Summary
I was doing something kind of impractical with quantified constraints
and such, and crashed the type checker. Fortunately (?) I was able to
reproduce the crash with a greatly stripped down example.
## Steps to reproduce
```haskell
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Buggle where
import Data.Kind
type Foo :: forall k. k -> k -> Constraint
class Foo s a
bob :: forall {k1} {ks} {ka} q (p :: k1 -> q -> Type) (f :: ka -> q) (s :: ks) (t :: ks) (a :: ka) (b :: ka). Foo s a => p a (f b) -> p s (f t)
bob f = undefined
```
When I compile this, I see no error messages, but also no compilation products. `-ddump-tc-trace` includes a bunch of call stacks for whatever reason. The first to come up:
```
newNoTcEvBinds unique = axp
attemptM recovering with insoluble constraints
WC {wc_impl =
Implic {
TcLevel = 1
Skolems =
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_impl =
Implic {
TcLevel = 1
Skolems =
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_impl =
Implic {
TcLevel = 2
Skolems = k1_auh[sk:2]
ks_aui[sk:2]
ka_auj[sk:2]
q_auk[sk:2]
(p_aul[sk:2] :: k1_auh[sk:2] -> q_auk[sk:2] -> *)
(f_aum[sk:2] :: ka_auj[sk:2] -> q_auk[sk:2])
(s_aun[sk:2] :: ks_aui[sk:2])
(t_auo[sk:2] :: ks_aui[sk:2])
(a_aup[sk:2] :: ka_auj[sk:2])
(b_auq[sk:2] :: ka_auj[sk:2])
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_simple =
[W] hole{co_avp} {1;{{co_ave}}}:: ks_aui[sk:2]
GHC.Prim.~# k1_auh[sk:2] (CNonCanonical)
[W] hole{co_avt} {1;{{co_avp}}}:: ka_auj[sk:2]
GHC.Prim.~# k1_auh[sk:2] (CNonCanonical)}
Binds = CoEvBindsVar<avn>
an explicit forall {k1_auh} {ks_aui} {ka_auj} q_auk
(p_aul :: k1_auh -> q_auk -> Type)
(f_aum :: ka_auj -> q_auk) (s_aun :: ks_aui)
(t_auo :: ks_aui) (a_aup :: ka_auj)
(b_auq :: ka_auj) }}
Binds = CoEvBindsVar<axn>
the type signature for ‘bob’ }}
Binds = CoEvBindsVar<axp>
UnkSkol (please report this as a bug)
Call stack:
CallStack (from HasCallStack):
unkSkolAnon, called at compiler/GHC/Tc/Solver.hs:231:57 in ghc:GHC.Tc.Solver }}
```
## Expected behavior
I expect compilation to either succeed or produce an error message.
## Environment
* GHC version used: 9.4.4
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/22932Unexpected kind error with type family and phantom datatype2023-02-08T02:29:26ZDaneel S. YaitskovUnexpected kind error with type family and phantom datatype```haskell
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RoleAnnotations #-}
class ToList l where
type Item l
toList :: l -> [Item l]
type role Foo nominal
data Foo a = Foo -- a
instance ToList (Foo a) where
type Item (Foo a) = a
...```haskell
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RoleAnnotations #-}
class ToList l where
type Item l
toList :: l -> [Item l]
type role Foo nominal
data Foo a = Foo -- a
instance ToList (Foo a) where
type Item (Foo a) = a
toList Foo = []
```
Error:
> Expected a type, but ‘a’ has kind ‘k’ ‘k’ is a rigid type variable bound by a family instance declaration
Explicit role specification of the type parameter doesn't affect anything. Once Foo is redefined as follows
```haskell
data Foo a = Foo a
```
The error disappears.
GHC 9.2.4https://gitlab.haskell.org/ghc/ghc/-/issues/19244Backpack + PolyKinds panic2022-05-16T23:59:20ZJoachim Breitnermail@joachim-breitner.deBackpack + PolyKinds panicWhile working on !4853 I could trigger the following panic:
* Add `{-# LANGUAGE PolyKinds #-}` to `./testsuite/tests/backpack/should_compile/bkp40.bkp`
* Run `ghc-8.10 --backpack bkp40.bkp`
With ghc-8.10, one gets:
```
ghc: panic! (th...While working on !4853 I could trigger the following panic:
* Add `{-# LANGUAGE PolyKinds #-}` to `./testsuite/tests/backpack/should_compile/bkp40.bkp`
* Run `ghc-8.10 --backpack bkp40.bkp`
With ghc-8.10, one gets:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.2:
flatten_args wandered into deeper water than usual
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcFlatten.hs:1029:21 in ghc:TcFlatten
```
With HEAD one gets:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210119:
funResultTy
Eq (*)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:1183:49 in ghc:GHC.Core.Type
```
I am not blocked on this, but obviously it’s a bug.ZubinZubinhttps://gitlab.haskell.org/ghc/ghc/-/issues/20527GHC 9.2 rejects certain poly-kinded unlifted newtype instances2022-02-13T02:59:37Zsheafsam.derbyshire@gmail.comGHC 9.2 rejects certain poly-kinded unlifted newtype instancesThe following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUA...The following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedNewtypes #-}
module NewtypeInstance where
import GHC.Exts
type DF :: TYPE r
data family DF
newtype instance DF = MkDF1 Int
newtype instance DF = MkDF2 Int#
newtype instance DF = MkDF3 (# Int#, Int, Word #)
newtype instance DF = MKDF4 (# (# #) | Float# #)
```
```
NewtypeInstance.hs:15:29: error:
* Expecting a lifted type, but `Int#' is unlifted
* In the type `Int#'
In the definition of data constructor `MkDF2'
In the newtype instance declaration for `DF'
|
15 | newtype instance DF = MkDF2 Int#
| ^^^^
NewtypeInstance.hs:16:29: error:
* Expecting a lifted type, but `(# Int#, Int, Word #)' is unlifted
* In the type `(# Int#, Int, Word #)'
In the definition of data constructor `MkDF3'
In the newtype instance declaration for `DF'
|
16 | newtype instance DF = MkDF3 (# Int#, Int, Word #)
| ^^^^^^^^^^^^^^^^^^^^^
NewtypeInstance.hs:17:29: error:
* Expecting a lifted type, but `(# (# #) | Float# #)' is unlifted
* In the type `(# (# #) | Float# #)'
In the definition of data constructor `MKDF4'
In the newtype instance declaration for `DF'
|
17 | newtype instance DF = MKDF4 (# (# #) | Float# #)
| ^^^^^^^^^^^^^^^^^^^^
```
I think the program should be accepted: we have an invisible kind argument which is taking a different value in each newtype instance. For some reason, starting with GHC 9.2, some defaulting seems to take place and we start expecting `r` to be `LiftedRep`.
I'm not sure what has caused the change in behaviour. Pinging the experts @rae and @RyanGlScott.9.2.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21040Curious kind-checking failure with GHC 9.2.1 and visible dependent quantifica...2022-02-04T14:33:59ZRyan ScottCurious kind-checking failure with GHC 9.2.1 and visible dependent quantificationWhile porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTyp...While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
```
```hs
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
```
The `A` module defines two data types, `T1` and `T2`, as well as some functions which use them. The only difference between `T1` and `T2` is that the latter uses visible dependent quantification while the former does not. The `B` module uses these functions in a relatively straightforward way. Note that `B` does _not_ enable `PolyKinds` (I distilled this from a `cabal` project which uses `Haskell2010`).
What's curious about this is that while both `g1` and `g2` will typecheck on GHC 9.0.2, only `g1` typechecks on GHC 9.2.1. On the other hand, `g2` will fail to typecheck in GHC 9.2.1:
```
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
```
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of `NoPolyKinds` might be throwing a wrench into things. Indeed, enabling `PolyKinds` is enough to make the program accepted again. Still, the fact that this _only_ fails if the data type uses visible dependent quantification (and _only_ with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.https://gitlab.haskell.org/ghc/ghc/-/issues/20675[regression] ghc 9.2.1 complains about "Uninferrable type variables" that ghc...2021-11-15T23:58:25ZJasonGross[regression] ghc 9.2.1 complains about "Uninferrable type variables" that ghc 9.0.1 can infer fine## Summary
Write a brief description of the issue.
## Steps to reproduce
Create a file `foo.hs` with the code
```haskell
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Main where
i...## Summary
Write a brief description of the issue.
## Steps to reproduce
Create a file `foo.hs` with the code
```haskell
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Main where
import qualified Prelude
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif
data Type base_type =
Base base_type
| Arrow (Type base_type) (Type base_type)
type Interp base_type base_interp = Any
data Type0 base_type =
Type_base base_type
| Prod (Type0 base_type) (Type0 base_type)
| List (Type0 base_type)
| Option (Type0 base_type)
| Unit
type Interp0 base base_interp = Any
type ExprInfoT =
(Type (Type0 Any)) -> Any -> Interp (Type0 Any) (Interp0 Any Any)
-- singleton inductive, whose constructor was Build_ExprInfoT
type Base0 = Any
type Ident = Any
type Base_interp = Any
ident_interp :: ExprInfoT -> (Type (Type0 Base0)) -> Ident -> Interp (Type0 Base0) (Interp0 Base0 Base_interp)
ident_interp exprInfoT =
exprInfoT
seq :: a1 -> a2 -> a2
seq _ y =
y
main :: GHC.Base.IO ()
main =
seq ident_interp (GHC.Base.return ())
```
Run `ghc foo.hs -o foo` with ghc 9.0.1 (executed on GH Actions [here](https://github.com/JasonGross/test-haskell-bug/runs/4194435425?check_suite_focus=true)) and note that it completes fine. Run the same command with ghc 9.2.1 (executed on GH Actions [here](https://github.com/JasonGross/test-haskell-bug/runs/4194435468?check_suite_focus=true) and note that it errors with
```
foo.hs:37:1: error:
Error: • Uninferrable type variables k0, k1, k2 in
the type synonym right-hand side:
Type (Type0 (Any @{*}))
-> Any @{*}
-> Interp
@{*}
@{*}
@{k0}
(Type0 (Any @{*}))
(Interp0 @{k0} @{k1} @{k2} (Any @{k1}) (Any @{k2}))
• In the type declaration for ‘ExprInfoT’
|
37 | type ExprInfoT =
| ^^^^^^^^^^^^^^^^...
```
## Expected behavior
I expect code that compiles fine in 9.0.1 to continue compiling fine in 9.2.1. If this is not supposed to work, then Coq needs to be updated so that it can extract code compatible with Haskell 9.2.1 (see [coq/coq#15180](https://github.com/coq/coq/issues/15180))
## Environment
* GHC version used: 9.2.1 (failing), 9.0.1 (succeeding)
Optional:
* Operating System: Linux
* System Architecture: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/19548Kind generalisation without -XPolyKinds leading to breakage2021-03-17T08:07:24ZSebastian GrafKind generalisation without -XPolyKinds leading to breakageThe following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal...The following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal.sh) today:
```hs
{-# LANGUAGE DeriveDataTypeable #-}
module Path where
import Data.Typeable
class Typeable a => C a where
data T a = T deriving Typeable
instance Typeable a => C (T a)
```
If compiled with HEAD (and `-fprint-explicit-kinds`, this errors
```
Path.hs:9:10: error:
• Could not deduce (Typeable @(*) k)
arising from the superclasses of an instance declaration
from the context: Typeable @k a
bound by the instance declaration at Path.hs:9:10-30
• In the instance declaration for ‘C @{*} (T @{k} a)’
|
9 | instance Typeable a => C (T a)
| ^^^^^^^^^^^^^^^^^^^^^
```
Apparently, `T`'s type parameter has been kind generalised. Why? I don't think `-XDeriveDataTypeable` implies `-XPolyKinds`.
Yet the error message mentions an implicit kind `k` that appears nowhere else in the program.https://gitlab.haskell.org/ghc/ghc/-/issues/18855GHC 9.0+ regression in checking program with higher-rank kinds2020-12-15T21:46:27ZRyan ScottGHC 9.0+ regression in checking program with higher-rank kindsGHC 8.10.2 typechecks the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{...GHC 8.10.2 typechecks the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type Nat :: Type
data Nat = Z | S Nat
type Vec :: Type -> Nat -> Type
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Z
VCons :: a -> Vec a n -> Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
-> forall (n :: Nat).
forall (v :: Vec a n)
-> Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1-alpha1 and HEAD reject it:
```
$ ~/Software/ghc-9.0.1-alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)-(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
40 | Apply p xs ~> Apply p (VCons x xs))
| ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v’
at Bug.hs:(35,17)-(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
41 | -> Apply p v
| ^
```9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/8707Kind inference fails in data instance definition2020-12-08T21:03:17ZRichard Eisenbergrae@richarde.devKind inference fails in data instance definitionConsider the following shenanigans:
```
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs #-}
data family SingDF (a :: (k, k2 -> *))
data Ctor :: k -> *
data instance SingDF (a :: (Bool, Bool -> *)) where
SFalse :: SingDF '(Fal...Consider the following shenanigans:
```
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs #-}
data family SingDF (a :: (k, k2 -> *))
data Ctor :: k -> *
data instance SingDF (a :: (Bool, Bool -> *)) where
SFalse :: SingDF '(False, Ctor)
```
HEAD reports (with `-fprint-explicit-kinds`)
```
Data constructor ‛SFalse’ returns type ‛SingDF
Bool k '('False, Ctor k)’
instead of an instance of its parent type ‛SingDF Bool Bool a’
In the definition of data constructor ‛SFalse’
In the data instance declaration for ‛SingDF’
```
I see two problems here:
1) Kind inference should fix the problem. If I add a kind annotation to `Ctor`, the code works. GHC should be able to infer this kind annotation for me.
2) The error message is not particularly helpful. GHC 7.6.3 had a more verbose, but more helpful message.
<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":"Kind inference fails in data instance definition","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following shenanigans:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs #-}\r\n\r\ndata family SingDF (a :: (k, k2 -> *))\r\ndata Ctor :: k -> *\r\n\r\ndata instance SingDF (a :: (Bool, Bool -> *)) where\r\n SFalse :: SingDF '(False, Ctor)\r\n}}}\r\n\r\nHEAD reports (with `-fprint-explicit-kinds`)\r\n\r\n{{{\r\n Data constructor ‛SFalse’ returns type ‛SingDF\r\n Bool k '('False, Ctor k)’\r\n instead of an instance of its parent type ‛SingDF Bool Bool a’\r\n In the definition of data constructor ‛SFalse’\r\n In the data instance declaration for ‛SingDF’\r\n}}}\r\n\r\nI see two problems here:\r\n\r\n1) Kind inference should fix the problem. If I add a kind annotation to `Ctor`, the code works. GHC should be able to infer this kind annotation for me.\r\n\r\n2) The error message is not particularly helpful. GHC 7.6.3 had a more verbose, but more helpful message.","type_of_failure":"OtherFailure","blocking":[]} -->9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/14111strange error when using data families with levity polymorphism and unboxed s...2020-12-08T21:03:17ZCarter Schonwaldstrange error when using data families with levity polymorphism and unboxed sums and data familiesI've the following small example
```
{-# LANGUAGE MagicHash, UnboxedSums, NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
-- {-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{...I've the following small example
```
{-# LANGUAGE MagicHash, UnboxedSums, NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
-- {-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs ,ExplicitNamespaces#-}
{-# LANGUAGE UnboxedTuples #-}
module Data.Unboxed.Maybe where
import GHC.Exts
import GHC.Types
import Prelude (undefined)
import Data.Void
data family Maybe(x :: TYPE (r :: RuntimeRep))
data instance Maybe (a :: * ) where
MaybeSum :: (# a | (# #) #) -> Maybe a
data instance Maybe (x :: TYPE 'UnliftedRep) where
MaybeSumU :: (# x | (# #) #) -> Maybe x
```
and then i get the error (made much saner to read by use of printing explicit kinds)
```
Prelude> :r
[1 of 1] Compiling Data.Unboxed.Maybe ( src/Data/Unboxed/Maybe.hs, interpreted )
src/Data/Unboxed/Maybe.hs:22:3: error:
• Data constructor ‘MaybeSumU’ returns type ‘Maybe 'LiftedRep x’
instead of an instance of its parent type ‘Maybe 'UnliftedRep x’
• In the definition of data constructor ‘MaybeSumU’
In the data instance declaration for ‘Maybe’
|
22 | MaybeSumU :: (# x | (# #) #) -> Maybe x
```
this is
a) a case where printing runtime reps makes things easier to debug :)
b) a very confusing type error since the data instance clearly says "x :: TYPE 'UnliftedRep "
is there something i'm overlooking, or is this a bug?
<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":"strange error when using data families with levity polymorphism and unboxed sums and data families","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":"I've the following small example\r\n\r\n{{{\r\n{-# LANGUAGE MagicHash, UnboxedSums, NoImplicitPrelude #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n-- {-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE GADTs ,ExplicitNamespaces#-}\r\n{-# LANGUAGE UnboxedTuples #-}\r\n\r\nmodule Data.Unboxed.Maybe where\r\n\r\nimport GHC.Exts\r\nimport GHC.Types\r\nimport Prelude (undefined)\r\nimport Data.Void\r\n\r\ndata family Maybe(x :: TYPE (r :: RuntimeRep))\r\n\r\ndata instance Maybe (a :: * ) where\r\n MaybeSum :: (# a | (# #) #) -> Maybe a\r\ndata instance Maybe (x :: TYPE 'UnliftedRep) where\r\n MaybeSumU :: (# x | (# #) #) -> Maybe x\r\n}}}\r\n\r\nand then i get the error (made much saner to read by use of printing explicit kinds)\r\n\r\n{{{\r\nPrelude> :r\r\n[1 of 1] Compiling Data.Unboxed.Maybe ( src/Data/Unboxed/Maybe.hs, interpreted )\r\n\r\nsrc/Data/Unboxed/Maybe.hs:22:3: error:\r\n • Data constructor ‘MaybeSumU’ returns type ‘Maybe 'LiftedRep x’\r\n instead of an instance of its parent type ‘Maybe 'UnliftedRep x’\r\n • In the definition of data constructor ‘MaybeSumU’\r\n In the data instance declaration for ‘Maybe’\r\n |\r\n22 | MaybeSumU :: (# x | (# #) #) -> Maybe x\r\n}}}\r\n\r\nthis is \r\n\r\na) a case where printing runtime reps makes things easier to debug :) \r\n\r\nb) a very confusing type error since the data instance clearly says \"x :: TYPE 'UnliftedRep \"\r\n\r\nis there something i'm overlooking, or is this a bug?","type_of_failure":"OtherFailure","blocking":[]} -->9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18891Kind inference for newtypes in GADT syntax is deeply broken2020-12-08T21:03:16ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In th...Here are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
------------------------
```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N -> N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/17841"No skolem info" panic with PolyKinds2020-10-19T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy...## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)
|
5 | class Foo (t :: k) where foo :: Proxy (a :: t)
|
```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/17566GHC 8.10 regression: Core Lint error when defining instance of CUSK-less class2020-10-19T09:14:39ZRyan ScottGHC 8.10 regression: Core Lint error when defining instance of CUSK-less classHere are two files:
```hs
-- Lib.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Lib where
import Data.Kind
class C (f :: k -> Type) z where
type T...Here are two files:
```hs
-- Lib.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Lib where
import Data.Kind
class C (f :: k -> Type) z where
type T (x :: f a) :: f a
```
```hs
-- App.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module App where
import Data.Kind
import Data.Proxy
import Lib
type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
type T x = F x
```
Compiling this with GHC 8.8.1 passes Core Lint:
```
$ /opt/ghc/8.8.1/bin/ghc -c Lib.hs && /opt/ghc/8.8.1/bin/ghc -c App.hs -dcore-lint
```
But it does _not_ pass Core Lint on GHC 8.10.1-alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc -c Lib.hs && /opt/ghc/8.10.1/bin/ghc -c App.hs -dcore-lint
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
Core Lint error
<no location info>: warning:
The variable @ k1_aiz is out of scope
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
T
[TCvSubst
In scope: InScope {k1_aiz a_awk x_awl}
Type env: [aig :-> x_awl, awg :-> a_awk]
Co env: []]
[a_awk, x_awl]
[]
[k1_aiz, Proxy, a_awk, x_awl]
F x_awl
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst
```
-----
Another curious thing is that if you load `Lib.hs` into GHCi, you'll observe something strange about the kind of `T`:
```
$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 -> *) -> k -> Constraint
class C f z where
type T :: forall k2 (f :: k1 -> *) (a :: k2). f a -> f a
type family T x
-- Defined at Lib.hs:11:3
```
Note that `T` has kind `forall k2 (f :: k1 -> *) (a :: k2). f a -> f a`, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.8.10.2https://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/17710Poly-kinded rewrite rule fails to typecheck (HEAD only)2020-03-15T18:51:16ZRyan ScottPoly-kinded rewrite rule fails to typecheck (HEAD only)I originally noticed this issue since it prevents the `free-algebras-0.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 demonst...I originally noticed this issue since it prevents the `free-algebras-0.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.1-alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 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 ill-scoped 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/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/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 Zavialov