Practical SMT-based type error localization

摘要: Compilers for statically typed functional programming languages are notorious generating confusing type error messages. When the compiler detects a error, it typically reports program location where checking failed as source of error. Since other sources not even considered, actual root cause is often missed. A more adequate approach to consider all possible and report most useful one subject some usefulness criterion. In our previous work, we showed that this can be formulated an optimization problem related satisfiability modulo theories (SMT). This formulation cleanly separates heuristic nature criteria from underlying search problem. Unfortunately, algorithms optimal cannot directly use principal types which crucial dealing with exponential-time complexity decision polymorphic checking. paper, present new algorithm efficiently finds in given ill-typed program. Our uses improved SMT encoding cope high typing by iteratively expanding constraints derived. The preserves clean separation between heuristics search. We have implemented OCaml. experimental evaluation, found reduces running times localization minutes seconds scales better than algorithms.