
| Yes, but where is it written that what cannot be expressed in system- | F is type incorrect? We think it is still type safe, and it is an | extrcat of a larger program that is quite useful (if we managed to | compile it), Indeed! Well-typed programs don't go wrong, but not every program that never goes wrong is well-typed. It's easy to exhibit programs that don't go wrong but are ill-typed in System F, or indeed any other decidable type system. Many such programs are useful, which is why dynamically-typed languages like Erlang and Lisp are justly popular. However, I think EHC is still in the statically-typed camp. In which case, if EHC accepts the program you sent then presumably EHC implements a type system in which the program is well-typed. What is that type system? I hazard that it is even more exotic than GHC's! And probably very interesting as well; I'd love to see it. I'm quite puzzled about why Hugs accepts it though. I don't think Hugs has ambitions to be more expressive than System F. (Incidentally, GHC is indeed going beyond System F -- we've recently changed GHC to use FC as its intermediate language -- paper on my home page. But even FC can't express your program.) Simon