Comment by Expurple

Idris is Turing complete [1] and has a very advanced and expressive type system (dependent types) where type checking is still guaranteed to halt.

That's because the language has a notion of `total` functions [2], and only `total` functions can be used for computing type signatures. These `total` functions must terminate in finite time and not crash. AFAIK, they aren't Turing complete, but they're still pretty expressive. `partial`, Turing complete functions are still allowed at runtime (outside of type signatures) [1].

If I understand correctly, running Idris in the type-checking mode (`--check`) should give you what you want.

[1]: https://cs.stackexchange.com/a/23916/159425

[2]: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h...