[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
----------------------------------------+-----------------------------------
Comment (by hpacheco):

 I understood your points and they do make sense, but do you think that
 this is a feasible feature request or it should never be supported?

 I have just remembered that, still for the family

 {{{
 type family F a x :: *

 type instance F [a] x = Either () (a,x)
 type instance F Int x = Either () x
 }}}


 we can write "partial-evaluated classes for F" whenever not all type
 parameters are in use.
 For the Functor class this would mean:


 {{{
 class FunctorF x where
         fmapF :: (a -> b) -> F x a -> F x b

 instance FunctorF [a] where
    fmapF _ (Left _) = Left ()
    fmapF f (Right (a,x)) = Right (a,f x)

 instance FunctorF Int where
    fmapF _ (Left ()) = Left ()
    fmapF f (Right n) = Right (f n)

 }}}

 At first glance it is less generic but seems to work.
 However, a previous function (for the family F a :: * -> *)

 {{{
 hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
 hylo d g h = g . fmap (hylo d g h) . h
 }}}


 if translated to


 {{{
 hylo :: (FunctorF d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
 hylo d g h = g . fmapF (hylo d g h) . h
 }}}


 does not compile with the explicit type signature.
 Without a type signature it compiles and infers the signature (does not
 make sense to me)


 {{{
 hylo :: forall t d c a. (FunctorF d) => t -> (F d c -> c) -> (a -> F d a)
 -> a -> c
 }}}


 However, if this signature is passed explicitly, it does not compile
 again.
 There must be a bug somewhere in this scheme, or am I missing something
 huge?

 Regards,
 hugo

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