I wrote something like this. It used the bytecode, simulating types on the stack. Functions with annotations had to be called with compatible types, functions

I wrote something like this. It used the bytecode, simulating types on the stack. Functions with annotations had to be called with compatible types, functions without annotations were symbolically executed for each call site. Constructors were special cased so that the object attributes were set up correctly. Types for a stack slot or local could diverge and be narrowed depending on the path through the program. The amount of metaprogramming used in practice in python made using it for real programs feel insurmountable. Also, I'm pretty sure performance would have been a problem beyond the toy programs I got it working on. But it was a fun exercise. I'll have to dig up that code