[gsg]

Types are usually understood as proofs: in this case, a proof about whether the tag of x is suitable for passing to cos without causing an error. (If you like, read "dynamic type" for "tag".)

So the proof and the tag are related in that one is about the other, but that does not mean they are the same thing.

[kazinator]

Indeed, just like a basket with three oranges in it, the numeral 3 written on a piece of paper, and a die with the three-dot face turned up, are not the same thing. They just potentially serve as representations of the same thing. Of course something at compile time isn't the same thing as at run time. They exist at different times in different spaces. Compile time might be on an x86 build machine, and run-time on an embedded ARM device.

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