GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-05-21T22:48:30Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13399Location of `forall` matters with higher-rank kind polymorphism2020-05-21T22:48:30ZEric CrockettLocation of `forall` matters with higher-rank kind polymorphismThe following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- erro...The following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- error on this line
```
with the error
```
• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* -> *) -> k -> *`
Decl 3: `data Foo (a :: * -> *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13391PolyKinds is more permissive in GHC 82019-07-07T18:22:06ZEric CrockettPolyKinds is more permissive in GHC 8The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
``...The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
```
{-# LANGUAGE PolyKinds, GADTs #-}
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
The example does \*not\* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"PolyKinds is more permissive in GHC 8","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The docs claim that the definition in section 9.11.10\r\n\r\n{{{\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\n\"requires that `-XTypeInType` be in effect\", but this isn't the case.\r\n\r\nThe following compiles with GHC-8.0.2:\r\n\r\n{{{\r\n\r\n{-# LANGUAGE PolyKinds, GADTs #-}\r\n\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\nThe example does *not* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1). ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13364Remove checkValidTelescope2019-07-07T18:22:16ZRichard Eisenbergrae@richarde.devRemove checkValidTelescopeAll of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b ...All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b :: a) (c :: Proxy d). SameKind b d
forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
forall d. forall a (b :: a). SameKind b d
```
Despite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for *every* new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)
It might all just work! And then we can delete gobs of hairy code. Hooray!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Remove checkValidTelescope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have\r\n\r\n{{{\r\ndata SameKind :: k -> k -> Type\r\n}}}\r\n\r\nand then here are three subtly ill-scoped kinds:\r\n\r\n{{{\r\nforall a (b :: a) (c :: Proxy d). SameKind b d\r\nforall a. forall (b :: a). forall (c :: Proxy d). SameKind b d\r\nforall d. forall a (b :: a). SameKind b d\r\n}}}\r\n\r\nDespite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.\r\n\r\nWhile I am unaware of a concrete bug this all causes, it's a mess.\r\n\r\nBetter would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for ''every'' new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)\r\n\r\nIt might all just work! And then we can delete gobs of hairy code. Hooray!","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13337GHC doesn't think a type is of kind *, despite having evidence for it2019-07-07T18:22:23ZRyan ScottGHC doesn't think a type is of kind *, despite having evidence for itThe easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
b...The easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
blah x = x
```
```
$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a -> a
```
I find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!
If the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing -> "Non-Type kind"
Just Refl ->
case eqT :: Maybe (a :~: Int) of
Nothing -> "Non-Int type"
Just Refl -> "It's an Int!"
```
This exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC doesn't think a type is of kind *, despite having evidence for it","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The easiest way to illustrate this bug is this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\n\r\nblah :: forall (a :: k). k ~ Type => a -> a\r\nblah x = x\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.0.2: 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\n\r\nFoo.hs:8:43: error:\r\n • Expected a type, but ‘a’ has kind ‘k’\r\n • In the type signature:\r\n blah :: forall (a :: k). k ~ Type => a -> a\r\n}}}\r\n\r\nI find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!\r\n\r\nIf the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Typeable\r\n\r\nfoo :: forall k (a :: k) proxy. (Typeable k, Typeable a)\r\n => proxy a -> String\r\nfoo _ =\r\n case eqT :: Maybe (k :~: Type) of\r\n Nothing -> \"Non-Type kind\"\r\n Just Refl ->\r\n case eqT :: Maybe (a :~: Int) of\r\n Nothing -> \"Non-Int type\"\r\n Just Refl -> \"It's an Int!\"\r\n}}}\r\n\r\nThis exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13333Typeable regression in GHC HEAD2019-07-07T18:22:24ZRyan ScottTypeable regression in GHC HEADI recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGU...I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k -> Constraint) (x :: j) where
D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
-> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
```
But on GHC HEAD, it barfs this error:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * -> *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) -> Maybe (c (T phantom))
at Bug.hs:(22,1)-(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D -> gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
|
28 | Just D -> gcast1 f
| ^^^^^^^^
```
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded `Typeable` nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12938Polykinded associated type family rejected on false pretenses2019-07-07T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to...If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<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":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12933Wrong class instance selection with Data.Kind.Type2022-08-04T22:32:56ZjulmWrong class instance selection with Data.Kind.TypeIf you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: S...If you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: SKind Type
SKiCo :: SKind Constraint
instance Show (SKind k) where
show SKiTy = "*"
show SKiCo = "Constraint"
class IKind k where
kind :: SKind k
instance IKind Constraint where
kind = SKiCo
```
Then, the main below will compile even though there is no (IKind Type) instance, and it will print "Constraint" two times,
instead of an expected "Constraint" then "\*":
```hs
main :: IO ()
main = do
print (kind::SKind Constraint)
print (kind::SKind Type)
```
And, the main below will print "\*" two times,
instead of an expected "\*" then "Constraint":
```hs
instance IKind Type where
kind = SKiTy
main :: IO ()
main = do
print (kind::SKind Type)
print (kind::SKind Constraint)
```
This can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.
Sorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Wrong class instance selection with Data.Kind.Type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If you consider the following code:\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Constraint)\r\nimport Data.Kind\r\n\r\n-- | Partial singleton for a kind type.\r\ndata SKind k where\r\n SKiTy :: SKind Type\r\n SKiCo :: SKind Constraint\r\n\r\ninstance Show (SKind k) where\r\n show SKiTy = \"*\"\r\n show SKiCo = \"Constraint\"\r\n\r\nclass IKind k where\r\n kind :: SKind k\r\ninstance IKind Constraint where\r\n kind = SKiCo\r\n}}}\r\n\r\nThen, the main below will compile even though there is no (IKind Type) instance, and it will print \"Constraint\" two times,\r\ninstead of an expected \"Constraint\" then \"*\":\r\n{{{#!hs\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Constraint)\r\n print (kind::SKind Type)\r\n}}}\r\n\r\nAnd, the main below will print \"*\" two times,\r\ninstead of an expected \"*\" then \"Constraint\":\r\n{{{#!hs\r\ninstance IKind Type where\r\n kind = SKiTy\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Type)\r\n print (kind::SKind Constraint)\r\n}}}\r\n\r\nThis can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.\r\n\r\nSorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12931tc_infer_args does not set in-scope set correctly2023-07-16T13:20:59Zjohnleotc_infer_args does not set in-scope set correctlyAs noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnche...As noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnchecked subst (tyVarKind tv)
```
This is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.
Note that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.
<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":"tc_infer_args does not set in-scope set correctly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As noted in https://ghc.haskell.org/trac/ghc/ticket/12785#comment:6, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line\r\n{{{\r\nkind = substTyUnchecked subst (tyVarKind tv)\r\n}}}\r\n\r\nThis is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.\r\n\r\nNote that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12922Kind classes compile with PolyKinds2019-07-07T18:24:37ZMatthías Páll GissurarsonKind classes compile with PolyKindsI was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeO...I was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-}
module Main where
-- Define a Type for the natural numbers, zero and a successor
data Nat = Z | S Nat
class Addable k where
type (a :: k) + (b :: k) :: k
instance Addable Nat where
type (Z + a) = a
type (S a) + b = S (a + b)
main :: IO ()
main = putStrLn "Shouldn't this need TypeInType?"
```
(for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930)
Since according to a responder on \#haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds.
As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12919Equality not used for substitution2019-07-07T18:24:38ZVladislav ZavialovEquality not used for substitutionThis code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
module T12919 where
import Data.Kind
data N = Z
data V :: N -> Type where
VZ :: V Z
type family VC (n :: N) :: Type where
VC Z = Type
type famil...This code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
module T12919 where
import Data.Kind
data N = Z
data V :: N -> Type where
VZ :: V Z
type family VC (n :: N) :: Type where
VC Z = Type
type family VF (xs :: V n) (f :: VC n) :: Type where
VF VZ f = f
data Dict c where
Dict :: c => Dict c
prop :: xs ~ VZ => Dict (VF xs f ~ f)
prop = Dict
```
fails with this error:
```
T12919.hs:22:8: error:
• Couldn't match type ‘f’ with ‘VF 'VZ f’
arising from a use of ‘Dict’
‘f’ is a rigid type variable bound by
the type signature for:
prop :: forall (xs :: V 'Z) f. xs ~ 'VZ => Dict VF xs f ~ f
at T12919.hs:21:9
• In the expression: Dict
In an equation for ‘prop’: prop = Dict
• Relevant bindings include
prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1)
```
However, if I substitute `xs` with `VZ` (by hand) in the type of `prop`, it compiles. Can be reproduced with GHC 8.0.1 but not HEAD.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12766Allow runtime-representation polymorphic data families2019-07-07T18:25:14ZIcelandjackAllow runtime-representation polymorphic data familiesThis is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```This is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/12742Instantiation of invisible type family arguments is too eager2019-07-07T18:25:20ZRichard Eisenbergrae@richarde.devInstantiation of invisible type family arguments is too eagerThis module looks, to me, like it should be accepted:
```
{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
module Bug where
import Data.Kind
type family F :: forall k2. (k1, k2)
data T :: (forall k2. (Bool, k2)) -> Type
type S...This module looks, to me, like it should be accepted:
```
{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
module Bug where
import Data.Kind
type family F :: forall k2. (k1, k2)
data T :: (forall k2. (Bool, k2)) -> Type
type S = T F
```
But it's not. The problem is that `TcHsType.handle_tyfams` eagerly instantiates *all* invisible arguments to a type family at every occurrence. Instead, it should instantiate only those that are counted in the TF's arity -- that is, those "before the colon".
Will fix.
<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":"Instantiation of invisible type family arguments is too eager","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This module looks, to me, like it should be accepted:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}\r\n\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family F :: forall k2. (k1, k2)\r\n\r\ndata T :: (forall k2. (Bool, k2)) -> Type\r\n\r\ntype S = T F\r\n}}}\r\n\r\nBut it's not. The problem is that `TcHsType.handle_tyfams` eagerly instantiates ''all'' invisible arguments to a type family at every occurrence. Instead, it should instantiate only those that are counted in the TF's arity -- that is, those \"before the colon\".\r\n\r\nWill fix.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12553Reference kind in a type instance declaration defined in another instance dec...2019-07-07T18:26:08ZIcelandjackReference kind in a type instance declaration defined in another instance declarationOld code:
```hs
data Full :: Type -> Type
data AST :: (Type -> Type) -> (Type -> Type)
-- ASTF :: (Type -> Type) -> (Type -> Type)
type ASTF dom a = AST dom (Full a)
class Syntactic a where
type Domain a :: Type -> Type
type In...Old code:
```hs
data Full :: Type -> Type
data AST :: (Type -> Type) -> (Type -> Type)
-- ASTF :: (Type -> Type) -> (Type -> Type)
type ASTF dom a = AST dom (Full a)
class Syntactic a where
type Domain a :: Type -> Type
type Internal a :: Type
desugar :: a -> ASTF (Domain a) (Internal a)
sugar :: ASTF (Domain a) (Internal a) -> a
```
----
New code with richer kinds
```hs
data Sig a = Full a | a :-> Sig a
data AST :: (Sig a -> Type) -> (Sig a -> Type)
data Sig a = Full a | a :-> Sig a
-- ASTF :: (Sig a -> Type) -> (a -> Type)
type ASTF dom a = AST dom (Full a)
class Syntactic a where
type Domain a :: Sig Type -> Type
type Internal a :: Type
desugar :: a -> ASTF (Domain a) (Internal a)
sugar :: ASTF (Domain a) (Internal a) -> a
```
As the type of `ASTF` hints at it could accept arguments of kind `Sig a -> Type` and `a`. I would like to reference the variable `a` from the kind of `Domain` in the kind of `Internal`, but this fails:
```hs
-- • Kind variable ‘u’ is implicitly bound in datatype
-- ‘Internal’, but does not appear as the kind of any
-- of its type variables. Perhaps you meant
-- to bind it (with TypeInType) explicitly somewhere?
-- Type variables with inferred kinds: a
-- • In the class declaration for ‘Syntactic’
class Syntactic a where
type Domain a :: Sig u -> Type
type Internal a :: u
desugar :: a -> ASTF (Domain a) (Internal a)
sugar :: ASTF (Domain a) (Internal a) -> a
```
----
Should the `u` in the kind of `Domain a` be quantified over (which makes this compile)?
```hs
type Domain a :: forall k. Sig k -> Type
```
- \*Edit\*\*: This doesn't work.https://gitlab.haskell.org/ghc/ghc/-/issues/12534GHC 8.0 accepts recursive kind signature that GHC 7.10 rejects2019-07-07T18:26:11ZRyan ScottGHC 8.0 accepts recursive kind signature that GHC 7.10 rejectsGHC 7.10 rejects this datatype:
```hs
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
data T (a :: a)
```
```
$ /opt/ghc/7.10.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:5...GHC 7.10 rejects this datatype:
```hs
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
data T (a :: a)
```
```
$ /opt/ghc/7.10.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:5:1:
Kind variable also used as type variable: ‘a’
In the data type declaration for ‘T’
```
But GHC 8.0 accepts the above code! It appears that GHC implicitly freshens the kind-level `a` so as to have a different name, since the following modification to `T`:
```hs
data T a (a :: a)
```
Results in this error:
```
$ /opt/ghc/8.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:5:8: error:
Conflicting definitions for ‘a’
Bound at: Bug.hs:5:8
Bug.hs:5:11
Bug.hs:5:16: error:
Type variable ‘a’ used in a kind.
Did you mean to use TypeInType?
the data type declaration for ‘T’
```
But with this modification:
```hs
data T (a :: a) a
```
You won't get an error message about `a` being used as both a kind and type:
```
$ /opt/ghc/8.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:5:9: error:
Conflicting definitions for ‘a’
Bound at: Bug.hs:5:9
Bug.hs:5:17
```
To make things even more confusing, this behavior doesn't seem to carry over to typeclass instances. For example: GHC 8.0 will (rightfully) reject this code:
```hs
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
data T (a :: a)
class C x
instance C (T (a :: a))
```
```
$ /opt/ghc/8.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:16: error:
Variable ‘a’ used as both a kind and a type
Did you intend to use TypeInType?
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.0 accepts recursive kind signature that GHC 7.10 rejects","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 7.10 rejects this datatype:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\nmodule Bug where\r\n\r\ndata T (a :: a)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/7.10.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:5:1:\r\n Kind variable also used as type variable: ‘a’\r\n In the data type declaration for ‘T’\r\n}}}\r\n\r\nBut GHC 8.0 accepts the above code! It appears that GHC implicitly freshens the kind-level `a` so as to have a different name, since the following modification to `T`:\r\n\r\n{{{#!hs\r\ndata T a (a :: a)\r\n}}}\r\n\r\nResults in this error:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:5:8: error:\r\n Conflicting definitions for ‘a’\r\n Bound at: Bug.hs:5:8\r\n Bug.hs:5:11\r\n\r\nBug.hs:5:16: error:\r\n Type variable ‘a’ used in a kind.\r\n Did you mean to use TypeInType?\r\n the data type declaration for ‘T’\r\n}}}\r\n\r\nBut with this modification:\r\n\r\n{{{#!hs\r\ndata T (a :: a) a\r\n}}}\r\n\r\nYou won't get an error message about `a` being used as both a kind and type:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:5:9: error:\r\n Conflicting definitions for ‘a’\r\n Bound at: Bug.hs:5:9\r\n Bug.hs:5:17\r\n}}}\r\n\r\nTo make things even more confusing, this behavior doesn't seem to carry over to typeclass instances. For example: GHC 8.0 will (rightfully) reject this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\nmodule Bug where\r\n\r\ndata T (a :: a)\r\n\r\nclass C x\r\ninstance C (T (a :: a))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:8:16: error:\r\n Variable ‘a’ used as both a kind and a type\r\n Did you intend to use TypeInType?\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12503Template Haskell regression: GHC erroneously thinks a type variable is also a...2019-07-07T18:26:20ZRyan ScottTemplate Haskell regression: GHC erroneously thinks a type variable is also a kindThe following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)
```hs
{-# LANGUAGE ...The following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)
```hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Regression where
import Language.Haskell.TH
data T k
class C a
$(do TyConI (DataD [] tName [ KindedTV kName kKind]
#if __GLASGOW_HASKELL__ >= 800
_
#endif
_ _) <- reify ''T
d <- instanceD (cxt []) (conT ''C `appT` (conT tName `appT` sigT (varT kName) kKind)) []
return [d])
```
```
$ /opt/ghc/8.0.1/bin/ghc Regression.hs
[1 of 1] Compiling Regression ( Regression.hs, Regression.o )
Regression.hs:(13,3)-(19,15): Splicing declarations
do { TyConI (DataD []
tName_a2RT
[KindedTV kName_a2RU kKind_a2RV]
_
_
_) <- reify ''T;
d_a31Y <- instanceD
(cxt [])
(conT ''C
`appT` (conT tName_a2RT `appT` sigT (varT kName_a2RU) kKind_a2RV))
[];
return [d_a31Y] }
======>
instance C (T (k_avB :: k_avC))
Regression.hs:13:3: error:
Variable ‘k_avB’ used as both a kind and a type
Did you intend to use TypeInType?
```
Somewhat confusingly, you can use `instance C (T (k_avB :: k_avC))` on its own, and it will compile without issue. Also, quoting it doesn't seem to trip up this bug, as this also compiles without issue:
```hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -ddump-splices #-}
module WorksSomehow where
import Language.Haskell.TH
data T k
class C a
$([d| instance C (T k) |])
```
The original program has several workarounds:
1. Turn off `PolyKinds` (OK, this isn't a very good workaround...)
1. Add an explicit kind signature to `T`, e.g., `data T (k :: k1)`
1. Change the type variable of `T` to some other letter, e.g., `data T p` or `data T k1`
Given that (3) is a successful workaround, I strongly suspect that GHC is confusing the type variable `k` (which gets `ddump-splice`d as `k_avB`) with the kind variable `k` (which gets `ddump-splice`d as `k_avC`) due to their common prefix `k`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell regression: GHC erroneously thinks a type variable is also a kind","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)\r\n\r\n{{{#!hs\r\n{-# LANGUAGE CPP #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule Regression where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata T k\r\nclass C a\r\n\r\n$(do TyConI (DataD [] tName [ KindedTV kName kKind]\r\n#if __GLASGOW_HASKELL__ >= 800\r\n _\r\n#endif\r\n _ _) <- reify ''T\r\n d <- instanceD (cxt []) (conT ''C `appT` (conT tName `appT` sigT (varT kName) kKind)) []\r\n return [d])\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Regression.hs \r\n[1 of 1] Compiling Regression ( Regression.hs, Regression.o )\r\nRegression.hs:(13,3)-(19,15): Splicing declarations\r\n do { TyConI (DataD []\r\n tName_a2RT\r\n [KindedTV kName_a2RU kKind_a2RV]\r\n _\r\n _\r\n _) <- reify ''T;\r\n d_a31Y <- instanceD\r\n (cxt [])\r\n (conT ''C\r\n `appT` (conT tName_a2RT `appT` sigT (varT kName_a2RU) kKind_a2RV))\r\n [];\r\n return [d_a31Y] }\r\n ======>\r\n instance C (T (k_avB :: k_avC))\r\n\r\nRegression.hs:13:3: error:\r\n Variable ‘k_avB’ used as both a kind and a type\r\n Did you intend to use TypeInType?\r\n}}}\r\n\r\nSomewhat confusingly, you can use `instance C (T (k_avB :: k_avC))` on its own, and it will compile without issue. Also, quoting it doesn't seem to trip up this bug, as this also compiles without issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE CPP #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule WorksSomehow where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata T k\r\nclass C a\r\n\r\n$([d| instance C (T k) |])\r\n}}}\r\n\r\nThe original program has several workarounds:\r\n\r\n1. Turn off `PolyKinds` (OK, this isn't a very good workaround...)\r\n2. Add an explicit kind signature to `T`, e.g., `data T (k :: k1)`\r\n3. Change the type variable of `T` to some other letter, e.g., `data T p` or `data T k1`\r\n\r\nGiven that (3) is a successful workaround, I strongly suspect that GHC is confusing the type variable `k` (which gets `ddump-splice`d as `k_avB`) with the kind variable `k` (which gets `ddump-splice`d as `k_avC`) due to their common prefix `k`.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12442Pure unifier usually doesn't need to unify kinds2019-07-07T18:26:36ZRichard Eisenbergrae@richarde.devPure unifier usually doesn't need to unify kindsThe pure unifier (in `types/Unify.hs`) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong.
It's wasteful bec...The pure unifier (in `types/Unify.hs`) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong.
It's wasteful because most invocations of the unifier on a list of types pass in well-kinded arguments to some type constructor. Because the kinds of type constructors are closed, if we process the list left-to-right, we will always unify the kinds of later arguments before we get to them. So we shouldn't take another pass on the kinds.
It's wrong because it's conceivable for the kind to include a type family application, and using a type family application as a template in the pure unifier is very silly, indeed.
I cam across this while trying to translate Idris's algebraic effects library to Haskell. My reduced test case is attached.
Patch on the way.
<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":"Pure unifier usually doesn't need to unify kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The pure unifier (in `types/Unify.hs`) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong.\r\n\r\nIt's wasteful because most invocations of the unifier on a list of types pass in well-kinded arguments to some type constructor. Because the kinds of type constructors are closed, if we process the list left-to-right, we will always unify the kinds of later arguments before we get to them. So we shouldn't take another pass on the kinds.\r\n\r\nIt's wrong because it's conceivable for the kind to include a type family application, and using a type family application as a template in the pure unifier is very silly, indeed.\r\n\r\nI cam across this while trying to translate Idris's algebraic effects library to Haskell. My reduced test case is attached.\r\n\r\nPatch on the way.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12369data families shouldn't be required to have return kind *, data instances should2021-09-09T23:17:59ZEdward Kmettdata families shouldn't be required to have return kind *, data instances shouldI'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1...I'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1: error:
• Kind signature on data type declaration has non-* return kind
(k -> *) -> k
• In the data family declaration for ‘Fix’
```
Ultimately I think the issue here is that data __instances__ should be required to end in kind \*, not the families, but this generalization didn't mean anything until we had `PolyKinds`.
As an example of a usecase, with the above, I could define a bifunctor fixed point such as
```hs
newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"data families shouldn't be required to have return kind *, data instances should","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'd like to be able to define\r\n\r\n{{{#!hs\r\n{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}\r\ndata family Fix :: (k -> *) -> k\r\nnewtype instance Fix f = In { out :: f (Fix f) }\r\n}}}\r\n\r\nBut currently this is disallowed:\r\n\r\n{{{\r\nFix.hs:2:1: error:\r\n • Kind signature on data type declaration has non-* return kind\r\n (k -> *) -> k\r\n • In the data family declaration for ‘Fix’\r\n}}}\r\n\r\nUltimately I think the issue here is that data __instances__ should be required to end in kind *, not the families, but this generalization didn't mean anything until we had `PolyKinds`.\r\n\r\nAs an example of a usecase, with the above, I could define a bifunctor fixed point such as\r\n\r\n{{{#!hs\r\nnewtype instance Fix f a = In2 { out2 :: f (Fix f a) a }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/12176Failure of bidirectional type inference at the kind level2019-07-07T18:27:19ZRichard Eisenbergrae@richarde.devFailure of bidirectional type inference at the kind levelI'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k...I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
```
Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`):
```
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
```
That is, I wished to extract the kind parameter to `MkK`, matching against a partially-applied `MkX`, and GHC understood that intention.
However, sadly, writing `Foo Expr` produces
```
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
```
For some reason, `Expr` is getting instantiated when it shouldn't be.
Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12174Recursive use of type-in-type results in infinite loop2020-09-19T19:52:25ZEdward Z. YangRecursive use of type-in-type results in infinite loopTypechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S...Typechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S). MkT (V a)
data S = forall (a :: T). MkS (V a)
```
There's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Recursive use of type-in-type results in infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Typechecking this module results in an infinite loop:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule X where\r\n\r\ndata V a\r\ndata T = forall (a :: S). MkT (V a)\r\ndata S = forall (a :: T). MkS (V a)\r\n}}}\r\n\r\nThere's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12102“Constraints in kinds” illegal family application in instance (+ documentatio...2022-10-22T21:03:44ZIcelandjack“Constraints in kinds” illegal family application in instance (+ documentation issues?)GHC 8.0.0.20160511. Example from the user guide: [Constraints in kinds](https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds)
```hs
type family IsTypeLit a where
IsTypeLit Nat = 'Tru...GHC 8.0.0.20160511. Example from the user guide: [Constraints in kinds](https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds)
```hs
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
```
Deriving a standalone `Show` instance \*without\* the constraint `(IsTypeLit a ~ 'True) => ` works fine
```hs
deriving instance Show (T a)
```
but I couldn't define a `Show` instance given the constraints:
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit a0’
-- The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
-- In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)
```
let's add constraints
```hs
-- • Couldn't match expected kind ‘'True’
-- with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
-- In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where
```
let's derive for a single literal
```hs
-- • Illegal type synonym family application in instance:
-- T Nat
-- ('Data.Type.Equality.C:~
-- Bool
-- (IsTypeLit Nat)
-- 'True
-- ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
-- 42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))
```
same happens with
```hs
instance Show (T 42) where
```
----
The documentation
> Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in
```
tVDv.hs:10:17-18: error: …
• Expected kind ‘a’, but ‘42’ has kind ‘Nat’
• In the first argument of ‘T’, namely ‘42’
In the type ‘T 42’
In the definition of data constructor ‘MkNat’
Compilation failed.
```8.10.1