Equality Constraints with Type Families
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 (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.