| | 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. Aha. Just to clarify, then, GHC's 'generalised type synonyms' behave like this. * H98 says that programmer-written types must obey certain constraints: - type synonym applications saturated - arguments of type applications are monotypes (apart from ->) * GHC says that these constraints must be obeyed only *after* the programmer-written type has been normalised by expanding saturated type synonyms http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions... I regard this as a kind of pre-pass, before serious type checking takes place, so I don't think it should interact with type checking at all. I don't think this normalisation should include type families, although H98 type synonyms are a kind of degenerate case of type families. Would that design resolve this particular issue? Simon