@Slava_Pestov
A question about this part.
Is it possible to replace the current algorithm type inference with one that produces correct answer in 80-90% of use cases, fails (instead of producing a wrong answer) in others and does it in reasonable polynomial time, while producing meaningful and helpful error messages (like pointing at the exact part of the expression which type could not be determined) while making it deterministic or at least reproducible?. While being optimized to work fast for common use cases? Because it still fails in non-negligible number of cases, in unreasonable amount of time (often several minutes) without giving any helpful hints.