https://hal.inria.fr/hal-01405792Lenglet, SergueïSergueïLengletFaculty of Mathematics and Computer Science [Wroclaw] - UWr - University of Wrocław [Poland]Wells, JJWellsMATHEMATICS DEPARTMENT OF HERIOT-WATT UNIVERSITY - School of Mathematical and Computer Sciences - HWU - Heriot-Watt University [Edinburgh]Expansion for Universal QuantifiersHAL CCSD2012[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]Lenglet, Sergueï2016-11-30 14:37:442020-12-29 10:02:012016-11-30 14:46:24enConference papershttps://hal.inria.fr/hal-01405792/document10.1007/978-3-642-28869-2_23application/pdf1Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the λ-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g.intersection introduction) until enough information hasbeen gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent yearsbecome simpler due to the use of expansion variables (e.g., in System E). This paper extends expansion and expansion variables to systems with ∀-quantifiers. We present System F s , an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.