I'm not sure I understand your last point. Do you desire for compilers to deduce the underlying type from the name of the variable or a type system that would let you create subtypes to give them additional contextual informations that the compiler would then use to enforce integrity?
Well, actually Kawa Scheme has a feature called quantities [1]. (+ 1cm 2m) equals to 201.0cm, (+ 1cm 2degr) throws an exception (degr has to be declared first, with (define-base-unit degr "Temperature")).
To tell the truth, I’ve never found any use for this feature.
I'd imagine that such type/units system would be most useful in interactive use, like in WolframAlpha where the system has quite good "understanding" of units and how they should be applied to formulas.
