How about a hybrid system? It would include a set of universal types such as
{integer, real, time, PI, imaginary} whose value spaces are well-understood
mathematically. But it would not include lexical representations, or value
spaces that are restricted by a domain, such as program language or machine.
In order to validate a universal type, a constraint system would have to be
applied that defined the lexical and value space (range) that is applicable
to a specific program environment. It's like a locale for types. Locales
would be comparable, so that you could determine programmatically how the
lexical/range definitions of one locale intersect another. You would then
know which out-of-bounds conditions are possible.
There could be a set of well-known type locales for languages/systems that
can be reused by applications.
There would have to be an additional mechanism for defining compound types
that are represented atomically (e.g., date).
