Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe t

Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.