'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?

It looks as if the former declares F k to be fixed for the whole declaration, while the latter allows H to be used in its own declaration at different kinds. I.e. it allows polykinded recursion. Could be similar to the "parameters vs indices" distinction in inductive types (as in Agda/Coq). — chi
Looks like this might be a (recently fixed) compiler bug. I can duplicate your error message with "ghc-8.0.1" but it compiles fine with "ghc-8.0.1.20161117", the latest version that "stack" decided to install for me (and which seems to be a release candidate for 8.0.2). — K. A. Buhr
@chi: I don't think that's it, for two reasons. First, because you can't refer to k in the constructor: data H' :: F k -> * where H' :: forall (x :: F k). H' x produces the same error as H. And second, because my understanding is that GHC doesn't have a parameter/index distinction, not even with TypeInType :-) — Antal Spector-Zabusky
@AntalSpector-Zabusky, GHC does make that distinction, but it's not syntactic. Rather, it infers whether an argument is "GADT-like" (an index) or not (a parameter). — dfeuer

Richard Eisenberg Richard Eisenberg · Accepted Answer · 2016-12-11T18:56:55

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.

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

1 Answers