> with the special "m" constant for meters.

Isn't the "special constant" exactly "value 1, type meters", defined as equal to "value <...very large number...> type atoms" etc?

If not, then what would be the result of the multiplication of 3 with "m"?

> Of course, you can define the type `square meter` as well, and define `pow -> meters -> positive integer -> square meters`

As long as your power is an integer, you can reduce it to multiplication. So what you'd really want to define is the result of "<value1 of type meter> * <value2 of type meter>", "(<value1 of type meter> * <value2 of type meter>) * <value3 of type meter>" etc.

What this gets you in the end is a type algebra, but that is also not exactly a new concept.