> What you want is guarantees that correct programs typecheck quickly.

In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.