GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:29:02Zhttps://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.1https://gitlab.haskell.org/ghc/ghc/-/issues/11719Cannot use higher-rank kinds with type families2019-07-07T18:28:55ZOllie CharlesCannot use higher-rank kinds with type familiesThis ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * ...This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html
Here's the code that should work, but doesn't:
```hs
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
type family (f :: a ~> b) @@ (x :: a) :: b
data Null a = Nullable a | NotNullable a
type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where
(f ∘ g) x = f @@ (g @@ x)
type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(
-- BaseType k x = (@@) k x
```8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/11732Deriving Generic1 interacts poorly with TypeInType2019-07-07T18:28:52ZRichard Eisenbergrae@richarde.devDeriving Generic1 interacts poorly with TypeInTypeFrom \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiate...From \@RyanGlScott, [ticket:11357\#comment:117922](https://gitlab.haskell.org//ghc/ghc/issues/11357#note_117922):
Vanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered "instantiated" in a `Generic1` instance. For instance, this is rejected:
```
λ> data Proxy k (a :: k) = ProxyCon deriving Generic1
```
```
<interactive>:32:43: error:
• Can't make a derived instance of ‘Generic1 (Proxy *)’:
Proxy must not be instantiated; try deriving `Proxy k a' instead
• In the data declaration for ‘Proxy’
```
And rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!
```
λ> data family ProxyFam (a :: y) (b :: z)
λ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1
==================== Derived instances ====================
Derived instances:
instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where
...
```
\[Ryan needs\] to investigate further to see why this is the case.
<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":"Deriving Generic1 interacts poorly with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Generics","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From @RyanGlScott, comment:9:ticket:11357:\r\n\r\nVanilla datatypes and data family instances are still inconsistent w.r.t. which type variables are considered \"instantiated\" in a `Generic1` instance. For instance, this is rejected:\r\n\r\n{{{\r\nλ> data Proxy k (a :: k) = ProxyCon deriving Generic1\r\n}}}\r\n\r\n{{{\r\n<interactive>:32:43: error:\r\n • Can't make a derived instance of ‘Generic1 (Proxy *)’:\r\n Proxy must not be instantiated; try deriving `Proxy k a' instead\r\n • In the data declaration for ‘Proxy’\r\n}}}\r\n\r\nAnd rightfully so, since the visible kind binder `k` is instantiated to `*`. But now it's possible to have an equivalent instance for a data family that squeaks past this check!\r\n\r\n{{{\r\nλ> data family ProxyFam (a :: y) (b :: z)\r\nλ> data instance ProxyFam k (a :: k) = ProxyFamCon deriving Generic1\r\n\r\n==================== Derived instances ====================\r\nDerived instances:\r\n instance GHC.Generics.Generic1 (Ghci13.ProxyFam *) where\r\n ...\r\n}}}\r\n\r\n[Ryan needs] to investigate further to see why this is the case. ","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11754Error in optCoercion2019-07-07T18:28:42ZSimon Peyton JonesError in optCoercionThis program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x...This program fails Lint after a run of the simplifier.
```hs
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures, TypeFamilies, FlexibleContexts #-}
module T11728a where
import Data.Kind
import Data.Void
newtype K a x = K a
newtype I x = I x
data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x
class Differentiable (D f) => Differentiable f where
type D (f :: Type -> Type) :: Type -> Type
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ + f₂) where
type D (f₁ + f₂) = D f₁ + D f₂
instance (Differentiable f₁, Differentiable f₂) => Differentiable (f₁ × f₂) where
type D (f₁ × f₂) = (D f₁ × f₂) + (f₁ × D f₂)
```
Originally reported in #11728, but it's a totally different problem.
Richard has nailed it already... patch coming from him.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11785Merge types and kinds in Template Haskell2019-07-07T18:28:33ZRichard Eisenbergrae@richarde.devMerge types and kinds in Template Haskell!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---...!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/11811GHC sometimes misses a CUSK2019-07-07T18:28:26ZRichard Eisenbergrae@richarde.devGHC sometimes misses a CUSK```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the...```
{-# LANGUAGE TypeInType #-}
data Test (a :: x) (b :: x) :: x -> *
where K :: Test Int Bool Double
```
fails, because GHC thinks that `Test` does not have a CUSK.
It should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.
Fix en route.
<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":"GHC sometimes misses a CUSK","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\n\r\ndata Test (a :: x) (b :: x) :: x -> *\r\n where K :: Test Int Bool Double\r\n}}}\r\n\r\nfails, because GHC thinks that `Test` does not have a CUSK.\r\n\r\nIt should have a CUSK, because while there is no `forall x` in the result kind, the `x` is in scope from previous use in kinds.\r\n\r\nFix en route.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11821Internal error: not in scope during type checking, but it passed the renamer2019-07-07T18:28:23ZdarchonInternal error: not in scope during type checking, but it passed the renamerWhile trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope....While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/11963GHC introduces kind equality without TypeInType2019-07-07T18:28:14ZEdward Z. YangGHC introduces kind equality without TypeInTypeThe following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a ...The following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<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 | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11964Without TypeInType, inconsistently accepts Data.Kind.Type but not type synonym2019-07-07T18:28:14ZEdward Z. YangWithout TypeInType, inconsistently accepts Data.Kind.Type but not type synonymFor convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`...For convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `-XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc-8.0 --interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `-TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11966Surprising behavior with higher-rank quantification of kind variables2019-07-07T18:28:13ZOllie CharlesSurprising behavior with higher-rank quantification of kind variablesSorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANG...Sorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/11995Can't infer type2019-07-07T18:28:05ZIcelandjackCan't infer type```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → N...```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.201604198.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/12029Notify user to import * from Data.Kind with TypeInType on2019-07-07T18:27:55ZIcelandjackNotify user to import * from Data.Kind with TypeInType onWith `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must impo...With `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set -XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a -> a -> a
...
-- Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | GHCi |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set -XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a -> a -> a\r\n ...\r\n -- Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/12030GHCi Proposal: Display (Data.Kind.)Type instead of *2019-07-07T18:27:55ZIcelandjackGHCi Proposal: Display (Data.Kind.)Type instead of *This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) ...This is premature but what the darn,
```
>>> :kind Maybe
Maybe :: Type -> Type
>>> :kind StateT
StateT :: Type -> (Type -> Type) -> Type -> Type
>>> :kind Eq
Eq :: Type -> Constraint
>>> :info Functor
class Functor (f :: Type -> Type) where
...
```
`*` throws students off in my experience, makes it seem scarier than it is. Symbols are harder to search for and understand without documentation, `Type` on the other hand is descriptive.
There are arguments against:
1. It's a recent feature that is subject to change.
1. `*` is established in questions online, educational material, logs and blogs.
1. `Type` is not in scope by default: user cannot query GHCi.
`*` is established and searching for “Haskell asterisk” yields a lot resources but [‘\*’ is also a wildcard](https://support.google.com/websearch/answer/2466433?hl=en) in Google and ignored by GitHub. With time `Type` would be a good search term but currently it's chicken-and-the-egg.
Previous versions of GHCi error on `:kind *` and `:info *` only shows multiplication so that wouldn't be a huge difference but we can qualify by default:
```
>>> :kind Maybe
Maybe :: Data.Kind.Type -> Data.Kind.Type
>>> :kind StateT
StateT :: Data.Kind.Type -> (Data.Kind.Type -> Data.Kind.Type) -> Data.Kind.Type -> Data.Kind.Type
>>> :kind Eq
Eq :: Data.Kind.Type -> Constraint
>>> :info Functor
class Functor (f :: Data.Kind.Type -> Data.Kind.Type) where
...
```
or display `*` normally and only when `TypeInType` is set do we display `Type`. I don't love it (and love `GHC.Types.Type` slightly less) but there is a precedent for unqualified names, browsing the Prelude for example:
```hs
($) ::
forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
(a -> b) -> a -> b
undefined ::
forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
```
__If__ the consensus is that this will happen sometime down the line consider that each passing release means many more books and blog posts get written using `*`.
I wasn't planning on resulting to scare tactics but [here we are](https://www.peoria.com/spaw/spawimages/members/member60763/shoot_this_dog.jpg)...
----
If needed a migration plan can be drafted like the Semigroup/FTP/AMP/BBP/MonadFail/expanding Float/... proposals, possibly culminating in `Type` fully replacing `*` and being imported by default. I'm sure there are some further reaching consequences to this and better arguments against.8.6.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/12045Visible kind application2019-07-07T18:27:52ZIcelandjackVisible kind applicationI've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -...I've wanted this for a while
```
ghci> :kind (:~:)
(:~:) :: k -> k -> Type
```
```
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type
ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type
```
Working like
```
ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
```
```
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeApplications","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I've wanted this for a while\r\n\r\n{{{\r\nghci> :kind (:~:)\r\n(:~:) :: k -> k -> Type\r\n}}}\r\n\r\n{{{\r\nghci> :kind (:~:) @(Type -> Type)\r\n(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) []\r\n(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type\r\n\r\nghci> :kind (:~:) @(Type -> Type) [] Maybe\r\n(:~:) @(Type -> Type) [] Maybe :: Type\r\n}}}\r\n\r\nWorking like\r\n\r\n{{{\r\nghci> type Same k (a::k) (b::k) = a :~: b\r\nghci> :kind Same\r\nSame :: forall k -> k -> k -> *\r\n}}}\r\n\r\n{{{\r\nghci> :kind Same (Type -> Type)\r\nSame (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) []\r\nSame (Type -> Type) [] :: (Type -> Type) -> *\r\nghci> :kind Same (Type -> Type) [] Maybe\r\nSame (Type -> Type) [] Maybe :: *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1My NguyenMy Nguyenhttps://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/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/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/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/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.