  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
Curry style variants of system Fat and show that typability is decidable and
that there is an algorithm for type inference which is capable of dealing with
non-redundancy constraints.
