This can lead to puzzling errors as discovered in #2714.

My conjecture is that isTypeCorrect (Lean/Meta/Check.lean) catches every exception and reports it as "motive is not type correct", and it inadvertently caught a max heartbeats exception in this case.