It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in system Fat and show that these two problems are decidable in the atomic polymorphic system.

翻译：众所周知,在Girard-Reynolds多形态系统F中,定型、类型居住和类型推断是不可确定的。 最近已经证明,即使在所有普遍性瞬间都有原子见证(系统脂肪)的F系统预言碎片中,也仍然无法确定定型居住。 在本文中,我们分析了法发系统中的定型和类型推论,并表明这两个问题在原子多形态系统中是可以分解的。