[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke:
>>>>>> type family F a :: * -> *
>>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>>
>>> why would F x and F u have to be the same functions?
>>> shouldn't it be sufficient for them to have the same result,
>>> when applied to y and v, respectively?
>> Oh, yes, that is sufficient and exactly what is meant by F x ~ F  
>> u.   It means, the two can be unified modulo any type instances and  
>> local  given equalities.
>
> sorry, i don't understand how that could be meant by 'F x ~ F u';
> that equality doesn't even refer to any specific point on which these
> two need to be equal, so it can only be a point-free higher-order
> equality, can't it?
>
> the right-to-left implication is obvious, but the left-to-right
> implication seems to say that, for 'F x' and 'F u' to be equal on  
> any concrete pair of types 'y' and 'u', they have to be equal on all  
> possible types and 'y' and 'u' themselves have to be equal.

You write 'y' and 'u'.  Do you mean 'x' and 'u'?  If so, why do you  
think the implication indicates that x and u need to be the same?

> again, i gave a concrete example of how ghc behaves as i would  
> expect, not as that decomposition rule would suggest.

Maybe you can explain why you think so.  I didn't understand why you  
think the example is not following the decomposition rule.

Manuel