Jacques Garrigue

Didier Rémy

Ambivalent Types for Principal Type Inference with GADTs (extended version)

GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTs introduces local type equality assumptions, which are a source of ambiguities that may destroy principal typesand must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.

Introduction

GADTs, short for Generalized Algebraic DataTypes, extend usual algebraic datatypes with a form of dependent typing by enabling type refinements in pattern-matching branches [START_REF] Cheney | First-class phantom types[END_REF][START_REF] Xi | Guarded recursive datatype constructors[END_REF][START_REF] Baars | Typing dynamic typing[END_REF]. They can express many useful invariants of data-structures, provide safer typing, and allow for more polymorphism [START_REF] Sheard | Programming in Omega[END_REF]. They have already been available in some Haskell implementations (in particular GHC) for many years and now appear as a natural addition to strongly typed functional programming languages.

However, this addition is by no means trivial. In their presence, full type inference seems undecidable in general, even in the restricted setting of ML-style polymorphism [START_REF] Schrijvers | Complete and decidable type inference for gadts[END_REF]. Moreover, many well-typed programs lack a most general type. Using explicit type annotations solves both problems. Unfortunately, while it is relatively easy to design a sound typing algorithm for a language with GADTs, it is surprisingly difficult to keep principal types without requesting full type annotations on every case analysis.

Repeatedly writing full type annotations being cumbersome, a first approach to a stronger type inference algorithm is to propagate annotations. This comes from the basic remark that, in many cases, the type of a function contains enough information to determine the type of its inner case analyses. A simple way to do this is to use program transformations, pushing type annotations inside the body of expressions.

Stratified type inference for GADTs [START_REF] Pottier | Stratified type inference for generalized algebraic data types[END_REF] goes further in that direction, converting from an external language where type annotations are optional to an internal language where the scrutinee of case analysis and all coercions between equivalent types must be annotated. This conversion is an elaboration phase that collects all typing information Part of this work has been done at IRILL.

-not only type annotations-and propagates it where it is needed. The internal language allows for straightforward type inference and it has the principal type property. It also enjoys monotonicity: strengthening the type of a free variable by making it more general preserves well-typedness. As expected, principality does not hold in general in the external type system (a program may be typable but have no principal type), but it does hold if we restrict ourselves to those programs whose elaboration in the internal language is typable. Still, the external type system is not compositional because of the elaboration phase. Moreover, since elaboration extracts information from the typing context, monotonicity is lost: strengthening the type of a free variable by making it more general before elaboration can reduce the amount of type information available on the elaborated program and make it ill-typed. Monotonicity is a property that has often been underestimated, because it usually (but not always) holds in languages with principal types. However, losing monotonicity can be worse for the programmer than losing principal types. It reveals a lack of modularity in the language, since some simple program transformations such as simplifying the body of a function may end up inferring more general types, which may subsequently break type inference. Propagating only type annotations would preserve monotonicity, but it is much weaker.

GHC 7 follows a similar strategy, called OutsideIn [START_REF] Vytiniotis | OutsideIn(X) Modular type inference with local assumptions[END_REF], using constraint solving rather than elaboration to extract all typing information from the outer context. As a result, propagation and inference are interleaved. That is, the typing information obtained by solving constraints on the outer context enclosing a GADT case analysis is directly used to determine the types of both the scrutinee and the result in this case analysis. Type inference can then be performed in the body of the case analysis. By allowing information to flow only from the outside to the inside, principality is preserved when inference succeeds. Yet, as for stratified type inference [START_REF] Pottier | Stratified type inference for generalized algebraic data types[END_REF], it lacks monotonicity.

While previous approaches have mostly attempted to propagate types to GADT case analyses, we aim in the opposite direction at reducing the need for type information in case analysis. This aspect is orthogonal to propagation and improving either one improves type inference as a whole. Actually, OutsideIn already goes one step in that direction, by allowing type information to flow out of a pattern-matching case when no type equation was added. But it stops there, because if type equations were added, they could have been used and consequently the type of the branch is flagged ambiguous.

This led us to focus our attention on the definition of ambiguity. Type equations are introduced inside a pattern-matching branch, but with a local scope: the equation is not valid outside of the branch. This becomes a source of ambiguities. Indeed, a type equation allows implicit type conversions, i.e. there are several inter-convertible forms for types that we need not distinguish while in the scope of the equation, but they become nonconvertible-hence ambiguous-when leaving its scope, as the equation can no longer be used. Ambiguity depends both on the equations available, and on the types that leak outside of the branch: if removing the equation does not impair convertibility for a type, either because it was not convertible to start with, or because other equations are available, it need not be seen as ambiguous.

Since ambiguities must generally be solved by adding type annotations, a more precise definition and better detection of ambiguities become essential to reduce the need for explicit type information. By defining ambiguity inside the type system, we are able to restrict the set of valid typings. In this paper we present a type system such that among the valid typings there is always a principal one (i.e. subsuming all of them) and we provide a type inference algorithm that returns the principal solution when it exists. Moreover, our type system keeps the usual properties of ML, including monotonicity. This detection of ambiguity is now part of OCaml [START_REF] Leroy | The OCaml system release 4.00, Documentation and user's manual[END_REF].

Since propagating type information and reducing the amount of type information needed by case analysis are orthogonal issues, our handling of ambiguity could be combined with existing type inference algorithms to further reduce the need for type annotations. As less type information is needed, it becomes possible to use a weaker propagation algorithm that preserves monotonicity. This is achieved in OCaml by relying on the approach previously developed for first-class polymorphism [START_REF] Garrigue | Semi-explicit first-class polymorphism for ML[END_REF].

The rest of this paper is organized as follows. We give an overview of our solution in §2. We present our system formally and state its soundness in §3. We state principality and monotonicity in §4; by lack of space, we leave out some technical developments, all proofs, and the description of the type inference algorithm, which can all be found in the accompanying technical report [START_REF] Garrigue | Ambivalent types for principal type inference with GADTs[END_REF]. Finally, we compare with related works in §5.

2 An overview of our solution

Using ambivalence for refining the definition of ambiguity

The standard notion of ambiguity is so general that it may just encompass too many cases. Consider the following program. 3type (_,_) eq = Eq : (α,α) eq let f (type a) (x : (a,int) eq) = match x with Eq -> 1

Type eq is the classical equality witness. It is a GADT with two index parameters, denoted by the two underscores, and a single case Eq, for which the indices are the same type variable α. Thus, a value of type (a, b) eq can be seen as a witness of the equality between types a and b.

In the definition of f, we first introduce an explicit universal variable a, called a rigid variable, treated in a special way in OCaml as it can be refined by GADT pattern matching. By constraining the type of x to be (a,int) eq, we are able to refine a when pattern-matching x against the constructor Eq: the equation a = int becomes available in the corresponding branch, i.e. when typechecking the expression 1, which can be assigned either type a or int. As a result, f can be given either type (α, int) eq → int or (α, int) eq → α. This fulfills the standard definition of ambiguity and so should be rejected. But should we really reject it? Consider these two slight variations in the definition of f: let f 1 (type a) (x : (a,int) eq) = match x with Eq -> true let f 2 (type a) (x : (a,int) eq) (y : a) = match x with Eq -> (y > 0)

In f 1 , we just return true, which has the type bool, unrelated to the equation. In f 2 , we actually use the equation to turn y into an int but eventually return a boolean. These variants are not ambiguous. How do they differ from the original f? The only reason we have deemed f to be ambiguous is that 1 could potentially have type a by using the equation. However, nothing forces us to use this equation, and, if we do not use it, the only possible type is int. It looks even more innocuous than f 2 , where we indirectly need the equation to infer the type of the body.

So, what would be a truly ambiguous type? We obtain one by mixing a's and int's in the returned value (the left-margin vertical rules indicate failure): let g (type a) (x : (a,int) eq) (y : a) = match x with Eq -> if y > 0 then y else 0

Here, the then branch has type a while the else branch has type int, so choosing either one would be ambiguous. How can we capture this refined notion of ambiguity? The idea is to track whether such mixed types are escaping from their scope. Intuitively, we may do so by disallowing the expression to have either type and instead viewing it with an ambivalent type a ≈ int, which we just see syntactically as a set of types.

An ambivalent type must still be coherent, i.e. all the types it contains must be provably equal under the equations available in the current scope. Hence, although a ≈ int can be interpreted as an intersection type, it is not more expressive than choosing either representation (since by equations this would be convertible to the other type), but more precise: it retains the information that the equivalence of a and int has been assumed to give the expression the type a or int.

Since coherence depends on the typing context, a coherent ambivalent type may suddenly become incoherent when leaving the scope of an equation. This is where ambiguity appears. Hence, while an ambivalent type is a set of types that have been assumed interchangeable, an ambiguity arises only when an ambivalent type becomes incoherent by escaping the scope of an equation it depends on.

Ambiguous programs are to be rejected. Fortunately, ambiguities can be eliminated by using type annotations. Intuitively, in an expression (e : τ), the expressions e and (e : τ) have sets of types ψ 1 and ψ 2 that may differ, but such that τ is included in both, ensuring soundness of the change of view. In particular, while the inner view, e.g. ψ 1 , may be large and a potential source of ambiguities, the outer view, e.g. ψ 2 , may contain fewer types and remain coherent; this way the ambivalence of the inner view does not leak outside and does not create ambiguities. Consider, for example the program: let g 1 (type a) (x : (a,int) eq) y = match x with Eq -> (if (y : a) > 0 then (y : a) else 0 : a)

Type annotations on y and the conditional let them have unique outer types, which are thus unambiguous when leaving the scope of the equation. More precisely, (y : a) and 0 can be both assigned type a ≈ int, which is also that of the conditional if ... else 0, while the annotation (if ... else 0 : a) and variable y both have the singleton type a. (Note that the type of the annotated expression is the inner view for y but the outer view for the conditional.) Of course, it would be quite verbose to write annotations everywhere, so in a real language we shall let annotations on parameters propagate to their uses and annotations on results propagate inside pattern-matching branches. The function g 1 may just be written: let g 2 (type a) (x : (a,int) eq) (y : a) : a = match x with Eq -> if y > 0 then y else 0 or, using the OCaml syntax for explicitly polymorphic types: let g 2 : type a. (a,int) eq -> a -> a = fun x y -> match x with Eq -> if y > 0 then y else 0

However, we will ignore this aspect in this work.

Avoiding aggressive propagation of type annotations

A natural question at this point is why not just require that the type of the result of pattern-matching a GADT be fully known from annotations? This would avoid the need for this new notion of ambiguity. This is perhaps good enough if we only consider small functions: as shown for g 2 , we may write the function type in one piece (as in either one of the last two versions) and still get the full type information. However, the situation degrades with local let bindings. For example, consider the function p below:

let p (type a) (x : (a,int) eq) : int = let y = (match x with Eq -> 1) in y * 2

The return type int only applies to y*2, so we cannot propagate it automatically as an annotation for the definition of y. Basically, one would have to explicitly annotate all let bindings whose definitions use pattern-matching on GADTs. This may easily become a burden, especially when the type is completely unrelated to the GADTs (or accidentally related as in the definition of f, above). We believe that our notion of ambiguity is simple enough to be understood easily by users, avoids an important number of seemingly redundant type annotations, and provides an interesting alternative to non-monotonic approaches (see §5 for comparison). Some type annotations are still required, since the type of the (GADT part of the) scrutinee must always be provided. directly or indirectly. For example, the following variant h of f 2 without type annotations fails: let h (type a) x (y : a) = match x with Eq -> (y > 0)

In OCaml, in the absence of annotation on the GADT part of a scrutinee, we do not immediately fail, but fall back to typechecking as an ordinary datatype, i.e. without enriching the context with equality constraints. Hence, removing all type information from the previous example, we actually succeed, but with type (α, α) eq-> int -> bool.

let h 1 x y = match x with Eq -> (y > 0)

Formal presentation

