[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.