Enumerating Ill-Typed Programs for Testing Type Analyzers

We propose error enumeration , a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program 𝑃 , it systematically injects type mismatches at all possible program locations to explore ill-typed programs that differ from 𝑃 by replacing one expression with incompatible ones. The core contributions of our work are: (1) soundly injecting type mismatches even in the presence of type inference and refinements, and (2) enabling practical exploration of large seed programs by pruning the search space. Incomplete type information complicates the injection of type mismatches, as type inference can silently "repair" the injected error by adjusting inferred types in the surrounding context so that the program still type-checks. We address this by introducing a lightweight, usage-based reasoning technique that recovers missing types of program elements by leveraging the existing type annotations at each element’s use site. This enables the injection of errors that guarantee type incompatibilities at the use sites of variables and other expressions. Finally, to prune the search space, we enumerate only those errors that ultimately lead to comparisons between types with distinct shape characteristics. We evaluated our implementation, Eris , on (1) three type analyzers integrated into the compilers of Kotlin, Scala, and Groovy, and (2) the Checker Framework, widely used to identify null-related errors in Java programs. Eris has uncovered 64 bugs caused by ill-typed programs: 51 leading to unsoundness, and 13 to compiletime crashes. Further investigation reveals that the majority of the soundness bugs discovered by Eris are triggered under highly complex conditions, where error injection requires (1) specific combinations of actual vs. expected type pairs at deeply-nested program locations, or (2) reasoning about control flow and missing type information, capabilities that lie beyond the scope of existing work.