Since our interest is type inference, we may assume without loss of generality that there is a unique predefined (binary) GADT eq(•, •) with a unique constructor Eq of type ∀(α) eq(α, α) and existential types. The equivalence of expressiveness between the general case and this special case has been studied from a semantic point of view [START_REF] Johann | Foundations for structured programming with gadts[END_REF]; it also holds from a type inference perspective (it is easy to see that they generate similar type inference constraints [START_REF] Simonet | A constraint-based approach to guarded algebraic data types[END_REF]). However, we also omit existential types here, as this is an orthogonal issue, which does not raise any problem for type inference. The type eq(τ 1 , τ 2 ) denotes a witness of the equality of τ 1 and τ 2 and Eq is the unique value of type eq(τ 1 , τ 2 ). For conciseness, we specialize pattern matching to this unique constructor and just write use M 1 : τ in M 2 for match M 1 : τ with Eq -> M 2 .

Simple types. Types occurring in the source program are simple types:

τ ::= α | a | τ → τ | eq(τ, τ) | int
Type variables are split into two different syntactic classes: flexible type variables, written α, and rigid type variables, written a. As usual, flexible type variable are meant to be instantiated by any type-either during type inference or after their generalization. Conversely, rigid variables stand for some unknown type and thus are not meant to be instantiated by an arbitrary type. They behave like skolem constants. We write V , V f , and V r for the set of variables, flexible variables, and rigid variables.

Terms. Terms are expressions of the λ -calculus with constants (written c), the datatype Eq, pattern matching use M 1 : τ in M 2 , the introduction of a rigid variable ν(a) M or a type annotation (τ), i.e. a type annotation behaves as a coercion function and the usual annotation (M : τ) is seen as the application (τ) M:

M ::= x | c | M 1 M 2 | λ (x) M | let x = M 1 in M 2 | Eq | use M 1 : τ in M 2 | ν(a) M | (τ)
Although type annotations in source programs are simple types, their flexible type variables are interpreted as universally quantified in the type of the annotation (see §3.5).

Besides, we use-and infer-ambivalent types internally to keep track of the use of typing equations and detect ambiguities more accurately.

Ambivalent types

Intuitively, ambivalent types are sets of types. Technically, they refine simple types to express certain type equivalences within the structure of types. Every node becomes a set of type expressions instead of a single type expression and is labeled with a flexible type variable. More precisely, ambivalent types, written ζ , are recursively defined as:

ρ ::= a | ζ → ζ | eq(ζ , ζ ) | int ψ ::= ε | ρ ≈ ψ ζ ::= ψ α σ ::= ∀( ᾱ) ζ
A raw type ρ is a rigid type variable a, an arrow type ζ → ζ , an equality type eq(ζ , ζ ), or the base type int. A proper raw type is one that is not a rigid type variable. An (ambivalent) type ζ is a pair ψ α of a set ψ of raw types ρ labeled with a flexible type variable α. We use ≈ to separate the elements of sets of raw types: it is associative commutative, has the empty set ε for neutral element, and satisfies the idempotence axiom (ψ ≈ ψ) = ψ. For example, int ≈ int is the same as int. An ambivalent type ζ is always of the form ψ α and we write ζ for ψ. When ψ is empty ζ is a leaf of the form ε α , which corresponds to a type variable in simple types, hence we may just write α instead of ε α , as in the examples above. Type schemes σ are defined as usual, by generalizing zero or more flexible type variables. Rigid type variables may only be used free and cannot be quantified over. We introduce them in the typing environment but turn them into flexible type variables before quantifying over them, so they never appear as bound variables in type schemes.

In our representation, every node is labeled by a flexible type variable. This is essential to make type inference modular, as it is needed for incremental instantiation.

To see this, consider a context that contains a rigid type variable a, an equation a .

= int, and a variable x of type a, under which we apply a function choice of type α → α → α to x and 1. We first reason in the absence of labels on inner nodes. The partial application choice x has type a → a. To further apply it to 1, we must use the equation to convert both 1 of type int and the domain of the partial application to the ambivalent type int ≈ a. The type of the full application is then a. However, if we inverted the order of arguments, it would be int. Something must be wrong. In fact, if we notice in advance that both types a and int will eventually have to be converted to int ≈ a, we may see both x and 1 with type int ≈ a before performing the applications. In this case, we get yet another result int ≈ a, which happens to be the right one.

What is still wrong is that as soon as we instantiate α, we lose the information that all occurrences of α must be synchronized. The role of labels on inner nodes is to preserve this information. Revisiting the example, the partial application now has type a α → a α (we still temporarily omit the annotation on arrow types, as they do not play a role in this example). This is saying that the type is currently a → a but remembering that the domain and codomain must be kept synchronized. Then, the integer 1 of type int γ can also be seen with type (int ≈ a) γ and unified with the domain of the function a α , with the effect of replacing all occurrences of a α and of int γ by (int ≈ a) α . Thus, the function has type (int≈a) α → (int≈a) α and the result of the application has type (int ≈ a) α -the correct one. We now obtain the same result whatever the scenario.

This result type may still be unified with some other rigid variable a , as long as this is allowed by having some equation a .

= int or a . = a in the context, and refine its type to (int ≈ a ≈ a ) α . Since we cannot tell in advance which type constructors will eventually be mixed with other ones, all nodes must keep their label when substituted.

Replaying the example with full label annotations, choice has type ∀(α, γ, γ ) (α → (α → α) γ ) γ and its partial application to x has type ∀(α, γ) (a α → a α ) γ after generalization. Observe that this is less general than ∀(α, α , γ) (a α → a α ) γ but more general than ∀(α, γ) ((int ≈ a) α → (int ≈ a) α ) γ . Type variables. Type variables are either rigid variables a or flexible variables α. We write frv(ζ ) for the set of rigid variables that are free in ζ and ffv(ζ ) for the set of flexible variables that are free in ζ . These definitions are standard. For example, free flexible variables are defined as:

ffv(ψ α ) = {α} ∪ ffv(ψ) ffv(ε) = / 0 ffv(ρ ≈ ψ) = ffv(ρ) ∪ ffv(ψ) ffv(∀(α) σ ) = ffv(σ ) \ {α} ffv(a) = / 0 ffv(int) = / 0 ffv(ζ 1 → ζ 2 ) = ffv(ζ 1 ) ∪ ffv(ζ 2 ) ffv(eq(ζ 1 , ζ 2 )) = ffv(ζ 1 ) ∪ ffv(ζ 2 )
The definition is analogous for free rigid variables, except that frv(ψ α ) is equal to frv(ψ) and frv(a) is equal to {a}.

We write ftv(ζ ) the subset of ffv(ζ ) of variables that appear as leaves, i.e. labeling empty nodes and fnv(ζ ) the subset of ffv(ζ ) that are labeling nonempty nodes. In wellformed types these two sets are disjoint, i.e. ffv(ζ ) is the disjoint union of ftv(ζ ) and fnv(ζ ).

Rigid type variables lie between flexible type variables and type constructors. A rigid variable a stands for explicit polymorphism: it behaves like a nullary type con-structor and clashes, by default, with any type constructor and any other rigid variable but itself. However, pattern matching a GADT may introduce type equations in the typing context while type checking the body of the corresponding branch, which may allow a rigid type variable to be compatible with another type. Type equations are used to verify that all ambivalent types occurring in the type derivation are well-formed, which requires in particular that all types of a same node can be proved equal.

Interpretation of types. Ambivalent types may be interpreted as sets of simple types by unfolding ambivalent nodes as follows:

[[ε α ]] = {α} [[(ρ 1 ≈ ψ) α ]] = ρ∈ρ 1 ≈ψ [[ρ]] [[a]] = a [[int]] = int [[ζ 1 → ζ 2 ]] = {τ 1 → τ 2 | τ 1 ∈ [[ζ 1 ]], τ 2 ∈ [[ζ 2 ]]} [[eq(ζ 1 , ζ 2 )]] = {eq(τ 1 , τ 2 ) | τ 1 ∈ [[ζ 1 ]], τ 2 ∈ [[ζ 2 ]]}
The interpretation ignores labels of inner nodes. It is used below for checking coherence of ambivalent types, which is a semantic issue and does not care about sharing of inner nodes. For example, types

(int ≈ a) α → (int ≈ a) α and (int ≈ a) α 1 → (int ≈ a) α 2 are interpreted in the same way, namely as {int → int, a → a, a → int, int → a}.
A type ζ is said truly ambivalent if its interpretation is not a singleton. Notice that ψ may be a singleton ρ even though ψ α is truly ambivalent, since ambivalence may be buried deeper inside ρ, as in

((int ≈ a) α → (int ≈ a) α ) α 0 .
Converting a simple type to an ambivalent type. Given a simple type τ, we may build a (not truly) ambivalent type ζ such that [[ζ ]] = {τ}. This introduces new variables γ that are in fnv(ζ ), while the variables of ftv(ζ ) come from τ. We write τ for the most general type scheme of the form ∀( γ) ζ , which is obtained by labeling all inner nodes of τ with different labels and quantifying over these fresh labels. For example,

int → int is ∀(γ 0 , γ 1 , γ 2 ) (int γ 1 → int γ 2 ) γ 0 and α → α is ∀(γ 0 ) (ε α → ε α ) α 0 .
Notice that free type variables of τ remain free in τ .

Typing contexts

Typing contexts Γ bind program variables to types, and introduce rigid type variables a, type equations τ 1 . = τ 2 , and node descriptions α :: ψ:

Γ ::= / 0 | Γ , x : σ | Γ , a | Γ , τ 1 . = τ 2 | Γ , α :: ψ
Both flexible and rigid type variables are explicitly introduced in typing contexts. Hence, well-formedness of types is defined relatively to some typing context. In addition to routine checks, well-formedness judgments also ensure soundness of ambivalent types and coherent use of type variables.

Well-formedness of contexts Γ is recursively defined with the well-formedness of types Γ ρ and type schemes Γ σ . Characteristic rules are in Figure 1. It also uses the entailment judgment Γ ψ, which means, intuitively, that all raw types appearing in the set ψ can be proved equal from the equations in Γ (see §3.3). The last premise of Rule WF-TYPE-AMBIVALENT ensures that ambivalent types contain at most one raw-type that is not a rigid variable. As usual well-formedness of contexts ensures that type variables

(Γ ρ) ρ∈ψ Γ ψ |ψ \ V r | ≤ 1 Γ ψ Fig. 1.
Well-formedness of contexts and types are introduced before being used and that types are well-formed. It also ensures coherent use of type variables: alias constraints α :: ψ in the context Γ define a mapping that provides evidence that α is used coherently in the type σ . This is an essential feature of our system so that refining ambivalence earlier or later commutes, as explained above.

Entailment

Typing contexts may contain type equations. Type equations are used to express equalities between types that are known to hold when the evaluation of a program has reached a given program point. Type equations are added to the typing context while typechecking the expression at the current program point. The set of equations in the context defines an equivalence between types. Rule WF-TYPE-AMBIVALENT shows that ambivalent types can only be formed between equivalent types: the well-formedness of the judgment Γ ψ requires Γ ψ, i.e. that all types in ψ are provably equal under the equations in Γ , which is critical for type soundness; the rightmost premise requires that at most one type in ψ is not a rigid variable. For example, the ambivalent types int ≈ (int γ → int γ ) and (int γ → int γ ) ≈ (a γ → a γ ) are ill-formed. This is however not restrictive as the former would be unsound in any consistent context while the later could instead be written

(int ≈ a) γ → (int ≈ a) γ .
Well-formedness of a type environment requires that its equations do not contain free type variables. Equalities in Γ may thus be seen as unification problems where rigid variables are the unknowns. If they admit a principal solution, it is a substitution of the form (a i → τ i ) i∈I ; then, the set of equations (a i . = τ i ) i∈I is equivalent to the equations in Γ . If the unification problem fails, then the equations are inconsistent-in the standard model where type constructors cannot be equated 4 . This is acceptable and it just means that the current program point cannot be reached. Therefore, any ambivalent type is admissible in an inconsistent context.

