To your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just

To your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just be some arbitrarily large number (but not infinite) number of loops. [1] https://www.idris-lang.org/docs/current/contrib_doc/docs/Data.Fuel.html https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...