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 Typescripts type system treated types as first class values and let you use standard syntax for interacting with them", but I've been finding various other rabbit holes to fall into along the way.
I'd be curious as to what is undecidable as a consequence of this, that sounds like something that's going to bite me in the ass at some point.