Compilers for langugages such as Standard ML and Haskell infer types even without explicit type annotations and check type consistency of programs. But, for un-typeful input programs, the compiler often reports too wide area of programs as error sites. Such a big type error message is hardly informative for the programmer to find his error. It is because the current type inference algorithm fails too late. The current algorithm is a bottom-up algorithm. After the algorithm blindly infers sub-expressions without information from super-expressions, it detects sub-expressions cannot agree at an application expression.
This paper introduces a new top-down type inference algorithm which stops early. The basic idea of the new algorithm is to enforce each sub-expression to have a type which satisfy some constraint. In this paper, it is proved the new algorithm is sound and complete to the type inference rule in order to be replaced the current algorithm. And it is proved the new algorithm generates short-ranged error messages than the current algorithm.
