Optimization is just a side benefit.

A corrolary to our previous definition of type systems as principally ways to prove correctness: many discussions programmers have about type systems seem to focus on the runtime cost of type checking, as if that were the primary issue. Common Lisp has a great answer to that in its optional type declaration system¹ and the powerful inference and inlining done by compilers such as CMU Python.²

To a typeful programmer, runtime optimizations are an interesting side-effect of types, but ultimately beside the point. The correctness-proving features have a much greater impact on how you think about data structure, algorithm, and API design, approaches to testing, etc.

Common Lisp's type declarations are very nice, but they are little help in broadly proving program correctness, which is mostly the point of typeful programming.

① The special form the offers a glimpse into this system.

② See the CMUCL FAQ question on Python for explanation.