| 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