[Smaug123]

A fully-featured dependent type system may be undecidable, but that doesn't mean you can't make one - it just means that there will be valid programs that the type checker nevertheless rejects, or there will be valid programs for which the type checker never terminates. It doesn't stop you from creating a type checker in the first place; it just weakens the guarantees you can make about that type checker.

The Typescript type checker is (or at least was) already Turing-complete (https://github.com/microsoft/TypeScript/issues/14833) without fully supporting dependent types.