Typescript is so much better than almost every other dependently typed language in terms of expressing these things[0], and it's still kind of miserable.

We still have a long way to go in figuring out how to get our type systems to be easy enough to use to where this stuff doesn't surprise people anymore (because it shouldn't! identifier manipulation should be table stakes and yet)

[0]: modulo soundness of course! Though I don't think that's intrinsic to the expressiveness