'Kind' of confused about forall in type-indexed GADTs

Question

I've run into an odd situation in GHC 8.0.1 with kind-indexed (?) GADTs where introducing foralls in the type vs kind signatures produces different type-checking behaviors.

Consider the following data types:

{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-}
-- Same thing happens when we replace ExplicitForAll with ScopedTypeVariables

import Data.Kind

data F (k :: * -> *) where

data G :: F k -> * where
  G :: G x

This data type compiles just fine. However, if we want to specify the kind of x in the constructor G, we get a type error.

data H :: F k -> * where
  H :: forall k' (x :: F k'). H x

The error message is

• Kind variable ‘k’ is implicitly bound in datatype
  ‘H’, but does not appear as the kind of any
  of its type variables. Perhaps you meant
  to bind it (with TypeInType) explicitly somewhere?
• In the data declaration for ‘H’

If we add the forall to the kind signature (with or without the forall in the constructor), there is no error.

data I :: forall k. F k -> * where
  I :: I x

data J :: forall k. F k -> * where
  J :: forall k' (x :: F k'). J x

What's going on?

Answer 1

Author of TypeInType here. K. A. Buhr gets it right above; this is just a bug. It's fixed in HEAD.

For the overly curious: this error message is meant to eliminate definitions like

data J = forall (a :: k). MkJ (Proxy a)

where

data Proxy (a :: k) = Proxy

can be imported from Data.Proxy. When declaring a datatype in Haskell98-style syntax, any existentially quantified variables must be explicitly brought into scope with a forall. But k is never brought into scope explicitly; it is just used in the kind of a. So that means that k should be universally quantified (in other words, it should be an invisible parameter to J, like the k parameter to Proxy)... but then when we write J, there is no way to determine what k should be, so it would always be ambiguous. (In contrast, we can discover the choice for the k parameter to Proxy by looking at a's kind.)

This definition for J is disallowed in 8.0.1 and in HEAD.