Summary: The well-known embedding of full intuitionistic propositional calculus into the atomic polymorphic system \(\mathbf{F}_{\mathbf{at}}\) is possible due to the intriguing phenomenon of instantiation overflow. Instantiation overflow ensures that (in \(\mathbf{F}_{\mathbf{at}}\) ) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in \(\mathbf{F}_{\mathbf{at}}\) were identified with such property: the types that result from the Prawitz translation of the propositional connectives (\(\bot\), \(\wedge\), \(\vee\)) into \(\mathbf{F}_{\mathbf{at}}\) (or Girard’s system \(\mathbf{F}\)). Are there other types in \(\mathbf{F}_{\mathbf{at}}\) with instantiation overflow? In this paper we show that the answer is yes and we isolate a class of formulas with such property.