The semantic judgment Γ ψ means by definition that any ground instance of Γ that satisfies the equations in Γ makes all types in the semantics of ψ equal. Formally: Definition 1 (Entailment). Let Γ be a typing environment. A ground substitution θ from rigid variables to simple types models Γ if θ (τ 1 ) and θ (τ 2 ) are equal for each equation τ 1 . = τ 2 in Γ . We say that Γ entails ψ and write

Γ ψ if θ ([[ψ]]
) is a singleton for any ground substitution θ that models Γ .

This gives a simple algorithm to check for entailment: compute the most general unifier θ of Γ ; then Γ ψ holds if and only if θ ([[ψ]]) is a singleton or θ does not exist.

Notice that the entailment depends on the equivalence relation defined by the equations in Γ and not on the particular set of equations that generates this equivalence. Hence, replacing equations in Γ by another set of equivalent equations or, in particular, adding an equation that is already a consequence of equations in Γ does not change entailment.

For instance, the following program is well-typed. because the inner equation learn on the inner match is a consequence of the equation learned on the outer match, hence z is not ambivalent on the inner match and only the outer match requires an annotation. let q (type a) (type b) (x0 : (b * b, a * int) eq) (x2 : (a, int) eq) (y : a) = match x0 with Eq -> let z = match x2 with Eq -> if y > 0 then y else 0 in (z : a)

Substitution

In our setting, substitutions operate on ambivalent types where type variables are used to label inner nodes of types and not just their leaves. They allow the replacement of an ambivalent node ψ α by a "more ambivalent" one ψ ≈ ψ α , using the substitution [α ← (ψ ≈ ψ ) α ]; or merging two ambivalent nodes ψ α 1 1 and ψ α 2 2 using the substitution

[α 1 , α 2 ← ψ 1 ≈ ψ 2 α 1 ].
To capture all these cases with the same operation, we define in Figure 2 a general form of substitution [α i ← ζ i ] i∈I that may graft arbitrary nodes ζ i at every occurrence of a label α i , written

[α ← ζ ];
As a result of this generality, substitutions are purely syntactic and may replace an ambivalent node with a less ambivalent one-or even prune types replacing a whole subtree by a leaf. Of course, we should only apply substitutions to types when they preserve (or increase) ambivalence. Definition 2. A substitution θ preserves ambivalence in a type ζ if and only if, for any α in dom(θ ) and any node ψ α in ζ , we have ψθ ⊆ (ψ α )θ .

(ψ α i )θ = ζ i (ψ γ )θ = (ψθ ) γ (ρ i∈I i )θ = (ρ i θ ) i∈I (∀(α) ζ )θ = ∀(α) ζ (θ \ {α})

Typing rules

Typing judgments are of the form Γ M : σ as in ML. However, typing rules, defined in Figure 3, differ from the traditional presentation of ML typing rules in two ways. On the one hand, we use a constraint framework where Γ carries node descriptions α :: ψ to enforce their sharing within different types. On the other hand, typing rules also carry type equations τ 1 . = τ 2 in typing contexts that are used to show the coherence of ambivalent types via direct or indirect uses of well-formedness judgments.

All axioms require well-formedness of Γ so that whenever a judgment Γ M : σ holds, we have Γ . Rule M-INST instantiates the outermost variable of a type scheme. It is unusual in two ways. First, we write σ [α ← ψ α 0 ] rather than just σ in the quantified type. This trick ensures that all nodes labeled with α were indeed ψ α 0 and overcomes the absence of ψ 0 in the binder. Intuitively, the instantiated type should be σ

[α ← ψ α 0 ][α ← ψ γ ],
but this happens to be equal to σ [α ← ψ γ ]. Second, we require ψ 0 ⊆ ψ to ensure preservation of ambivalence, as explained in the previous subsection. Finally, the premise Γ ψ γ ensures that the resulting type is well-formed.

Rule M-GEN introduces polymorphism implicitly, as in ML: variables that do not appear in the context can be generalized. The following rule is derivable from M-GEN and M-INST, and can be used as a shortcut when variable α does not appear in ψ γ : M-BIND Γ , α ::

ψ 1 M : ψ γ α = γ Γ M : ψ γ
Rule M-NEW enables explicit polymorphism (and explicit type equations using witnesses). For that purpose, it introduces a rigid type variable a in the typing context that may be used inside M-typically for introducing type annotations. However, polymorphism becomes implicit in the conclusion by turning the rigid type variable a into a quantified flexible type variable α when exiting the scope of the ν-form. Polymorphism can then be eliminated implicitly 5 as regular polymorphism in ML. The second premise ensures that the rigid type variable a does not appear anywhere else but in a α .

Our version of Rule M-FUN generalizes the type γ introduced for annotating the arrow type. We could also have used this other equivalent but less readable rule:

Γ , γ :: ζ 0 → ζ , x : ζ 0 M : ζ Γ λ (x) M : (ζ 0 → ζ ) γ
Rule M-APP differs from the standard application rule in two ways: a minor difference is that the arrow type has a label as in Rule M-FUN; a major difference is that the type of M 1 may be ambivalent-as long as it contains an arrow (raw) type of the form

ζ 2 → ζ . In particular, the premise Γ M 1 : ((ζ 2 → ζ ) ≈ ψ) α does not, in general, im- ply Γ M 1 : (ζ 2 → ζ ) α ,
as this could lose sharing. Hence, we have to read the arrow structure directly from the ambivalent type. Since well-formedness ensures that there is at most one arrow type in an ambivalent type (Rule WF-TYPE-AMBIVALENT), ψ can only be composed of rigid type variables. So the application rule remains deterministic. Rule M-LET is as usual.

Rule M-ANN allows explicit loss of sharing via type annotations. It is presented as a retyping function of type scheme (τ), i.e. a function that changes the labeling of the type of its argument without changing its behavior. The types of the argument and the result need not be exactly τ but consistent instances of τ-see the definition of τ , above. Annotations are typically meant to be used in expressions such as (τ) M, also written (M : τ), which forces M to have a type that is an instance of τ. While this is the only effect it would have in ML, here it also duplicates the polymorphic skeleton of M, which allows different labeling of inner nodes in the type of M passed to the annotation and its type after the annotation. By contrast, free type variables of τ remain shared between both types. The example below illustrates how type annotations can be used to remove ambivalence.

Rule M-WITNESS says that the Eq type constructor can be used to witness an equality between equal types as eq(ζ , ζ ) γ , for any type ζ . Conversely, an equality type eq(ζ 1 , ζ 2 ) γ , can only have been built from the Eq type constructor.

Rule M-USE uses this fact to learn and add the equation τ 1 . = τ 2 in the typing context while typechecking the body of M 2 ; the witness M 1 must be typable as an instance of the type eq(τ 1 , τ 2 ) up to sharing of inner nodes. Since the equation is only available while typechecking M 2 , it is not present in the typing context of the conclusion. Hence, the type ζ 2 must be well-formed in Γ . But this is a direct consequence of the second premise: it implies Γ , τ 1 . = τ 2 ζ 2 , which in turn requires that all labels of ζ 2 (which contain no quantifiers) have node descriptions in Γ , so that they cannot depend on τ 1 . = τ 2 . Typically, ambivalent types needed for the typing of M 2 are introduced using rule M-BIND, which means that they cannot remain inside ζ 2 , so that there is no way to keep an ambiguous type. Notice that the well-formedness of Γ , τ 1 . = τ 2 implies that τ 1 and τ 2 contain no flexible type variables (rules WF-TYPE-EQUAL and WF-CTX-EQUAL).

Example

We now illustrate the typing rules through an example. Assume that (if then else ) is given as a primitive with type scheme

∀(γ b , γ 2 , γ 1 , γ 0 ) ∀(α) (bool γ b → (α → (α → α) γ 2 ) γ 1 ) γ 0 . Let Γ be Γ a , ∆ , ∆ , y : (int ≈ a) α where Γ a is a, a . = int and ∆ is α :: int, γ 2 :: α → α, γ 1 :: α → (α → α) γ 2 and ∆ is γ b :: bool, γ 0 :: γ b → (α → (α → α) γ 2 ) γ 1 .
Using M-VAR for premises, we have:

M-APP Γ if then else : (bool γ b → (α → (α → α) γ 2 ) γ 1 ) γ 0 Γ true : γ b Γ if true then else : (α → (α → α) γ 2 ) γ 1
We also have Γ 1 : (int ≈ a) α and Γ y : (int ≈ a) α by M-INST and M-VAR. Hence, we have Γ if true then 1 else y : (int ≈ a) α by M-APP. This leads to the following derivation:

M-FUN Γ if true then 1 else y : (int ≈ a) α M-INST Γ a , ∆ , ∆ λ (y) if true then 1 else y : ∀(γ) ((int ≈ a) α → (int ≈ a) α ) γ M-BIND Γ a , ∆ , ∆ M : ((int ≈ a) α → (int ≈ a) α ) γ 2 M-GEN Γ a , ∆ M : ((int ≈ a) α → (int ≈ a) α ) γ 2 Γ a M : ∀(α, γ) ((int ≈ a) α → (int ≈ a) α ) γ
where M is λ (y) if true then 1 else y. Rule M-BIND is used for variables γ b and γ 0 in ∆ that are no longer used (we omitted the other premises), while Rule M-GEN is used for variables α and γ 2 in ∆ . Notice that neither Γ a M : ∀(α, α , γ) ((int ≈ a) α → int ≈ a α ) γ nor Γ a M : ∀(α, γ) (int α → int α ) γ are derivable. It is a key feature of our system that sharing and ambivalence can only be increased implicitly. Still, it is sound to decrease them explicitly, using a type annotation, as in Γ a (a → int) M :

∀(α, α , γ) (a α → int α ) γ .
The expression M 0 equal to use x : eq(a, int) in (a → int) M is not ambiguous thanks to the annotation around M. Indeed, use x : eq(a, int) in M would be rejected, since an instance of the type of M always will contain an ambivalent type of the from (int ≈ a ≈ . . .) α which cannot be well-formed in a, a . = int. Hence, we have:

M-USE* Γ (eq(a, int)) x : ζ 1 Γ , a . = int (a → int) M : a → int M-APP* M-NEW M-FUN* ∆ , a, ∆ , x : eq(a γ 1 , int γ 2 ) γ M 0 : a → int ∆ , a, α :: a λ (x) M 0 : eq(a, int) → a → int ∆ ν(a) λ (x) M 0 : ∀(α) eq(α, int) → α → int ∆ Eq : . . . (ν(a) λ (x) M 0 ) Eq : int → int ∀( ᾱ) ζ = ∀( ᾱ) ζ ε α = α āα = min ā int ≈ āα = int ζ 1 → ζ 2 ≈ āα = ζ 1 → ζ 2 eq(ζ 1 , ζ 2 ) ≈ āα = eq( ζ 1 , ζ 2 ) Fig. 4. Canonical types x = x c = c M 1 M 2 = M 1 M 2 λ (x) M = λ (x) M Eq = Eq let x = M 1 in M 2 = let x = M 1 in M 2 use M 1 : τ . = τ in M 2 = (λ (Eq) M 2 ) M 1 ν(a) M = M (τ) = λ (x) x
Fig. 5. Elaboration of terms for some well-chosen ∆ , ∆ and Γ , where R * means R preceded and followed by a sequence of M-INST, M-BIND, and M-GEN. The rigid variable a is turned into the polymorphic variable α which is then instantiated to int α before the application to Eq.

Type soundness

Type soundness is established by seeing our system as a subset of HMG(X) [START_REF] Simonet | A constraint-based approach to guarded algebraic data types[END_REF]. For this purpose, we exhibit a translation from our language to HMG(X) that preserves well-typedness. Types and typing contexts are translated as well so that the translation of typing judgments in our language is a valid typing judgment in HMG(X).

The translation emphasizes an interesting aspects of our system: ambivalent types are only a gadget for type inference and can be dropped in the translation. The key is that well-formed ambivalent types are such that all simple types in their interpretation are provably equivalent in the current context, i.e. under the equality assumptions that have been introduced by use expressions.

