> And I don't even see how "decideable" is a desireable property at all. So what if the type checker can infloop? It won't in practice.

I am not so optimistic after having worked with Swift, where simple arithmetic expressions and array literals can bring the compiler to its knees: https://twitter.com/steipete/status/1361596975150493700

(As noted in a reply, this particular bug has been fixed...but still.)