id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
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 None/Unknown T2157