That's true, because doing so in Lisp is undecidable and because you allow function definitions to change (that's why type checking works better with inline and local functions).
The type of analysis applied to Lisp is adapted to its type system: you have ranges of values, unions, etc. In particular SBCL can exploit some relationships between runtime values and types (I detailed it recently, so I prefer not to repeat myself: https://news.ycombinator.com/item?id=12222404)
As far as I am concerned, it is already quite powerful to detect the type-related errors that I tend to do.
The part that cannot be decided during compilation is left to be checked at runtime, which is strong dynamic safety. Instead of manipulating untyped bits, you have all you need to never corrupt the state of your program.
The good news is that if implementors make progress with type inference, you don't have to change the language: more checks can move from runtime to compile-time (the hard stuff would be the check the "satisfy" type ;-).
With some types left to be checked at runtime, you end up in a situation that is no worse than statically typed programs which throw exceptions for other kinds of errors. Sometimes, those errors arise because programmers implement a dynamic things, like ad-hoc tags to identify objects at runtime (so this is basically a dynamic type system in disguise). Other errors related to safety are tied to temporal issues, deadlocks, permissions, priority, security, etc. You can't always encode them with types. There are formal tools for dealing with them, but at this point, whether you use them generate safe code in Lisp or OCaml is not very important (and generating Lisp code is straightforward).
> Even worse, Common Lisp will use your type annotations to optimize code, which can change the behavior of your program.
This is a strange concern. The modified behavior belongs to the set of behaviors that would be possible without checking types, not a new, faulty behavior that contradicts what the code says.
The type of analysis applied to Lisp is adapted to its type system: you have ranges of values, unions, etc. In particular SBCL can exploit some relationships between runtime values and types (I detailed it recently, so I prefer not to repeat myself: https://news.ycombinator.com/item?id=12222404)
As far as I am concerned, it is already quite powerful to detect the type-related errors that I tend to do. The part that cannot be decided during compilation is left to be checked at runtime, which is strong dynamic safety. Instead of manipulating untyped bits, you have all you need to never corrupt the state of your program. The good news is that if implementors make progress with type inference, you don't have to change the language: more checks can move from runtime to compile-time (the hard stuff would be the check the "satisfy" type ;-).
With some types left to be checked at runtime, you end up in a situation that is no worse than statically typed programs which throw exceptions for other kinds of errors. Sometimes, those errors arise because programmers implement a dynamic things, like ad-hoc tags to identify objects at runtime (so this is basically a dynamic type system in disguise). Other errors related to safety are tied to temporal issues, deadlocks, permissions, priority, security, etc. You can't always encode them with types. There are formal tools for dealing with them, but at this point, whether you use them generate safe code in Lisp or OCaml is not very important (and generating Lisp code is straightforward).
> Even worse, Common Lisp will use your type annotations to optimize code, which can change the behavior of your program.
This is a strange concern. The modified behavior belongs to the set of behaviors that would be possible without checking types, not a new, faulty behavior that contradicts what the code says.