[Haskell-cafe] Equality constraints in type families

[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?

oops, sorry, i meant 'y' and 'v' - the second parameters.

but my concern here was with the 'F x ~ F u' part - since
it doesn't refer to the 'y' and 'v' parameters, i suspect that 
means a semantic comparison over all possible parameters

    forall y,v: F x y ~ F u v

ie, comparing the type-level 'functions', implying some decidable
approximation. my second example, using two partially applied 
type families G3 and G4, aimed to demonstrate that this doesn't 
happen in ghc, and that equality on specific points is sufficient. 

perhaps you want to exclude those partial applications as well,
but i'm concerned that type families appear less and less as
the straightforward type-level functional programming that i
was hoping for. in fact, the decomposition rule seems to be 
saying that type function results cannot matter, only the 
structure of type family applications does:

    F x y ~ F u v <=> F x ~ F u /\ y ~ v

or do you have a specific type rule application order in mind
where all type-level reductions are performed before this
decomposition rule can be applied?

claus