One of the counterexamples given is the concept of "context" in Perl: functions behave differently depending on the type of expected return value. For example,
% perl -e '@a = localtime(); $, = " "; print @a;'
6 58 9 1 11 104 3 335 0
% perl -e '$a = localtime(); print $a;'
Wed Dec 1 09:58:12 2004
and this can't be done with ML's type system.
Now, C++ allows functions to behave differently with different arguments with static overloading. But you can't statically overload return types:
int f() { return 3; }
bool f() { return true; }
produces
error: new declaration `bool f()'
error: ambiguates old declaration `int f()'
I imagine this is only because of implicit type coercions in C; otherwise you (almost) always know from a call to f() what return type you'd expect.
In fact, that's how Haskell's type classes do it. A function like read has type forall a. (Read a) => String -> a which can be read as "for all types a that implement the 'Read' class, this function maps strings to that type a". But it also means that the code chosen when you call read varies depending on how its return type is used!
So this means an expression like read "123" + 3 is well-typed, for it uses the integer definition of read. But if read "123" then 1 else 2 produces a (runtime) parse error, for the boolean read implementation expects its input to be either "True" or "False".
Haskell's type clasess are really interesting. I had an a-ha moment a long time ago in a class where the idea was presented as a generalization of parametric polymorphism. When I asked afterward why it wasn't popular, it was pointed out that you can't do type inference; you have to manually annotate with the types. And the whole thing sorta came together in one of those flashes of illumination. But now I can't remember the details, or even what the theoretic term for it is called... extensional polymorphism, maybe? I really wish I had someone to talk to about these sorts of things so I could keep my memory fresh. :(