Remove restrictions on promoting GADT's
(Also allow the promotion of data types whose kind is not (* -> ... -> *))
I have been using -XDataKinds lately to explore the sorts of dependently typed programming that are currently possible in GHC. I am particularly interested in DSL's and embedding other languages' type systems into Haskell so that GHC can help verify the correctness of the program fragments I construct for those languages. From my point of view as an end-user, the restrictions on what data get promoted is inconsistent and oftentimes annoying to deal with. There are two related issues on my end:
- The restriction that a data type cannot have a kind mentioning a promoted kind means that the way I stratify my type machinery impacts whether or not GHC will promote everything as I would like.
- The inability to use promoted GADT's forces me to encode relationships between my type building blocks in trickier ways, and sometimes I am simply unable to come up with an alternative.
I have found that these issues get in my way as a programmer of modest skill. Oftentimes I will explore a particular design but be forced to abandon it because my "natural" line of reasoning runs into GHC's restrictions. With sufficient cleverness you can do quite a lot of impressive stuff with the current system, but I am often not sufficiently clever nor am I equipped to determine when something is outright impossible.
Lifting these restriction, from my point of view, would simplify the machinery a great deal and allow me to do type-level programming that is currently out of my reach. It would make the kind extensions more uniform and more complete to us end-users. #6024 would complete them in another way.