Type reconstruction with recursive types and atomic subtyping

Abstract

We consider the problem of type reconstruction for λ-terms over a type system with recursive types and atomic subsumptions. This problem reduces to the problem of solving a finite set of inequalities over infinite trees. We show how to solve such inequalities by reduction to an infinite but well-structured set of inequalities over the base types. This infinite set of inequalities is solved using Büchi automata. The resulting algorithm is in DEXPTIME. This also improves the previous NEXPTIME upper bound for type reconstruction for finite types with atomic subtyping. We show that the key steps in the algorithm are PSPACE-hard.