[GHC] #6150: Nested instances

[GHC]

#6150: Nested instances
------------------------------+---------------------------------------------
 Reporter:  exFalso           |          Owner:                              
     Type:  feature request   |         Status:  new                         
 Priority:  normal            |      Component:  Compiler                    
  Version:  7.4.1             |       Keywords:  DataKinds, typeclass, nested
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple            
  Failure:  None/Unknown      |       Testcase:                              
Blockedby:                    |       Blocking:                              
  Related:                    |  
------------------------------+---------------------------------------------
 With the introduction of DataKinds it became possible to define class
 instances that cover all type constructors of a kind:

 {{{
 class SomeClass (b :: Bool) where
   boolStr :: Proxy b -> String
 instance SomeClass 'True where
   boolStr _ = "True"
 instance SomeClass 'False where
   boolStr _ = "False"
 }}}

 It is clear that all types of kind 'Bool are instances of SomeClass.
 However the compiler doesn't know about this, and we always have to put a
 class restriction on a function that wants to use SomeClass, which is
 quite superfluous.

 {{{
 printBool :: (SomeClass b) => Proxy (b :: Bool) -> IO ()
 printBool = putStrLn . boolStr
 }}}

 If we had an instance like this:

 {{{
 instance SomeClass (b :: 'Bool) where
   {...}
 }}}

 then the restriction would not be needed. So I think a consistent way of
 handling this would be to create "nested" instances:

 {{{
 instance SomeClass (b :: 'Bool) where
   instance SomeClass 'True where
     boolStr _ = "True"
   instance SomeClass 'False where
     boolStr _ = "False"
 }}}

 An instance body could therefore either be the list of function
 definitions, or a list of sub-instances.
 This would also ensure that all relevant instances are defined in the same
 module.
 The nesting could be of arbitrary depth which would allow the handling of
 more complicated cases:

 {{{
 instance SomeOtherClass (bs :: [Bool]) where
   instance SomeOtherClass '[] where
     {...}
   instance SomeOtherClass (b ': bs) where
     instance SomeOtherClass ('True ': bs) where
       {...}
     instance SomeOtherClass ('False ': bs) where
       {...}
 }}}

 The compiler's job would be to essentially check that all type "patterns"
 are matched.

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