Hi Fergus,
| > Without the restriction, it is easy to come up with examples that could
| > lead to non-termination.
|
| Is non-termination really a problem in practice?
I don't think so, which is why I've been happy not to enforce
restrictions in Hugs. For example, Gofer programs can potentially
cause the type checker to go into an infinite loop for much the same
reasons that we see here, but it seems that very few users ever
noticed, or even realized that this was possible. Those that did
were usually trying to probe the limits of what was decidable,
coding up all kinds of interesting logic programs using instance
decls as horn clauses.
If anything, the problems would have been even easier to spot with
Gofer than Hugs because Gofer is more strict in building dictionaries;
it insists on building all of the dictionaries that might be needed
before the program is executed. Hugs, by contrast, will build
dictionaries more lazily as it goes.
So practical experience suggests that people just don't tend to write
programs that cause non-terminating type checking unless that is
specifically what they were trying to do!
| A simple work-around is for the type checker to perform only
| up to a certain number of iterations, and if that fails, to
| report an error message, with the error message specifying
| the compiler option that can be used to increase the iteration
| limit.
Gofer had a similar mechanism, but Hugs doesn't bother ... the type
checker isn't really likely to go into an infinite loop ... instead,
it will just run out of stack or heap space, and so just fail to
terminate `properly'.
All the best,
Mark
