[GHC] #2157: Equality Constraints with Type Families

[GHC]

#2157: Equality Constraints with Type Families
----------------------------------------+-----------------------------------
    Reporter:  hpacheco                 |        Owner:  chak    
        Type:  feature request          |       Status:  new     
    Priority:  normal                   |    Milestone:          
   Component:  Compiler (Type checker)  |      Version:  6.9     
    Severity:  normal                   |   Resolution:          
    Keywords:                           |     Testcase:          
Architecture:  Multiple                 |           Os:  Multiple
----------------------------------------+-----------------------------------
Changes (by chak):

  * owner:  => chak
  * type:  bug => feature request
  * os:  Unknown => Multiple
  * component:  Compiler => Compiler (Type checker)
  * architecture:  Unknown => Multiple

Comment:

 I'd like to find a solution here, but as far as I can see, there is no bug
 in GHC's type checker.  In fact, if GHC would admit any of your code, it
 would also allow programs that are not type safe.

 In particular, given your second definition,
 {{{
 type family F a x :: *
 }}}
 if we would allow partial applications, as in `Functor (F a)`, we would
 get an inconsistent system; see Section 3.6 in
 [http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html].

 On the other hand, given
 {{{
 type family F a :: * -> *
 }}}
 an equality of the form `F a1 b1 ~ F a2 b2` implies `F a1 ~ F a2` and `b1
 ~ b2` as always in Haskell (this is what Mark Jones called higher-kinded
 unification in his paper about constructor classes).

 In other words, given a type (f :: * -> * -> *), the partial application
 `f t` is well-formed exactly if the decomposition rule holds (i.e., `f a1
 b1 ~ f a2 b2` implies `f a1 ~ f a2` and `b1 ~ b2`).  These two properties
 are causally linked, you cannot get one without the other.

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