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?
hmm, it seems that here i was confused by the extra syntactic restrictions you have alluded to, meaning that the decomposition rule only applies to extra parameters, not to the type indices. also, given type family F a :: * -> * 'F x' and 'F u' are full applications, so may still be rewritten according to the family instance rules, which means that decomposition does not prevent reduction. it would really be helpful to have local indications of such differences that have an influence on interpretation, eg, a way to distinguish the type indices from the extra parameters. given that type families are never meant to be partially applied, perhaps a different notation, avoiding confusion with type constructor applications in favour of something resembling products, could make that clearer? something simple, like braces to group families and indices: type family {F a} :: * -> * {F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v would avoid confusion about which parameters need to be present (no partial application possible) and are subject to family instance rules, and which parameters are subject to the decomposition rule. assuming that you are going to rule out partial applications of type synonyms (example 1) and type families (example 2) in the rhs of type family instances for now, i think that answers my questions in this thread, although i'd strongly recommend the alternative syntax, grouping type indices with braces. sorry about the confusion, claus