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...
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?
Not quite, but it refines my proposal of requiring that type synonyms in the rhs of type instances need to be saturated. Let me elaborate. The current implementation is wrong, as it permits type S a b = a type family F a :: * -> * type instance F a = S a Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations: (1) F Int Bool ~ F Int Char ==> DECOMP F Int ~ F Int, Bool ~ Char ==> FAIL (2) F Int Bool ~ F Int Char ==> TOP S Int Bool ~ S Int Char ==> (expand type synonym) Int ~ Int ==> TRIVIAL However, here is a (somewhat silly) program that does have partially applied type synonyms in a type instances' rhs and that is perfectly ok: type S a b = a type family F (a :: * -> *) b :: * -> * type instance F a b = S (S a) b b This is ok, because we can expand the type synonyms in the rhs of the type instance S (S a) b b = S a b = a and get a valid type. So, the crucial point is that, as you wrote,
I don't think this normalisation should include type families, although H98 type synonyms are a kind of degenerate case of type families.
The only way to stratify the normalisation of type synonyms and type families such that all type synonyms are expanded before any family applications are normalised is by requiring that after normalising the rhs of a type instance declaration *by itself*, we get a type that only contains saturated applications of type synonyms. (As Claus wrote, this is after all what we do for class instance heads.) Manuel