[GHC] #7961: Remove restrictions on promoting GADT's

[GHC]

#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