Comment by cwhy

This is rather a math-specific operation (type conversion on math operators), not the scope of general purpose language. A lot of dependent typed language can achieve this naturally and most languages with ADT can simulate this.