The type system HMG(X) is designed for expressiveness rather than type inference and expressions contain no explicit type information at all. Moreover, the language is quite rich, and assume arbitrary GADT type-definitions while we only use one predefined datatype Eq with a single data-constructor Eq of type ∀(α) α → α → eq(α, α). In particular, the expression use M 1 : eq(τ 1 , τ 2 ) in M 2 that destructs a GADT stands for the immediate application (λ (Eq) M 2 ) M 1 in HMG(X). Notice that we only use HMG(X) with equality constraints-and with general subtyping constraints.

The translation of ambivalent types into simple types is given in Figure 4. The translation ζ of a well-formed type ζ always picks a simple type that is in the interpretation

[[ζ ]] of ζ .
To simplify, we make the translation deterministic. For that purpose, we assume given an ordering of rigid variables (which may coincide with the order in which variables are introduced in the context). The translation is only defined for well-formed types, for which every raw type contains at most one type that is not a rigid variable, i.e. a structured type. Leaves ε α are translated into regular type variables; Inner nodes ρ ≈ ψ α are recursively translated into ρ , where ρ is a structure type or a rigid type variable smaller than all rigid type variables of ψ.

The translation of contexts is the point-wise translation of bindings, except for variable bindings (both rigid-variables and node descriptions), which are simply dropped.

The translation of terms is given on Figure 5. It is an homorphism, except for two things: on the one hand, it drops all type information; on the other hand, it translates use M 1 : τ 1 . = τ 2 in M 2 into the immediate application (λ (Eq) M 2 ) M 1 as described above. Equality constraints and our two constructs Use and Eq are just a particular instance of a GADT, with a single data-constructor Eq of type ∀(α) α → α → eq(α, α).

Theorem 1. If Γ M : σ then Γ M : σ .
The proof is by structural induction on the derivation of the typing judgment in our system. The key is that well-typedness implies well-formedness of ambivalent types, which implies that all types in the semantics of a well-formed ambivalent types are provably equal under the equalities in the typing context. This is used in particular in the translation of instantiation, which changes ambivalence in our system and relies on constraint entailment in HMG(X).

Properties

In this section we will prove the following properties.

Monotonicity Let Γ σ ≺ σ be the instantiation relation, which says that any monomorphic instance of σ well-formed in Γ is also a monomorphic instance of σ . This relation is extended point-wise to typing contexts: Γ ≺ Γ if for any term variable x in dom(Γ ), Γ Γ (x) ≺ Γ (x), all other components of Γ and Γ being identical. We may now state monotonicity: in our system, if Γ M : ζ and Γ ≺ Γ , then Γ M : ζ .

Existence of principal solutions to type inference problems This is our main result. Although further developments in this section will use the split form, described below, we first formulate this important result in the mixed form used up to now. A typing problem is a typing judgment skeleton Γ M : ζ , where Γ omits all node descriptions α :: ψ (hence, Γ is usually not well-formed, but can be extended into a well-formed environment by interleaving the appropriate node descriptions with other bindings in Γ ).

A solution to a typing problem is a pair of a substitution θ that preserves ambivalence for the types in Γ and ζ , together with a context ∆ that contains only node descriptions, such that Γ θ and ∆ can be interleaved to produce a well-formed typing context, written Γ θ | ∆ , and the judgment Γ θ | ∆ M : ζ θ holds.

For any typing problem, the set of solutions is stable by substitution and is either empty or has a principal solution (∆ , θ ), i.e. one such that any other solution (∆ , θ ) is of the form θ = θ • θ for some substitution θ that preserves well-formedness in

Γ θ | ∆ , i.e. for any type ζ such that Γ θ | ∆ ζ , we have Γ θ | ∆ ζ θ .
Sound and complete type inference Principality of type inference is proved as usual by exhibiting a concrete type inference algorithm. This algorithm (presented in subsection 4.5) relies on a variant of the standard unification algorithm that works on ambivalent types and preserves their sharing. It uses a typing constraint approach, which converts typing problems to unification problems, while also ensuring that inferred types are well-formed, i.e. coherent, properly scoped, and acyclic. The use of constraints here is however just a convenience: since the ambivalence information is contained in types themselves, constraints can always be solved prior to type generalization so that we do not need constrained type schemes. That is, constraints are just a way to describe the algorithmic steps without getting into implementation details: OCaml itself uses a variant of Milner's algorithm J [START_REF] Milner | A theory of type polymorphism in programming[END_REF].

Split view

The grammar of types we have presented so far is quite convenient for the user to read or write types, since it is presented as a usual tree-structure with additional label decorations on every node. However, while close to our usual representation of types, there is redundancy: the description of nodes is repeated on every node but also in the typing context. While this eases the reading of types, it makes them harder to manipulate technical developments and proofs.

To solve this tension, we introduce an alternative view, call the split view, which is strictly equivalent to the mixed view, but avoids redundancy by representing internal nodes only by their labels. To avoid confusion, we will refer to the previous definition as types in the mixed view.

Types The grammar of ambivalent types ς in split form is defined as:

ρ :: = a | α → α | eq(α, α) | int ψ :: = ε | ρ ≈ ψ ∆ :: = / 0 | ∆ , α :: ψ ς :: = ∆ α
We reuse the same non-terminals for raw types ρ-as both forms are have the same meaning, indeed. However, we write ς instead of ζ for types in split form so as to avoid the confusion. By contrast with mixed types ζ , the syntactic definition of split types ς is not recursive, as we just write a labels α instead of nodes ψ α and recover ψ from α using a label context ∆ mapping labels to their content ψ. As a result, an ambivalent type is now a pair ∆ α of a type context and a flexible type variable. In practice, however, the label context is often part of a larger context, which is either left implicit or fixed explicitly.

The mixed form of ∆ α can be obtained by starting from α and recursively recovering contents from ∆ . For instance, the split form α :: int, α 0 :: α → α α 0 corresponds to the mixed form (int α → int α ) α 0 . Here is the formal translation:

∆ α = α ∆ α ∆ = ( ∆ (α) ∆ ) α ε ∆ = ε ρ ≈ ψ ∆ = ρ ∆ ≈ ψ ∆ a ∆ = a α 1 → α 2 ∆ = α 1 ∆ → α 2 ∆ eq(α 1 , α 2 ) ∆ = eq( α 1 ∆ , α 2 ∆ ) int ∆ = int
Well-formed types have both a mixed form and a split form. Let ζ be a well-formed type in mixed form. Then, the split form of ζ is ∆ α where ∆ is mapping every flexible variable α of ζ to the unique set ψ in ζ that α labels. Reciprocally, a wellformed type ∆ α in split form is such that α ∈ dom(∆ ), and there is a strict partial order ≺ ∆ on dom(∆ ) such that for each γ ∈ dom(∆ ), the variables of ∆ (γ) precede γ. This guarantees that the above translation function is well-defined and terminates.

Given a type ψ α in mixed form, we write |ψ α | for the minimal context of ψ α , i.e. the smallest well-formed ∆ such that α ∆ = ψ α .

Free variables Free variables of a type in mixed form are defined as follows:

ffv(∆ α) = ffv ∆ (α) ffv ∆ (α) = {α} ∪ ffv ∆ (∆ (α)) ffv ∆ (ε) = / 0 ffv ∆ (ρ ≈ ψ) = ffv ∆ (ρ) ∪ ffv ∆ (ψ) ffv ∆ (a) = / 0 ffv ∆ (int) = / 0 ffv ∆ (α 1 → α 2 ) = ffv ∆ (α 1 ) ∪ ffv ∆ (α 2 ) ffv ∆ (eq(α 1 , α 2 )) = ffv ∆ (α 1 ) ∪ ffv ∆ (α 2 )
Definitions for frv ∆ (α) are similar, with frv ∆ (α) and frv ∆ (a) becoming equal to frv ∆ (∆ (α)) and {a}, respectively.

Type schemes In the split view, we need to include a label context inside type schemes, since the description of nodes is not inlined anymore: The translation from split form to mixed form is then extended to type schemes.

σ ::= ∀(∆ ) α ∀(∆ 1 ) α ∆ = ∀(dom(∆ 1 )) α ∆ ,∆ 1 For instance, ∀(γ b , γ 1 , γ b , γ 0 ) ∀(α) (bool γ b → (α → (α → α) γ 2 ) γ 1 ) γ becomes ∀(∆ ) γ where ∆ is α, γ b :: bool, γ 2 :: α → α, γ 1 :: α → γ 2 , γ 0 :: bool γ b → γ 1 .
Substitution In the split view, node descriptions must always preexist in the typing context (during type inference, the typing context will be extended as needed with new node descriptions). Thus, it is sufficient for substitutions to substitute variables for variables-and extend these structurally to substitutions on raw types, Preservation of ambivalence is slightly generalized: Typing rules Typing rules in split form are given in figure 6. Most of them can be obtained by replacing mixed types of the form ζ = ψ γ by simply γ. When Γ already contains γ :: ψ, this alone is sufficient. But we need to be a bit more careful with type schemes and substitution. An advantage of split form schemes is that they contain the specification of quantified nodes inside their binders. This simplifies rule S-INST and S-NEW. However, a side-effect of this specification is that even variables that do not occur in the body of the scheme are constrained. As a result, some uses of M-INST, which ignored the constraint as it was not kept in the type scheme, are no longer valid with S-INST.

To assist the weaker S-INST we add a new rule S-BIND, which mimics the derived rule M-BIND, allowing to discard node descriptions that are not referenced anymore. Since α :: ψ is rightmost in the context of the premise, and γ is not α, it can safely be discarded in the conclusion. To replace a use of M-INST on an absent variable, one just needs the following two steps, when there is only one quantifier.

S-BIND

S-INST

Γ , α :: If there are several quantifiers, they must first all be instantiated, then S-BIND is applied for unused variables, which must be on the right of the context, then S-GEN is used repeatedly to reconstruct the type scheme.

ψ M : ∀(α :: ψ) γ Γ , α :: ψ M : γ[α ← α] α = γ Γ M : γ Γ (eq(τ 1 , τ 2 )) M 1 : γ 1 Γ , τ 1 . = τ 2 M 2 : γ 2 Γ use M 1 : eq(τ 1 , τ 2 ) in M 2 : γ 2
As we mentioned before, in the mixed form M-BIND is derivable, so we can translate back from split form to mixed form:

M-INST M-GEN Γ , α :: ψ 1 M : ψ γ Γ M : ∀(α) ψ γ [α ← ψ α 1 ] Γ ψ γ Γ M : ψ γ [α ← ψ γ ]

Substitutivity

As we just mentioned at the beginning of this section, an essential property of type systems is substitutivity of types. We restate it formally in split form, as the presence of node descriptions in the typing context makes it differ from other type systems.

To simplify the handling of the context, we first define an interleaving operation Γ | ∆ , which merges a pure typing context Γ , which term variables, rigid type variables, and equations -but no node descriptions-, with a label context ∆ , composed only of node descriptions α :: ψ. The non-deterministic interleaving operation Γ | ∆ is defined by reordering the components of ∆ , and inserting them between the components of Γ .

Γ | ∆ expresses that Γ and ∆ can be merged to obtain a well-formed typing context. Checking the well-formedness is decidable: one just has to try inserting at all possible positions, and check whether the result is well-formed. The judgment

Γ | ∆ M : ζ implies Γ | ∆ .
Now the intuition is that apply a substitution ∆ θ : ∆ to a typing context Γ | ∆ turns it into the typing context θ (Γ ) | ∆ .

Our first lemma checks that well-formedness is preserved. We can then state and prove the substitution lemma. Case S-BIND is similar. Case S-INST: By induction hypothesis we have θ (Γ ) | ∆ M : ∀(α :: ψ) σ . We assume that θ (γ) = γ . From ∆ θ : ∆ , we know that γ :: ψ 3 ∈ ∆ and ψ 2 ⊆ ψ 3 . As a result we also get ψ ⊆ ψ 3 , and we conclude by rule S-INST.

Other cases are easy.

Generic instance

