GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-20T14:46:22Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23839Replacing `CUSKs` examples with `StandaloneKindSignatures` throughout Kind Po...2023-08-20T14:46:22ZArtin Ghasivandghasivand.artin@gmail.comReplacing `CUSKs` examples with `StandaloneKindSignatures` throughout Kind Polymorphism's documentation## Summary
Location of documentation issue: GHC user's guide, Kind Polymorphism
Even thought `CUSKs` is now considered legacy, it is used throughout the kind polymorphism section a number of times as an example.
This example is from...## Summary
Location of documentation issue: GHC user's guide, Kind Polymorphism
Even thought `CUSKs` is now considered legacy, it is used throughout the kind polymorphism section a number of times as an example.
This example is from [kind inference in closed type families](https://downloads.haskell.org/~ghc/9.6.2/docs/users_guide/exts/poly_kinds.html#kind-inference-in-closed-type-families):
```haskell
type family F1 a where
F1 True = False
F1 False = True
F1 x = x
-- F1 fails to compile: kind-indexing is not inferred
type family F2 (a :: k) where
F2 True = False
F2 False = True
F2 x = x
-- F2 fails to compile: no complete signature
type family F3 (a :: k) :: k where
F3 True = False
F3 False = True
F3 x = x
-- OK
```
## Proposed improvements or changes
I think there are 3 good options:
- Remove them and rewrite them using `StandaloneKindSignatures`
- Add equivalent examples using `StandaloneKindSignatures`, comment the original `CUSKs` examples, and add a little note to them explaining that they are legacy
- Add the examples using `StandaloneKindSignatures`, and add a short comment to the `CUSKs` examples, stating that they are legacyArtin Ghasivandghasivand.artin@gmail.comArtin Ghasivandghasivand.artin@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21126Definition of heterogeneous equality rejected unless using a SAKS2022-04-07T16:01:28Zsheafsam.derbyshire@gmail.comDefinition of heterogeneous equality rejected unless using a SAKSThe following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the da...The following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (a :: k1) :~~: (b :: k2) where
| ^^^^^^^^^^^^^^^^^^^^^^
```
```haskell
data (:~~:) :: k1 -> k2 -> Type where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
Note that this remains true even if one enables `-XCUSKs`, so this doesn't fit the diagnostic of https://gitlab.haskell.org/ghc/ghc/-/issues/20752#note_394357.
The only way to get this accepted is to write a standalone kind signature:
```haskell
type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
HRefl :: a :~~: a
```
It seems to me that the "different names for the same type variable" check is overly-eager for GADTs. In particular, the following is also rejected:
```haskell
data (:~~:) :: k1 -> k2 -> Type where
NotHRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: b
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
I don't know how GHC concludes that `k1` and `k2` must refer to the same kind variable there.9.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/16609Only skip decls with CUSKs in kcLTyClDecl with PolyKinds on2020-11-02T14:31:51ZNingning XieOnly skip decls with CUSKs in kcLTyClDecl with PolyKinds on# Summary
Data type kind checking skips decls with CUSKs in `kcLTyClDecl` (see note [Skip decls with CUSKs in kcLTyClDecl] in `TcTyClsDecls`).
However, when we have no PolyKinds, we shouldn't skip the check, because we have defaulting....# Summary
Data type kind checking skips decls with CUSKs in `kcLTyClDecl` (see note [Skip decls with CUSKs in kcLTyClDecl] in `TcTyClsDecls`).
However, when we have no PolyKinds, we shouldn't skip the check, because we have defaulting. Skipping won't bring us more polymorphism when we have defaulting.
WITHOUT any language extension, the following program is rejected nowadays.
```
data T1 a = MkT1 T2
data T2 = MkT2 (T1 Maybe)
```
What happened: `T1` and `T2` are in the same recursive group. Since `T2` has a CUSK (which is `Type`), `(T1 Maybe)` is skipped when kind-checking. So the kind of `a` remains unsolved and is thus defaulted to `Type`. Then `(T1 Maybe)` fails to type-check because of a kind mismatch between `Type` and `Type -> Type`.
The program type-checks in GHC 8.4 but fails to type-check since GHC 8.6.
Propose: when we have NoPolyKinds, we don't skip the check; when we have PolyKinds, we skip the check.
# Steps to reproduce
Type-check the example program.
# Expected behavior
The program should type-check.
# Environment
* GHC version used: since 8.68.10.1https://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/11498GHC requires kind-polymorphic signatures on class head2019-07-07T18:30:10ZEric CrockettGHC requires kind-polymorphic signatures on class headI have the following compiling example:
```
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes,
ScopedTypeVariables, TypeFamilies, TypeOp...I have the following compiling example:
```
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes,
ScopedTypeVariables, TypeFamilies, TypeOperators #-}
import Data.Proxy
import GHC.Prim
type family CtxOf d (args :: k) :: Constraint
class Run ctx (params :: [k]) where
runAll :: Proxy params
-> Proxy ctx
-> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)
-> [Bool]
data BasicCtxD
type instance CtxOf BasicCtxD '(a,b) = (a ~ b)
instance (Run BasicCtxD params, a ~ b)
=> Run BasicCtxD ( '(a,b) ': params) where
runAll _ pctx f = (f (Proxy::Proxy '(a,b))) :
(runAll (Proxy::Proxy params) pctx f)
```
But if I move the kind signature of `params` to its occurrence in the signature of `runAll`:
```
class Run ctx params where
runAll :: Proxy (params :: [k])
-> Proxy ctx
-> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)
-> [Bool]
```
I get a couple of nasty (and confusing) compile errors.
```
Main.hs:20:25:
Couldn't match kind ‘k1’ with ‘(,) k k’
‘k1’ is a rigid type variable bound by
the type signature for
runAll :: Proxy ('(a, b) : params)
-> Proxy BasicCtxD
-> (forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool)
-> [Bool]
at Main.hs:20:3
Expected type: Proxy args0
Actual type: Proxy '(a, b)
Relevant bindings include
f :: forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool
(bound at Main.hs:20:17)
runAll :: Proxy ('(a, b) : params)
-> Proxy BasicCtxD
-> (forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool)
-> [Bool]
(bound at Main.hs:20:3)
In the first argument of ‘f’, namely ‘(Proxy :: Proxy '(a, b))’
In the first argument of ‘(:)’, namely
‘(f (Proxy :: Proxy '(a, b)))’
In the expression:
(f (Proxy :: Proxy '(a, b)))
: (runAll (Proxy :: Proxy params) pctx f)
Main.hs:21:42:
Could not deduce (k1 ~ (,) k k)
from the context (CtxOf BasicCtxD args)
bound by a type expected by the context:
CtxOf BasicCtxD args => Proxy args -> Bool
at Main.hs:21:8-42
‘k1’ is a rigid type variable bound by
the type signature for
runAll :: Proxy ('(a, b) : params)
-> Proxy BasicCtxD
-> (forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool)
-> [Bool]
at Main.hs:20:3
Expected type: Proxy args -> Bool
Actual type: Proxy args1 -> Bool
Relevant bindings include
f :: forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool
(bound at Main.hs:20:17)
runAll :: Proxy ('(a, b) : params)
-> Proxy BasicCtxD
-> (forall (args :: k1).
CtxOf BasicCtxD args =>
Proxy args -> Bool)
-> [Bool]
(bound at Main.hs:20:3)
In the third argument of ‘runAll’, namely ‘f’
In the second argument of ‘(:)’, namely
‘(runAll (Proxy :: Proxy params) pctx f)’
```
It seems to me that the two definitions of the class are equivalent, so it would be nice if they both compiled. It wasn't obvious to me that the kind signature had to go on the class parameter rather than somewhere else.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.2-rc2 |
| 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":"GHC requires kind-polymorphic signatures on class head","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I have the following compiling example:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures, \r\n MultiParamTypeClasses, PolyKinds, RankNTypes, \r\n ScopedTypeVariables, TypeFamilies, TypeOperators #-}\r\n\r\nimport Data.Proxy\r\nimport GHC.Prim\r\n\r\ntype family CtxOf d (args :: k) :: Constraint\r\n\r\nclass Run ctx (params :: [k]) where\r\n runAll :: Proxy params\r\n -> Proxy ctx\r\n -> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)\r\n -> [Bool]\r\n\r\ndata BasicCtxD\r\ntype instance CtxOf BasicCtxD '(a,b) = (a ~ b)\r\ninstance (Run BasicCtxD params, a ~ b) \r\n => Run BasicCtxD ( '(a,b) ': params) where\r\n runAll _ pctx f = (f (Proxy::Proxy '(a,b))) : \r\n (runAll (Proxy::Proxy params) pctx f)\r\n}}}\r\n\r\nBut if I move the kind signature of `params` to its occurrence in the signature of `runAll`:\r\n{{{\r\nclass Run ctx params where\r\n runAll :: Proxy (params :: [k])\r\n -> Proxy ctx\r\n -> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)\r\n -> [Bool]\r\n}}}\r\n\r\nI get a couple of nasty (and confusing) compile errors. \r\n\r\n{{{\r\nMain.hs:20:25:\r\n Couldn't match kind ‘k1’ with ‘(,) k k’\r\n ‘k1’ is a rigid type variable bound by\r\n the type signature for\r\n runAll :: Proxy ('(a, b) : params)\r\n -> Proxy BasicCtxD\r\n -> (forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool)\r\n -> [Bool]\r\n at Main.hs:20:3\r\n Expected type: Proxy args0\r\n Actual type: Proxy '(a, b)\r\n Relevant bindings include\r\n f :: forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool\r\n (bound at Main.hs:20:17)\r\n runAll :: Proxy ('(a, b) : params)\r\n -> Proxy BasicCtxD\r\n -> (forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool)\r\n -> [Bool]\r\n (bound at Main.hs:20:3)\r\n In the first argument of ‘f’, namely ‘(Proxy :: Proxy '(a, b))’\r\n In the first argument of ‘(:)’, namely\r\n ‘(f (Proxy :: Proxy '(a, b)))’\r\n In the expression:\r\n (f (Proxy :: Proxy '(a, b)))\r\n : (runAll (Proxy :: Proxy params) pctx f)\r\n\r\nMain.hs:21:42:\r\n Could not deduce (k1 ~ (,) k k)\r\n from the context (CtxOf BasicCtxD args)\r\n bound by a type expected by the context:\r\n CtxOf BasicCtxD args => Proxy args -> Bool\r\n at Main.hs:21:8-42\r\n ‘k1’ is a rigid type variable bound by\r\n the type signature for\r\n runAll :: Proxy ('(a, b) : params)\r\n -> Proxy BasicCtxD\r\n -> (forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool)\r\n -> [Bool]\r\n at Main.hs:20:3\r\n Expected type: Proxy args -> Bool\r\n Actual type: Proxy args1 -> Bool\r\n Relevant bindings include\r\n f :: forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool\r\n (bound at Main.hs:20:17)\r\n runAll :: Proxy ('(a, b) : params)\r\n -> Proxy BasicCtxD\r\n -> (forall (args :: k1).\r\n CtxOf BasicCtxD args =>\r\n Proxy args -> Bool)\r\n -> [Bool]\r\n (bound at Main.hs:20:3)\r\n In the third argument of ‘runAll’, namely ‘f’\r\n In the second argument of ‘(:)’, namely\r\n ‘(runAll (Proxy :: Proxy params) pctx f)’\r\n}}}\r\nIt seems to me that the two definitions of the class are equivalent, so it would be nice if they both compiled. It wasn't obvious to me that the kind signature had to go on the class parameter rather than somewhere else.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13109CUSK improvements2019-07-07T18:23:36ZSimon Peyton JonesCUSK improvementsInspired by looking at `RnTypes.bindLHsTyVarBndr`, and driven by #11592, Richard and I decided to make some improvements to the treatment of CUSKs.
Here's a scrappy Skype dump as a memory-jogger; it is a memory-jogger, not a full descri...Inspired by looking at `RnTypes.bindLHsTyVarBndr`, and driven by #11592, Richard and I decided to make some improvements to the treatment of CUSKs.
Here's a scrappy Skype dump as a memory-jogger; it is a memory-jogger, not a full description.
Richard has notes too
```
Richard Eisenberg: data F (x :: B a)
data G (x :: C b)
You have written a complete user-suppled kind signature,
but the following variable is undetermined: a0 :: A
Perhaps add a kind signature.
Inferred kinds of user-written variables:
b :: B a0
x :: C b
SPJ claim: CUSKs should be handled INDIVIDUALLY and in isoloation, just like term-level type signatures
SPJ claim: get rid of the "after the ::" side condition for data types (last bullet of HsDecls Note about CUSKs
All of this should mean (SPJ claims) no need for dep_vars returns by bindHsQTyVar, bindLHsTyVarBnrds etc
ToDo: clarify comments etc in bindLHStyVarBndr
Related to D2914
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"CUSK improvements","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Inspired by looking at `RnTypes.bindLHsTyVarBndr`, and driven by #11592, Richard and I decided to make some improvements to the treatment of CUSKs.\r\n\r\nHere's a scrappy Skype dump as a memory-jogger; it is a memory-jogger, not a full description.\r\nRichard has notes too\r\n{{{\r\nRichard Eisenberg: data F (x :: B a)\r\n data G (x :: C b)\r\n You have written a complete user-suppled kind signature,\r\n but the following variable is undetermined: a0 :: A\r\n Perhaps add a kind signature.\r\n Inferred kinds of user-written variables:\r\n b :: B a0\r\n x :: C b\r\n\r\nSPJ claim: CUSKs should be handled INDIVIDUALLY and in isoloation, just like term-level type signatures\r\nSPJ claim: get rid of the \"after the ::\" side condition for data types (last bullet of HsDecls Note about CUSKs\r\nAll of this should mean (SPJ claims) no need for dep_vars returns by bindHsQTyVar, bindLHsTyVarBnrds etc\r\nToDo: clarify comments etc in bindLHStyVarBndr\r\n\r\nRelated to D2914\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13777Poor error message around CUSKs2019-07-07T18:20:07ZRichard Eisenbergrae@richarde.devPoor error message around CUSKsWhile typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :...While typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :: S (P :: Proxy Maybe)
```
produces
```
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
```
That promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| 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":"Poor error message around CUSKs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["CUSKs","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While typing up comment:7:ticket:13761, I came across a poor error message around CUSKs.\r\n\r\n{{{\r\ndata Proxy (a :: k) = P\r\ndata S :: forall k. Proxy k -> Type where\r\n MkS :: S (P :: Proxy Maybe)\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n You have written a *complete user-suppled kind signature*,\r\n but the following variable is undetermined: k0 :: *\r\n Perhaps add a kind signature.\r\n Inferred kinds of user-written variables:\r\n}}}\r\n\r\nThat promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14139Kind signature not accepted (singletons)2019-07-07T18:18:17ZIcelandjackKind signature not accepted (singletons)I don't understand the rules for kind signatures / CUSKs but this works
```hs
import Data.Singletons.Prelude
data Some (f :: u ~> v) where
Some :: Sing (x :: u) -> f @@ x -> Some f
```
but this doesn't?
```hs
import Data.Kind
impor...I don't understand the rules for kind signatures / CUSKs but this works
```hs
import Data.Singletons.Prelude
data Some (f :: u ~> v) where
Some :: Sing (x :: u) -> f @@ x -> Some f
```
but this doesn't?
```hs
import Data.Kind
import Data.Singletons.Prelude
data Some :: (u ~> v) -> Type where
Some :: Sing (x :: u) -> f @@ x -> Some f
-- • Expected kind ‘u ~> v’, but ‘f’ has kind ‘u ~> *’
-- • In the first argument of ‘Some’, namely ‘f’
-- In the type ‘Some f’
-- In the definition of data constructor ‘Some’
-- |
-- 5 | Some :: Sing (x :: u) -> f @@ x -> Some f
-- | ^
-- Failed, modules loaded: none.
```
I have to quantify over them for it to work `forall u v. (u ~> v) -> Type`, if this is expected I feel like the error message ought to be improved.
<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":"Kind signature","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 don't understand the rules for kind signatures / CUSKs but this works\r\n\r\n{{{#!hs\r\nimport Data.Singletons.Prelude\r\n\r\ndata Some (f :: u ~> v) where\r\n Some :: Sing (x :: u) -> f @@ x -> Some f\r\n}}}\r\n\r\nbut this doesn't?\r\n\r\n{{{#!hs\r\nimport Data.Kind\r\nimport Data.Singletons.Prelude\r\n\r\ndata Some :: (u ~> v) -> Type where\r\n Some :: Sing (x :: u) -> f @@ x -> Some f\r\n\r\n-- • Expected kind ‘u ~> v’, but ‘f’ has kind ‘u ~> *’\r\n-- • In the first argument of ‘Some’, namely ‘f’\r\n-- In the type ‘Some f’\r\n-- In the definition of data constructor ‘Some’\r\n-- |\r\n-- 5 | Some :: Sing (x :: u) -> f @@ x -> Some f\r\n-- | ^\r\n-- Failed, modules loaded: none.\r\n}}}\r\n\r\nI have to quantify over them for it to work `forall u v. (u ~> v) -> Type`, if this is expected I feel like the error message ought to be improved.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14207Levity polymorphic GADT requires extra type signatures2019-07-07T18:17:56ZAndrew MartinLevity polymorphic GADT requires extra type signaturesThis does not compile:
```hs
data Foo s (a :: TYPE k) where
FooC :: Foo s Int#
```
However, this does:
```hs
data Foo (s :: Type) (a :: TYPE k) where
FooC :: Foo s Int#
```
This also works:
```hs
data Foo (s :: j) (a :: TYPE k) ...This does not compile:
```hs
data Foo s (a :: TYPE k) where
FooC :: Foo s Int#
```
However, this does:
```hs
data Foo (s :: Type) (a :: TYPE k) where
FooC :: Foo s Int#
```
This also works:
```hs
data Foo (s :: j) (a :: TYPE k) where
FooC :: Foo s Int#
```
These are all of the language pragmas I have enabled:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
```
This is pretty easy to work around, but I think it's an incorrect behavior.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Levity polymorphic GADT requires extra type signatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This does not compile:\r\n\r\n{{{#!hs\r\ndata Foo s (a :: TYPE k) where\r\n FooC :: Foo s Int#\r\n}}}\r\n\r\nHowever, this does:\r\n\r\n{{{#!hs\r\ndata Foo (s :: Type) (a :: TYPE k) where\r\n FooC :: Foo s Int#\r\n}}}\r\n\r\nThis also works:\r\n\r\n{{{#!hs\r\ndata Foo (s :: j) (a :: TYPE k) where\r\n FooC :: Foo s Int#\r\n}}}\r\n\r\nThese are all of the language pragmas I have enabled:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE BangPatterns #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE UnboxedSums #-}\r\n{-# LANGUAGE UnboxedTuples #-}\r\n{-# LANGUAGE MagicHash #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n}}}\r\n\r\nThis is pretty easy to work around, but I think it's an incorrect behavior.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14451Need proper SCC analysis of type declarations, taking account of CUSKs2019-07-07T18:16:59ZIcelandjackNeed proper SCC analysis of type declarations, taking account of CUSKs```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}
import Data.Kind
data TyFu...```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type Cat ob = ob -> ob -> Type
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply (CompSym2 f g) a = Comp f g a
data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c)
type a·b = Apply a b
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' -> Cod f (f·a) (f·a')
type family
Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where
Comp f g a = f · (Apply g a)
```
This compiles, but if I replace the final line by
```hs
Comp f g a = f · (g · a)
```
oddly enough I get an error message about the method `varpa`! Seemingly unrelated apart from using `(·)`:
```
$ ghci2 hs/093-bug.hs
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/093-bug.hs, interpreted )
hs/093-bug.hs:23:33: error:
• Expected kind ‘i ~> i’, but ‘f’ has kind ‘i ~> j’
• In the first argument of ‘(·)’, namely ‘f’
In the second argument of ‘Cod’, namely ‘(f · a)’
In the type signature:
varpa :: Dom f a a' -> Cod f (f · a) (f · a')
|
23 | varpa :: Dom f a a' -> Cod f (f·a) (f·a')
| ^
Failed, 0 modules loaded.
Prelude>
```
NOW — let's randomly remove both lines that mention `CompSym2` and it mysteriously works, again!
`Apply` and `(·)` seem to be equal up to variable names, I can't spot why
```
>> :set -fprint-explicit-foralls
>> :set -fprint-explicit-kinds
>> :set -fprint-explicit-coercions
>>
>> :kind Apply
Apply :: forall {a} {b}. (a ~> b) -> a -> b
>> :kind (·)
(·) :: forall {a} {k}. (a ~> k) -> a -> k
```
but it works if I define `(·)` as a type family rather than a synonym:
```hs
type family
(f::a ~> b) · (x::a) :: b where
f · x = Apply f x
```
so it's some difference between synonyms and TFs, but is it intentional? It's certainly odd how the error messages jumped the `varpa` method when we actually modified `Comp`.
<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":"Type synonym of type family causes error, error jumps to (fairly) unrelated source location","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":"{{{#!hs\r\n{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type -> Type -> Type\r\n\r\ntype a ~> b = TyFun a b -> Type\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply (CompSym2 f g) a = Comp f g a\r\n\r\ndata CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c) \r\n\r\ntype a·b = Apply a b \r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' -> Cod f (f·a) (f·a')\r\n\r\ntype family \r\n Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where\r\n Comp f g a = f · (Apply g a)\r\n}}}\r\n\r\nThis compiles, but if I replace the final line by\r\n\r\n{{{#!hs\r\n Comp f g a = f · (g · a)\r\n}}}\r\n\r\noddly enough I get an error message about the method `varpa`! Seemingly unrelated apart from using `(·)`:\r\n\r\n{{{\r\n$ ghci2 hs/093-bug.hs\r\nGHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/093-bug.hs, interpreted )\r\n\r\nhs/093-bug.hs:23:33: error:\r\n • Expected kind ‘i ~> i’, but ‘f’ has kind ‘i ~> j’\r\n • In the first argument of ‘(·)’, namely ‘f’\r\n In the second argument of ‘Cod’, namely ‘(f · a)’\r\n In the type signature:\r\n varpa :: Dom f a a' -> Cod f (f · a) (f · a')\r\n |\r\n23 | varpa :: Dom f a a' -> Cod f (f·a) (f·a')\r\n | ^\r\nFailed, 0 modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nNOW — let's randomly remove both lines that mention `CompSym2` and it mysteriously works, again!\r\n\r\n`Apply` and `(·)` seem to be equal up to variable names, I can't spot why \r\n\r\n{{{\r\n>> :set -fprint-explicit-foralls \r\n>> :set -fprint-explicit-kinds \r\n>> :set -fprint-explicit-coercions \r\n>> \r\n>> :kind Apply\r\nApply :: forall {a} {b}. (a ~> b) -> a -> b\r\n>> :kind (·)\r\n(·) :: forall {a} {k}. (a ~> k) -> a -> k\r\n}}}\r\n\r\nbut it works if I define `(·)` as a type family rather than a synonym:\r\n\r\n{{{#!hs\r\ntype family\r\n (f::a ~> b) · (x::a) :: b where\r\n f · x = Apply f x\r\n}}}\r\n\r\nso it's some difference between synonyms and TFs, but is it intentional? It's certainly odd how the error messages jumped the `varpa` method when we actually modified `Comp`.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15142GHC HEAD regression: tcTyVarDetails2019-07-07T18:14:05ZRyan ScottGHC HEAD regression: tcTyVarDetailsThis regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
...This regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
```
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180511 for x86_64-unknown-linux):
tcTyVarDetails
co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression: tcTyVarDetails","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This regression prevents the `generic-lens` library from building. Here is a minimized test case:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass ListTuple (tuple :: Type) (as :: [(k, Type)]) where\r\n type ListToTuple as :: Type\r\n}}}\r\n\r\nOn GHC 8.4.2, this compiles, but on GHC HEAD, it panics:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180511 for x86_64-unknown-linux):\r\n tcTyVarDetails\r\n co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15592Type families without CUSKs cannot be given visible kind variable binders2019-07-07T18:04:00ZRyan ScottType families without CUSKs cannot be given visible kind variable bindersConsider the following program and GHCi session which uses it:
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: Type) (y :: a) :: Type where {}
type family T2 x ...Consider the following program and GHCi session which uses it:
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: Type) (y :: a) :: Type where {}
type family T2 x (y :: a) :: Type where {}
```
```
$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall a. * -> a -> *
λ> :kind T2
T2 :: forall {k} {a}. k -> a -> *
```
Note that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not.
This isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application.
It's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| 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":"Type families without CUSKs cannot be given visible kind variable binders","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["CUSKs","TypeApplications,","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program and GHCi session which uses it:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family T1 (x :: Type) (y :: a) :: Type where {}\r\ntype family T2 x (y :: a) :: Type where {}\r\n}}}\r\n{{{\r\n$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls\r\nGHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :kind T1\r\nT1 :: forall a. * -> a -> *\r\nλ> :kind T2\r\nT2 :: forall {k} {a}. k -> a -> *\r\n}}}\r\n\r\nNote that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not.\r\n\r\nThis isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application.\r\n\r\nIt's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1