Aren't most type systems in widely used languages Turing complete and (consequently) undecidable? Typescript and python are two examples that come to mind

But yeah maybe expressive enough refinement typing leads to hard to write and slow type inference engines