[GHC] #11080: Open data kinds

[GHC]

#11080: Open data kinds
-------------------------------------+-------------------------------------
        Reporter:  dmcclean          |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler          |              Version:
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Simon PJ, Stephanie Weirich, Andres Löh, Kenny Foner, and I discussed this
 recently, and we didn't spot any problems with the proposal, neither in
 terms of theory nor implementation.

 * Question: can open kinds be parameterized? Answer: Yes. Example:
 {{{
 data open Dimension :: *
 data constructor Length :: Dimension
 data open Unit :: Dimension -> *
 data constructor Meter :: Unit 'Length
 data constructor Foot :: Unit 'Length
 }}}

 * Alternative syntax: `data constructor` is noisy. Just omit, allowing a
 declaration like `Length :: Dimension`. Objection: this overlaps with a
 naked top-level Template Haskell splice.

 * Alternative syntax: `data constructor` is noisy. How about this:
 {{{
 data open Unit :: *
 data extension Unit where
   Meter :: Unit
   Foot :: Unit
 }}}
     My (Richard's) objection: But this grouping of `Meter` and `Foot` is
 meaningless. Breaking up the group is the same as grouping. It's just
 syntactic. But this isn't a hard objection if others like the idea.

 * Related topic: What about other design points as explored in
 comment:6:ticket:9840? In particular, how does this relate to non-
 generative, non-injective symbols whose equational theory is given by a
 plugin? (Non-generative, non-injective symbols whose equational theory is
 given by GHC are known as type families.) Defining such a symbol was the
 point of #9840 to begin with, and we settled on an empty closed type
 family as the nearest approximation. After some discussion, it seemed that
 the open kind proposal was separate enough that these don't need to be
 considered together. But a suggestion for a unifying syntax would be
 welcome!

 Bottom line: let's do it, once we decide on a syntax. I still favor the
 syntax proposed, with `data constructor`. Other opinions are welcome.

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