PL research is not necessarily for "contributing to programmer productivity." Formalization of various programming language concepts into a type system[0] allows researchers to apply analysis and verification techniques. The simplest example I can think of is the Maybe type. Instead of having null pointers and, if you forget to check for NULL, getting a runtime error (segfault, NullPointerException, whatever), instead you would fail to compile since the "null-like" pointer would be a Maybe type, not the concrete value. You can't use it without unwrapping it. Concretely, the code:
int foo(int *p) {
return *p + 17; //well, probably something more complicated.
}
if p is NULL, this code doesn't work. In a language with a more expressive type system, we would write:
foo :: Maybe Int -> Maybe Int
foo p = case p of
Just x -> Just (x + 17)
Nothing -> Nothing
(Note: there are more succinct ways to write this example in Haskell, but I'm trying to illustrate the code.)
In this case, we have demonstrably covered every case. That's what an expressive type system gets you: you can completely preclude certain classes of bugs like null pointer dereferences by having a sufficiently expressive type system. It's the same in more relevant PL research: people are attempting to formalize systems so that whole classes of bugs can be removed at compile time. It's not about user case studies or anything like that: those can come later, when features look like they'd be useful to integrate into languages.
It looks like the featured article gives a case study about a pretty bad type system. A sufficiently expressive type system doesn't get in the way--it aids the programmer, not hinders her. Heck, in Haskell and ML, you don't even have write down types--the compiler will infer them for you. (It is Haskell practice to type-annotate toplevel functions anyway).
[0] When I say type system, I mean a static type system. For the purposes of this discussion, dynamically typed programs are statically typed, just with not-very-useful types.