I think you misunderstand me. I'm not talking about computation languages. I'm talking about type languages (as was the OP). As in, the grammatical construct

I think you misunderstand me. I'm not talking about computation languages. I'm talking about type languages (as was the OP). As in, the grammatical construction in which types are expressed. For example, OCaml has a separate type language (the module system) from its computation language. Languages like Python and Elixir do not (you can define classes as part of a computation). The OP is advocating that the type language be one in the same as the language in which computation is performed. I'm suggesting that this leads to usability issues, as it's not clear from the syntax what type expressions are and are not usable by the compiler to check/optimize/etc. the value-level computation. This is entirely orthogonal to the point you seem to be making about expressive vs. inexpressive type systems.