Now you're confusing the implementation with the abstraction. Types can be modeled by tags. They can be modeled by trees. Or any other data structure that you can analyze with a program.
>The actual function of types, on the other hand, is to prove simple propositions about a program without running it.
The value of a tag proves something about the program. You're just proving it at run-time rather than compile time.
Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.
This is the problem with this entire debate. People act like there are two sides arguing from positions of equal merit. That is not the case. One (static) is a strict superset of the other (dynamic).
[1] https://en.m.wikipedia.org/wiki/Tag_(programming)