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.
Trac metadata
Trac field | Value |
---|---|
Version | 6.9 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | Unknown |
Architecture | Unknown |