  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.