Generic instance in ML is defined as the iteration of type instantiation, followed by generalization of freshly introduced type variables. Namely, σ 1 is more general than σ 2 , written σ 1 ≺ σ 2 if and only if σ 1 and σ 2 are of the form ∀( ᾱ1 ) τ and ∀( ᾱ2

) τ[ ᾱ1 ← τ 1 ],
respectively, where α 2 are not free in σ 1 .

While ≺ is a binary relation in ML, it also depends on the typing context in our setting, because type instantiation must preserve well-formedness, which depends on the typing context. Definition 4. We say that σ 2 is an instance of σ 1 under Γ , which we write Γ σ 1 ≺ σ 2 , if and only if σ 1 and σ 2 are of the form ∀(∆ 1 ) α and ∀(∆ 2 ) θ (α) such that ∆ 1 θ :

(Γ , ∆ 2 ), dom(θ ) ⊆ dom(∆ 1 ), dom(∆ 2 ) ∩ dom(Γ ) = / 0, and Γ , ∆ 2 .
If the judgment Γ M : σ holds and Γ σ ≺ σ , then the judgment Γ M : σ also holds-it is in fact derivable from the former by a sequence of S-INST, S-BIND, and S-GEN rules.

The generic instance relation between type schemes may be lifted into a relation between contexts. We write Γ ≺ Γ to mean that Γ and Γ coincide except on program variables where the images are in a point-wise generic instance relation.

Strengthening of the typing context is the opposite of generic instance. We prove monotonicity with respect to strengthening.

Lemma 3 (Monotonicity).

If Γ M : σ and Γ ≺ Γ then Γ M : σ .

Proof. The proof goes by induction on the derivation.

-Rule S-VAR: we have x : σ ∈ Γ and x : σ ∈ Γ , with Γ σ ≺ σ . We can replace Γ x : σ by Γ x : σ followed by instantiation and generalization steps leading to Γ | ∆ x : σ .

-All other cases are trivial induction steps.

Canonical derivations

The rules in Figure 6 are not syntax directed. Indeed, rules S-INST, S-GEN and S-BIND may be used anywhere in a derivation. However, we may put derivations in canonical forms-which helps reasoning by cases on derivation in proofs. We will also replace S-NEW by the following S-NEW', which is trivially derivable by the addition S-GEN steps before S-NEW, and S-INST steps after.

S-NEW'

Γ , a, α :: a, ∆ M : γ Γ , α :: ε, ∆ γ Γ , α :: ε, ∆ ν(a) M : γ Notice that α is the unique flexible type variable that labels a. Proof. We prove that S-INST can be pushed up until it reaches a legal position, and S-BIND and S-GEN can be pushed down similarly.

For rule S-BIND we need to see all the rules which do not allow S-BIND as a premise.

-Rule S-INST is impossible, since its premise is not a monotype.

-In rule S-FUN, we move S-BIND to the conclusion, applying permutaiton to the premise, to put x : γ 0 last.

-In rule S-APP, from either of the premise, we move S-BIND to the conclusion, weakening the other premise (i.e. adding α :: ψ to Γ .) -Similarly for the second premise of rule S-LET and the first premise of S-USE.

The only remaining case is rule S-GEN above rule S-INST. This amounts to the derivation:

S-INST S-GEN Γ , α :: ψ M : σ Γ M : ∀(α :: ψ) σ γ :: ψ 2 ∈ Γ ψ ⊆ ψ 2 Γ M : σ [α ← γ]
We split Γ as Γ 0 | ∆ . We can apply the substitution lemma to Γ 0 | ∆ , α ::

ψ M : σ , with ∆ , α :: ψ [α ← γ] : ∆ , which gives Γ 0 | ∆ M : σ [α ← γ],
with a derivation two steps shorter than the original one.

SUBST α 1 ∈ ffv(ϕ) α 1 = α 2 ϕ ∧ α 1 → α 2 ϕ[α 1 → α 2 ] ∧ α 1 → α 2 DELETE ϕ ∧ α → α ϕ MERGE ϕ ∧ α :: ψ 1 ∧ α :: ψ 2 ϕ ∧ α :: ψ 1 ≈ ψ 2 DECOMP-ARR ϕ ∧ α :: (α 1 → α 2 ) ≈ (α 1 → α 2 ) ≈ ψ ϕ ∧ α :: (α 1 → α 2 ) ≈ ψ ∧ α 1 → α 1 ∧ α 2 → α 2 DECOMP-EQ ϕ ∧ α :: eq(α 1 , α 2 ) ≈ eq(α 1 , α 2 ) ≈ ψ ϕ ∧ α :: eq(α 1 , α 2 ) ≈ ψ ∧ α 1 → α 1 ∧ α 2 → α 2 CONTEXT ϕ ϕ ∃α.ϕ ∃α.ϕ EXTRUDE α ∈ ffv(ϕ 1 ) ϕ 1 ∧ (∃α.ϕ 2 ) ∃α.(ϕ 1 ∧ ϕ 2 )
Fig. 7. Unification algorithm

Existence of principal derivations

In this section, we prove the existence of principal derivations by providing an algorithm that either finds one, or fails when the input program admits no typing derivation. Our algorithm is a constraint-based variant of W. The unification part takes inspiration from a structural polymorphism framework developed for variants and records [START_REF] Garrigue | A certified implementation of ML with structural polymorphism[END_REF], and the inference part reproduces the style used for semi-explicit first-class polymorphism [START_REF] Garrigue | Semi-explicit first-class polymorphism for ML[END_REF].

We first describe unification on ambivalent types. Definition 6. A unification problem ϕ is a formula of the form:

ϕ ::= / 0 | ∃(α) ϕ | ϕ ∧ ϕ | α :: ψ | α → α Definition 7.
A unifier (also called a solution) of a unification problem ϕ is a pair of a label context ∆ and a variable substitution θ such that θ maps both sides of every elementary substitution α 1 → α 2 in ϕ to the same variable, and for any equation α :: ψ in ϕ, there is a ψ 0 containing at most one proper raw type, such that θ (α) ::

ψ 0 ∈ ∆ and θ (ψ) ⊆ ψ 0 .
The pair (∆ , θ ) corresponds to a substitution in the mixed view. The resolution of a unification problem is a sequence of transformations that preserve the set of unifiers. These transformations are defined on Figure 7. They are of three kinds.

we may apply a substitution (or, as a special case, discard it if meaningless); we may merge two constraints; or we may decompose a constraint, introducing new substitutions, when the same constructor → or eq appears twice in a constraint.

A unifier (∆ , θ ) is more general than (∆ , θ ), noted (∆ , θ ) (∆ , θ ), if there exists a substitution θ 1 such that θ 1 • θ = θ and (∆ , θ 1 ) is a unifier of ∆ , or equivalently ∆ θ 1 : ∆ .

A unification problem (∆ , θ ) is solved when no applicable substitution is left, and the merging and decomposition rules do not apply anymore. At that point we can directly read a unifier from the solved problem, collecting the substitutions in θ , and the constraints in ∆ .

Lemma 5. Unification of ambivalent types admits a most general unifier, and there exists an algorithm returning such an unifier.

Proof. We first prove termination. We say that a variable is solved if it appears at most once, and only on the left hand side of a substitution. We take as measure number of unsolved variables, total size of node descriptions, number of substitutions . DELETE decreases the number of substitutions, SUBST decreases the number of unsolved variables, remaining ones decrease the total size.

Next we prove that if ϕ ϕ , and ∃ ᾱ.∆ ∧ θ is a solution of ϕ, then it is also a solution of ϕ , and reciprocally.

In rule SUBST, any solution of the premise or the conclusion must satisfy θ

(α 1 ) = θ (α 2 ), so that θ (ϕ) = θ (ϕ[α 1 ← α 2 ]).
In rule DELETE, α → α is redundant, so that the two constraints are equivalent.

In rule MERGE, a solution of either the premise or the conclusion must satisfy

θ (α) = α and θ (ψ 1 ≈ ψ 2 ) = θ (ψ 1 ) ≈ θ (ψ 2 ) ⊂ ∆ (α ), so they are equivalent. In rule DECOMP-ARR, if (∆ , θ ) is a solution of the premise then θ (α 1 → α 2 ≈ α 1 → α 2 ≈ψ) ⊆ ∆ (α)
, which, combined with the above restriction on ∆ , means that ∆ (α 1 ) = ∆ (α 1 ) and ∆ (α 2 ) = ∆ (α 2 ), and as a result this is also a solution of the conclusion. Reciprocally, as solution of the conclusion must satisfy the same equalities on type variables, so the it is also a solution of the premise. The correctness of rule DECOMP-EQ can be proved similarly.

Our type inference algorithm, given in figure 8, is based on constraint generation and solving. For each rewriting rule of the form Γ M : γ ∃ ᾱ.ϕ we assume implicitly the premise ᾱ ∩ (ffv(Γ ) ∪ {γ}) = / 0. In these rules, Γ does not contain node descriptions. To solve the type inference problem of whether Γ M : γ is true for some instance Γ of Γ , we first split Γ into Γ 0 and ∆ 0 such that Γ = Γ 0 | ∆ 0 , and then apply the rewriting rules of figures 7 and 8 starting from the inference constraint Γ 0 ; ∆ 0 M : γ.

If we can rewrite it to ∃ ᾱ.∆ 1 ∧ θ , we obtain a principal derivation θ (Γ 0 ) ∧ ∆ 1 M : θ (γ). Otherwise, since the unification rules can never fail, rewriting must have been blocked by one of the premises. But again, premises about variable names never fail: we can always choose some variable names to satisfy them. The remaining premises are variable access for Γ x : γ, which may fail if x is not defined in Γ , and the wellformedness checks Γ | ∆ , in the last 3 rules. The well-formedness checks ensure simultaneously coherence, proper scoping of rigid variables, and the absence of cycles inside ambivalent types.

We define the restriction of a unifier to a set of variables as

(∆ , θ )| ᾱ = (∆ | ffv ∆ (θ ( ᾱ)) , θ | ᾱ )
. This is used in rules I-NEW, I-USE and I-CONCL.

The following lemma justifies our delayed well-formedness checks.

I-VAR Γ (x) = ∀(∆ ) α dom(∆ ) = ᾱ Γ x : γ ∃ ᾱ.∆ ∧ γ → α I-NEW Γ , a M 1 : γ ∃ ᾱ.∆ ∧ θ θ (Γ ), a | ∆ ∆ = ∆ \ {α :: a ∈ ∆ } Γ ν(a) M 1 : γ ∃ ᾱα 1 .((∆ [α ← α 1 ] α::a∈∆ , α 1 :: ε), θ [α ← α 1 ] α::a∈∆ )| ffv(Γ ),γ I-FUN Γ λ (x) M 1 : γ ∃α 1 α 2 .(Γ , x : α 1 M 1 : α 2 ) ∧ α 1 :: ε ∧ α 2 :: ε ∧ γ :: α 1 → α 2 I-APP Γ M 1 M 2 : γ ∃α 1 α 2 .(Γ M 1 : α 1 ) ∧ (Γ M 2 : α 2 ) ∧ α 1 :: α 2 → γ I-LET Γ M 1 : γ 1 ∃ ᾱ.∆ ∧ θ γ 1 ∈ ᾱ σ = Gen(θ (γ 1 ), θ (Γ ), ∆ ) Γ let x = M 1 in M 2 : γ ∃ ᾱ, γ 1 .∆ ∧ θ ∧ (θ (Γ ), x : σ M 2 : θ (γ)) I-ANN τ → τ = ∀(∆ ) α ftv ∆ (α) = ᾱ Γ (τ) : γ ∃ ᾱ, dom(∆ ).∆ ∧ γ → α I-WITNESS
Γ Eq : γ ∃α.γ :: eq(α, α) Proof. An environment is well-formed if 1. term and type variable are introduced only once (rules WF-CTX-EXPR, WF-CTX-RIGID and WF-CTX-FLEX), 2. type variables (both rigid and flexible) are introduced before they are used (rules WF-TYPE-and WF-SCHEME), 3. all ambivalent types are coherent (rule WF-TYPE-AMBIVALENT).

