[GHC] #1968: data family + GADT: not implemented yet

[GHC]

#1968: data family + GADT: not implemented yet
---------------------------------------------------+------------------------
    Reporter:  Remi                                |        Owner:  chak            
        Type:  bug                                 |       Status:  new             
    Priority:  normal                              |    Milestone:  6.10 branch     
   Component:  Compiler (Type checker)             |      Version:  6.9             
    Severity:  normal                              |   Resolution:                  
    Keywords:  data type family GADT choose_univs  |   Difficulty:  Moderate (1 day)
    Testcase:  GADT13                              |           Os:  Unknown/Multiple
Architecture:  Unknown/Multiple                    |  
---------------------------------------------------+------------------------
Changes (by jeltsch):

 * cc: g9ks157k at acme.softbase.org (added)

Comment:

 Replying to [comment:4 chak]:
 > What do you mean by "varying non-instance type"?  Whether you write
 > {{{data family Blah x y :: *}}} or {{{data family Blah x :: * -> *}}}
 > makes no difference whatsoever for data families.

 I think it ''does'' make a difference if you use associated types.
 Consider this:
 {{{
 {-# LANGUAGE TypeFamilies, GADTs #-}

 class C t where

     data D t :: * -> *

 instance C Bool where

     data D Bool Int = A
 }}}
 This doesn’t work, since the compiler expects a type variable at the place
 of the {{{Int}}}.  Even more, you cannot introduce another constructor
 which constructs a {{{D Bool Char}}}, for example. With GADT syntax
 allowed in data family instance declarations, you could write the
 following:
 {{{
 {-# LANGUAGE TypeFamilies, GADTs #-}

 class C t where

     data D t :: * -> *

 instance C Bool where

     data D Bool where

         A :: D Bool Int

         B :: D Bool Char
 }}}
 This code would also be different to declaring two different data family
 instances ({{{D Bool Int}}} and {{{D Bool Char}}}) in that it makes it
 impossible to introduce, say, a {{{D Bool Double}}} instance later. This
 might be exactly what a library designer wants

 I’d like to be able to use GADTs as data family instances for both of the
 above reasons. I think, I’d have good use for them.

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