What is a non-contrived example of static type-checking being too conservative?

In Concepts in Programming Languages, John Mitchell writes that static type checking is necessarily conservative (overly strict) because of the Halting Problem. He gives as an example:

if (complicated-expression-that-could-run-forever)
   then (expression-with-type-error)
   else (expression-with-type-error)

Can someone provide a non-contrived answer that would really be a practical concern?

I understand that Java allows dynamically-checked casts for cases like this:

if (foo instanceof Person) {
    Person p = (Person) foo;
    :
}

but I consider the necessity of that more a Java language/compiler deficiency than a cross-language issue.

I've always viewed it more as a matter of convenience, than about whether an algorithm can or can not be expressed at all. If I really wanted to run programs like Mitchell's contrived one, I'd just write the appropriate Turing Machine simulator in my statically typed language.

The trick with a static type system is to offer the right kinds of flexibility just for the cases where the flexibility allows you to write code that is more easily maintainable.

Here's some examples of program structuring techniques that are sometimes thought to be easier to manage in dynamically than statically typed languages.

Generics and Containers

In statically typed languages before ML (c. 1973) and CLU (c. 1974) it was not difficult to create a red-black tree of strings, a red-black tree of integers, a red-black tree of floats, or a red-black tree of elements of specific type Foo. It was, however, difficult (maybe impossible) to create a single implementation of a red-black tree that was both statically checked and which could handle any one of these data types. The ways around the problem were (1) to break out of the type system completely (for example: by using void * in C), (2) to write yourself some kind of macro preprocessor and then write macros that produce the code for each specific type you want or (3) use the Lisp/Smalltalk (and Java) approach of checking the type of the extracted object dynamically.

ML and CLU introduced the notion of, respectively, inferred and explicitly declared (static) parameterized types, which allow you to write generic, statically typed, container types.

Subtype Polymorphism

In statically typed languages before Simula67 (c. 1967) and Hope (c. 1977) it was not possible to both do dynamic dispatch and statically check that you had covered the case for every subtype. Many languages had some form of tagged unions, but it was the responsibility of the programmer to make sure that their case or switch statements, or their jump tables, covered every possible tag.

Languages following the Simula model (C++, Java, C#, Eiffel) provide abstract classes with subclassing where the compiler can check that each subclass has implemented all the methods declared by the parent class. Languages following the Hope model (all the ML variants, from SML/NJ through Haskell) have algebraic subtypes where the compiler can check that every typecase statement covers all the subtypes.

Monkey Patching and Aspect Oriented Programming

Dynamic type systems make a variety of prototyping techniques much easier. In languages where types are represented by hash maps from strings to functions (e.g., Python, Javascript, Ruby) it is quite easy to globally change the behavior of every module that relies on a particular type, simply by dynamically modifying the hash map representing that type.

While there are obvious ways in which monkey patching can be used to make programs harder to maintain, there are also ways in which it can actually be used for "good" rather than "evil". In particular with aspect oriented programming one can use monkey-patching like techniques to do things like modify the file type to point to a virtualized file system, permitting the construction of unit-testing infrastructures for "free", or modify simple exception types so they print log messages every time they are caught for better debuggability.

Unlike Generics and Subtype Polymorphism where the key static checking ideas were available in the 1970s, static checking for aspect oriented programming is (I think) an active research area. I don't know much about it except that there's a language called AspectJ since about 2001.

StackExchange Computer Science Q#38464, answer score: 7