The biggest worry for me in using graph unification for type checking is the
potential effect on error messages from the type checker. While dropping
the restriction makes some sensible programs well-typed, it also makes some
senseless programs well-typed, thus delaying the moment at which type
errors are discovered.
For example, consider
iterate 0 f x = x
iterate (n+1) f x = f (iterate n x)
At present this produces an occurrence type error. With recursive type
synonyms, it would be well-typed with the type
iterate :: Num a => a -> b -> b
where b = (b->b) -> b
The error can only be discovered at a call of iterate.
We already have a problem understanding type errors. Consider a very simple
example:
\f -> f 1 + f 1 2
A Pascal compiler, if Pascal had lambda-expressions, could report a missing
parameter. An ML compiler objects that Int->*a and Int cannot be unified.
Haskell is worse: hbc says there is no instance Num (a->b). Not easy for the
naive user to diagnose.
I think it would be wise to implement graph unification and get some experience
with it first, before adding it to Haskell. Personally, I get `occurs check'
messages from the type checker fairly often, and they are almost always
caused by mistakes I am happy to find. I am not at all convinced that, on
balance, graph unification would make Haskell more useable.
John Hughes
