#7961: Remove restrictions on promoting GADT's -----------------------------+---------------------------------------------- Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: #6204 -----------------------------+---------------------------------------------- (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: 1. 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. 2. 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. #6204 would complete them in another way. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler