Yea I never bought this assertion from the TS team, saying “given the trade-offs at the time” is the same as saying “we’re already backed into a corner by previous decisions” - the decision(s) may have been intentional at each step but the design itself probably was not. Given the choice of sound or unsound, considering that the purpose of a type system is to give certain guarantees, a type system design must always choose soundness to be considered reasonable.

That being said, I don’t think it’s possible to “pull off soundness without compromising expressivity” because the expressivity in this context is self-referential types which equate to non-terminating unification logic (and thus, unsoundness). Still, I’m excited to see what they do with this type system! Reminds me a bit of Shen’s type system.