>>8 Doing type inference naively is double exponential, by cleverly using sharing in the type expressions you can bring it down to just exponential. But not matter what you do, there will be some rather simple expressions that will make the type checker explode. Luckily, these do not occur in practical programming.