[jerf]

I think it would also be interesting for the compiler to modify the source code (with a flag, presumably, or possibly through the local LSP server) with the solved result as needed. This would also feedback to the programmer what the problem is, what the compiler thought the solution is (and under the circumstances, while it can't be "wrong" there's a decent chance it is suboptimal or not what the programmer expected), and not require future caching.

I kind of feel like that for more advanced languages this sort of back-and-forth between the type checker and the language has some potential to it.

[irq-1]

Why not make it a warning if the compiler leaves the happy path? The fix is easy for the programmer (enums, casting, etc.) and could be left unfixed if the programmer knows its OK (meaning it wont take 42 seconds and give an error.) The LSP would have to know when the compiler ran into this, but if the compiler can identify the type explosion problem, it can tell the LSP.