[Haskell-cafe] Equality constraints in type families
simonpj at microsoft.com
Tue Mar 25 12:24:11 EDT 2008
| | 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.
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
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?
More information about the Haskell-Cafe