[ghc-steering-committee] Proposal: Define Kinds Without Promotion (#106)

[Eric Seidel]

Hi everyone!

This proposal would allow the declaration of new kinds and type constructors, without the associated data constructors that would have been generated by -XDataKinds.

https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0000-type-data.rst

It introduces a new language extension, -XTypeData, which allows declarations like the following:

  type data Universe = Character | Number | Boolean

This introduces a new kind, Universe, with three associated type constructors

  Character :: Universe
  Number :: Universe
  Boolean :: Universe

Notably, no data constructors are introduced.

The proposal aims to solve several usability issues with -XDataKinds:

1. We often don't want the data constructors, which simply pollute the value namespace.
2. We cannot easily control the export behavior of promoted types (instead we resort to tricks like the alias `type Character = 'Character`).
3. The name resolution rules involving promoted types can be confusing.

I find these issues (particularly #2) compelling, and the community response seems to be mostly positive, so I recommend accepting the proposal. 

I'm not particularly fond of the proposed syntax (`type data` makes it sound like we're doing something with data constructors, which is precisely what we're NOT doing), but the proposal has already had a good bit of bikeshedding, and people seem mostly happy with the current syntax, so I think we should probably stick with `type data`.

Eric