[GHC] #4259: Relax restrictions on type family instance overlap

[GHC]

#4259: Relax restrictions on type family instance overlap
----------------------------------------+-----------------------------------
    Reporter:  lilac                    |       Owner:                  
        Type:  feature request          |      Status:  new             
    Priority:  normal                   |   Milestone:  7.6.2           
   Component:  Compiler (Type checker)  |     Version:  6.12.1          
    Keywords:                           |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple         |     Failure:  None/Unknown    
  Difficulty:                           |    Testcase:                  
   Blockedby:                           |    Blocking:                  
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by goldfire):

 The implementation of ordered type family instances is complete, and
 pushed to HEAD. A brief description of how it all works can be found
 [http://typesandkinds.wordpress.com/2012/12/22/ordered-overlapping-type-
 family-instances/ here]. In the process of writing this extension to type
 families, a lot of the issues discussed in this bug report came up,
 unfortunately without much resolution.

 Because getting the overlap discussed here working with ordered overlap is
 delicate (we weren't quite sure how to do it and retain type soundness),
 ordered overlap and confluent overlap do not currently mix. Specifically,
 any instance declared with the {{{type instance where}}} syntax may not
 have confluent overlap with any other instance. It's conceivable that
 there is a way to make it all work together, but it's nontrivial, and
 without a compelling reason to do it, the feature may not be worth the
 implementation complexity.

 It has also become clear that the ideas leading to this thread have a more
 general setting than just allowing for relaxed overlap restrictions. For
 example, given a type family for {{{And}}}, we may want GHC to be able to
 simplify {{{And x y ~ True}}} to {{{(x ~ True, y ~ True)}}}... but this is
 certainly not straightforward type family simplification. I'm still not
 quite sure what the solution is, but my thought is that simply relaxed
 restrictions on overlap will be 1) hard to do right and 2) not quite
 enough power anyway.

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