#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