Hi everyone, The proposal is about adding support for dependent quantification to kind signatures: https://github.com/ghc-proposals/ghc-proposals/pull/81 Consider the following declaration (example lifted from the proposal): data T k (a :: k) GHC accepts this but it can't be given an explicit kind. Internally, it is assigned a kind which is rendered as forall k -> k -> * but this isn't accepted in source code. Note that in applications of T, k must be specified explicitly (e.g., T Type Int) which is why T does *not* have the kind forall k. k -> * Moreover, k is mentioned later in the kind which is why something like Type -> k -> * doesn't work, either. The proposal is to allow forall k -> k -> * and similar kinds to appear in source code. This is actually intended as the first in a series of proposals driving us towards dependent types in Haskell as described in Richard's thesis (https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf). Ultimately, the intention is to have all of the following (cf. Chapter 4 of the thesis): forall a. t forall a -> t pi a. t pi a -> t Here, forall and pi express relevance (does it exist at runtime) and . and -> express visibility (does it have to be specified explicitly). Because of this, my recommendation is to strongly encourage the author to submit an extended proposal which reserves (but doesn't specify the semantics of) the above syntax wholesale. This would allow us to ensure that various bits of Dependent Haskell use consistent syntax and language extensions once implemented. I find it quite difficult to discuss just this specific bit of syntax in isolation. Indeed, the public discussion was rather confused without an explanation of the roadmap (https://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-33689292...). Alternatively, we could just agree on the roadmap ourselves, without public discussion. This would somewhat circumvent the process, though. If we decide to discuss just the proposal as is, though, then I'd be weakly against the proposed syntax as it is too subtle for my taste and abuses familiar mathematical notation somewhat. I'd probably prefer something like: type a -> t The proposal also doesn't specify what language extension would turn on support for the syntax so this would have to be rectified. Thanks, Roman