[Haskell-cafe] Equality constraints in type families

[Simon Peyton-Jones]

| | 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.html#type-synonyms

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