GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-01-07T00:39:23Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16754Can't use multiple names in a standalone kind signature2020-01-07T00:39:23ZRyan ScottCan't use multiple names in a standalone kind signatureYou can put multiple names in a single type signature, like so:
```hs
id1, id2 :: a -> a
id1 = id
id2 = id
```
However, the same does not hold for `StandaloneKindSignatures`. For example, the following program fails to parse:
```hs
{-...You can put multiple names in a single type signature, like so:
```hs
id1, id2 :: a -> a
id1 = id
id2 = id
```
However, the same does not hold for `StandaloneKindSignatures`. For example, the following program fails to parse:
```hs
{-# LANGUAGE StandaloneKindSignatures #-}
module Bug where
import Data.Kind
type T1, T2 :: Type -> Type
type T1 = Maybe
type T2 = Maybe
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:8: error: parse error on input ‘,’
|
6 | type T1, T2 :: Type -> Type
| ^
```
This seems like it would be nice to have for consistency's sake.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/17268Arcane interaction of RuntimeRep with StandaloneKindSignatures2019-10-08T17:16:17ZVladislav ZavialovArcane interaction of RuntimeRep with StandaloneKindSignaturesConsider this program:
```
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
data R
type TY :: R -> Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```...Consider this program:
```
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
data R
type TY :: R -> Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
We can discover the inferred kind of `A` in GHCi:
```
ghci> :k A
A :: forall (r :: R). TY r -> Type
```
And then, sure enough, we can copy this signature into the original program:
```
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
data R
type TY :: R -> Type
data TY r
type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
This compiles fine. Now, let's repeat the experiment using `RuntimeRep` instead of a new data type `R`:
```
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R -> Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
To check the kind of `A` in GHCi, let's not forget `-fprint-explicit-runtime-reps`:
```
ghci> :set -fprint-explicit-runtime-reps
ghci> :k A
A :: forall (r :: R). TY r -> Type
```
This time, if we paste this signature into the original program, we get a kind error:
```
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R -> Type
data TY r
type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
```
Test.hs:12:29: error:
• Expected kind ‘TY 'LiftedRep’, but ‘a’ has kind ‘TY r’
• In the first argument of ‘B’, namely ‘a’
In the type ‘(B a)’
In the definition of data constructor ‘MkA’
|
12 | data A (a :: TY r) = MkA (B a)
|
```
How come?https://gitlab.haskell.org/ghc/ghc/-/issues/17277Inconsistent behaviour of StandaloneKindSignatures with type families which a...2020-04-15T15:28:19Zsheafsam.derbyshire@gmail.comInconsistent behaviour of StandaloneKindSignatures with type families which are not given standalone kind signaturesTurning on `StandaloneKindSignatures` stops the following program from typechecking:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE S...Turning on `StandaloneKindSignatures` stops the following program from typechecking:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
data AB = A | B
data SAB (ab :: AB) where
SA :: SAB 'A
SB :: SAB 'B
--type SingAB :: forall (ab :: AB) -> SAB ab
type family SingAB (ab :: AB) :: SAB ab where
SingAB A = 'SA
SingAB B = 'SB
```
```
saks.hs:15:12: error:
* Expected kind `SAB ab', but 'SA has kind `SAB 'A'
* In the type 'SA
In the type family declaration for `SingAB'
|
15 | SingAB A = 'SA
|
```
Uncommenting the standalone kind signature allows the program to typecheck.
When removing the equations for the type family `SingAB`, with or without the standalone kind signature, one has:
```haskell
> :set -fprint-explicit-foralls -fprint-explicit-kinds
> :kind! SingAB
SingAB :: forall (ab :: AB) -> SAB ab
= SingAB
```
So I'm not sure why the equations fail to typecheck without the standalone kind signature.
Similar behaviour also happens for the invisible equivalent:
```haskell
--type SingAB2 :: forall (ab :: AB). SAB ab
type family SingAB2 :: SAB ab where
SingAB2 = ( 'SA :: SAB 'A )
SingAB2 = ( 'SB :: SAB 'B )
```
```
saks.hs:21:15: error:
* Expected kind `SAB ab', but 'SA :: SAB 'A has kind `SAB 'A'
* In the type `('SA :: SAB 'A)'
In the type family declaration for `SingAB2'
|
21 | SingAB2 = ( 'SA :: SAB 'A )
| ^^^
```
Ditto for passing the type explicitly:
```haskell
--type SingAB3 :: forall (ab :: AB). Proxy ab -> SAB ab
type family SingAB3 ( px :: Proxy ab ) :: SAB ab where
SingAB3 ( _ :: Proxy 'A ) = 'SA
SingAB3 ( _ :: Proxy 'B ) = 'SB
```
With `StandaloneKindSignatures` enabled, this causes the following error:
```
saks.hs:28:13: error:
* Expected kind `Proxy @{AB} ab',
but `_ :: Proxy 'A' has kind `Proxy @{AB} 'A'
* In the first argument of `SingAB3', namely `(_ :: Proxy 'A)'
In the type family declaration for `SingAB3'
|
28 | SingAB3 ( _ :: Proxy 'A ) = 'SA
| ^^^^^^^
```
Either turning off `StandaloneKindSignatures`, or uncommenting the standalone kind signature, allows the program to typecheck.8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/17432Wildcards in standalone kind signatures2023-07-14T19:19:52ZRichard Eisenbergrae@richarde.devWildcards in standalone kind signaturesWe should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polym...We should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.https://gitlab.haskell.org/ghc/ghc/-/issues/17537StandaloneKindSignatures/TH panic (updateRole) when reusing unique names2023-07-21T12:25:14ZRyan ScottStandaloneKindSignatures/TH panic (updateRole) when reusing unique namesThe following program panics on GHC 8.10.1-alpha1:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #...The following program panics on GHC 8.10.1-alpha1:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Language.Haskell.TH hiding (Type)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type SameKind (a :: k) (b :: k) = (() :: Constraint)
$(do let pc = mkName "PC"
m1 = mkName "M1"
m2 = mkName "M2"
m1Sym0 = mkName "M1Sym0"
m2Sym0 = mkName "M2Sym0"
m2Sym1 = mkName "M2Sym1"
m1Sym0KI = mkName "M1Sym0KindInference"
m2Sym0KI = mkName "M2Sym0KindInference"
m2Sym1KI = mkName "M2Sym1KindInference"
f <- newName "f"
a <- newName "a"
b <- newName "b"
c <- newName "c"
d <- newName "d"
-- d <- pure $ mkName "d"
e <- newName "e"
-- e <- pure $ mkName "e"
argx <- newName "argx"
argy <- newName "argy"
argz <- newName "argz"
extra1 <- newName "extra1"
extra2 <- newName "extra2"
let m1Sym0_sak = ForallT [PlainTV a, PlainTV f] [] $
ConT ''(~>) `AppT` VarT a `AppT` (VarT f `AppT` VarT a)
mk_m2Sym_sak t
= ForallT [PlainTV f, PlainTV a, PlainTV b] [] $
t `AppT` (VarT f `AppT` VarT a) `AppT`
(ConT ''(~>) `AppT` (VarT f `AppT` VarT b)
`AppT` (VarT f `AppT` VarT a))
m2Sym0_sak = mk_m2Sym_sak (ConT ''(~>))
m2Sym1_sak = mk_m2Sym_sak ArrowT
m1Sym0_sak_dec = KiSigD m1Sym0 m1Sym0_sak
m2Sym0_sak_dec = KiSigD m2Sym0 m2Sym0_sak
m2Sym1_sak_dec = KiSigD m2Sym1 m2Sym1_sak
mk_same_kind t1 t2 = ConT ''SameKind `AppT` t1
`AppT` t2
apply rator rand = ConT ''Apply `AppT` rator `AppT` rand
m1Sym0_body_dec = DataD [] m1Sym0 [PlainTV c] Nothing
[ ForallC [PlainTV c, PlainTV extra1]
[ mk_same_kind (apply (ConT m1Sym0) (VarT extra1))
(ConT m1 `AppT` VarT extra1)
]
(GadtC [m1Sym0KI] [] (ConT m1Sym0 `AppT` VarT c))
] []
m2Sym0_body_dec = DataD [] m2Sym0 [PlainTV d] Nothing
[ ForallC [PlainTV d, PlainTV extra2]
[ mk_same_kind (apply (ConT m2Sym0) (VarT extra2))
(ConT m2Sym1 `AppT` VarT extra2)
]
(GadtC [m2Sym0KI] [] (ConT m2Sym0 `AppT` VarT d))
] []
m2Sym1_body_dec = DataD [] m2Sym1 [PlainTV d, PlainTV e] Nothing
[ ForallC [PlainTV d, PlainTV e, PlainTV extra2]
[ mk_same_kind (apply (ConT m2Sym1 `AppT` VarT d)
(VarT extra2))
(ConT m2 `AppT` VarT d
`AppT` VarT extra2)
]
(GadtC [m2Sym1KI] [] (ConT m2Sym1 `AppT` VarT d
`AppT` VarT e))
] []
pc_dec = ClassD [] pc [PlainTV f] []
[ OpenTypeFamilyD $
TypeFamilyHead m1 [ KindedTV argx (VarT a)
]
(KindSig (VarT f `AppT` VarT a)) Nothing
, OpenTypeFamilyD $
TypeFamilyHead m2 [ KindedTV argy (VarT f `AppT` VarT a)
, KindedTV argz (VarT f `AppT` VarT b)
]
(KindSig (VarT f `AppT` VarT a)) Nothing
]
pure [ m1Sym0_sak_dec
, m1Sym0_body_dec
, m2Sym0_sak_dec
, m2Sym0_body_dec
, m2Sym1_sak_dec
, m2Sym1_body_dec
, pc_dec
])
```
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
updateRole
M2Sym1
a_a32O
[a31l :-> 1, a31m :-> 2, a31n :-> 3, a31p :-> 4, a31q :-> 5,
a32k :-> 0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcTyDecls.hs:664:23 in ghc:TcTyDecls
```
Notes:
* The use of `m2Sym1_sak_dec` (i.e., `type M2Sym1 :: forall f_a35o a_a35p b_a35q. f_a35o a_a35p -> (~>) (f_a35o b_a35q) (f_a35o a_a35p)`) is essential to triggering the panic, as removing it will make the panic go away.
* If you create `d` and `e` with `pure . mkName` instead of `newName`, then the panic will also go away. This suggests that reusing `NameU`s is to blame.
There is a chance that this is related to #11812, but since this requires ~StandaloneKindSignatures, I figured I would file a new issue just to be safe.https://gitlab.haskell.org/ghc/ghc/-/issues/17705Bind kind variables in type synonyms2021-03-06T23:30:26ZLeanderKBind kind variables in type synonymsI wonder if GHC could support the binding of kind-variables in type-synonyms (I am using standalone kind signatures):
```
type F :: forall a (b :: a -> Type). a -> Type
type F @_ @f x = f x
```
or even (still new to VDQ):
```
type F ::...I wonder if GHC could support the binding of kind-variables in type-synonyms (I am using standalone kind signatures):
```
type F :: forall a (b :: a -> Type). a -> Type
type F @_ @f x = f x
```
or even (still new to VDQ):
```
type F :: forall a. forall (b :: a -> Type) -> a -> Type
type F @_ f x = f x
```
This would mirror the term-level after proposals like *Binding type variables in lambda-expressions* are implemented.https://gitlab.haskell.org/ghc/ghc/-/issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant2021-03-31T15:14:45ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the...## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding stand-alone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE CUSKs #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
but this doesn't:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE CUSKs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/18725GHC panic: tcLookupGlobalOnly2020-09-30T20:59:32ZVladislav ZavialovGHC panic: tcLookupGlobalOnly```haskell
{-# LANGUAGE ExplicitForAll, KindSignatures, StandaloneKindSignatures,
DataKinds, GADTs #-}
module T18725 where
import Data.Kind (Type)
type U :: Type
data U where P :: forall u. E u -> U
data E (u :: U)
```
T...```haskell
{-# LANGUAGE ExplicitForAll, KindSignatures, StandaloneKindSignatures,
DataKinds, GADTs #-}
module T18725 where
import Data.Kind (Type)
type U :: Type
data U where P :: forall u. E u -> U
data E (u :: U)
```
This program results in a panic with GHC HEAD:
```
GHCi, version 9.1.0.20200918: https://www.haskell.org/ghc/ :? for help
Prelude> :load T18725.hs
[1 of 1] Compiling T18725 ( T18725.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 9.1.0.20200918:
tcLookupGlobalOnly
U
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:185:37 in ghc:GHC.Utils.Pa
nic
pprPanic, called at compiler/GHC/Tc/Utils/Env.hs:256:35 in ghc:GHC.Tc.Utils.En
v
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
However, it gives a reasonable error message with GHC 8.10:
```
GHCi, version 8.10.1: https://www.haskell.org/ghc/ :? for help
Prelude> :load T18725.hs
[1 of 1] Compiling T18725 ( T18725.hs, interpreted )
T18725.hs:10:14: error:
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
|
10 | data E (u :: U)
| ^
Failed, no modules loaded.
```
The regression appears related to `StandaloneKindSignatures`, as removing the `type U :: Type` line makes the issue go away.https://gitlab.haskell.org/ghc/ghc/-/issues/207529.2.1 regression: GHC fails to load program with: Expected kind ‘k’, but ‘a’ ...2023-01-23T08:31:00ZRoland Senn9.2.1 regression: GHC fails to load program with: Expected kind ‘k’, but ‘a’ has kind ‘k -> k’## Summary
GHC 9.2.1 is no longer able to compile the test program of ticket #10617.
## Steps to reproduce
Load the following program (T10617) into GHCi:
````
{-# LANGUAGE GADTs , PolyKinds #-}
data AppTreeT (a::k) where
Con :: Ap...## Summary
GHC 9.2.1 is no longer able to compile the test program of ticket #10617.
## Steps to reproduce
Load the following program (T10617) into GHCi:
````
{-# LANGUAGE GADTs , PolyKinds #-}
data AppTreeT (a::k) where
Con :: AppTreeT a
App :: AppTreeT a -> AppTreeT b -> AppTreeT (a b)
tmt :: AppTreeT (Maybe Bool)
tmt = App (Con :: AppTreeT Maybe) Con
f :: AppTreeT a -> Bool
f (App (c@Con) _) = const True c
f _ = False
````
This gives the following error:
````
roland@goms:~/Projekte/ghctest/T10617$ switchghc 9.2.1
The Glorious Glasgow Haskell Compilation System, version 9.2.1
roland@goms:~/Projekte/ghctest/T10617$ ghci T10617
GHCi, version 9.2.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( T10617.hs, interpreted )
T10617.hs:5:19: error:
• Expected kind ‘k’, but ‘a’ has kind ‘k -> k’
• In the first argument of ‘AppTreeT’, namely ‘a’
In the type ‘AppTreeT a’
In the definition of data constructor ‘App’
|
5 | App :: AppTreeT a -> AppTreeT b -> AppTreeT (a b)
| ^
Failed, no modules loaded.
````
The error is independent of GHCi. When I add a `main` function
and call plain `ghc` then I also see the error message.
## Expected behavior
As @rae explaines [below](https://gitlab.haskell.org/ghc/ghc/-/issues/20752#note_394357) this is due to the introduction of `GHC2021` in GHC 9.2.1.
The error message should contain some hints, what changes the user could try to get a program that compiles.
## Circumvention
In the above program, replace the first 2 lines with
````
{-# LANGUAGE GADTs, StandaloneKindSignatures #-}
type AppTreeT :: forall k. k -> *
data AppTreeT a where
````
## Environment
* GHC version used: 9.2.1, HEAD 9.3.20211125
Optional:
* Debian 10
* System Architecture: x86_64sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20936Decide about naming of variables in TyCons2022-01-17T08:52:38ZSimon Peyton JonesDecide about naming of variables in TyConsConsider
```
type T :: forall (x :: Type). x -> Type -- Standalone kind signature
data T (a :: k) = MkT (a :: k) -- Declaration
```
Now suppose, in GHCi, you say `:kind T`.
* What kind would you expect to see?
* `T :: fora...Consider
```
type T :: forall (x :: Type). x -> Type -- Standalone kind signature
data T (a :: k) = MkT (a :: k) -- Declaration
```
Now suppose, in GHCi, you say `:kind T`.
* What kind would you expect to see?
* `T :: forall x. x -> Type`, taking the name of the kind variable from the kind signature.
* `T :: forall k. k -> Type`, taking the name of the kind variable from the header of the declaration.
* Does it matter anyway?
The names used in the kind signature are fully alpha-renamable. The names used in the header of
the declaration are not so renamable, because they scope over the body of the declaration, in this case
the data constructors. (In a class declaration the type variables in the header scope over the
method signatures and associated types.)
In HEAD we took the names from the kind signature, and used a variety of extra plumbing to
make the declaration variables scope correctly. In !7105 I changed this to use the variable
names from the declaration header, because the ones from the signature are fully alpha-renamable.
If we wanted to revert to the previous behaviour, we could do so by making the `tyConKind` field of a `TyCon` hold
the kind from the signature, perhaps with different naming than the `[TyConBinder]` for the
`TyCon`. (Currently the `tyConKind` field is just a cache for `mkTyConKind tyConBinders tyConResKind`.)
Not difficult, but a bit of extra plumbing.
This ticket is to describe the issue and ask what choice we should make.https://gitlab.haskell.org/ghc/ghc/-/issues/21793PolyKinds: kind information for variables bound in instance heads propagates ...2022-07-04T09:11:09ZMichael Peyton JonesPolyKinds: kind information for variables bound in instance heads propagates surprisingly badly## Summary
Here's a a reduction of a program I was writing.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GA...## Summary
Here's a a reduction of a program I was writing.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Repro where
import Data.Kind
data P = L | R
data T (a :: P) where
A :: T a
B :: T R
type TConstraint = forall a . T a -> Constraint
class (forall a . constr @a A) => ForAllA (constr :: TConstraint)
instance (forall a . constr @a A) => ForAllA constr
```
GHC says:
```
Repro.hs:18:22: error:
• Cannot apply function of kind ‘k0’
to visible kind argument ‘a’
• In the instance declaration for ‘ForAllA constr’
|
18 | instance (forall a . constr @a A) => ForAllA constr
```
i.e. it has inferred that `constr` in the instance declaration should have kind `k`. I already find this suprising: the class declaration states that for this class, `constr` always has the given kind, so I'd have expected that to propagate. Anyway, let's try and fix it.
1. Kind signature on the instance head
```haskell
instance (forall a . constr @a A) => ForAllA (constr :: TConstraint)
```
Same error.
2. Standalone kind signatures
```haskell
type ForAllA :: TConstraint -> Constraint
class (forall a . constr @a A) => ForAllA constr
instance (forall a . constr @a A) => ForAllA constr
```
Same error.
3. Explicit quantification in the instance head
```haskell
instance forall (constr :: MethodConstraint) . (forall a . constr @a A) => ForAllA constr
```
That finally works!
I'm not totally surprised that 2 doesn't work, but I *am* surprised that 1 doesn't work. That's usually how we constrain type variables in the absence of standalone kind signatures (which we can't write for instance declarations).
## Steps to reproduce
The file above should be independently compilable.
## Environment
* GHC version used: 9.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/22104Error message UX around CUSKs and GHC20212023-08-09T18:16:25ZparsonsmattError message UX around CUSKs and GHC2021`GHC2021` does not enable `CUSKs`, like `Haskell2010` did, and so a common pattern of use will have a mysterious error message.
Consider the following module:
```haskell
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module ...`GHC2021` does not enable `CUSKs`, like `Haskell2010` did, and so a common pattern of use will have a mysterious error message.
Consider the following module:
```haskell
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
type family T (a :: k) :: k where
T Char = Int
T a = a
main = pure ()
```
With GHC 9.0, this compiles fine:
```
λ ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.0.1
λ ghc --make Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
```
If you upgrade to GHC 9.2, then this fails:
```
λ ghcup set ghc 9.2.4
[ Info ] GHC 9.2.4 successfully set as default version
λ ghc --make Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
Main.hs:8:5: error:
• Expected kind ‘k’, but ‘Char’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Char’
In the type family declaration for ‘T’
|
8 | T Char = Int
| ^^^^
λ ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.2.4
```
The `cabal` file specifies `default-language: Haskell2010`, and so `cabal build` works, while `ghc --make` does not.
However, suppose a project switches from `Haskell2010` to `GHC2021`. They'll receive those confusing error messages. I was able to diagnose this by diffing the `cabal build --verbose` to get the `ghc` invocation from `cabal`, and noticed the `-XHaskell2010` flag passed in. I checked to see what that implied, and fortunately `CUSKs` was the first extension, which is the culprit.
I've never heard of `CUSKs`, since it's an implied feature in the language for the entire time that I've been using it. So I had no idea that I needed an extension at all to get this behavior.
Since `CUSKs` are on the Path to Deprecation and Removal, it'd be *great* if we could get an informative error message about the situation.
```
λ ghc --make Main.hs
[1 of 2] Compiling Main ( Main.hs, Main.o )
Main.hs:8:5: error:
• Expected kind ‘k’, but ‘Char’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Char’
In the type family declaration for ‘T’
• The language extension `CUSKs` may fix this behavior,
but it will soon been deprecated in favor of `StandaloneKingSignatures`.
|
8 | T Char = Int
| ^^^^
```sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22230Uninferrable type variable in type family2022-09-29T13:06:44ZDenis StoyanovUninferrable type variable in type familyHello everyone. I have this code (I use ghc-9.2.4)
```haskell
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Undecid...Hello everyone. I have this code (I use ghc-9.2.4)
```haskell
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
module Main where
import Data.Proxy
import Data.Kind
import Data.Type.Equality
import qualified GHC.TypeLits as TL
import qualified Data.Type.Bool as TB
type Undefined :: k
type family Undefined where {}
type LoT :: Type -> Type
data LoT k where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
type HeadLoT :: forall k k'. LoT (k -> k') -> k
type family HeadLoT tys where
HeadLoT (a ':&&: _) = a
type TailLoT :: forall k k'. LoT (k -> k') -> LoT k'
type family TailLoT tys where
TailLoT (_ ':&&: as) = as
type (:@@:) :: forall k. k -> LoT k -> Type
type family f :@@: tys where
f :@@: _ = f
f :@@: as = f (HeadLoT as) :@@: TailLoT as
type (~>) :: forall k1 k2. k1 -> k2 -> Type
type (~>) f g = Proxy f -> Proxy g -> Type
type Eval :: forall as f g. (f ~> g) -> f :@@: as -> g :@@: as
type family Eval nat t
-- >>> :k Eval
-- Eval :: forall {k} (as :: LoT k) (f :: k) (g :: k).
-- (f ~> g) -> (f :@@: as) -> g :@@: as
type Exp_ :: forall k. k -> Type
type Exp_ a = () ~> a
type Eval_ :: forall k. Exp_ k -> k
type Eval_ (e :: Exp_ a) = Eval e '()
```
And I got this error
```
• Uninferrable type variable (as0 :: LoT (*)) in
the type synonym right-hand side: Eval @{*} @as0 @() @k e '()
• In the type declaration for 'Eval_'
|
| type Eval_ (e :: Exp_ a) = Eval e '()
```
In ghc-8.10.7 it’s ok, and compile, but Eval has different kind
```haskell
-- >>> :kind Eval
-- Eval :: forall k (as :: LoT k) (f :: k) (g :: k).
-- (f ~> g) -> (f :@@: as) -> g :@@: as
```