GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200920T08:52:57Zhttps://gitlab.haskell.org/ghc/ghc//issues/18725GHC panic: tcLookupGlobalOnly20200920T08:52:57ZVladislav 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)
```
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.```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/18640Skolem error (panic) with StandaloneKindSignatures20200924T12:15:48ZCsongor KissSkolem error (panic) with StandaloneKindSignaturesThe following program:
```haskell
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE StandaloneKindSignatures #}
module Bug where
import Data.Kind
type F2 :: forall a b. Type > a
type family F2 :: forall b. Type > Type where
```
panics on HEAD:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200901:
No skolem info:
[a_auL]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:185:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2812:17 in ghc:GHC.Tc.Errors
```
It looks like the issue is that `a` doesn't get bound by the implication constraint that's emitted when unifying `forall b. Type > a ~ forall b. Type > Type`.The following program:
```haskell
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE StandaloneKindSignatures #}
module Bug where
import Data.Kind
type F2 :: forall a b. Type > a
type family F2 :: forall b. Type > Type where
```
panics on HEAD:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200901:
No skolem info:
[a_auL]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:185:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2812:17 in ghc:GHC.Tc.Errors
```
It looks like the issue is that `a` doesn't get bound by the implication constraint that's emitted when unifying `forall b. Type > a ~ forall b. Type > Type`.Csongor KissCsongor Kisshttps://gitlab.haskell.org/ghc/ghc//issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant20200626T16:28:20ZBjö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 `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 standalone 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.1## 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 standalone 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/17705Bind kind variables in type synonyms20200425T14:22:20ZLeanderKBind kind variables in type synonymsI wonder if GHC could support the binding of kindvariables in typesynonyms (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 termlevel after proposals like *Binding type variables in lambdaexpressions* are implemented.I wonder if GHC could support the binding of kindvariables in typesynonyms (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 termlevel after proposals like *Binding type variables in lambdaexpressions* are implemented.https://gitlab.haskell.org/ghc/ghc//issues/17537StandaloneKindSignatures/TH panic (updateRole) when reusing unique names20191210T21:34:14ZRyan ScottStandaloneKindSignatures/TH panic (updateRole) when reusing unique namesThe following program panics on GHC 8.10.1alpha1:
```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.The following program panics on GHC 8.10.1alpha1:
```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/17432Wildcards in standalone kind signatures20200112T20:22:51ZRichard 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 polymorphic recursion would not be allowed. It's all just like at the term level.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/17277Inconsistent behaviour of StandaloneKindSignatures with type families which a...20200415T15:28:19ZsheafInconsistent 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 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 fprintexplicitforalls fprintexplicitkinds
> :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.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 fprintexplicitforalls fprintexplicitkinds
> :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/17268Arcane interaction of RuntimeRep with StandaloneKindSignatures20191008T17: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)
```
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 `fprintexplicitruntimereps`:
```
ghci> :set fprintexplicitruntimereps
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?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 `fprintexplicitruntimereps`:
```
ghci> :set fprintexplicitruntimereps
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/16754Can't use multiple names in a standalone kind signature20200107T00: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
{# 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.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 Zavialov