> with almost no one in industry applying these lessons
Straight-up incorrect. Language designers think long and hard about how typings work in their languages. Rob Pike, Ken Thompson, and Russ Cox deliberated generics for like a decade[1] before finally allowing them in Go.
> a proper type system
I'm not sure exactly what you mean by "proper" -- but "rigid" type systems are extremely cumbersome to use practically. (Typed) λ-calculus is an academic example; Haskell is a real-world example.
> not too hard to retrofit dependent types (just don’t bother with Turing-incompleteness)
Hard disagree. It actually is extremely hard: type resolution is undecidable, for one. So you need to carefully design type resolution in a way that the "edges" of types don't (or can't) break the runtime too badly.
> why not go the extensible route of letting anyone hook into the “type checking” phase
Absolutely terrible idea, for many reasons, but mainly because, if C/C++ macros are any indication, people will abuse any kind of compile-time (or pre-processing) trickery you give them access to.
> write your own domain-specific checker, even
I guess I'm in the opposite camp here, I think domain specific languages are an absolute dumpster fire of abstraction and 99.9% of the time completely exceed the scope of the problem they're trying to solve. The purpose of a programming language is to be applicable to many classes of problems, and DSLs fly in the face of that pretty common-sense tenet.