There is generally no typing in run time. One of the practices in writing compilers is to skip type checks during run time, because you know beforehand that no

There is generally no typing in run time. One of the practices in writing compilers is to skip type checks during run time, because you know beforehand that no type errors are possible. That is type erasure. If you're interested, lookup existential types. Very interesting stuff.