[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Wed Mar 26 07:24:46 EDT 2008
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?
Maybe I was thinking too much in terms of GHC's implementation, but
due to the lazy expansion type synonyms, the expansion is interleaved
with all the rest of type checking. But I think I now know what you
meant: the outcome should be *as if* type synonym expansion was done
as a pre-pass.
> | 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)
I agree.
> 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.
I'll check that. Might be an oversight.
> So I think we are agreed. I think the above statement of validity
> should probably appear in the user manual.
Yes, I'll take care of that.
Manuel
More information about the Haskell-Cafe
mailing list