GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-03-13T14:10:58Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/9427Do finer-grained dependency analysis to infer more general kinds on type/clas...2020-03-13T14:10:58ZRichard Eisenbergrae@richarde.devDo finer-grained dependency analysis to infer more general kinds on type/class declarationsIn the resolution to #9200, as detailed [here](https://gitlab.haskell.org/ghc/ghc/wikis/ghc-kinds/kind-inference/#a-possible-variation), we identified an area for improvement. This improvement was not implemented in the fix for #9200. Th...In the resolution to #9200, as detailed [here](https://gitlab.haskell.org/ghc/ghc/wikis/ghc-kinds/kind-inference/#a-possible-variation), we identified an area for improvement. This improvement was not implemented in the fix for #9200. This ticket will track just this improvement.
(In brief: we can do better dependency analysis on mutually recursive type/class declarations to allow more kinds to generalize earlier. This would lessen the burden on programmers to put in kind annotations. See the wiki page.)
A solid but unfinished attempt is [here](https://github.com/goldfirere/ghc/tree/re-sort-non-cusk-decls).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.8.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Do finer-grained dependency analysis to infer more general kinds on type/class declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the resolution to #9200, as detailed [wiki:GhcKinds/KindInference#Apossiblevariation here], we identified an area for improvement. This improvement was not implemented in the fix for #9200. This ticket will track just this improvement.\r\n\r\n(In brief: we can do better dependency analysis on mutually recursive type/class declarations to allow more kinds to generalize earlier. This would lessen the burden on programmers to put in kind annotations. See the wiki page.)\r\n\r\nA solid but unfinished attempt is [https://github.com/goldfirere/ghc/tree/re-sort-non-cusk-decls here].","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10141CUSK mysteries2019-07-07T18:37:21ZRichard Eisenbergrae@richarde.devCUSK mysteriesTake the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)Take the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12088Type/data family instances in kind checking2024-02-27T13:56:52ZalexviethType/data family instances in kind checkingSee
* [Artem's blog post](https://serokell.io/blog/dependency-analysis-haskell) about this stuff; it's very helpful.
* [This wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/interleaving-type-instance-checking), written in response ...See
* [Artem's blog post](https://serokell.io/blog/dependency-analysis-haskell) about this stuff; it's very helpful.
* [This wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/interleaving-type-instance-checking), written in response to this ticket
* [This later wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/Type-&-Class-Dependency-Analysis), also written in response to this ticket
In `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note
```hs
data family T a
data instance T Int = MkT
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
-ddump-rn-trace shows these groups
```
rnTycl dependency analysis made groups
[[data family T a_apG]
[]
[data instance T Int = MkT],
[data Proxy (a_apF :: k_apE)]
[]
[],
[data S = MkS (Proxy MkT)]
[]
[]]
```
That's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.
See also (NB: "closed" means "closed because #12088 takes precendence")
* #11348
* #16693
* #16410
* #16448
* #19527
* #19611
* #20875
* #20885
* #21172
* #22257
* #23496
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #11348 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Promote data family instance constructors","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[11348],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note\r\n\r\n{{{#!hs\r\ndata family T a\r\ndata instance T Int = MkT\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\n-ddump-rn-trace shows these groups\r\n\r\n{{{\r\nrnTycl dependency analysis made groups\r\n [[data family T a_apG]\r\n []\r\n [data instance T Int = MkT],\r\n [data Proxy (a_apF :: k_apE)]\r\n []\r\n [],\r\n [data S = MkS (Proxy MkT)]\r\n []\r\n []]\r\n}}}\r\n\r\nThat's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.","type_of_failure":"OtherFailure","blocking":[]} -->Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/13365Notify user when adding a CUSK might help fix a type error2019-07-07T18:22:16ZEric CrockettNotify user when adding a CUSK might help fix a type errorWith `-XPolyKinds`, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling.
```
{-# LANGUAGE PolyKinds, GADTs #-}
import GHC.TypeLits
data Foo
(x :: k)
a
whe...With `-XPolyKinds`, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling.
```
{-# LANGUAGE PolyKinds, GADTs #-}
import GHC.TypeLits
data Foo
(x :: k)
a
where
C1 :: (KnownNat x) => a -> Foo x a
C2 :: a -> Foo Int a
```
```
error:
• Expected kind ‘k’, but ‘x1’ has kind ‘Nat’
• In the first argument of ‘Foo’, namely ‘x’
In the type ‘Foo x a’
In the definition of data constructor ‘C1’
```
From this error, I would never expect that putting a kind signature on `a` would help here. But a signature shouldn't be required at all: it's clear from the GADT constructors that `a :: *`.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/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/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.com