| judgements (rather than boxes), no impredicativity, etc? As I recall the | treatment of application expressions there (infer type of the function, | then check the argument) was considered a bit restrictive. (It forbids | runST $ foo, for example.)
That requires impredicativity, and that's the bit we don't understand very well yet. Simon _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