I-USE Γ , τ 1 = τ 2 M 2 : γ ∃ ᾱ.∆ ∧ θ θ (Γ ), τ 1 = τ 2 | ∆ Γ use M 1 : eq(τ 1 , τ 2 ) in M 2 : γ ∃ ᾱ, α 1 .(Γ (eq(τ 1 , τ 2 )) M 1 : α 1 ) ∧ (∆ , θ )| ffv(Γ ),γ I-CONCL ∆ 0 ∧ (Γ 0 M : γ) ∃ ᾱ.∆ ∧ θ θ (Γ 0 ) | ∆ Γ 0 ; ∆ 0 M : γ ∃ ᾱ.(∆ , θ )| ffv(Γ 0 ,∆ 0 ),γ
The first point is independent of substitution and merging (∆ and ∆ are already functions). The second one requires that a node constraint α :: ψ appears after the variables in ffv(ψ) and frv(ψ) are introduced, and before α is used. The last one requires that this node constraint appears after the equations required for Γ ψ; the requirement on function and eq types is already fulfilled since ∆ and ∆ are parts of solutions. To summarize, for obtaining Γ | ∆ to be well-formed when θ (Γ ) | ∆ is well-formed, we only need the order of node constraints to satisfy the above ordering requirements.

Let Γ = θ (Γ ) | ∆ such that Γ . We construct Γ 0 = Γ | ∆ from Γ in the following way:

we replace each x : θ (σ ) in Γ by x : σ from Γ ; we replace each α :: ψ in Γ , by the set of node constraints {α ::

ψ ∈ ∆ | θ (α) = α }. Since {θ (∆ (α)) | θ (α) = α } ⊂ ∆ (α )
, and α ∈ ffv(∆ (α )) (by wellformedness), the order of between these node constraints doesn't matter, the other components (rigid variables and equations) are left unchanged.

Since we have preserved the ordering of components in Γ , all ordering constraints are satisfied, and Γ 0 is well-formed.

Theorem 2. If Γ M : γ ∃ ᾱ.∆ ∧ θ and θ (Γ ) | ∆ then θ (Γ ) | ∆ M : θ (γ).
Proof. Note first that since the rewriting rules for typing problems convert them to unification problems, in a way that does not depend on other constraints, when it succeeds the type inference algorithm of figure 8 provides a unique solution modulo a renaming between equivalent type variables. This allows us to choose whatever resolution strategy we wish.

The proof is by induction on M.

If M = x, the constraint ∆ ensures that α is bound to an instance of ∀(∆ ) α, so that in the resulting ∆ , α → γ, θ (γ) is bound to such an instance. The corresponding derivation is obtained with S-VAR followed by repeated uses of S-INST.

If M = Eq or M = (ψ), the constraint is already solved and satisfies the requirements. For M = (ψ) we need to apply repeatedly S-INST after S-ANN.

If M = λ (x) M 1 , since we assumed Γ λ (x) M 1 : γ ∃α 1 α 2 ᾱ.∆ ∧ θ , we have also Γ , x : α 1 M 1 : α 2 ∃ ᾱ.∆ 1 ∧ θ 1 , and (∆ 1 , θ 1 ) (∆ , θ ). This means there is a substitution ∆ 1 θ 2 : ∆ such that θ 2 • θ 1 = θ . By lemma 6 θ 1 (Γ ) | ∆ 1 , which implies θ 1 (Γ ), x : θ 1 (α 1 ) | ∆ 1 . By induction hypothesis we get θ 1 (Γ ), x : θ 1 (α 1 ) | ∆ 1 M 1 : θ 1 (α 2 ). By the substitution lemma, θ (Γ ), x : θ (α 1 ) | ∆ M 1 : θ (α 2 ). Since we also have θ (α 1 ) → θ (α 2 ) ∈ ∆ (θ (γ)), we can conclude that θ (Γ ) | ∆ λ (x) M 1 : θ (γ), using rule S-FUN.

If M = M 1 M 2 , then Γ M 1 : α 1 ∃ ᾱ1 .∆ 1 ∧ θ 1 and Γ M 2 : α 2 ∃ ᾱ2 .∆ 2 ∧ θ 2 , with ∆ 1 θ 1 : ∆ and ∆ 2 θ 2 : ∆ such that θ = θ 1 • θ 1 = θ 2 • θ 2 . By lemma 6 we have θ 1 (Γ ) | ∆ 1 and θ 2 (Γ ) | ∆ 2 .
By induction hypothesis and the substitution lemma, we obtain θ (Γ ) | ∆ M 1 : θ (α 1 ) and θ (Γ ) | ∆ M 2 : θ (α 2 ). Thanks to α 1 :: α 2 → γ, we also have θ (α 2 ) → θ (γ) ∈ ∆ (θ (α 1 )), so that we can conclude by S-APP.

If

M = let x = M 1 in M 2 , then Γ M 1 : γ 1 ∃ ᾱ1 .∆ 1 ∧θ 1 and Γ , x : ∀( ᾱ1 ) γ 1 M 2 : γ ∃ ᾱ2 .∆ 2 ∧ θ 2 with ∀( ᾱ1 ) γ 1 = Gen(θ 1 (γ 1 ), θ 1 (Γ ), ∆ 1 ), ∆ 1 θ 1 : ∆ and ∆ 2 θ 2 : ∆ such that θ = θ 1 • θ 1 = θ 2 • θ 2 .
As in previous cases, we obtain θ (Γ ) | ∆ M 1 : θ (γ 1 ) and θ (G), x : θ 1 (∀( ᾱ1 ) γ 1 ) | ∆ M 2 : θ (γ). Note that the variables ᾱ1 are a subset of ᾱ not accessible from other constraints (they are neither free in Γ and θ ), and as a result they are not touched by subsequent constraint solving. That is, if α ∈ ᾱ1 , then θ (α) = α and ∆ (α) = θ 1 (∆ 1 (α)). We can build a derivation by first applying S-GEN for each variable in ᾱ1 , obtaining θ (Γ ) | ∆ \ ᾱ1 M 1 : ∀( ᾱ1 ) γ 1 , then applying the weakening lemma for node descriptions in order to reintroduce in Γ the nodes that S-GEN removed. Then we can apply S-LET.

If M = Γ use M 1 : eq(τ 1 , τ 2 ) in M 2 : γ, then Γ (eq(τ 1 , τ 2 )) M 1 : γ 1 ∃ ᾱ1 .∆ 1 ∧ θ 1 and Γ , τ 1 = τ 2 M 2 : γ ∃ ᾱ2 .∆ 2 ∧ θ 2 with ∆ 1 θ 1 : ∆ and ∆ 2 | ffv ∆ 2 (θ 2 (Γ ),θ 2 (γ)) θ 2 : ∆ such that θ = θ 1 • θ 1 = θ 2 • θ 2 | ffv(Γ ),γ . We obtain θ (Γ ) | ∆ (eq(τ 1 , τ 2 )) M 1 : θ (γ 1 ) and θ (G), τ 1 . = τ 2 | ∆ M 2 :
θ (γ) (after applying S-BIND to remove useless variables). We conclude by rule S-USE.

If M = Γ ν(a) M 1 : γ, then Γ , a M 1 : γ ∃ ᾱ.∆ 1 ∧ θ 1 and θ 1 (Γ ), a | ∆ 1 , which gives θ 1 (Γ ), a | ∆ 1 M 1 : θ 1 (γ) by induction hypothesis. We can split ∆ 1 into 4 parts,

∆ 2 , ∆ 3 , ∆ 4 , ∆ 5 , such that dom(∆ 2 ) ⊂ ffv ∆ 1 (θ 1 (Γ )), ∆ 3 = {α :: a ∈ ∆ 1 }, dom(∆ 4 ) ⊂ ffv ∆ 1 (θ 1 (γ)) \ ffv ∆ 1 (θ 1 (Γ )), and dom(∆ 5 ) ∩ ffv ∆ 1 (θ 1 (Γ ), θ 1 (γ)) = / 0. We first discard ∆ 5 using S-BIND to obtain θ 1 (Γ ) | ∆ 2 , a, ∆ 3 , ∆ 4 M 1 : θ 1 (γ).
We then merge all variables in ∆ 3 , since they all represent the same type, using θ 3 = [α ← α 1 ] α::a∈∆ 1 , and obtain θ 1 (Γ ) | ∆ 2 , a, α 1 :: a, θ 3 (∆ 4 ) θ 3 (θ 1 (γ)). We can then apply S-NEW', to obtain

θ 1 (Γ ) | ∆ 2 , α :: ε, θ 3 (∆ 4 ) M 1 : θ 3 (θ 1 (γ)), which is actually identical to θ 3 (θ 1 (Γ )) | ∆ | ffv ∆ (θ 3 (su 1 (Γ )),θ 3 (θ 1 (γ))) M 1 : θ 3 (θ 1 (γ))
where ∆ = θ 3 (∆ 1 \ ∆ 3 ) ∪ {α :: ε}, and lets us conclude.

Corollary 1 (Soundness). If Γ 0 ; ∆ 0 M : γ ∃ ᾱ.∆ ∧ θ then θ (Γ 0 ) | ∆ M : θ (γ) and ∆ 0 θ : ∆ .
Proof. From the hypothesis, we must have ∆ 0 ∧ (Γ 0 M : γ) ∃ ᾱ.∆ ∧ θ and ∆ 0 θ : ∆ with (∆ , θ ) = (∆ , θ )| ffv(Γ 0 ,∆ 0 ),γ . In turn this means that we have

Γ 0 M : γ ∃ ᾱ.∆ 1 ∧ θ 1 with ∆ 1 θ 2 : ∆ and θ 2 • θ 1 = θ . Since θ (Γ 0 ) | ∆ , by lemma 6 θ 1 (Γ 0 ) | ∆ 1 . By theorem 2, we have θ 1 (Γ 0 ) | ∆ 1 M : θ 1 (γ)
. By the substitution lemma we have θ (Γ 0 ) | ∆ M : θ (γ). By repeated uses of S-BIND we obtain θ (Γ 0 ) | ∆ M : θ (γ). We also have ∆ 0 θ : ∆ , since θ (dom(∆ 0 )) ⊂ dom(∆ ). Proof. We prove the theorem by induction on M. Concerning θ (Γ ) | ∆ , it is a consequence of (∆ , θ )| ffv(Γ ),γ (∆ , θ ) and θ (Γ ) | ∆ by lemma 6 for the part of ∆ which is not filtered out, and this is also true for the remnant as long as equations in Γ are not removed, as it is no longer changed by unification: all variables discarded from ∆ by the restriction are included in ᾱ. So we do not mention it in those cases.

If M = x, then rule S-VAR was applied, followed by S-INST. Assume Γ (x) = ∀(∆ 0 ) α, with dom(∆ 0 ) fresh. The S-INST steps mean that θ is extended into ∆ 0 θ : ∆ , such that θ (α) = θ (γ). As a result (∆ 0 , [γ → α]) (∆ , θ ), and we conclude.

Similarly, if M = Eq or M = (a), then the inferred type is the most general one. If M = λ (x) M 1 , then rule S-FUN was applied, followed by S-INST. That is, we have θ (Γ ) | ∆ M : ∀(α ::

γ 0 → γ 1 ) α and ∆ (θ (γ)) = γ 0 → γ 1 ≈ψ. By inversion θ (Γ ) | ∆ , x : γ 0 M 1 : γ 1 , and θ (Γ ) | ∆ γ 0 . By induction hypothesis, Γ , x : γ 0 M 1 : γ 1 ∃ ᾱ.∆ 1 ∧θ 1 and (∆ 1 , θ 1 )| ffv(Γ ),γ 0 ,γ 1 (∆ , θ ). This means that θ 1 (Γ ) | ∆ 1 M : ∀(α :: θ 1 (γ 0 → γ 1 )) α. By applying S-INST once we obtain Γ | ∆ 1 , α :: θ 1 (γ 0 → γ 1 ) M : α, we set θ = θ 1 [γ ← α], ∆ = ∆ 1 , α :: θ 1 (γ 0 → γ 1 )
, and we conclude with (∆ , θ )| ffv(Γ ),γ (∆ , θ ).

