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.
Actually, see
http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10
Manuel
for those following along here: | However, I think I now understand what you are worried about. It is the | interaction of type families and GHC's generalised type synonyms (i.e., | type synonyms that may be partially applied). I agree that it does lead | to an odd interaction, because the outcome may depend on the order in | which the type checker performs various operations. In particular, | whether it first applies a type instance declaration to reduce a type | family application or whether it first performs decomposition. yes, indeed, thanks! that was the central point of example one. 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). 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. my suggestion was to annotate the results of type family application reductions with the type parameters. in essence, that would carry the phantom types along for type checking, and the decomposition rule could be taken care of even after reduction, by comparing these annotations. alternatively, use the decomposition rule as the reduction rule. both would make clear that one is *not* dealing with simple type-level function applications. | 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. 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!-) but in terms of actually implementing your design, and matching your theory and proofs, it might be best to treat the rhs of a type family instance like a type class instance parameter (where partial applications of synonyms and families are ruled out), not like the rhs of a type synonym definition (where everything is allowed). then users can try out an implementation that does what you say it would, including constraints needed for your proofs, which might lead to extension requests later - as Tom said, there may still be some open ends. perhaps you could keep those two examples around in a separate ticket, collecting experiences with and limitations of type families? thanks, claus