@Leo Um yeah, when I said nondeterminism, I really meant backtracking (as in "the list monad models nondeterministic computation"). Implementing our own type inference engine may also enable us to guide the backtracking and possibly make it faster on average (like, if the return type of most functions is determined by the types of the arguments, then it makes sense to find out the arguments' types first and unify the function's type with them, and proceed to the return type afterwards).

Another crazy idea: the invisible infix operator for function application is overloaded to one or more forms of function composition. :P Then we could do +K+TQ as in the above example and have the type inference engine work out the semantics that make sense.

@Leo Heh. :P I don't know, there probably is a "sweet spot" between overloading everything to the max and having the inference engine always spit out the wrong types, and not overloading enough to get any real benefit. I want to believe that the invisible operator can be overloaded in that sweet spot, but we'll see.