]. Bibliography-[-boe85 and . Boehm, Partial polymorphic type inference is undecidable, 26th Annual Symposium on Foundations of Computer Science, pp.339-345

G. Bracha, M. Odersky, D. Stoutamire, and P. Wadler, Making the future safe for the past: Adding genericity to the java programming language, Proc. OPPSLA'98, 1998.

[. Cardelli, A semantics of multiple inheritance, Information and Computation, vol.76, issue.2-3, pp.138-164, 1988.
DOI : 10.1016/0890-5401(88)90007-7

[. Cardelli, An implementation of FSub, Digital Equipment Corporation Systems Research Center, 1993.

F. Cardone and M. Coppo, Two extensions of Curry's type inference system, Logic and Computer Science, pp.19-76, 1990.

M. Coppo and M. Dezani-ciancaglini, A new type assignment for ??-terms, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.5, issue.1, pp.139-156, 1978.
DOI : 10.1007/BF02011875

M. Coppo, M. Dezani-ciancaglini, and P. Sallé, Functional characterization of some semantic equalities inside ??-calculus, Proceedings of the 6th Colloquium on Automata, Languages and Programming, pp.133-146, 1979.
DOI : 10.1007/3-540-09510-1_11

[. Dowek, T. Hardin, C. Kirchner, and F. Pfenning, Higher-order unification via explicit substitutions: the case of higher-order patterns, Joint international conference and symposium on logic programming, pp.259-273, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00077203

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

J. Garrigue, Relaxing the Value Restriction, Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS), 2002.
DOI : 10.1007/978-3-540-24754-8_15

J. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse d'état, 1972.

S. [. Giannini and . Rocca, Characterization of typings in polymorphic type discipline, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.61-70, 1988.
DOI : 10.1109/LICS.1988.5101

J. Garrigue and D. Rémy, Extending ML with semi-explicit higher-order polymorphism, Journal of Functional Programming, vol.155, pp.134-169, 1999.
DOI : 10.1007/BFb0014546
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.456.3425

[. Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems, vol.15, issue.2, pp.253-289, 1993.
DOI : 10.1145/169701.169692
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.430

H. Hosoya and B. C. Pierce, How good is local type inference?, 1999.

T. Jim, Rank-2 type systems and recursive definitions, 1995.

T. Jim, What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.42-53, 1996.
DOI : 10.1145/237721.237728

T. Jim, A polar type system, Electronic Notes in Theoretical Computer Science, 2000.

[. Jones and M. Shields, Practical type inference for arbitrary-rank types, Journal of Functional Programming, vol.17, issue.01, 2004.
DOI : 10.1017/S0956796806006034

J. Jr, O. William, D. K. Toole, and . Gifford, Type reconstruction with first-class polymorphic values, SIGPLAN '89 Conference on Programming Language Design and Implementation, 1989.

J. Assaf, J. B. Kfoury, and . Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order lambda -calculus, ACM Conference on LISP and Functional Programming, 1994.

J. Assaf, J. B. Kfoury, and . Wells, Principality and decidable type inference for finite-rank intersection types, ACM Symposium on Principles of Programming Languages (POPL), pp.161-174, 1999.

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, documentation and user's manual -release 3.05, 2002.

K. Läufer and M. Odersky, Polymorphic type inference and abstract data types, An earlier version appeared in the Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, pp.1411-1430, 1992.
DOI : 10.1145/186025.186031

K. Läufer and M. Odersky, Polymorphic type inference and abstract data types, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1411-1430, 1994.
DOI : 10.1145/186025.186031

]. R. Mil78 and . Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, pp.348-375, 1978.

[. Miller, Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992.
DOI : 10.1016/0747-7171(92)90011-R

C. John and . Mitchel, Coercion and type inference, In ACM Symp. on Priciples of Programming Languages, pp.175-185, 1983.

C. John and . Mitchell, Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988.

C. Okasaki, Purely Functional Data Structures, 1998.
DOI : 10.1017/CBO9780511530104

M. Odersky and K. Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.54-67, 1996.
DOI : 10.1145/237721.237729

M. Odersky, M. Sulzmann, and M. Wehr, Type inference with constrained types, Theory and Practice of Object Systems, vol.X, issue.1, pp.35-55, 1999.
DOI : 10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4

[. Odersky, C. Zenger, and M. Zenger, Colored local type inference, ACM SIGPLAN Notices, vol.36, issue.3, pp.41-53, 2001.
DOI : 10.1145/373243.360207

[. Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming , LFP '88, pp.153-163, 1988.
DOI : 10.1145/62678.62697
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.1446

[. Pfenning, On the undecidability of partial polymorphic type reconstruction, Fundamenta Informaticae, vol.19, issue.12, pp.185-199, 1992.

C. Benjamin and . Pierce, Programming with Intersection Types and Bounded Polymorphism Available as School of Computer Science technical report CMU-CS, pp.91-205, 1991.

. Pottinger, A type assignment for the strongly normalizable ?-terms

I. To and H. B. , Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.561-577, 1980.

[. Pottier, A framework for type inference with subtyping, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP'98), pp.228-238, 1998.

[. Pottier, Synthèse de types en présence de sous-typage: de la théorie à la pratique, 1998.

C. Benjamin, D. N. Pierce, and . Turner, Local type inference, Proceedings of the 25th ACM Conference on Principles of Programming Languages, pp.1-44, 1998.

D. Rémy, Extending ML type system with a sorted equational theory, Institut National de Recherche en Informatique et Automatisme, p.153, 1992.

[. Rémy, Programming objects with ML-ART an extension to ML with abstract and record types, Theoretical Aspects of Computer Software, pp.321-346, 1994.
DOI : 10.1007/3-540-57887-0_102

C. John and . Reynolds, Towards a theory of type structure, Proc. Colloque sur la Programmation, pp.408-425, 1974.

]. P. Sal82 and . Sallé, Une extension de la theorie des types en ?-calcul, In Lecture Notes in Computer Science No, vol.62, pp.398-410, 1982.

A. Schubert, Second-order unification and type inference for Churchstyle polymorphism, Conference Record of POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.279-288, 1998.
DOI : 10.1145/268946.268969
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3618

[. Simonet, The Flow Caml System: documentation and user's manual, Institut National de Recherche en Informatique et en Automatique (INRIA), 2003.

]. J. Wel94 and . Wells, Typability and type checking in the second order ?-calculus are equivalent and undecidable, Ninth annual IEEE Symposium on Logic in Computer Science, pp.176-185, 1994.

J. B. Wells, Type Inference for System F with and without the Eta Rule, 1996.

]. J. Wel02 and . Wells, The essence of principal typings, Proc. 29th Int'l Coll

K. Andrew and . Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, pp.343-355, 1995.

?. Subcase-?, Then nf(?) = ? by definition By Property 1.5.6.ii (page 51), we have ? ? ftv(?) By well-formedness, we must have ? ? dom(Q)

. By-rule-equiv-r, we have a restricted derivation of (Q) ? ? ?

. Moreover, If nf(? ) is ?, (Q) ? ? ? by Property 1.5.6.i (page 51), and (12) holds by Equiv-R. In both cases, we have a restricted derivation of (12) If ? is in T , then (Q) ? ? (13) holds by Eq-Mono and I-Equiv, Otherwise, (13) holds by I-Hyp

?. Hence, 1 ) ? 2 ? ? (? ? 1 ) ? (2) holds by R-Context-R. This equivalence is thrifty since nf(? 2 ) and nf(?) are both ?

@. Case and N. , We have a thrifty derivation of ? 2 ? nf(? 2 ) by induction hypothesis, thus we get a thrifty derivation of ? ? ? (? ? 1 ) nf

R. Moreover, This derivation is thrifty We conclude by observing that nf(?) is nf(? 2 )[? 1 /?]. ? Case ? / ? ftv(? 2 ): Then nf(?) is nf(? 2 ), and ? ? ? 2 by Eq-Free, thus we get a thrifty derivation of ? ? nf(? 2 ) by induction hypothesis and R-Trans. ? Otherwise, nf(?) is ? (? nf(? 1 )) nf(? 2 ) By induction hypothesis Hence, pp.1-1

R. By, R. , and R. , we get a thrifty derivation of ? ? nf(?)

. Assume, If (Q) ? 1 ? ? 2 is thrifty, and (Q) ? 2 ? ? holds but (Q) ? 1 ? ? does not hold, then there exists a thrifty derivation of (Q)

S. Hyp and S. , Alias are similar to cases StSh-Hyp, StSh-Up, and StSh-Alias of Property ii. ? Case S-Nil: immediate. ? Case S-Rigid: immediate. w(?) + X × w(? ) + A × w A (? ). Hence, w(? 1 )

@. Case and A. , If ? is neither ? nor ? , we get the result by A-Hyp If ? is ?, we have ? 1 = ?, and (Q, ? ?, ? = ? , Q 0 ) ? 1 ? ? holds by A-Hyp, thus (Q, ? ?, ? = ? , Q 0 ) ? 1 ? ? holds by R-Trans, Eq-Mono and A-Equiv. If ? is ?

. Property-iv, We have (Q) ? ? ? (1) and (Q, ? ?, Q 0 ) ? 1 ? ? 2 . As explained above, we only need to consider cases A-Hyp and I-Hyp

@. Case and A. , If ? is not ?, the result is by A-Hyp. Otherwise, we have ? 1 = ? and is =. We have (Q, ? ? , Q 0 ) ? ? ? (2) from (1) and Property 1, pp.5-8

. Additionally, ? ? (3) holds by A-Hyp. Hence, (Q, ? ? , Q 0 ) ? ? ? holds by A-Equiv

@. Case and A. , We have ? 2 = ?. If ? is not ?, we get the result by A-Hyp

@. Case and I. , We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is rigid. Thus, we get the result by I-Hyp

. Property-vi, We have (Q) ? ? (1) and (Q, ? ? ?

@. Case and A. , We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is flexible. Thus, we get the result by A-Hyp

@. Case and I. , We have ? 2 = ?. If ? is not ?, we get the result by I-Hyp. Otherwise, ? 1 is ?. By Property 1.7.2.iii (page 59) and (1), (Q, ??? , Q 0 ) ? ? (2) holds. Hence, pp.and I-Hyp

@. Case and A. , We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is flexible. Thus, we get the result by A-Hyp

@. Case and I. , We have ? 2 = ?. If ? is not ?, we get the result by I-Hyp. Otherwise, ? 1 is ?. By A-Hyp

@. Case, or (?, ?) with (? ? ) ? Q: In this case, unify simply returns unify (Q, ?, ? ), while unify is more elaborate. We have to consider the two following sub- cases: Subcase ? ? dom, we have Q(? ) =, p.54

. Hence, we get ? (Q b ) ? ? ?. Hence, (6) gives (Q) ? ? . By Lemma 2.1.6, it leads to (Q) ? ? ? . This is a contradiction with the hypothesis that (2) does not hold. Hence, unify cannot succeed, and this is the expected result. Otherwise, (2) holds, and unify returns Q. From (2), we have (Q) ? ? ? (8) We have to show that unify returns a rearrangement of Q. From (1), Q is of the form (Q a , ? ?, Q b ) and ? ? ftv(? (Q b ) ? ) (9). Hence, we can derive (Q) ? (Q b ) ? ? by I-Drop . From (8), we get (Q) ? (Q b ) ? ? (10) By Property 2 ? Case Let: We have (Q) ? a 1 : ? 1 and (Q) ?, x : ? 1 a 2 : ?. By induction hypothesis, we have (Q) ?, ? a 1 : ? 1 and (Q) ?, x : ? 1 , ? a 2 : ?, which can be written (Q) ?, ? , x : ? 1 a 2 : ?. Hence, by Rule Let, we get the expected result. ? Case Gen: The premise is (Q, ?? a ) ? a : ? (1), and ? is ? (?? a ) ? . Besides, ? / ? ftv(?) Let ? be a fresh variable (that is By Lemma 6.1.1 applied to (1) with the renaming Hence, by induction hypothesis, Applying Gen, we get (Q) ?, ? a : ? (? ? a ) ? [? /?], that is (by alpha-conversion) (Q) ?, ? a : ?, which is the expected result. Proof of Lemma 6

. @bullet-case-fun, By hypothesis By Corollary 6.1.3 (page 153), we get (QQ , ? ? ?) ?, x : ? 0 a : ?. Hence, the following derivation: (QQ , ? ? ?) ?, x : ? 0 a : ? (QQ , ? ? ?) ? ? I-Hyp (QQ , ? ? ?) ?, x : ? 0 a : ? (QQ , ? ? ?) ? ?(x) a : ? 0 ? ? (Q) ? ?(x) a : ? (Q , ? ? ?)

. @bullet-case-fun, The premise is (Q, ? ?, Q ) ?, x : ? 0 a 0 : ? 0 (9) and dom(Q ) # ftv(?) (10). Besides, ? is ? (Q , ? ? ? 0 ) ? 0 ? ? (11). Hence

. Hence, we get (Q) ? ?(x) a 0 : ? (? ?

A. @bullet-case, Moreover, we have (Q, ? ?) ? 1 ? (Q ) ? 2 ? ? 1 (15) and (Q, ? ?) ? 2 ? (Q ) ? 2 (16). Besides, ? is ? (Q ) ? 1 . By (3), (13) and Rule Gen, we get (Q) ? a 1 : ? (? ?) ? 1 (17). Besides, the size of (17) is the size of (13) plus one. By induction hypothesis, p.1

. Similarly, By (18), 22), and (23), and Rule App , we get (Q) ? a 1 a 2 : ? (? ? This corresponds to

. Additionally, the size of (24) is one plus the size of (18) and the size of (20). Hence, it is smaller than or equal to one plus the size of (13) plus the size of (14), that is, the size of

I. @bullet-case, The premises are (Q, ??) ? a : ? 0 (25). and (Q, ??) ? 0 ?

G. By-rule, By induction hypothesis, (Q) ? a : ? 0 (27) holds, with ? 0 ? ? (? ?) ? 0 (28), and the size of (27) is smaller than or equal to the size of (25), we get (Q) ? 0 ? (? ?) ?

L. @bullet-case, The premises are (Q, ? ?) ? a 1 : ? 1 (35) as well as (Q, ? ?) ?, x : ? 1 a 2 : ? (36) By Gen and (35), we get (Q) ? a 1 : ? (? ?) ? 1 . By induction (Q) ? 1 ? 1 holds, Hence, by Rule Strengthen, we have (Q) ?, x : ? 1 a 2

. Hence, we get (Q 0 Q ) ? ? ? 1 , that is Similarly, we can derive (Q 0 Q ) ? ? ? 0 . Hence, (Q 0 ) ? (Q ) ? ? (Q ) ? 0 (20) holds by R- Context-R. We have (Q 0 ) ? (Q ) ? 0 ? ? (P 1 ) ? 0 from (19) By alpha-conversion, we have (Q 0 ) ? (Q ) ? 0 ? ? (Q 1 ) ? 0 (21), ) we get (Q 0 ) ? (Q ) ? ? 0