What's Wrong with Hindley-Milner?

Almost all students of CS learn basic type theory. In that setting, usually type systems are studied for lambda calculi where the starting point is the simply typed lambda calculus. Type systems are usually developed with an emphasis on a number of academic invariants, such as normalization, and the Curry-Howard correspondence.

I sometimes doubt the assumptions used and the usefulness of some of the type systems developed - especially within the context of the Hi language. As far as I am concerned, such a thing as normalization is only interesting in the context of long-term studies where programming languages are developed where well-typed programs terminate, a thing I am not very interested in within the pragmatic choices of a functional programming language which should work today. Moreover, from a programmer's point of view, as far as I am concerned, the only interesting property of the Curry-Howard correspondence is that it shows that you need a prover, or 'proving power,' to show that programs are well-typed.

Given those observations, I have a certain amount of distrust towards impredicative type systems which were originally developed within the context of types for logical statements, but now are implemented in functional programming languages. Are programming language developers progressing in the right direction, or are they progressing in a certain direction because of a lack of imagination at developing more pragmatic typing systems?

In that context, I would like to rethink the assumptions of Hindley-Milner based typing systems and go back to the only interesting property for type systems for programming languages: A well-typed program labels terms such that all values compute correctly.

But, there are an enormous amount of typing systems. Only experts know how to value them, I am not that big an expert, so the only option I have is to go back to simple examples and hope that I can make some sense of them and show where the theoretical pain lies.

A simple example:

      def f: (α → β) → α = f

Note that most Hindley-Milner based systems for functional programming languages will accept the above function.

I am interested in this particular example since it shows three things.

1. One, normalization is a non-issue, from that respect it is well-typed. A pragmatic type system should not care about normalization.
2. However, it shows a type for a function which I think should be rejected since one cannot construct a value from the domain of a function; a naive Hindley-Milner type derivation of the term can trick the type system in believing that all is okay. 
3. Lastly, it shows that this is not a problem of impredicativeness, but more a problem on what we believe a type denotes, and how to manage the unification of type variables.

The problem at the moment is that I have ideas on how to tackle this, but lack the oversight and vocabulary to correctly work towards a solution.

Not sure anymore. Possibly it is sufficient to keep HM style inference, but restrict the declared types to constructive types with a simple validity check.