Claus Reinke:
one might say that the central point of example two were two partially applied type synonym families in the same position (rhs of a type synonym family instance definition).
usually, when reduction meets typing, there is a subject reduction theorem, stating that types do not change during reduction. since, in this case, reduction and constraint generation happen at the same (type) level, the equivalent would be a proof of confluence, so that it doesn't matter which type rules are applied in which order (in this case, decomposition and reduction).
Well, we still need normal subject reduction (i.e., types don't change under value term reduction), and we have established that for System FC (in the TLDI paper). In addition, type term normalisation (much like value term normalisation) needs to be confluent; otherwise, you won't get a complete type inference/checking algorithm.
as far as i could determine, the TLDI paper does not deal with the full generality of ghc's type extensions, so it doesn't stumble over this issue, and might need elaboration.
System FC as described in the paper is GHC's current Core language. What are you missing?
| The most clean solution may indeed be to outlaw partial applications of | vanilla type synonyms in the rhes of type instances. (Which is what I | will implement unless anybody has a better idea.)
i always dislike losing expressiveness, and ghc does almost seem to behave as i would expect in those examples, so perhaps there is a way to fit the partial applications into the theory of your TLDI paper.
I don't think we can avoid losing that expressiveness, as you demonstrated that it leads to non-confluence of type term normalisation - see also my reply to SimonPJ's message in this thread.
and i still don't like the decomposition rule, and i still don't even understand that first part about comparing partially applied type constructors!-)
Haskell always had the decomposition rule. Maybe we confused the matter, by always showing a particular instance of the decomposition rule, rather than the general rule. Here it is in all it's glory: t1 t2 ~ t1' t2' <==> t1 ~ t1', t2 ~ t2' No mention of a type family. However, the rule obviously still needs to be correct if we allow any of the type terms (including t1 and t1') to include *saturated* applications of type families. Manuel