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.

You could call it x.val, no need to use a long field name. But you would rarely access it directly anyway. I do not see any type checking advantage here for other languages.