[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            |   Milestone:                  
   Component:  Compiler          |     Version:  7.6.3           
    Keywords:                    |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |     Failure:  None/Unknown    
  Difficulty:  Unknown           |    Testcase:                  
   Blockedby:                    |    Blocking:                  
     Related:  #6204             |  
---------------------------------+------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Old description:

> (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.

New description:

 (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. #6024 would complete them in another
 way.

--

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7961#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler