I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:

{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data Hm (k :: Type) (a :: k) :: Type

class HasName (a :: k) where
  getName :: proxy a -> String

instance HasName Hm where
  getName _ = "Hm"

This is rejected, however:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:11:18: error:
    • Expecting two more arguments to ‘Hm’
      Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
    • In the first argument of ‘HasName’, namely ‘Hm’
      In the instance declaration for ‘HasName Hm’
   |
11 | instance HasName Hm where
   |                  ^^

The culprit appears to be the fact that Hm has kind forall k -> k -> *, which uses a visible quantifier. Does this prevent partial applications of Hm? Or is this simply a GHC bug?