[Haskell-cafe] Equality constraints in type families

[Simon Peyton-Jones]

| > * 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