[GHC] #2157: Equality Constraints with Type Families

[GHC]

#2157: Equality Constraints with Type Families
-------------------------+--------------------------------------------------
    Reporter:  hpacheco  |       Owner:          
        Type:  bug       |      Status:  new     
    Priority:  normal    |   Component:  Compiler
     Version:  6.9       |    Severity:  normal  
    Keywords:            |    Testcase:          
Architecture:  Unknown   |          Os:  Unknown 
-------------------------+--------------------------------------------------
 For the implementation of fixpoint recursive definitions for a datatype I
 have defined the family:


 {{{
 type family F a :: * -> *
 type FList a x = Either () (a,x)
 type instance F [a] = FList a
 type instance F Int = Either One
 }}}


 for which we can define functor instances


 {{{
 instance (Functor (F [a])) where
    fmap _ (Left _) = Left ()
    fmap f (Right (a,x)) = Right (a,f x)
 ...
 }}}


 However, in the definition of recursive patterns over these
 representation, I need some coercions to hold such as


 {{{
 F d c ~  F a (c,a)
 }}}


 but in the current implementation they are evaluated as


 {{{
 F d ~ F a /\ c ~(c,a)
 }}}

 what does not express the semantics of "fully parameterized equality" that
 I was expecting

 You can find a pratical example in
 ([http://groups.google.com/group/fa.haskell/browse_thread/thread/6ea21dcade9e632f/01148521c33ac29a
 my conversions at the haskell-cafe mailing list])

 In order to avoid this, the family could be redefined as


 {{{
 type family F a x :: *
 type instance F [a] x = Either() (a,x)
 type instance F Int x = Either One x
 }}}


 but this would mean that I cannot define instances for Functor (F a)
 because not enough parameters passed to F.

 PS. This might sound more as a feature request than a bug, so sorry if I
 misplaced this information. I am willing to work on this subject to help
 supporting my test case.

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