| > * 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? | | 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. Why not quite? | 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. Exactly! Just to state it more clearly again: Any programmer-written type (i.e one forming part of the source text of the program) must obey the following rules: - well-kinded - type synonyms saturated - arguments of type applications are monotypes (but -> is special) However these rules are checked ONLY AFTER EXPANDING SATURATE TYPE SYNONYMS (but doing no reduction on type families) OK, let's try the examples Manuel suggests: | The current implementation is wrong, as it permits | | type S a b = a | type family F a :: * -> * | type instance F a = S a This is illegal because a programmer-written type (the (S a) on the rhs) is an unsaturated type synonym. | type S a b = a | type family F (a :: * -> *) b :: * -> * | type instance F a b = S (S a) b b This is legal because the programmer-written type (S (S a) b b) can be simplified to 'a' by expanding type synonyms. The above checks are performed by checkValidType in TcMType. In particular, the check for saturated synonyms is in check_type (line 1134 or thereabouts). I'm not sure why these checks are not firing for the RHS of a type family declaration. Maybe we aren't calling checkValidType on it. So I think we are agreed. I think the above statement of validity should probably appear in the user manual. Simon