If M = M 1 M 2 , then rule S-APP was applied. That is, we have θ

(Γ ) | ∆ M 1 : γ 1 , θ (Γ ) | ∆ M 2 : γ 2 and γ 2 → θ (γ) ∈ ∆ (γ 1 ). By induction hypothesis, Γ M 1 : γ 1 ∃ ᾱ.∆ 1 ∧ θ 1 and Γ M 2 : γ 2 ∃ ᾱ.∆ 2 ∧ θ 2 , with (∆ 1 , θ 1 )| ffv(Γ ),γ 1 (∆ , θ ) and (∆ 2 , θ 2 )| ffv(Γ ),γ 2 (∆ , θ ).
Note that here ∆ is unchanged by S-APP, and θ already correctly handles γ 1 and γ 2 , since we had γ 1 :: γ 2 → θ (γ) ≈ ψ ∈ ∆ . For the same reason the unification problem (∃ ᾱ.∆ 1 ∧ θ 1 ) ∧ (∃ ᾱ.∆ 2 ∧ θ 2 ) ∧ γ 1 :: γ 2 → γ has a solution ∃ ᾱ.(∆ , θ ), and (∆ , θ )| ffv(Γ ),γ,γ 1 ,γ 2 (∆ , θ ), since it is a conjunction of unification problems for which (∆ , θ ) is a solution. We obtain θ (Γ ) | ∆ by lemma 6, and the fact other variables of ∆ are not shared between ∆ 1 and ∆ 2 . And we also have (∆ , θ )| ffv(Γ ),γ (∆ , θ )| ffv(Γ ),γ,γ 1 ,γ 2 (∆ , θ ), since this is only a further restriction.

If M = let x = M 1 in M 2 , then rule S-LET was applied. That is, we have θ (Γ ) | ∆ M 1 : σ 1 and θ (Γ ), x : σ 1 | ∆ M 2 : γ 2 . For the left branch, there may be S-BIND and S-GEN steps. That is, there are α 1 , ∆ 1 and ∆ 2 such that σ 1 = ∀(∆ 1 ) α 1 , and

(θ (G) | ∆ ), ∆ 1 , ∆ 2 M 1 : α 1 . By induction hypothesis, Γ M 1 : α 1 ∃ ᾱ.∆ 1 ∧ θ 1 and (∆ 1 , θ 1 ) | ffv(Γ ),α 1 (∆ , ∆ 1 , ∆ 2 , θ ). As a consequence, if we pose σ 1 = Gen(θ (γ 1 ), θ 1 (Γ ), ∆ 1 )
where θ = θ 1 • θ 1 , we have that any instance of σ 1 is an instance of σ 1 . We can use the monotonicity lemma to obtain θ

1 (θ 1 (Γ ), x : σ 1 ) | ∆ M 2 : θ 1 (θ 1 (γ 2 )), which gives by induction hypothesis θ 1 (Γ ), x : σ 1 M 2 : θ 1 (γ 2 ) ∃ ᾱ.∆ 2 ∧ θ 2 and (∆ 2 , θ 2 ) | ffv(θ 1 (Γ ),x:σ 1 ),θ 1 (γ 2 ) (∆ , θ ).
Again we conclude by combining those two results.

If M = use M 1 : eq(τ 1 , τ 2 ) in M 2 , then rule S-USE was applied. For the left premise, by combining the induction hypothesis for M 1 with the case for S-ANN and S-APP, we have Γ (eq(τ 1 , τ

2 )) M 1 : γ 1 ∃ ᾱ.∆ 1 ∧ θ 1 with (∆ 1 , θ 1 )| ffv(Γ ),γ 1 (∆ , θ ).
For the right premise, some S-BIND steps may have been involved, and the real premise becomes

(θ (Γ ) | ∆ ), ∆ 2 M 2 : θ (γ), so that (θ (Γ ) | ∆ ), ∆ 2 . By induction hypothesis we have Γ , τ 1 . = τ 2 M 2 : γ ∃ ᾱ.∆ 2 ∧ θ 2 with (∆ 2 , θ 2 )| ffv(Γ ),γ ((∆ , ∆ 2 ), θ ) and θ 2 (Γ ), τ 1 . = τ 2 | ∆ 2 .
The last hypothesis satisfies the second premise of rule I-USE. Since dom(∆ 2 ) ∩ ffv ∆ (θ (Γ ), γ) = / 0, the second hypothesis gives (∆ 2 , θ 2 )| ffv(Γ ),γ (∆ , θ ). Combined with the first premise we obtain (∆ , θ )| ffv(Γ ),γ (∆ , θ ), since (∆ 1 , θ 1 ) may only instantiate γ if γ ∈ ffv(Γ ). Finally, the outer Γ does not contain τ

1 . = τ 2 , but (∆ 2 | ffv ∆ 2 (θ 2 (Γ ),θ 2 (γ)) , θ 2 ) = (∆ 2 , θ 2 )| ffv(Γ ),γ (∆ , θ ) so that we obtain θ 2 (Γ ) | ∆ 2 | ffv ∆ 2 (θ 2 (Γ ),θ 2 (γ)
) by lemma 6, and conclude that θ (Γ ) | ∆ as usual. If M = Γ ν(a) M 1 : γ, then rule S-NEW' was applied. ∆ is of the form ∆ 1 , α 0 :: ε, ∆ 2 , the conclusion being (θ (Γ ) | ∆ 1 ), α 0 :: ε, ∆ 2 M 1 : θ (γ), and the premise, (θ (Γ ) | ∆ 1 ), α 0 :: a, ∆ 2 M 1 : θ (γ). Some S-BIND steps may have been used in the premise, so that our starting point for induction is (θ (Γ ) | ∆ 1 ), a, α 0 :: a, ∆ 2 , ∆ 3 M 1 : θ (γ), with θ (γ) ∈ dom(∆ 3 ). The induction hypothesis gives Γ , a M 1 : γ ∃ ᾱ.∆ 1 ∧ θ 1 with (∆ 1 , θ 1 )| ffv(Γ ),γ ((∆ 1 , α 0 :: a, ∆ 2 , ∆ 3 ), θ ) and θ 1 (Γ ), a | ∆ . Since we have restricted ourselves to ffv(Γ ), γ, the variables in ∆ 3 are irrelevant, and we have (∆ 1 , θ 2 )| ffv(Γ ),γ ((∆ 1 , α 0 :: a, ∆ 2 ), θ ). The well-formedness of (θ (Γ ) | ∆ 1 ), α 0 :: ε, ∆ 2 means that neither ∆ 1 nor ∆ 2 contain a, so that all descriptions containing a in ∆ 1 | ffv ∆ 1

(θ 1 (Γ ),θ 1 (γ)) must be of the form α :: a, so that we can map them to α 0 . We pose

∆ 2 = ∆ 1 \ {α :: a ∈ ∆ 1 }, θ 2 = [α ← α 0 ] α::a∈∆ 1 and (θ , ∆ ) = ((θ 2 (∆ 2 ), α 0 :: ε), θ 2 • θ 1 )| ffv(Γ ),γ . We obtain (θ , ∆ ) ((∆ 1 , α 0 :: ε, ∆ 2 ), θ
), and we get θ (Γ ) | ∆ by lemma 6.

Corollary 2 (Principality). For any Γ , ∆ 0 , M, γ, if there exists a substitution ∆ 0

θ : ∆ such that θ (Γ ) | ∆ M : θ (γ), then Γ ; ∆ 0 M : γ ∃ ᾱ.∆ ∧ θ and (∆ , θ ) (∆ , θ ).
Proof. We first remark that we can assume (dom(∆ 0 ) ∪ ffv(∆ 0 )) ⊆ ffv ∆ 0 (Γ , γ), i.e. if ∆ 0 contained variables that are not accessible from Γ and γ, then we could just rename them outside of dom(θ ) and dom(∆ ).

Since the canonical derivation may finish with S-BIND steps, we first remove them, and obtain θ (Γ ) | ∆ , ∆ 1 M : θ (γ). Since ∆ 0 θ : ∆ implies / 0 θ : ∆ , ∆ 1 , we can use theorem to obtain Γ M : γ ∃ ᾱ.∆ 1 ∧ θ 1 with (∆ 1 , θ 1 )| ffv(Γ ),γ ((∆ , ∆ 1 ), θ ) and θ 1 (Γ ) | ∆ 1 . Due to the restriction, we can strengthen the second property into (∆ 1 , θ 1 )| ffv(Γ ),γ (∆ , θ ), i.e. variables in ffv ∆ 1 (θ 1 (Γ ), θ 1 (γ)), being accessible from Γ , γ, cannot be mapped into variables of ∆ 1 , which are not accessible from Γ , γ. Moreover ∆ 0 θ : ∆ implies (∆ 0 , id) (∆ , θ ), and from the remark above the non-filtered part of (∆ 1 , θ 1 ) has no common variables with ∆ 0 , so we can conclude that

∆ 0 ∧ (G M : γ) ∃ ᾱ.∆ 2 ∧ θ 2 with (∆ 2 , θ 2 ) (∆ , θ ). The returned substitution is (∆ , θ ) = (∆ 2 , θ 2 )| ffv(Γ ,∆ 0 ),γ .
Again, this amounts to weakening the substitution, and we obtain (∆ , θ ) (∆ , θ ).

The statement in mixed form that we presented at the beginning of this section can be obtained in the following way: for the mixed form typing problem Γ

M : ζ , let ∆ 0 = |Γ |, then if Γ -1 ∆ 0 ; ∆ 0 M : ζ -1
∆ 0 has a solution (∆ , θ ), then there exists a principal solution.

Related works

While GADTs have been an active research area for about 10 years, early works on GADTs usually focused on their type checking and expressiveness, ignoring ML-style type inference. Typically, they rely on an explicitly typed core language and use local type inference techniques to leave some type information implicit. Other recent works with rich dependent type systems also fit in this category and are only loosely related to ours.

Comparison

Relatively few papers are dedicated to principal type inference for GADTs. The tension between ambiguity and principality is so strong that it has been assumed that the only way to reach principality is to know exactly the external type of each GADT match case. As a result, research has not been so much focused on finding a type system with principal types, but rather on clever propagation of type information so that programs have enough type annotations after propagation to admit principal types-or are rejected otherwise. Hence, some existing approaches always return principal solutions, but do not have a clear specification of when they will succeed, because this depends on the propagation algorithm (or some idealized version of it) which does not have a compositional specification.

OutsideIn improves on this by using uses constraint solving in place of directional annotation propagation, which greatly reduces the need for annotations. Stratified type inference [START_REF] Pottier | Stratified type inference for generalized algebraic data types[END_REF] is another interesting approach to type inference for GADTs that uses several sophisticated passes to propagate local typing constraints (and not just type annotations) progressively to the rest of the program.

The following table summarizes the typability of the programs given in the overview, for our approach (including simple syntactic propagation of type annotations), Out-sideIn 6 , and stratified type inference [START_REF] Pottier | Stratified type inference for generalized algebraic data types[END_REF].

Program

f f 1 f 2 g g 1 g 2 p p 1 Ambivalent

√ √ √ - √ √ √ - OutsideIn ----- √ √ √ Stratified - √ √ -- √ --
The results for f are unsurprising: this is the motivating example for introducing ambivalence, and it is not even principal in the naive type system: without an internal notion of ambivalence, a type system is unable to tell that the equality between two types is only accidental and should not be considered as a source of ambiguity.

The results for f 1 and f 2 are more interesting. While OutsideIn requires an external type annotation in both cases, stratified type inference accepts to infer the type of the branch from its body. More precisely, the propagation algorithm operates in a bidirectional way and is able to extract non-ambiguous information from GADT patternmatching branches. The exported information is pruned so that it remains compatible with any interpretation of the internal information, even in a context with fewer type equations. Thus, the type of the result is pruned in function f, but it can be propagated for f 1 and f 2 . This corresponds exactly to the naive notion of ambiguity.

