[GHC] #6074: Instance inference failure with GADTs

[GHC]

#6074: Instance inference failure with GADTs
---------------------------------+------------------------------------------
    Reporter:  goldfire          |       Owner:                  
        Type:  feature request   |      Status:  new             
    Priority:  normal            |   Milestone:                  
   Component:  Compiler          |     Version:  7.5             
    Keywords:  GADTs             |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |     Failure:  None/Unknown    
  Difficulty:  Unknown           |    Testcase:                  
   Blockedby:                    |    Blocking:                  
     Related:                    |  
---------------------------------+------------------------------------------

Comment(by dreixel):

 I think there's quite some interest in this feature. Ian previously
 pointed out this example:
 {{{
    data MyKind = K1 | K2

    type family F (i :: MyKind) :: *
    type instance F K1 = Int
    type instance F K2 = Bool

    data D i = D (F i)
        deriving (Data, Typeable)
 }}}
 This triggers an error:
 {{{
    3.hs:13:15:
        No instances for (Data (F i), Typeable (D i))
          arising from the 'deriving' clause of a data type declaration
        Possible fix:
          add instance declarations for (Data (F i), Typeable (D i))
          or use a standalone 'deriving instance' declaration,
               so you can specify the instance context yourself
        When deriving the instance for (Data (D i))
 }}}
 But we know what `F i` can give us for any `i :: MyKind`, and that is
 `Int` or `Bool`, both unproblematic for deriving `Data`. In particular, we
 know that the type family `F` is closed! The general question is how we
 can have the type checker take advantage of this.

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