[gsg]

I didn't say that types are tags at a different time, I said they are different things.

And only concrete types are about representation. Abstract, universal, existential and uninhabited types are all useful and meaningful concepts without any particular relation to representation.

[kazinator]

But a concrete value, like a symbol or string, has a concrete type, and that better agree with what its tag information says (if it has it).

Sure, expressions like "for all x: function from x to x" may not have concrete instantiations: there is no thing that is type tagged that way. It could be, of course; there is no limitation on what constitutes a type tag. Any compile time information, whether it is a universally quantified expression or whatever, can be represented at run-time also. In practice, that isn't done.