There are few dynamic languages that go that far. Python isn't currently one of them; the runtime is still doing low-level type-compliance checks under the hood

There are few dynamic languages that go that far. Python isn't currently one of them; the runtime is still doing low-level type-compliance checks under the hood even if the static typing layer "knows" those checks are wasteful. At least in every compiler / runtime I'm familiar with for Python; maybe someone has built one that uses the types to generate faster code that's unsound if the static type assertions are violated. Other dynamic-typed-and-also-static-typed languages do allow for this. Many Common Lisp compiler implementations, for example, respect things like the (the) special form (https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node106.html https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node106.html), which acts as a static type assertion that allows the compiler to actually throw away the runtime sanity-checking (at the cost of producing actual unsafe code if the constraints of the form are violated).