GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:27:52Zhttps://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/15568Kind variables in type family aren't quantified in toposorted order2019-07-07T18:04:06ZRyan ScottKind variables in type family aren't quantified in toposorted orderRecently, I noticed that an error message I was experiencing differs between GHC 8.4.3 and GHC 8.6.1+. Take this program:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Proxy
import GHC.Exts...Recently, I noticed that an error message I was experiencing differs between GHC 8.4.3 and GHC 8.6.1+. Take this program:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Proxy
import GHC.Exts (Any)
type family F (a :: j) :: k
f :: Proxy a -> Proxy (F (a :: j) :: k)
f _ = Proxy :: Proxy (Any :: k)
```
On 8.4.3, you'll get:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:7: error:
• Couldn't match type ‘Any k’ with ‘F j k a’
Expected type: Proxy k (F j k a)
Actual type: Proxy k (Any k)
• In the expression: Proxy :: Proxy (Any :: k)
In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
• Relevant bindings include
f :: Proxy j a -> Proxy k (F j k a) (bound at Bug.hs:11:1)
|
11 | f _ = Proxy :: Proxy (Any :: k)
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```
But on 8.6.1 and HEAD, you'll instead get:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:7: error:
• Couldn't match type ‘Any k’ with ‘F k j a’
Expected type: Proxy k (F k j a)
Actual type: Proxy k (Any k)
• In the expression: Proxy :: Proxy (Any :: k)
In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
• Relevant bindings include
f :: Proxy j a -> Proxy k (F k j a) (bound at Bug.hs:11:1)
|
11 | f _ = Proxy :: Proxy (Any :: k)
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notice that on 8.4.3, it displays `F j k a`, but on 8.6.1, it displays `F k j a`! After some digging, it turns out that this is because on 8.6.1, the order of `F`'s kind variables are quantified completely differently! On 8.4.3, we have:
```
λ> :kind F
F :: forall j k. j -> k
```
But on 8.6.1, we have:
```
λ> :kind F
F :: forall k j. j -> k
```
I would prefer the old behavior of 8.4.3, since `j k` is what you get after performing a left-to-right, reverse topological sort on the kind variables of `F`, which is consistent with how type signatures quantify their type variables. Currently, this quirk doesn't matter that much (except for error messages, as shown above), but if/when visible kind application is implemented, it'll be more noticeable.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind variables in type family aren't quantified in toposorted order","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Recently, I noticed that an error message I was experiencing differs between GHC 8.4.3 and GHC 8.6.1+. Take this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\nimport GHC.Exts (Any)\r\n\r\ntype family F (a :: j) :: k\r\n\r\nf :: Proxy a -> Proxy (F (a :: j) :: k)\r\nf _ = Proxy :: Proxy (Any :: k)\r\n}}}\r\n\r\nOn 8.4.3, you'll get:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs -fprint-explicit-kinds\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:7: error:\r\n • Couldn't match type ‘Any k’ with ‘F j k a’\r\n Expected type: Proxy k (F j k a)\r\n Actual type: Proxy k (Any k)\r\n • In the expression: Proxy :: Proxy (Any :: k)\r\n In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)\r\n • Relevant bindings include\r\n f :: Proxy j a -> Proxy k (F j k a) (bound at Bug.hs:11:1)\r\n |\r\n11 | f _ = Proxy :: Proxy (Any :: k)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut on 8.6.1 and HEAD, you'll instead get:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs -fprint-explicit-kinds\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:7: error:\r\n • Couldn't match type ‘Any k’ with ‘F k j a’\r\n Expected type: Proxy k (F k j a)\r\n Actual type: Proxy k (Any k)\r\n • In the expression: Proxy :: Proxy (Any :: k)\r\n In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)\r\n • Relevant bindings include\r\n f :: Proxy j a -> Proxy k (F k j a) (bound at Bug.hs:11:1)\r\n |\r\n11 | f _ = Proxy :: Proxy (Any :: k)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotice that on 8.4.3, it displays `F j k a`, but on 8.6.1, it displays `F k j a`! After some digging, it turns out that this is because on 8.6.1, the order of `F`'s kind variables are quantified completely differently! On 8.4.3, we have:\r\n\r\n{{{\r\nλ> :kind F\r\nF :: forall j k. j -> k\r\n}}}\r\n\r\nBut on 8.6.1, we have:\r\n\r\n{{{\r\nλ> :kind F\r\nF :: forall k j. j -> k\r\n}}}\r\n\r\nI would prefer the old behavior of 8.4.3, since `j k` is what you get after performing a left-to-right, reverse topological sort on the kind variables of `F`, which is consistent with how type signatures quantify their type variables. Currently, this quirk doesn't matter that much (except for error messages, as shown above), but if/when visible kind application is implemented, it'll be more noticeable.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15591Inconsistent kind variable binder visibility between associated and non-assoc...2019-07-07T18:04:00ZRyan ScottInconsistent kind variable binder visibility between associated and non-associated type familiesConsider the following program and GHCi session which uses it:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: f (a :: Type))
class C (a :: Type) where
type T2 (...Consider the following program and GHCi session which uses it:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: f (a :: Type))
class C (a :: Type) where
type T2 (x :: f a)
```
```
$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall (f :: * -> *) a. f a -> *
λ> :kind T2
T2 :: forall {a} (f :: * -> *). f a -> *
```
Something is strange about the visibility of `a` in the kinds of `T1` and `T2`. In `T1`, it's visible, but in `T2`, it's not! I would expect them to both be visible, since they were both mentioned by name in each type family's definition.
This isn't of much importance at the moment, but it will be once visible kind application lands, as this bug will prevent anyone from instantiating the `a` in `T2` using a kind application.
I indicated 8.5 as the version for this ticket since this behavior has changed since GHC 8.4, where you'd get the following:
```
$ /opt/ghc/8.4.3/bin/ghci Foo.hs -fprint-explicit-foralls
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall (f :: * -> *) a. f a -> *
λ> :kind T2
T2 :: forall (f :: * -> *) a. f a -> *
```
Here, both `a`s are visible. However, it's still wrong in that `a` should be listed before `f` in `T2`'s telescope, since `a` was bound first (in `C`'s class head), before `f`. In that sense, the current behavior is a slight improvement, although we're not fully correct yet.
The only difference between `T1` and `T2` is that `T2` is associated with a class, which suggests that there is some difference in code paths between the two that is accounting for this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| 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":"Inconsistent kind variable binder visibility between associated and non-associated type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program and GHCi session which uses it:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family T1 (x :: f (a :: Type))\r\n\r\nclass C (a :: Type) where\r\n type T2 (x :: f a)\r\n}}}\r\n{{{\r\n$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls\r\nGHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :kind T1\r\nT1 :: forall (f :: * -> *) a. f a -> *\r\nλ> :kind T2\r\nT2 :: forall {a} (f :: * -> *). f a -> *\r\n}}}\r\n\r\nSomething is strange about the visibility of `a` in the kinds of `T1` and `T2`. In `T1`, it's visible, but in `T2`, it's not! I would expect them to both be visible, since they were both mentioned by name in each type family's definition.\r\n\r\nThis isn't of much importance at the moment, but it will be once visible kind application lands, as this bug will prevent anyone from instantiating the `a` in `T2` using a kind application.\r\n\r\nI indicated 8.5 as the version for this ticket since this behavior has changed since GHC 8.4, where you'd get the following:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghci Foo.hs -fprint-explicit-foralls\r\nGHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :kind T1\r\nT1 :: forall (f :: * -> *) a. f a -> *\r\nλ> :kind T2\r\nT2 :: forall (f :: * -> *) a. f a -> *\r\n}}}\r\n\r\nHere, both `a`s are visible. However, it's still wrong in that `a` should be listed before `f` in `T2`'s telescope, since `a` was bound first (in `C`'s class head), before `f`. In that sense, the current behavior is a slight improvement, although we're not fully correct yet.\r\n\r\nThe only difference between `T1` and `T2` is that `T2` is associated with a class, which suggests that there is some difference in code paths between the two that is accounting for this.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15592Type families without CUSKs cannot be given visible kind variable binders2019-07-07T18:04:00ZRyan ScottType families without CUSKs cannot be given visible kind variable bindersConsider the following program and GHCi session which uses it:
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: Type) (y :: a) :: Type where {}
type family T2 x ...Consider the following program and GHCi session which uses it:
```
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind
type family T1 (x :: Type) (y :: a) :: Type where {}
type family T2 x (y :: a) :: Type where {}
```
```
$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T1
T1 :: forall a. * -> a -> *
λ> :kind T2
T2 :: forall {k} {a}. k -> a -> *
```
Note that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not.
This isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application.
It's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type families without CUSKs cannot be given visible kind variable binders","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["CUSKs","TypeApplications,","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program and GHCi session which uses it:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family T1 (x :: Type) (y :: a) :: Type where {}\r\ntype family T2 x (y :: a) :: Type where {}\r\n}}}\r\n{{{\r\n$ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-foralls\r\nGHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :kind T1\r\nT1 :: forall a. * -> a -> *\r\nλ> :kind T2\r\nT2 :: forall {k} {a}. k -> a -> *\r\n}}}\r\n\r\nNote that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not.\r\n\r\nThis isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application.\r\n\r\nIt's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15793Type family doesn't reduce with visible kind application2019-07-07T18:02:57ZIcelandjackType family doesn't reduce with visible kind applicationIf we un-comment `f2`
```hs
{-# Language RankNTypes #-}
{-# Language TypeFamilies #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
import Data.Kind
type family
F1 (a :: Type) :: Type where
F1 a = M...If we un-comment `f2`
```hs
{-# Language RankNTypes #-}
{-# Language TypeFamilies #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
import Data.Kind
type family
F1 (a :: Type) :: Type where
F1 a = Maybe a
f1 :: F1 a
f1 = Nothing
type family
F2 :: forall (a :: Type). Type where
F2 @a = Maybe a
-- f2 :: F2 @a
-- f2 = Nothing
```
this program fails with
```
• Couldn't match kind ‘forall a1. *’ with ‘* -> *’
When matching types
F2 :: forall a. *
Maybe :: * -> *
Expected type: F2
Actual type: Maybe a
• In the expression: Nothing
In an equation for ‘f2’: f2 = Nothing
|
20 | f2 = Nothing
| ^^^^^^^
Failed, no modules loaded.
```
It also succeeds replacing `Nothing` with `undefined`
```hs
f2 :: F2 @a
f2 = undefined
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family doesn't reduce with visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"If we un-comment `f2`\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeFamilies #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ntype family\r\n F1 (a :: Type) :: Type where\r\n F1 a = Maybe a\r\n\r\nf1 :: F1 a\r\nf1 = Nothing\r\n\r\ntype family\r\n F2 :: forall (a :: Type). Type where\r\n F2 @a = Maybe a\r\n\r\n-- f2 :: F2 @a\r\n-- f2 = Nothing\r\n}}}\r\n\r\nthis program fails with\r\n\r\n{{{\r\n • Couldn't match kind ‘forall a1. *’ with ‘* -> *’\r\n When matching types\r\n F2 :: forall a. *\r\n Maybe :: * -> *\r\n Expected type: F2\r\n Actual type: Maybe a\r\n • In the expression: Nothing\r\n In an equation for ‘f2’: f2 = Nothing\r\n |\r\n 20 | f2 = Nothing\r\n | ^^^^^^^\r\n Failed, no modules loaded.\r\n}}}\r\n\r\nIt also succeeds replacing `Nothing` with `undefined`\r\n\r\n{{{#!hs\r\nf2 :: F2 @a\r\nf2 = undefined\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15797GHC panic using visible kind application2019-07-07T18:02:56ZIcelandjackGHC panic using visible kind application```hs
{-# Language RankNTypes #-}
{-# Language TypeFamilies #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds ...```hs
{-# Language RankNTypes #-}
{-# Language TypeFamilies #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Options_GHC -dcore-lint #-}
import Data.Kind
class Ríki (obj :: Type) where
type Obj :: obj -> Constraint
type Obj = Bæ @obj
class Bæ (a :: k)
instance Bæ @k (a :: k)
data
EQ :: forall ob. ob -> ob -> Type where
EQ :: EQ a a
instance
Ríki (EQ @ob)
```
```
$ ghci -dcore-lint 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 568_bug.hs, interpreted )
WARNING: file compiler/types/TyCoRep.hs, line 2567
in_scope InScope {ob_a1zs co_a1zt}
tenv []
cenv [a1zt :-> co_a1zt]
tys [Bæ]
cos []
needInScope [a1zn :-> co_a1zn, a1zs :-> ob_a1zs]
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
Core Lint error
<no location info>: warning:
In the type ‘Bæ’
Unfilled coercion hole: {co_a1zn}
<no location info>: warning:
In the type ‘Bæ’
co_a1zn :: (ob_a1zs -> ob_a1zs -> *) ~# *
[LclId[CoVarId]] is out of scope
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic using visible kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeFamilies #-}\r\n{-# Language ScopedTypeVariables #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language TypeOperators #-}\r\n{-# Language GADTs #-}\r\n\r\n{-# Options_GHC -dcore-lint #-}\r\n\r\nimport Data.Kind\r\n\r\nclass Ríki (obj :: Type) where\r\n type Obj :: obj -> Constraint\r\n type Obj = Bæ @obj\r\n\r\nclass Bæ (a :: k)\r\ninstance Bæ @k (a :: k)\r\n\r\ndata\r\n EQ :: forall ob. ob -> ob -> Type where\r\n EQ :: EQ a a\r\n\r\ninstance\r\n Ríki (EQ @ob)\r\n}}}\r\n\r\n{{{\r\n$ ghci -dcore-lint 568_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 568_bug.hs, interpreted )\r\nWARNING: file compiler/types/TyCoRep.hs, line 2567\r\n in_scope InScope {ob_a1zs co_a1zt}\r\n tenv []\r\n cenv [a1zt :-> co_a1zt]\r\n tys [Bæ]\r\n cos []\r\n needInScope [a1zn :-> co_a1zn, a1zs :-> ob_a1zs]\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n Core Lint error\r\n <no location info>: warning:\r\n In the type ‘Bæ’\r\n Unfilled coercion hole: {co_a1zn}\r\n <no location info>: warning:\r\n In the type ‘Bæ’\r\n co_a1zn :: (ob_a1zs -> ob_a1zs -> *) ~# *\r\n [LclId[CoVarId]] is out of scope\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15801"ASSERT failed!" with visible kind applications2019-07-07T18:02:55ZIcelandjack"ASSERT failed!" with visible kind applicationsSorry for the workload mnguyen. This gives a very short error (using diff for visible kind application: https://phabricator.haskell.org/D5229)
```hs
{-# Language CPP #-}
{-# Language QuantifiedConstraints #-}
{-# Langu...Sorry for the workload mnguyen. This gives a very short error (using diff for visible kind application: https://phabricator.haskell.org/D5229)
```hs
{-# Language CPP #-}
{-# Language QuantifiedConstraints #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language TypeOperators #-}
{-# Language DataKinds #-}
{-# Language TypeFamilies #-}
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language UndecidableInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleContexts #-}
import Data.Coerce
import Data.Kind
type Cat ob = ob -> ob -> Type
type Obj = Type
class Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
instance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
class (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
instance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
class
Ríki (obj :: Obj) where
type (-->) :: obj -> obj -> Type
ið :: a --> (a::obj)
class
OpOpNoOp obj
=>
OpRíki (obj :: Obj) where
type (<--) :: obj -> obj -> Type
data Op a = Op a
type family UnOp op where UnOp ('Op obj) = obj
newtype Y :: Cat (Op a) where
Y :: (UnOp b --> UnOp a) -> Y a b
instance Ríki Type where
type (-->) = (->)
ið x = x
instance OpRíki (Op Type) where
type (<--) @(Op Type) = Y @Type
```
```
$ ghci -ignore-dot-ghci 577.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 577.hs, interpreted )
*** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line 1285
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"\"ASSERT failed!\" with visible kind applications","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"Sorry for the workload mnguyen. This gives a very short error (using diff for visible kind application: https://phabricator.haskell.org/D5229)\r\n\r\n{{{#!hs\r\n{-# Language CPP #-}\r\n{-# Language QuantifiedConstraints #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language TypeOperators #-}\r\n{-# Language DataKinds #-}\r\n{-# Language TypeFamilies #-}\r\n{-# Language TypeSynonymInstances #-}\r\n{-# Language FlexibleInstances #-}\r\n{-# Language GADTs #-}\r\n{-# Language UndecidableInstances #-}\r\n{-# Language MultiParamTypeClasses #-}\r\n{-# Language FlexibleContexts #-}\r\n\r\nimport Data.Coerce\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ntype Obj = Type\r\n\r\nclass Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)\r\ninstance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)\r\n\r\nclass (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj\r\ninstance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj\r\n\r\nclass\r\n Ríki (obj :: Obj) where\r\n type (-->) :: obj -> obj -> Type\r\n\r\n ið :: a --> (a::obj)\r\n\r\nclass\r\n OpOpNoOp obj\r\n =>\r\n OpRíki (obj :: Obj) where\r\n type (<--) :: obj -> obj -> Type\r\n\r\ndata Op a = Op a\r\n\r\ntype family UnOp op where UnOp ('Op obj) = obj\r\n\r\nnewtype Y :: Cat (Op a) where\r\n Y :: (UnOp b --> UnOp a) -> Y a b\r\n\r\ninstance Ríki Type where\r\n type (-->) = (->)\r\n ið x = x\r\n\r\ninstance OpRíki (Op Type) where\r\n type (<--) @(Op Type) = Y @Type\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 577.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 577.hs, interpreted )\r\n*** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line 1285\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15807GHC panic with visible kind applications2019-07-07T18:02:54ZIcelandjackGHC panic with visible kind applicationsUsing the https://phabricator.haskell.org/D5229 diff
This is **fine**
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data...Using the https://phabricator.haskell.org/D5229 diff
This is **fine**
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data
App :: forall (f :: Type -> Type). Type -> Type
where
MkApp :: f a -> App @f a
```
Kind polymorphic is **fine**
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data
App :: forall k (f :: k -> Type). k -> Type
where
MkApp :: f a -> App @k @(f :: k -> Type) (a :: k)
```
But offing the visibility of `k` **fails**
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data
App :: forall (f :: k -> Type). k -> Type
where
MkApp :: f a -> App @(f :: k -> Type) (a :: k)
```
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data
App :: forall (f :: k -> Type). k -> Type
where
MkApp :: f a -> App @f a
```
```
$ ghci -ignore-dot-ghci 581_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 581_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
2
1
f_a1yB[tau:1]
f_a1yx[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:778:54 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic with visible kind applications","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"Using the https://phabricator.haskell.org/D5229 diff\r\n\r\nThis is '''fine'''\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata\r\n App :: forall (f :: Type -> Type). Type -> Type\r\n where\r\n MkApp :: f a -> App @f a\r\n}}}\r\n\r\nKind polymorphic is '''fine'''\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata\r\n App :: forall k (f :: k -> Type). k -> Type\r\n where\r\n MkApp :: f a -> App @k @(f :: k -> Type) (a :: k)\r\n}}}\r\n\r\nBut offing the visibility of `k` '''fails'''\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata\r\n App :: forall (f :: k -> Type). k -> Type\r\n where\r\n MkApp :: f a -> App @(f :: k -> Type) (a :: k)\r\n}}}\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata\r\n App :: forall (f :: k -> Type). k -> Type\r\n where\r\n MkApp :: f a -> App @f a\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 581_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 581_bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n ASSERT failed!\r\n 2\r\n 1\r\n f_a1yB[tau:1]\r\n f_a1yx[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:778:54 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15816Visible kind applications + data family: `U :: Type' said to be of kind `k0 -...2019-07-07T18:02:52ZIcelandjackVisible kind applications + data family: `U :: Type' said to be of kind `k0 -> k1` in error messageUsing the [visible kind applications (D5229)](https://phabricator.haskell.org/D5229) (#12045) patch.
GHC erroneously calls `U :: Type` a "function" of kind `k0 -> k1` if I understand this right,
```
$ ghci
GHCi, version 8.7.20181017: ...Using the [visible kind applications (D5229)](https://phabricator.haskell.org/D5229) (#12045) patch.
GHC erroneously calls `U :: Type` a "function" of kind `k0 -> k1` if I understand this right,
```
$ ghci
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
Prelude> :set prompt "> "
> import Data.Kind (Type)
>
> :set -XTypeFamilies
> :set -XTypeApplications
>
> data family U :: Type
> data instance U @Int
<interactive>:7:1: error:
• Cannot apply function of kind ‘k0 -> k1’
to visible kind argument ‘Int’
• In the data instance declaration for ‘U’
>
```
I expect something like "Cannot apply type `U` to visible kind argument `Int`" or
```
> data instance U Int = MkU
<interactive>:7:1: error:
• Expected kind ‘* -> *’, but ‘U’ has kind ‘*’
• In the data instance declaration for ‘U’
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.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":"Visible kind applications + data family: `U :: Type' said to be of kind `k0 -> k1` in error message","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Using the [https://phabricator.haskell.org/D5229 visible kind applications (D5229)] (#12045) patch.\r\n\r\nGHC erroneously calls `U :: Type` a \"function\" of kind `k0 -> k1` if I understand this right,\r\n\r\n{{{\r\n$ ghci \r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set prompt \"> \"\r\n> import Data.Kind (Type)\r\n>\r\n> :set -XTypeFamilies \r\n> :set -XTypeApplications\r\n>\r\n> data family U :: Type\r\n> data instance U @Int\r\n\r\n<interactive>:7:1: error:\r\n • Cannot apply function of kind ‘k0 -> k1’\r\n to visible kind argument ‘Int’\r\n • In the data instance declaration for ‘U’\r\n> \r\n}}}\r\n\r\nI expect something like \"Cannot apply type `U` to visible kind argument `Int`\" or\r\n\r\n{{{\r\n> data instance U Int = MkU\r\n\r\n<interactive>:7:1: error:\r\n • Expected kind ‘* -> *’, but ‘U’ has kind ‘*’\r\n • In the data instance declaration for ‘U’\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/16255Visible kind application defeats type family with higher-rank result kind2019-07-07T18:00:47ZRyan ScottVisible kind application defeats type family with higher-rank result kindAfter #15740, GHC now (correctly) rejects this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Dat...After #15740, GHC now (correctly) rejects this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
data SBool :: Bool -> Type
type family F :: forall k. k -> Type where
F = SBool
```
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:7: error:
• Expected kind ‘forall k. k -> *’,
but ‘SBool’ has kind ‘Bool -> *’
• In the type ‘SBool’
In the type family declaration for ‘F’
|
12 | F = SBool
| ^^^^^
```
However, there's a very simple way to circumvent this: add a visible kind application to `F`'s equation.
```hs
type family F :: forall k. k -> Type where
F @Bool = SBool
```
If I understand things correctly, GHC shouldn't allow this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| 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":"Visible kind application defeats type family with higher-rank result kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeApplications,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"After #15740, GHC now (correctly) rejects this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata SBool :: Bool -> Type\r\ntype family F :: forall k. k -> Type where\r\n F = SBool\r\n}}}\r\n{{{\r\n$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:12:7: error:\r\n • Expected kind ‘forall k. k -> *’,\r\n but ‘SBool’ has kind ‘Bool -> *’\r\n • In the type ‘SBool’\r\n In the type family declaration for ‘F’\r\n |\r\n12 | F = SBool\r\n | ^^^^^\r\n}}}\r\n\r\nHowever, there's a very simple way to circumvent this: add a visible kind application to `F`'s equation.\r\n\r\n{{{#!hs\r\ntype family F :: forall k. k -> Type where\r\n F @Bool = SBool\r\n}}}\r\n\r\nIf I understand things correctly, GHC shouldn't allow this.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1