Indeed, that is the standard approach. It is also how some of the aforementioned languages desugar opaque type synonyms during compilation. It has the slight disadvantage that we can no longer use variables like

    x

in some situations, but need to use

    x._polynomials_gf_2

or whatever is the structure's field name. It is nice to avoid this boilerplate, which can become annoying quickly. Let the type-checker not the human do this work ...

> You do not need another language for this.

By the Church-Turing thesis you never need another language, but empirical practise has shown that the software engineering properties we see with real-world code and real-world programmers differ significantly between languages.