>I believe that type checking in unextended Hindley-Milner type systems is exponential Yes it recursively solves for function typing parameters though the call

>I believe that type checking in unextended Hindley-Milner type systems is exponential Yes it recursively solves for function typing parameters though the call graph. This isn't guaranteed to exit. If the language you are using annotates function argument's with types[1] then this behavior is avoided and Hindly-Milner becomes effectively linear. This is why type-inference is starting to become a common feature in most languages. [1] Nearly every language does this, but inline clojure are sometimes type inferred. Depends on language/language family.