Last time I had to implement a typed programming language, it was for short programs only. So for typing I just converted the program into a large set of constraints and throw z4 at it, asking to optimize for smallest possible types. If z4 could find types for every expressions in less than a few seconds then it was well typed.

You had to use a few trick for larger programs, but basically it managed to type any real programs and I never encountered an ambihuous case that caused a problem in practice. In case of failure, the small set of unsatisfiable constraints was easy to translate into nice error messages. This also allows for typing rules that are easy to state and can accomodate operators that adapts nicely to their environment.

I would understand if this approach would be frowned upon, but I still wonder if any serious language ever used this approach?