But what it's reasoning about coincides with the dynamic type which will exist at run time, so that means we cannot say the two have nothing to do with each other. It's the same knowledge, just known at different times, right?
Just because we have stuffed some knowledge into tags that exist at run time (and chosen suitable machine representations to make that possible) doesn't mean it's a different class of knowledge.
Types are propositions for which the text of your program is the proof. Type theory arose as an alternative to set theory in order to deal with Russell's paradox[0]. Types have been around for a lot longer than computers have. They have nothing at all to do with a running program.
What is missing from the above articulation of a view is that the run-time state of the program is also text. (It's made up of the symbols "0" and "1", at one level.) There can be propositions about that text.
Such a proposition pertains to a mathematical function. A running computer program does not contain mathematical functions, merely representations of them.
It is akin the difference between the theory of gravity and a falling rock. You can describe the rock with all manner of equations but you will not find any equations inside the rock.
Just because we have stuffed some knowledge into tags that exist at run time (and chosen suitable machine representations to make that possible) doesn't mean it's a different class of knowledge.