Type systems are often criticised, for being to restrictive, that is limiting programming languages and prohibiting programmers to write interesting programmes.
Chris Smith claims:
We get assurance that the program is correct (in the properties checked by this type checker), but in turn we must reject some interesting programs.
and
Furthermore, there is an ironclad mathematical proof that a type checker of any interest at all is always conservative. Building a type checker that doesn't reject any correct programs isn't just difficult; it's impossible.
Could someone please outline what kind interesting programmes this could be? Where is it proven that type checkers have to conservative?
And more general: What are the limits of type checking and type systems?