The reason typing is not a solved problem is this: there are valid programs which can be expressed in an untyped language that cannot be (directly) expressed in a typed one at the moment. For example:
(define (foo p?)
(if p?
42
"forty-two"))
What is the type of `foo`? It could be `bool -> int` or `bool -> string`, depending on the result of `p?`! In an untyped language, this is a perfectly valid program. In a typed language, this presents a type error, even if `p?` happens to
always result in `true` or
always result in `false`. The programmer reading the program knows that if `p?` is always `true`, then the type of `foo` is `bool -> int`, and that if `p?` is always `false`, the type is `bool -> string`. However, this program, as-is, is will be rejected as ill-typed.
In a language providing sum types, we can work around this by using a type like `(int * string) either`:
(define (foo p?)
(if p?
(left 42)
(right "forty-two")))
Where `left` and `right` are type constructors for values of type `('a * 'b) either`. Now, the type of `foo` is `bool -> (int * string) either`. This workaround effectively adds a run-time tag to the `either` values to distinguish the `left` case from the `right` case, which is essentially the way dynamically checked languages operate for values of all types but in a more restricted, specific, and arguably meaningful form. In many (most?) languages with sum types, the language will ensure that the programmer
always checks the tag of the `either` values before accessing the underlying "actual" value -- this is the only way to guarantee type safety while ensuring that the program does not barf due to a "type" error at run-time.
Now, it could be argued that the typing problem presented above is basically solved by sum types. But it could also be argued that this doesn't really solve the problem, because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?`, which could maybe be written as `p:=bool -> (p ? int : string)`, for example. Perhaps dependent typing could help us come to a true solution for this case, but there are other cases where other solutions will be needed.
According to Benjamin C. Pierce in Types and Programming Languages:
"Being static, type systems are necessarily also conservative : they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. ... The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed -- by assigning more accurate types to their parts -- is the main force driving research in the field.[0]
In essence, while there is already a vast array of programs we already know how to type, and while it's possible to work around cases that resist typing, type theory is still an active field of research with plenty of open questions yet to be answered. The corollary to this is that there are still valid reasons to prefer untyped languages to typed ones, as my sibling commentor pointed out. The day when typing is solved is the day people can no longer not look like an bozos for preferring untyped languages, but until that day comes, untyped languages remain fundamentally more expressive than typed ones (in the sense that they're fundamentally capable of expressing more programs[1]).
---
[0]: Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. §1.1, pp. 2,3.
[1]: There's also a sense in which typed languages are more expressive than untyped ones, and that's the sense that they are capable of expressing more properties of the program as part of the program itself.