一句话：提出存在类型见证保护机制，形式化核心演算并证明可靠，可避免 Java 通配符不健全性且误报极少。
Java 泛型的通配符（wildcards）曾被 Amin 与 Tate（2016）指出存在不健全性。本文表明，即使没有 nullness-aware 类型系统，该不健全性也可避免。核心洞见是：在通过子类型隐式引入存在类型时，要保持类型系统可靠，必须在引入存在量化类型变量时确保存在合适的见证类型（witness type）。作者为此形式化了一个核心演算并证明其可靠性，同时基于该思路实现静态分析，用于扫描大规模 Java 语料中的潜在问题。分析未发现真实问题，仅有 1 个误报，说明 Java 通配符不健全性在实践中影响很小，而所提方法能以极低误报完全规避它。
In this paper, we show that the unsoundness discovered by Amin and Tate (2016) in Java’s wildcards is avoidable, even in the absence of a nullness-aware type system. The key insight of this paper is that soundness in type systems that implicitly introduce existential types through subtyping hinges on still making sure there are suitable witness types when introducing existentially quantified type variables. To show that this approach is viable, this paper formalizes a core calculus and proves it sound. We used a static analysis based on our approach to look for potential issues in a vast corpus of Java code and found none (with 1 false positive). This confirms both that Java's unsoundness has minimal practical consequence, and that our approach can avoid it entirely with minimal false positives.