Nothing is wrong with it, it's just as relevant today as it was 40 years ago, if not more. Most of the really interesting modern work is just building on top of some form intensional Martin-Löf theory.

I don't think there's anything implicitly wrong with a 40 year old type theory. Rather, C's type system is pretty decrepit.

This was a rhetorical question, it is clearly ridiculous to toss things out just because they are 40 years old

Because older type systems aren't webscale /s.