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

 * cc: dimitris@… (added)


Comment:

 I agree with Manuel points, but I can see the attraction of Lilac's
 suggestion.  Leaving aside the exact rules, the point is that the rules
 for `LessEq` ''are'' confluent, even though more than one may apply.  I
 wonder whether this is an unusual example, or whether there are many like
 it?

 Beyond that, I think it's true that one can have two overlapping
 instances, even if their RHSs are entirely different, provided they are
 given together. Thus
 {{{
 type family F a
 type instance F [a] = Bool
 type instance F [Int] = Char
 }}}
 Now, the term `F [Char]` is unambiguously equal to `Bool`.  But `F [b]`
 can't reduce, because we don't know what `b` will be instantiated to.

 On reflection though, I was too hasty in making this suggestion yesterday.
 It might be fine for a ''source'' language, but I'm not sure how to
 express it in System FC, the ''intermediate'' language.   If we have the
 above two rules as axioms we could just compose them in sequence to get
 `Bool ~ Char` which is obvious nonsense.  The only decent approach I can
 see is for the first rule to take a proof that `a` is ''not'' `Int`, and
 that seems pretty complicated.

 So I'm not sure of the best way to proceed here.

 Simon

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