Typing of g fails in all three systems, as it is fundamentally ambiguous, whichever definition is chosen. The results for g 1 may look surprising: while it contains many type annotations, both OutsideIn and stratified type inference still fail on it. The reason is that type annotations are inside the branch: in both systems, only type annotations outside of a branch can disambiguate types for which an equation has been introduced. We find this behavior counter-intuitive. The freedom of where to add type annotations stands as a clear advantage of ambivalent types. By contrast, g 2 provides full type annotations in a standard style, so that all systems succeed-although ambivalent types need some (simple) propagation mechanism to push annotations inside.

Programs p and p 1 demonstrate the power of OutsideIn. The program p 1 is the following variant of p, which we deem ambiguous: let p 1 (type a) (x : (a,int) eq) (y : a) = let z = (match x with Eq -> if y>0 then y else 0) in z + 1

Indeed, the match expression in p 1 would have to be given the ambivalent type a ≈ int, which is not allowed outside the scope of the equation a = int. Both p and p 1 are accepted by OutsideIn, since type information can be propagated upward, even for local let definitions. This comes at a cost, though: local let-definitions are monomorphic by default (but can be made polymorphic by adding a type annotation). While local polymorphic definitions are relatively rare, so that this change of behavior appears as a good compromise for Haskell, they are still frequent enough, and their corresponding type annotations large enough, so that we prefer to keep local polymorphism in OCaml [START_REF] Garrigue | Monomophic let in OCaml? Blog article at[END_REF].

Moreover, local polymorphism is critical to the annotation propagation mechanism used by OCaml, originally for polymorphic methods, and now for GADTs too. All examples above are specifically chosen to illustrate the mechanisms underlying ambivalence and do not cover all uses of GADTs. Thus, they do not mean that our approach always outperforms other ones, but they emphasize the relevance of ambivalence. The question is not whichever approach taken alone performs better, but rather how ambivalence can be used to improve type inference with GADTs. Indeed, ambivalence could be added to other existing approaches to improve them as well.

Besides this comparison on examples, the main advantage of ambivalent types is to preserve principal type inference and monotonicity, so that type inference and program refactoring are less surprising.

An interesting proposal by Lin and Sheard [START_REF] Lin | Pointwise generalized algebraic data types[END_REF], called point-wise type inference, is also tackling type inference à la ML, but restricting the expressiveness of the systemsome uses of GADT will be rejected-so that more aggressive type propagation can be done in a principal way. Point-wise type inference is hard to compare to our approach, as many programs have to be modified. For instance, it rejects all our examples, because equality witnesses can only be matched on if they relate two rigid type variables. To be accepted, we could replace eq by a specialized version, type t = Int : int t.

Formalization techniques

Ambivalent types borrow ideas from earlier works. The use of sharing to track known type information was already present in our work on semi-explicit first-class polymorphism [START_REF] Garrigue | Semi-explicit first-class polymorphism for ML[END_REF]. There, we only tracked sharing on a special category of nodes containing explicitly polymorphic types. Here, we need to track sharing on all nodes, as any type can become ambivalent. In our type inference algorithm, we also reuse the same definition style, describing type inference as a constraint resolution process, but introducing some points where constraints have to be solved before continuing.

The formalization itself borrows a lot from previous work on structural polymorphism for polymorphic variant and record types [START_REF] Garrigue | A certified implementation of ML with structural polymorphism[END_REF]. In particular, unification of ambivalent types, which merges sets of rigid variables and requires checking coherence constraints, can be seen as an instance of the unification of structurally polymorphic nodes. The difference is again that all nodes are potentially ambivalent in our case, while structural polymorphism only cares about variant and record types.

Conclusion

Ambivalent types are a refinement of ML types, which represents within types themselves ambiguities resulting from the use of local equations. They permit a more accurate definition of ambiguity, which in turn reduces the need for type annotations while preserving both the principal type property and monotonicity.

This approach has been implemented in OCaml. We have not addressed propagation of type information in this work, although this is quite useful in practice. A simple propagation mechanism based on polymorphism, similar to that used for semi-explicit first-class polymorphism, as already in use in OCaml, seems sufficient to alleviate the need for most local type annotations, while preserving principality of type inference.

The notion of ambivalence is orthogonal to previous techniques used for GADT type inference. Therefore, it should also benefit other approaches such as OutsideIn or stratified type inference. Hopefully, ambivalent types might be transferable to ML F [START_REF] Le Botlan | Recasting MLF[END_REF], as the techniques underlying both ambivalent types and semi-explicit first-class polymorphism have many similarities.

Fig. 3 .

 3 Fig. 3. Typing rules

Definition 3 .

 3 A variable substitution θ preserves ambivalence between label contexts ∆ and ∆ , written ∆ θ : ∆ , if and only if, for any α ::ψ in ∆ , θ (α ) :: ψ is in ∆ and θ (ψ) ⊆ ψ .The two definitions coincide in the following way: the substitution θ preserves ambivalence in a type ζ if and only if |ζ | θ : |ζ θ |, where θ (α) is either α if α ∈ dom(θ ) and θ (α) = ψ α or α otherwise.

Fig. 6 .

 6 Fig. 6. Typing rules in split form

Lemma 1 (

 1 Substitution-WF). If Γ | ∆ σ and ∆ θ : ∆ , and θ (Γ ) | ∆ , then θ (Γ ) | ∆ θ (σ ).

Lemma 2 (

 2 Substitution). If Γ | ∆ M : σ and ∆ θ : ∆ , and θ (Γ ) | ∆ , then θ (Γ ) | ∆ M : θ (σ ), using the same derivation. Proof. By induction on Γ | ∆ M : σ . Case S-GEN: by induction hypothesis, we know that θ (Γ ) | ∆ . Since Γ | ∆ ψ, if we choose α outside of dom(∆ ), by lemma 1, (θ (Γ ) | ∆ ), α :: ψ, and as a result (θ (Γ ) | ∆ ), α :: ψ M : θ (σ ) and we conclude.

Definition 5 .Lemma 4 .

 54 A derivation is canonical if: -It uses S-NEW' in place of S-NEW. -Rule S-INST is only used immediately below another rule S-INST, or one of rules S-VAR, S-FUN, S-ANN or S-WITNESS. -Rule S-GEN is only used immediately above another rule S-GEN or the left premise of rule S-LET, or at the end of the derivation. -Rule S-BIND is only used immediately above another rule S-BIND, the left premise of rule S-LET, the right premise of S-USE, or rules S-GEN and S-NEW', or at the end of the derivation. Any judgment has a canonical derivation.

Fig. 8 .

 8 Fig. 8. Constraint generation

Theorem 3 .

 3 For any Γ , M, γ, if there exists a substitution / 0 θ : ∆ such that θ (Γ ) | ∆ M : θ (γ) has a canonical derivation not finishing with S-BIND, then Γ M : γ ∃ ᾱ.∆ ∧ θ and (∆ , θ )| ffv(Γ ),γ (∆ , θ ) and θ (Γ ) | ∆ .

Examples in this section use OCaml syntax[START_REF] Leroy | The OCaml system release 4.00, Documentation and user's manual[END_REF]. Letter α stands for a flexible variable as usual while letter a stands for a rigid variable that cannot be instantiated. This will be detailed later.

WF-CTX-EXPRΓ σx / ∈ dom(Γ )Γ , x : σ WF-CTX-RIGID Γ a / ∈ dom(Γ ) Γ , a WF-TYPE-RIGID Γ a ∈ dom(Γ ) Γ a WF-TYPE-INT Γ Γ int WF-STYPE-ARROW Γ τ 1 Γ τ 2 Γ τ 1 → τ 2 WF-STYPE-EQ Γ τ 1 Γ τ 2 Γ eq(τ 1 , τ 2 ) WF-TYPE-ARROW Γ ζ 1 Γ ζ 2 Γ ζ 1 → ζ 2 WF-TYPE-EQ Γ ζ 1 Γ ζ 2 Γ eq(ζ 1 , ζ 2 ) WF-STYPE-FLEX Γ α ∈ dom(Γ ) Γ α WF-SCHEME Γ , α :: ψ σ Γ ∀(α) σ WF-CTX-EQUAL Γ Γ τ 1 . = τ 2 Γ , τ 1 . = τ 2 WF-TYPE-EQUAL Γ τ 1 Γ τ 2 ftv(τ 1 ) = ftv(τ 2 ) = / 0 Γ τ 1 . = τ 2 WF-TYPE-FLEX Γ α :: ψ ∈ Γ Γ ψ α WF-CTX-FLEX Γ Γ ψ α / ∈ dom(Γ )Γ , α :: ψ WF-TYPE-AMBIVALENT

This is not always true for ML abstract types, as type constructors may be compatible in another context, but we do not address this problem here.

(a)θ = a (int)θ = int (ζ 1 → ζ 2 )θ = ζ 1 θ → ζ 2 θ (eq(ζ 1 , ζ 2 ))θ = eq(ζ 1 θ , ζ 2 θ ) Fig. 2. Application of substitution θ equal to [α i ← ζ i ] i∈I M-VAR Γ x : σ ∈ Γ Γ x : σ M-INST Γ M : ∀(α) (σ [α ← ψ α 0 ]) ψ 0 ⊆ ψ Γ ψ γ Γ M : σ [α ← ψ γ ] M-GEN Γ , α :: ψ M : σ Γ M : ∀(α) σ M-NEW Γ, a, α :: a M : σ Γ ∀(α) σ [α ← ε α ] Γ ν(a) M : ∀(α) σ [α ← ε α ] M-FUN Γ , x : ζ 0 M : ζ Γ λ (x) M : ∀(γ) (ζ 0 → ζ ) γ M-APP Γ M 1 : ((ζ 2 → ζ ) ≈ ψ) α Γ M 2 : ζ 2 Γ M 1 M 2 : ζ M-LET Γ M 1 : σ 1 Γ , x : σ 1 M 2 : ζ 2 Γ let x = M 1 in M 2 : ζ 2 M-ANN Γ ∀(ftv(τ)) τ Γ (τ) : ∀(ftv(τ)) τ → τ M-WITNESS Γ Γ Eq : ∀(α, γ) eq(α, α) γ M-USE Γ (eq(τ 1 , τ 2 )) M 1 : ζ 1 Γ , τ 1 . = τ 2 M 2 : ζ 2 Γ use M 1 : eq(τ 1 , τ 2 ) in M 2 : ζ 2

This is why we write this ν(a) M rather than Λ a M.

Jacques Garrigue and Didier RémyS-VAR Γ x : σ ∈ Γ Γ x : σ S-INST Γ M : ∀(α :: ψ) σ γ :: ψ 2 ∈ Γ ψ ⊆ ψ 2 Γ M : σ [α ← γ] S-GEN Γ , α :: ψ M : σ Γ M : ∀(α :: ψ) σ S-BIND Γ , α :: ψ M : γ α = γ Γ M : γ S-NEW Γ , a, α :: a M : σ Γ ∀(α :: ε) σ Γ ν(a) M : ∀(α :: ε) σ S-FUN Γ , x : γ 0 M : γ 1 Γ λ (x) M : ∀(γ :: γ 0 → γ 1 ) γ S-APP Γ M 1 : γ 1 Γ M 2 : γ 2 γ 1 :: γ 2 → γ ≈ ψ ∈ Γ Γ M 1 M 2 : γ S-LET Γ M 1 : σ 1 Γ , x : σ 1 M 2 : γ 2 Γ let x = M 1 in M 2 : γ 2 S-ANN Γ ∀(ftv(τ)) τ Γ (τ) : ∀(ftv(τ)) τ → τ S-WITNESSΓ Γ Eq : ∀(α, γ :: eq(α, α)) γS-USE

Results differ for GHC

7.6, as it slightly departs from OutsideIn allowing some biased choices, but next versions of GHC should strictly comply with OutsideIn.

Acknowledgments We thank Gabriel Scherer and the anonymous reviewers for detailed comments on this paper.