id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential
2157,Equality Constraints with Type Families,hpacheco,chak,"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.",feature request,closed,normal,6.10 branch,Compiler (Type checker),6.9,fixed,,hpacheco@…,Unknown/Multiple,Unknown/Multiple,,T2157,,,,