3 ms·
A turing complete type system is undecidable.
A turing complete type system is undecidable.
I think it's tolerable if the recursion limit is low, preferably single digit.
My point is that's not as interesting or practical as a type system for which you can write an expression that can't be checked. They may be roughly equivalent, but only one is esoteric.