Type families without CUSKs cannot be given visible kind variable binders

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.

Trac metadata

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