Существуют ли языки программирования, позволяющие присваивать численным переменным не только значение, но и размерность?

Отличный вопрос, и ответ на него, насколько мне известно, "нет". Традиционно на уровне языка среди атомарных типов определяются просто "числа", а конкретный смысл этих чисел остаётся за разработчиком.

Термин, который вам нужно искать, называется strong typedef. Вы можете начать вот с этого вопроса на stackoverflow: https://stackoverflow.com/questions/376452/enforce-strong-type-checking-in-c-type-strictness-for-typedefs

Для решения вашей конкретной задачи, чтобы можно было объявить разные типы у двух числовых переменных и компилятор ловил места, где мы смешиваем использование этих переменных, используется чаще всего боксинг в том или ином виде. Для большинства мейнстримных языков вы можете найти библиотеку для этого, и не одну. Но использовать такие значения будет, конечно, не так удобно, как нативные атомарные типы данных.

Боксинг выглядит так. Объявляется класс, членом этого класса объявляется число. Идентификатором размерности будет являться либо само название класса (например, мы объявляем `class MetersInSecond { int value; }`), либо второй член этого класса (например, мы объявляем `class Speed { int value; Dimension dimension; }` и при создании объектов этого класса указываем размерность: `Speed speedInMps{0.05,  Dimension.SPEED_IN_METERS_IN_SECOND}`). Конечно же, вам придётся все математические операции объявить для этих новых классов самому.

В Haskell вы можете объявить новый тип, и добавить его инстансы к тем же классам типов, что и другие числа: Ord, Num, и все соответствующие операторы переопределить. Проверка типов будет работать так же хорошо, как и на встроенных Integer и Rational, использовать такие значения будет так же просто. Но это всё равно довольно много работы вручную.