my understanding is that this makes certain typing decisions undecidable? I agree though the the special parallel type language is a huge amount of added complexity and source of pain.
This was exactly what initially motivated me to write my own language. I was spending a bunch of time writing complex types in typescript (for SQL query builder type stuff - essentially data schema -> TS type transformation) as what was essentially just a bunch of regular boolean logic and iteration that would be simple, but because the 'type' world uses a completely different syntax to the 'value' world it gets unreadable really fast.
My language was originally basically "what if Typescript had types as first class values and wasn't permanently tied to the unsound foundation of Javascript", but I've been finding various other rabbit holes to fall into along the way.
With erased static types, you can do arbitrary operations on types-as-values at compile time and just compile the static result into the runtime code, so it doesn't even cost anything at runtime to do this. Generic functions just turn into curried functions with the type params as their first param set.