GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:04:00Zhttps://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.1