On Tue, 11 Mar 2008, Hugo Pacheco wrote:
I know I do not need these constraints, it was just the simplest way I found to explain the problem.
I have fought about that: I was not expecting F d c ~ F a (c,a) not mean that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized". If I encoded the family
type family F a x :: *
F d c ~ F a (c,a) would be semantically different, meaning that this "decomposition rule" does not apply?
Correct. However, then you cannot write "Functor (F a)" because type functions must be fully applied. So either way you have a problem. Could you show the type instances for F you have (in mind)? This way we can maybe see whether what you want to is valid and the type checker could be adjusted to cope with it, or whether what you're trying to do would not be valid (in general). I have my suspicions about your mentioning of both Functor (F d) and Functor (F a) in the signature. Which implementation of fmap do you want? Or should they be both the same (i.e. F d ~ F a)? Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/