  will be the type of the polymorphic identity function. Despite this circularity, J.Y. Girard was able to show normalisation for type systems with this form of polymorphism. However, the extension of Church’s simple type theory with polymorphism is inconsistent as a logical system, i.e. all propositions (terms of type o) are provable.