GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11453Kinds in type synonym/data declarations can unexpectedly unify2019-07-07T18:30:21ZRyan ScottKinds in type synonym/data declarations can unexpectedly unifyWhile trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType ...While trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall (f :: k1 -> *). Either (f a) (f b)
-- Defined at <interactive>:2:1
```
This is pretty odd for two reasons. One, the kind `k1` was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:
```
λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall k2 (f :: k2 -> *). Either (f a) (f b)
-- Defined at <interactive>:4:1
```
We still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.
Note that this doesn't happen if you use explicit kind binders:
```
type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
<interactive>:6:74: error:
• Expected kind ‘k1’, but ‘a’ has kind ‘k2’
• In the first argument of ‘f’, namely ‘a’
In the first argument of ‘Either’, namely ‘f a’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
<interactive>:6:80: error:
• Expected kind ‘k1’, but ‘b’ has kind ‘k3’
• In the first argument of ‘f’, namely ‘b’
In the second argument of ‘Either’, namely ‘f b’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
```
only when the kinds are specified but not visible.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Kinds in type synonym/data declarations can unexpectedly unify","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"While trying out ideas to fix [https://github.com/ekmett/lens/issues/626 this lens issue], I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators\r\nGHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/xnux/.ghci\r\nλ> import Data.Kind\r\nλ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall (f :: k1 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:2:1\r\n}}}\r\n\r\nThis is pretty odd for two reasons. One, the kind {{{k1}}} was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:\r\n\r\n{{{\r\nλ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall k2 (f :: k2 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:4:1\r\n}}}\r\n\r\nWe still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.\r\n\r\nNote that this doesn't happen if you use explicit kind binders:\r\n\r\n{{{\r\ntype Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\n\r\n<interactive>:6:74: error:\r\n • Expected kind ‘k1’, but ‘a’ has kind ‘k2’\r\n • In the first argument of ‘f’, namely ‘a’\r\n In the first argument of ‘Either’, namely ‘f a’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n\r\n<interactive>:6:80: error:\r\n • Expected kind ‘k1’, but ‘b’ has kind ‘k3’\r\n • In the first argument of ‘f’, namely ‘b’\r\n In the second argument of ‘Either’, namely ‘f b’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n}}}\r\n\r\nonly when the kinds are specified but not visible.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11463Template Haskell applies too many arguments to kind synonym2022-02-08T15:14:11ZRyan ScottTemplate Haskell applies too many arguments to kind synonymRunning the following code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module IdStarK where
import Data.Kind
import Language.Haskell.TH
type Id a = a
data Proxy (a :: Id k) = Proxy
$(return [])
main :: IO ()
...Running the following code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module IdStarK where
import Data.Kind
import Language.Haskell.TH
type Id a = a
data Proxy (a :: Id k) = Proxy
$(return [])
main :: IO ()
main = do
putStrLn $(reify ''Proxy >>= stringE . pprint)
putStrLn $(reify ''Proxy >>= stringE . show)
```
Gives a result I wouldn't have expected:
```
$ /opt/ghc/head/bin/runghc IdStarK.hs
data IdStarK.Proxy (a_0 :: IdStarK.Id * k_1) = IdStarK.Proxy
TyConI (DataD [] IdStarK.Proxy [KindedTV a_1627394516 (AppT (AppT (ConT IdStarK.Id) StarT) (VarT k_1627394515))] Nothing [NormalC IdStarK.Proxy []] [])
```
From the output, it appears that `Id` is being applied to *two* arguments, both `*` and `k`! Perhaps this indirectly (or directly) a consequence of #11376?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #11376 |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell applies too many arguments to kind synonym","status":"New","operating_system":"","component":"Template Haskell","related":[11376],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["TypeApplications","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Running the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule IdStarK where\r\n\r\nimport Data.Kind\r\nimport Language.Haskell.TH\r\n\r\ntype Id a = a\r\ndata Proxy (a :: Id k) = Proxy\r\n\r\n$(return [])\r\n\r\nmain :: IO ()\r\nmain = do\r\n putStrLn $(reify ''Proxy >>= stringE . pprint)\r\n putStrLn $(reify ''Proxy >>= stringE . show)\r\n}}}\r\n\r\nGives a result I wouldn't have expected:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/runghc IdStarK.hs \r\ndata IdStarK.Proxy (a_0 :: IdStarK.Id * k_1) = IdStarK.Proxy\r\nTyConI (DataD [] IdStarK.Proxy [KindedTV a_1627394516 (AppT (AppT (ConT IdStarK.Id) StarT) (VarT k_1627394515))] Nothing [NormalC IdStarK.Proxy []] [])\r\n}}}\r\n\r\nFrom the output, it appears that `Id` is being applied to ''two'' arguments, both `*` and `k`! Perhaps this indirectly (or directly) a consequence of #11376?","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11471Kind polymorphism and unboxed types: bad things are happening2019-07-07T18:30:16ZBen GamariKind polymorphism and unboxed types: bad things are happeningThis Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---...This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Task |
| 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":"Note [The kind invariant] in TyCoRep needs to be updated","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11473Levity polymorphism checks are inadequate2019-07-07T18:30:16ZSimon Peyton JonesLevity polymorphism checks are inadequateBen found
```hs
{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
import GHC.Exts
import GHC.Types
type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char = Char
...Ben found
```hs
{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
import GHC.Exts
import GHC.Types
type family Boxed (a :: k) :: *
type instance Boxed Char# = Char
type instance Boxed Char = Char
class BoxIt (a :: TYPE lev) where
boxed :: a -> Boxed a
instance BoxIt Char# where boxed x = C# x
instance BoxIt Char where boxed = id
hello :: forall (lev :: Levity). forall (a :: TYPE lev). BoxIt a => a -> Boxed a
hello x = boxed x
{-# NOINLINE hello #-}
main :: IO ()
main = do
print $ boxed 'c'#
print $ boxed 'c'
print $ hello 'c'
print $ hello 'c'#
```
This is plainly wrong because we have a polymorphic function `boxed` that is being passed both boxed and unboxed arguments.
You do get a Lint error with `-dcore-lint`.
But the original problem is with the type signature for `boxed`. We should never have a levity-polymorphic type to the left of an arrow. To the right yes, but to the left no. I suppose we could check that in `TcValidity`.
See also #114718.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11484Type synonym using -XTypeInType can't be spliced with TH2019-07-07T18:30:13ZRyan ScottType synonym using -XTypeInType can't be spliced with THThe following code compiles:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Foo where
import Data.Kind
type TySyn (k :: *) (a :: k) = ()
-- $([d| type TySyn2 (k :: *) (a :...The following code compiles:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Foo where
import Data.Kind
type TySyn (k :: *) (a :: k) = ()
-- $([d| type TySyn2 (k :: *) (a :: k) = () |])
```
But uncomment the last line, and it doesn't compile:
```
$ /opt/ghc/head/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:10:3-43: Splicing declarations
[d| type TySyn2_aBH (k_aBI :: *) (a_aBJ :: k_aBI) = () |]
======>
type TySyn2_a4BF (k_a4BG :: Type) (a_a4BH :: k_a4BG) = ()
Foo.hs:10:3: error:
• Couldn't match expected kind ‘GHC.Prim.Any’ with actual kind ‘k1’
• In the type declaration for ‘TySyn2’
Foo.hs:10:3: error:
• Kind variable ‘k_a4BG’ is implicitly bound in datatype
‘TySyn2’, 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: k_a4BG (a_a4BH :: GHC.Prim.Any)
• In the type declaration for ‘TySyn2’
```
There are two issues here:
1. The error message claims that `TySyn2` is a datatype when it is actually a type synonym. This should be easy enough to fix; just change [the code](http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/typecheck/TcHsType.hs#l1874) that throws the error message to invoke [tyConFlavour](http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/types/TyCon.hs#l1957).
1. For some reason, the type variable `a` in `TySyn2` fails to kind-check. Somehow, an `Any` got in there, but I'm not sure where it snuck in.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type synonym using -XTypeInType can't be spliced with TH","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The following code compiles:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype TySyn (k :: *) (a :: k) = ()\r\n\r\n-- $([d| type TySyn2 (k :: *) (a :: k) = () |])\r\n}}}\r\n\r\nBut uncomment the last line, and it doesn't compile:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Foo.hs \r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\nFoo.hs:10:3-43: Splicing declarations\r\n [d| type TySyn2_aBH (k_aBI :: *) (a_aBJ :: k_aBI) = () |]\r\n ======>\r\n type TySyn2_a4BF (k_a4BG :: Type) (a_a4BH :: k_a4BG) = ()\r\n\r\nFoo.hs:10:3: error:\r\n • Couldn't match expected kind ‘GHC.Prim.Any’ with actual kind ‘k1’\r\n • In the type declaration for ‘TySyn2’\r\n\r\nFoo.hs:10:3: error:\r\n • Kind variable ‘k_a4BG’ is implicitly bound in datatype\r\n ‘TySyn2’, 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: k_a4BG (a_a4BH :: GHC.Prim.Any)\r\n • In the type declaration for ‘TySyn2’\r\n}}}\r\n\r\nThere are two issues here:\r\n\r\n1. The error message claims that `TySyn2` is a datatype when it is actually a type synonym. This should be easy enough to fix; just change [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/typecheck/TcHsType.hs#l1874 the code] that throws the error message to invoke [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/types/TyCon.hs#l1957 tyConFlavour].\r\n2. For some reason, the type variable `a` in `TySyn2` fails to kind-check. Somehow, an `Any` got in there, but I'm not sure where it snuck in.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/11485Very unhelpful message resulting from kind mismatch2019-07-07T18:30:13ZRyan ScottVery unhelpful message resulting from kind mismatchThe following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not e...The following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.
On GHC 7.10.3:
```
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:9:19:
Couldn't match kind ‘* -> *’ with ‘*’
Expected type: Proxy a0
Actual type: Proxy []
In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
But on GHC 8.0.1-rc1:
```
Foo.hs:9:19: error:
• Expected kind ‘Proxy []’,
but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’
• In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| 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":"Very unhelpful message resulting from kind mismatch","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Data.Typeable\r\n\r\ntyConOf :: Typeable a => Proxy a -> TyCon\r\ntyConOf = typeRepTyCon . typeRep\r\n\r\ntcList :: TyCon\r\ntcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nfails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.\r\n\r\nOn GHC 7.10.3:\r\n\r\n{{{\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:9:19:\r\n Couldn't match kind ‘* -> *’ with ‘*’\r\n Expected type: Proxy a0\r\n Actual type: Proxy []\r\n In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’\r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nBut on GHC 8.0.1-rc1:\r\n\r\n{{{\r\nFoo.hs:9:19: error: \r\n • Expected kind ‘Proxy []’, \r\n but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’ \r\n • In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’ \r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11519Inferring non-tau kinds2019-07-07T18:30:05ZRichard Eisenbergrae@richarde.devInferring non-tau kindsWhile up to my usual type-level shenanigans, I found that I want this definition:
```
data TypeRep (a :: k) -- abstract
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint...While up to my usual type-level shenanigans, I found that I want this definition:
```
data TypeRep (a :: k) -- abstract
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
c a => TypeRep a -> TypeRepX c
```
Note `TypeRepX`'s higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`'s payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`, where
```
class ConstTrue (a :: k)
instance ConstTrue a
```
This actually works just fine, and I've been using the above definition to good effect.
But then I wanted a `Show` instance:
```
instance Show (TypeRep a) -- elsewhere
instance Show (TypeRepX c) where
show (TypeRepX tr) = show t
```
Looks sensible. But GHC complains. This is because it tries to infer `c`'s kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`'s kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c` with the correct kind, unification *still* fails. This is because that `c` is a *usage* of `c`, not a *binding* of `c`. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.
I'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c` is perfectly safe, because the kind is known from the use of `TypeRepX`. This would allow me to drop the kind annotation in the definition of `TypeRepX`, which looks redundant to me. But I'm not fully sure about this assumption.
At the least, we could introduce a spot for explicit binding of type variables in instance declarations.
I think, actually, I just figured it out. Use `ExpType`s when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Inferring non-tau kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While up to my usual type-level shenanigans, I found that I want this definition:\r\n\r\n{{{\r\ndata TypeRep (a :: k) -- abstract\r\n\r\ndata TypeRepX :: (forall k. k -> Constraint) -> Type where\r\n TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).\r\n c a => TypeRep a -> TypeRepX c\r\n}}}\r\n\r\nNote `TypeRepX`'s higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`'s payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`, where\r\n\r\n{{{\r\nclass ConstTrue (a :: k)\r\ninstance ConstTrue a\r\n}}}\r\n\r\nThis actually works just fine, and I've been using the above definition to good effect.\r\n\r\nBut then I wanted a `Show` instance:\r\n\r\n{{{\r\ninstance Show (TypeRep a) -- elsewhere\r\n\r\ninstance Show (TypeRepX c) where\r\n show (TypeRepX tr) = show t\r\n}}}\r\n\r\nLooks sensible. But GHC complains. This is because it tries to infer `c`'s kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`'s kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c` with the correct kind, unification ''still'' fails. This is because that `c` is a ''usage'' of `c`, not a ''binding'' of `c`. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.\r\n\r\nI'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c` is perfectly safe, because the kind is known from the use of `TypeRepX`. This would allow me to drop the kind annotation in the definition of `TypeRepX`, which looks redundant to me. But I'm not fully sure about this assumption.\r\n\r\nAt the least, we could introduce a spot for explicit binding of type variables in instance declarations.\r\n\r\nI think, actually, I just figured it out. Use `ExpType`s when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11520GHC falls into a hole if given incorrect kind signature2019-07-07T18:30:05ZBen GamariGHC falls into a hole if given incorrect kind signatureIf one provides an incorrect kind signature GHC throws up. For instance, this non-sense,
```hs
{-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-}
module Play where
import GHC.Types hiding (TyCon)
data ...If one provides an incorrect kind signature GHC throws up. For instance, this non-sense,
```hs
{-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-}
module Play where
import GHC.Types hiding (TyCon)
data TypeRep (a :: k)
class Typeable k => Typeable (a :: k) where
typeRep :: TypeRep a
data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a))
-- Note how the kind signature on g is incorrect
instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where
typeRep = undefined
```
fails with
```
λ> :load Bug.hs
[1 of 1] Compiling Play ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160122 for x86_64-unknown-linux):
fvProv falls into a hole {abet}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11548Absolutely misleading error message on kind error2019-07-07T18:29:53ZmniipAbsolutely misleading error message on kind error```hs
module Bug where
import Data.Proxy
fun :: Proxy a -> ()
fun Proxy = ()
bug :: ()
bug = fun (Proxy :: Proxy Maybe)
```
```hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:12: error:
• Expected kind ‘Proxy M...```hs
module Bug where
import Data.Proxy
fun :: Proxy a -> ()
fun Proxy = ()
bug :: ()
bug = fun (Proxy :: Proxy Maybe)
```
```hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:12: error:
• Expected kind ‘Proxy Maybe’,
but ‘Data.Proxy.Proxy :: Proxy Maybe’ has kind ‘Proxy Maybe’
• In the first argument of ‘fun’, namely ‘(Proxy :: Proxy Maybe)’
In the expression: fun (Proxy :: Proxy Maybe)
In an equation for ‘bug’: bug = fun (Proxy :: Proxy Maybe)
```
1. 10 gives the appropriate `Couldn't match kind ‘* -> *’ with ‘*’` message.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Absolutely misleading error message on kind error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nfun :: Proxy a -> ()\r\nfun Proxy = ()\r\n\r\nbug :: ()\r\nbug = fun (Proxy :: Proxy Maybe)\r\n}}}\r\n\r\n{{{#!hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:12: error:\r\n • Expected kind ‘Proxy Maybe’,\r\n but ‘Data.Proxy.Proxy :: Proxy Maybe’ has kind ‘Proxy Maybe’\r\n • In the first argument of ‘fun’, namely ‘(Proxy :: Proxy Maybe)’\r\n In the expression: fun (Proxy :: Proxy Maybe)\r\n In an equation for ‘bug’: bug = fun (Proxy :: Proxy Maybe)\r\n}}}\r\n\r\n7.10 gives the appropriate `Couldn't match kind ‘* -> *’ with ‘*’` message.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11549Add -fshow-runtime-rep2019-07-07T18:29:53ZRichard Eisenbergrae@richarde.devAdd -fshow-runtime-repAs discussed in several interwoven threads ([original](https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html), [café](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html)), it has been suggested to a...As discussed in several interwoven threads ([original](https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html), [café](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html)), it has been suggested to add a flag `-fshow-runtime-rep`. Without this flag enabled, the pretty printer will instantiate any `RuntimeRep` type parameters to `PtrRep Lifted`. This has the effect of changing
```
($) :: forall (r :: RuntimeRep) (a :: *) (b :: TYPE r). (a -> b) -> a -> b
```
to
```
($) :: (a -> b) -> a -> b
```
under the default GHCi settings.
Note that `Levity` becomes `RuntimeRep` after #11471 is complete.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Add -fshow-runtime-rep","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As discussed in several interwoven threads ([https://mail.haskell.org/pipermail/ghc-devs/2016-February/011268.html original], [https://mail.haskell.org/pipermail/haskell-cafe/2016-February/122914.html café]), it has been suggested to add a flag `-fshow-runtime-rep`. Without this flag enabled, the pretty printer will instantiate any `RuntimeRep` type parameters to `PtrRep Lifted`. This has the effect of changing\r\n\r\n{{{\r\n($) :: forall (r :: RuntimeRep) (a :: *) (b :: TYPE r). (a -> b) -> a -> b\r\n}}}\r\n\r\nto\r\n\r\n{{{\r\n($) :: (a -> b) -> a -> b\r\n}}}\r\n\r\nunder the default GHCi settings.\r\n\r\nNote that `Levity` becomes `RuntimeRep` after #11471 is complete.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11554Self quantification in GADT data declarations2020-09-19T20:01:19ZRafbillSelf quantification in GADT data declarationsGHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType...GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{-# LANGUAGE GADTs, TypeInType #-}
import Data.Kind
data A :: Type where
B :: forall (a :: A). A
```
I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"Self quantification in GADT data declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56) :\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeInType #-}\r\nimport Data.Kind\r\ndata A :: Type where\r\n B :: forall (a :: A). A\r\n}}}\r\n\r\nI guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11560panic: isInjectiveTyCon sees a TcTyCon2019-07-07T18:29:48Zrwbartonpanic: isInjectiveTyCon sees a TcTyConI typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160201: htt...I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeFamilies -XTypeInType
Prelude> :m +Data.Kind
Prelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160201 for x86_64-unknown-linux):
isInjectiveTyCon sees a TcTyCon T
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"panic: isInjectiveTyCon sees a TcTyCon","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.\r\n{{{\r\nrwbarton@morphism:~/ghc-newest$ ./inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XTypeFamilies -XTypeInType\r\nPrelude> :m +Data.Kind\r\nPrelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160201 for x86_64-unknown-linux):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11592Self-kinded type variable accepted2019-07-07T18:29:41ZSimon Peyton JonesSelf-kinded type variable acceptedFound when chasing #11407
```
data T (a::a) = Blah -- Accepted
data S (b :: a) a = ...
-- Rejected with: variable ‘a’ used as a kind variable before being bound
-- as a type variable. Perhaps reorder your variables?
...Found when chasing #11407
```
data T (a::a) = Blah -- Accepted
data S (b :: a) a = ...
-- Rejected with: variable ‘a’ used as a kind variable before being bound
-- as a type variable. Perhaps reorder your variables?
```
But `T` should be rejected too, for the same reason as `S`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.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":"Self-kinded type varialbe accepted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Found when chasing #11407\r\n{{{\r\ndata T (a::a) = Blah -- Accepted\r\n\r\ndata S (b :: a) a = ...\r\n -- Rejected with: variable ‘a’ used as a kind variable before being bound\r\n -- as a type variable. Perhaps reorder your variables?\r\n}}}\r\nBut `T` should be rejected too, for the same reason as `S`","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11614document TypeInType2019-07-07T18:29:36Zrwbartondocument TypeInType(Just to keep track of the status for 8.0.1.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------- |
| Version | 8.0.1-rc2 |
| Type ...(Just to keep track of the status for 8.0.1.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------- |
| Version | 8.0.1-rc2 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Documentation |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"document TypeInType","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"(Just to keep track of the status for 8.0.1.)","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11635Higher-rank kind in datatype definition rejected2019-07-07T18:29:23ZOleg GrenrusHigher-rank kind in datatype definition rejectedExample program:
```hs
{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
import Data.Kind
data X (a :: forall k. k -> * ) = X
```
errors with
```
polykind.hs:3:1: error:
Expecting one more argument to ‘a’
Expected ki...Example program:
```hs
{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
import Data.Kind
data X (a :: forall k. k -> * ) = X
```
errors with
```
polykind.hs:3:1: error:
Expecting one more argument to ‘a’
Expected kind ‘k0’, but ‘a’ has kind ‘forall k. k -> *’
```
Without `TypeInType`, the error is better, yet gives false hint:
```
polykind.hs:3:23: error:
Illegal kind: forall k. k -> *
Did you mean to enable TypeInType?
```
---
For the record 7.10.3 doesn't recognise polymorphic kinds at all (same program, without `Data.Kind` import):
```
polykind.hs:3:23: parse error on input ‘forall’
```
Which makes me think that polymorphic kinds are somehow supported, but maybe not.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11642Heterogeneous type equality evidence ignored2019-07-07T18:29:20ZBen GamariHeterogeneous type equality evidence ignoredEither that or I am missing something...
Consider the following,
```hs
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
module Test where
data TypeRep (a :: k) where
TypeCon :...Either that or I am missing something...
Consider the following,
```hs
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
module Test where
data TypeRep (a :: k) where
TypeCon :: String -> TypeRep a
TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)
data TypeRepX where
TypeRepX :: TypeRep a -> TypeRepX
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
trArrow :: TypeRep (->)
trArrow = undefined
eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res
buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
case typeRepKind f of
TRFun arg _ ->
case eqTypeRep arg x of
Just HRefl ->
TypeRepX $ TypeApp f x
```
This fails with,
```
$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:38:30: error:
• Expected kind ‘TypeRep (k1 -> res) a’,
but ‘f’ has kind ‘TypeRep k a’
• In the first argument of ‘TypeApp’, namely ‘f’
In the second argument of ‘($)’, namely ‘TypeApp f x’
In the expression: TypeRepX $ TypeApp f x
• Relevant bindings include
arg :: TypeRep * arg (bound at Test.hs:35:11)
```
That is, the typechecker doesn't believe that `f`'s type (why is it saying "kind" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.
This was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).
Am I missing something here or is this a bug?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker doesn't use evidence available from pattern synonym?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Either that or I am missing something...\r\n\r\nConsider the following,\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,\r\n TypeOperators, ViewPatterns #-}\r\n\r\nmodule Test where\r\n\r\ndata TypeRep (a :: k) where\r\n TypeCon :: String -> TypeRep a\r\n TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)\r\n\r\ndata TypeRepX where\r\n TypeRepX :: TypeRep a -> TypeRepX\r\n\r\ndata (a :: k1) :~~: (b :: k2) where\r\n HRefl :: a :~~: a\r\n\r\ntrArrow :: TypeRep (->)\r\ntrArrow = undefined\r\n\r\neqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)\r\neqTypeRep = undefined\r\n\r\ntypeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k\r\ntypeRepKind = undefined\r\n\r\npattern TRFun :: forall fun. ()\r\n => forall arg res. (fun ~ (arg -> res))\r\n => TypeRep arg\r\n -> TypeRep res\r\n -> TypeRep fun\r\npattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res\r\n\r\nbuildApp :: TypeRepX -> TypeRepX -> TypeRepX\r\nbuildApp (TypeRepX f) (TypeRepX x) =\r\n case typeRepKind f of\r\n TRFun arg _ ->\r\n case eqTypeRep arg x of\r\n Just HRefl ->\r\n TypeRepX $ TypeApp f x\r\n}}}\r\n\r\nThis fails with,\r\n{{{\r\n$ ghc Test.hs -fprint-explicit-kinds\r\n[1 of 1] Compiling Test ( Test.hs, Test.o )\r\n\r\nTest.hs:38:30: error:\r\n • Expected kind ‘TypeRep (k1 -> res) a’,\r\n but ‘f’ has kind ‘TypeRep k a’\r\n • In the first argument of ‘TypeApp’, namely ‘f’\r\n In the second argument of ‘($)’, namely ‘TypeApp f x’\r\n In the expression: TypeRepX $ TypeApp f x\r\n • Relevant bindings include\r\n arg :: TypeRep * arg (bound at Test.hs:35:11)\r\n}}}\r\n\r\nThat is, the typechecker doesn't believe that `f`'s type (why is it saying \"kind\" here?), `TypeRep k a`, will unify with `TypeRep (k1 -> res) a`, despite the `TRFun` pattern match, which should have brought into scope that `k ~ (arg -> res)`.\r\n\r\nThis was tested with a recent snapshot from `ghc-8.0` (23baff798aca5856650508ad0f7727045efe3680).\r\n\r\nAm I missing something here or is this a bug?","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11648assertPprPanic, called at compiler/types/TyCoRep.hs:19322019-07-07T18:29:18ZThomas MiedemaassertPprPanic, called at compiler/types/TyCoRep.hs:1932As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:
```
patsyn/should_compile MoreEx [exit code non-0] (normal)
...As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:
```
patsyn/should_compile MoreEx [exit code non-0] (normal)
patsyn/should_compile T11224b [exit code non-0] (normal)
polykinds MonoidsTF [exit code non-0] (normal)
polykinds T11480b [exit code non-0] (normal)
polykinds T11523 [exit code non-0] (normal)
```
```
Compile failed (status 256) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160218 for x86_64-unknown-linux):
ASSERT failed!
CallStack (from HasCallStack):
assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in
ghc:TyCoRep
substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep
substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in
ghc:TcPatSyn
in_scope InScope {d_ap0 c_apv}
tenv [ap1 :-> c_apv[tau:5]]
tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]
cenv []
cenvFVs []
tys []
cos []
```
[D1951](https://phabricator.haskell.org/D1951) contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.
The offending commit is b5292557dcf2e3844b4837172230575d40a8917e.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"assertPprPanic, called at compiler/types/TyCoRep.hs:1932","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:\r\n\r\n{{{\r\n patsyn/should_compile MoreEx [exit code non-0] (normal)\r\n patsyn/should_compile T11224b [exit code non-0] (normal)\r\n polykinds MonoidsTF [exit code non-0] (normal)\r\n polykinds T11480b [exit code non-0] (normal)\r\n polykinds T11523 [exit code non-0] (normal)\r\n}}}\r\n\r\n{{{\r\nCompile failed (status 256) errors were:\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160218 for x86_64-unknown-linux):\r\nASSERT failed!\r\n CallStack (from HasCallStack):\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in\r\nghc:TyCoRep\r\n substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep\r\n substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in\r\nghc:TcPatSyn\r\n in_scope InScope {d_ap0 c_apv}\r\n tenv [ap1 :-> c_apv[tau:5]]\r\n tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]\r\n cenv []\r\n cenvFVs []\r\n tys []\r\n cos []\r\n}}}\r\n\r\nPhab:D1951 contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.\r\n\r\nThe offending commit is b5292557dcf2e3844b4837172230575d40a8917e.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11672Poor error message2019-07-07T18:29:09ZAdam GundryPoor error message[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures ...[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) -> Int
f _ = f (Proxy :: Proxy (Int -> Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((->) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy
(Int -> Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int -> Bool))’
In the expression: f (Proxy :: Proxy (Int -> Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
```
or with `-fprint-explicit-kinds -fprint-explicit-coercions`:
```
• Expected kind ‘Proxy
Symbol
(((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
- It says `kind` when it should say `type`.
- `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).
- The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki, goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1-rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskell-cafe/2016-February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) -> Int\r\nf _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((->) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int -> Bool)’ has kind ‘Proxy\r\n (Int -> Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int -> Bool))’\r\n In the expression: f (Proxy :: Proxy (Int -> Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))\r\n}}}\r\nor with `-fprint-explicit-kinds -fprint-explicit-coercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((->) |> <*>_N -> <*>_N -> U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int -> Bool)’ has kind ‘Proxy * (Int -> Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((->) Int Bool)` is printed instead of `Int -> Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} -->Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc/-/issues/11699Type families mistakingly report kind variables as unbound type variables2019-07-07T18:29:02ZmniipType families mistakingly report kind variables as unbound type variablesGHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variable...GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.
Simplest test case:
```hs
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family F a where F (f a) = f a
```
As seen on 8.0.1-rc2 and 7.10.2:
```
../File.hs:3:23:
Family instance purports to bind type variable ‘k1’
but the real LHS (expanding synonyms) is: F (f a) = ...
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
```
The culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.
Now, I'm not too sure whether this is a "GHC rejects valid program", or "Incorrect warning at compile time", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"Type families mistakingly report kind variables as unbound type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC verifies that if some equation of a type family binds a type variable, that this type variable actually exists and doesn't disappear through type synonym/family application (#7536). However this also mistakingly catches kind variables that aren't present in the type family head.\r\n\r\nSimplest test case:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, PolyKinds #-}\r\ntype family F a where F (f a) = f a\r\n}}}\r\nAs seen on 8.0.1-rc2 and 7.10.2:\r\n{{{\r\n../File.hs:3:23:\r\n Family instance purports to bind type variable ‘k1’\r\n but the real LHS (expanding synonyms) is: F (f a) = ...\r\n In the equations for closed type family ‘F’\r\n In the type family declaration for ‘F’\r\n}}}\r\n\r\nThe culprit seems to be in `exactTyCoVarsOfType`, which doesn't grab kind variables from a type variable's kind, even though `tyCoVarsOfType` does.\r\n\r\nNow, I'm not too sure whether this is a \"GHC rejects valid program\", or \"Incorrect warning at compile time\", as I'm not sure if type families like the aforementioned `F` are actually okay. (Are they?)","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11716Make TypeInType stress test work2019-07-07T18:28:57ZRichard Eisenbergrae@richarde.devMake TypeInType stress test workI used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>T...I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Make TypeInType stress test work","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I used the attached file during my job talk. It is good `TypeInType` stress test. This bug is to track several fixes that have been necessary to get it working. I have these fixes locally and will push in due course.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1