[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.8.1           
   Component:  Compiler (Type checker)  |     Version:  6.12.1          
    Keywords:                           |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple         |     Failure:  None/Unknown    
  Difficulty:  Unknown                  |    Testcase:                  
   Blockedby:                           |    Blocking:                  
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by carter):

 Replying to [comment:23 goldfire]:

 > 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.


 being able to "prove" (And x y) ~ True ---> (x~ True,y~True), and other
 things like it, that seems like it'd be a generalization of whats needed
 for Injective type families, right?

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