Lower Bounds on Type Checking Overloading

Abstract

Smith has proposed an elegant extension of the ML type system for polymorphic functional languages with overloading. Type inference in his system requires solving a satisfiability problem that is undecidable if no restrictions are imposed on overloading. This short note explores the effect of recursion and the structure of type assumptions in overloadings on the problem's complexity.