GHC Kind level

This page gives the theory and implementation overview and details about GHC's kind level. This work is related to  Conor's SHE system and will be related to Iavor's work on TypeNats to deal with primitive types.

Theory

We use the mechanism of promotion to lift a data type to the kind level. This gives access at the type level to the data constructors, and at the kind level to the type constructor. All data types cannot be promoted. For examples GADTs or data types with higher-order kinds.

Implementation

The branch is called ghc-kinds. Its current state is:

	ADT promotion	Primitives	Kind polymorphism
Parser	Yes	Yes	Yes
Renamer	In progress	Yes
Typechecker