Elementary Type Inference
Jinxu Zhao !
Department of Computer Science, The University of Hong Kong, China

Bruno C. d. S. Oliveira !
Department of Computer Science, The University of Hong Kong, China

Abstract
Languages with polymorphic type systems are made convenient to use by employing type inference
to avoid redundant type information. Unfortunately, features such as impredicative types andsubtyping make complete type inference very challenging or impossible to realize.
This paper presents a form of partial type inference called elementary type inference. Elementary
type inference adopts the idea of inferring only monotypes from past work on predicative higherranked polymorphism. This idea is extended with the addition of explicit type applications thatwork for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise
in expressiveness. Our target is a System F extension with top and bottom types, similar to thelanguage employed by Pierce and Turner in their seminal work on local type inference. We show aesound, complete and decidable type system for a calculus called F<:, that targets that extensioneof System F. A key design choice in F<: is to consider top and bottom types as polytypes only.
An important technical challenge is that the combination of predicative implicit instantiation andimpredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial.
Without some restrictions, key properties, such as subsumption and stability of type substitution
lemmas, break. To address this problem we introduce a variant of polymorphic subtyping calledstable subtyping with some mild restrictions on implicit instantiation. All the results are mechanicallyformalized in the Abella theorem prover.
2012 ACM Subject Classification Software and its engineering → General programming languages
Keywords and phrases Type Inference
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2022.2
Acknowledgements We are grateful to the anonymous reviewers for their valuable comments
which helped to improve the presentation of this work. We also thank Chen Cui for creating theimplementation for our prototype. The research is supported by the Type Inference for Complex
Type Systems collaboration project (TC20210422012) between Huawei, and the University of Hong
Kong and Hong Kong Research Grants Council projects number 17209520 and 17209821.

1

Introduction

Many programming languages, such as Java, C#, Scala or TypeScript (among others)
have type systems with parametric polymorphism, subtyping and first-class functions. For
convenience, some form of type inference is desirable in those languages. Type inference avoids
code being cluttered with redundant type annotations, as well as explicit type instantiationsof polymorphic functions. For instance, in Java, we can write code such as:
List<String> numbers = Arrays.asList("1", "2", "3", "4", "5", "6");
List<Integer> even = numbers.stream().map(s -> Integer.valueOf(s)).filter(number -> number % 2 == 0).collect(Collectors.toList());

This code processes a list of strings representing numbers, converts the strings into numbers,
and filters the even numbers. Thus the list even is [2,4,6]. The code is made practical by aform of local type inference [27, 21, 4, 28], which helps in two ways. Firstly, local type inference© Jinxu Zhao and Bruno C. d. S. Oliveira;licensed under Creative Commons License CC-BY 4.0
36th European Conference on Object-Oriented Programming (ECOOP 2022).
Editors: Karim Ali and Jan Vitek; Article No. 2; pp. 2:1–2:28
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2:2

Elementary Type Inference

enables synthesis of type arguments in many cases. That is, applications of generic methods(i.e. methods parametrized by some types) will automatically infer the type arguments.
An example of type argument synthesis is the method call map(s -> Integer.valueOf(s)).
The polymorphic map function allows taking a function that converts values in the list withsome type A into values of some other type B, thus producing a list with type List<B>. In
the code above, B is Integer, and such instantiation is implicitly done by the compiler.
Secondly, local type inference employs bidirectional type-checking [27, 10] to propagate known
type-information. For example, in the snippet above the type of numbers is List<String>,
therefore in map(s -> Integer.valueOf(s)) we can deduce that s is of type String.
Without local type inference, the code above would need to explicitly provide the types for
instantiation and the types of arguments for the lambda functions, making the code clutteredwith type annotations. Nonetheless, some instantiations cannot be automatically inferred.
For such cases, languages like Java support explicit type applications as well. For instance,
we can write an alternative invocation of the map function with explicit type application as:.<Integer>map(s -> Integer.valueOf(s))

In their original work on local type inference, Pierce and Turner [27] considered a System
F language extended with subtyping and a top and a bottom type. Such a language captures
most of the essential features of interest to write code such as the above. In particular, their
System F variant captures essential forms of subtyping by including top and bottom types,
supports both implicit instantiation and explicit type application, and employs bidirectional
type-checking for inferring types in simple cases with lambdas as arguments.
Local type inference is a pragmatic approach. It is not aimed to provide the same degreeof type inference that is possible in languages with Hindley-Milner type inference [16, 19, 5].
Instead, as Pierce and Turner state, the goal is to “exchange complete type inference forsimpler methods that work well in the presence of more powerful type-theoretic features suchas subtyping and impredicative polymorphism”. In local type inference, the main design
decision that is made to simplify type inference is to avoid forms of global type inference
that employ long-distance constraints such as unification variables.
The issues caused by both subtyping and impredicative polymorphism for more ambitious
global type inference methods are well-known. There are several important undecidability
results that are relevant. For instance, for System F, full type inference is undecidable [38] andan impredicative polymorphic subtyping relation for System F is undecidable as well [35, 3].
For a type system with top and bottom types and type variables, subtyping can also easily
run into undecidable problems [34]. Despite those problems, several different approaches
and restrictions have been developed for allowing type inference for: predicative versionsof System F [25, 8, 9, 20, 39]; impredicative versions of System F [17, 18, 36, 33, 32, 14]; aswell as several Hindley-Milner extensions with subtyping [11, 30, 6, 23].
Perhaps surprisingly, follow-up research on local type inference and type inference fortype systems that include higher-ranked polymorphism, impredicativity and subtyping (with
top and bottom types) has been relatively limited. In contrast, closely related global type
inference approaches with higher-ranked polymorphism (HRP) for System-F-like languages
have seen quite a bit of development. Such HRP approaches [8, 17, 18, 36, 25, 33, 20]
extend the classic Hindley-Milner type system, removing the restriction of top-level (let)polymorphism only. Both local type inference and HRP type inference techniques allow
synthesis of type arguments and use type annotations to aid inference. The main differenceis that HRP type inference targets a System-F-like language without subtyping, whereas the
local type inference targets a System-F-like language with subtyping. Another difference isthat most HRP techniques support implicit instantiation only, although there is some work

J. Zhao and B. C. d. S. Oliveira

2:3

on supporting visible (or explicit) type applications as well in HRP approaches [13, 32].
In this paper, we propose a form of partial type inference called elementary type inference.
Like local type inference, we aim at having a pragmatic approach. We are willing to sacrificesome power in terms of what can be inferred, in exchange for an approach that can deal
with both subtyping in the presence of top and bottom types, as well as impredicative
polymorphism. Like local type inference we support synthesis of type arguments and bidirectional type-checking, but do not support Hindley-Milner style generalization. Unlike
local type inference, our type inference is global and employs long-distance constraints. We
build on recent developments in predicative type inference with HRP for System-F-likelanguages. The philosophy in elementary type inference is to infer only monotypes, but also
include an explicit type application construct that can be used to instantiate any types (orpolytypes). In other words, many programs where instantiations are monotypes can still
benefit from type inference, while no expressive power is sacrificed. We can always resort to
explicit type application for dealing with general polytypes.
e
We present a calculus with elementary type inference, called F<:, that can encode alleterms in a variant of System F with subtyping. The type system of F<:
is a variant of theDunfield and Krishnaswami [8] (DK) type system, extended with top and bottom types andeimpredicative explicit type application. The algorithmic formulation of F<:
is based on theworklist algorithm by Zhao et al. [39]. We have a prototype implementation, as well as a fullmechanical formalization (including results such as soundness, completeness and decidability)ein the Abella theorem prover [15]. A key design choice in F<:
is to consider top and bottom
types as polytypes only. In other words, we avoid guessing types for implicit instantiationthat use top and bottom types. This design choice avoids many of the technical challenges
that would otherwise occur in the inference of terms with top and bottom types.
A key technical challenge is that the combination of predicative implicit instantiation andimpredicative explicit type applications is problematic. Without some restrictions, important
properties, such as subsumption and type substitution lemmas, break. To address thisproblem we introduce a novel polymorphic subtyping relation called stable subtyping. Stable
subtyping has some mild restrictions, compared to the well-known Odersky and Läufer [20]formulation, but accounts for top and bottom types and impredicative instantiations. In
essence, due to the presence of explicit impredicative type applications, out-of-order implicit
instantiation and unused type variables are forbidden.
In summary, the contributions of this work are:Elementary type inference: A form of partial type inference that combines predicative
implicit instantiation with impredicative explicit type application, in the presence of
conventional subtyping rules and top and bottom types.
e
The F<:
calculus: We present a syntax-directed specification and an algorithmic version
eof the F<:
calculus. We show that the algorithmic version is sound and complete to theespecification, and its type system is also decidable. Furthermore, F<:is type-safe andcomplete with respect to a variant of System F with subtyping and top and bottom types.
Stable subtyping: A new form of polymorphic subtyping, based on the well-known
polymorphic subtyping relation by Odersky and Läufer [20], but with some restrictions.
The restrictions are needed to ensure important properties such as subsumption andstability of type substitutions in the presence of impredicative type applications.
Implementation and mechanical formalization. All the calculi and proofs presented
in this paper are mechanically formalized in the Abella theorem prover. The formalization,
an implementation and the extended version of the paper can be found in:
https://github.com/JimmyZJX/ElementaryTypeInference

ECOOP 2022

2:4

Elementary Type Inference2

Overview

We start with a background on higher-ranked polymorphic (HRP) type inference and thedeclarative type system by Dunfield and Krishnaswami [8]. Then we discuss the challenges
of extending such HRP systems with explicit type applications and top and bottom types.
Finally, we illustrate the key ideas in our work to address those challenges.

2.1

Background: Higher-Ranked Type Inference and Type Applications

Our work builds on prior work on HRP type inference. In HRP type systems, universal
quantification can appear in arbitrary positions in types. This lifts a restriction of HindleyMilner type inference [16, 19, 5], where universal quantification can only appear at the top
level. To introduce HRP type inference we will use examples in GHC 8, whose type inference
algorithm is closely based on the work by Eisenberg et al. [13] on visible type application.
The use of GHC 8 will later be helpful to illustrate some challenges of combining HRP type
inference with explicit type applications and standard subtyping rules.1
A canonical example of an expression with an arbitrary higher-ranked type is:
hpoly = \(f :: forall a. a -> a) -> (f 1, f ’c’)

The type of this function is (forall a. a -> a) -> (Int, Char). A type annotation helps
the type system to infer a type. In general, HRP type systems require some type annotations.
In many such systems, it is enough to provide type annotations for polymorphic arguments(such as above). The use of some type annotations means that type inference is partial.
Predicativity, Polymorphic Subtyping and Explicit Type Applications In predicative typesystems, universally quantified types can only be instantiated with monotypes, which aretypes that do not contain universal quantifiers. For instance, the following definition of f:
f :: (forall a. Int -> a -> Int) -> Bool -> Int
f k = k 3

illustrates a higher-ranked function, where the argument k is polymorphic. In the body,
implicit instantiation is used when applying k to an argument. In that application, the typeargument of k is left implicit and is instantiated automatically with the monotype Bool.
The polymorphic subtyping relation used in GHC 8 (based on Peyton Jones et al.’s
work [25]) and also by DK’s type system allows implicit instantiation of type arguments inpolymorphic types, which follows Hindley-Milner. This allows us, for instance, to define afunction h, with a different but compatible type with f:h :: (forall b a. b -> a -> b) -> Bool -> Int
h k = f k

Notice that in h, one more universal variable is added, generalizing the argument typecompared to f. However, since subtyping of functions is contravariant on the input types,
the type of h is less general (or a supertype) of the type of f.
Another alternative to support instantiation is to employ an explicit type application.
For example, function g illustrates explicit type applications in GHC Haskell:g :: (forall a. Int -> a -> Int) -> Bool -> Int
g k = k @Bool 3

The function g has the same type as f but explicitly instantiates the type arguments of theargument k. The notation e @τ (for instance k @Bool in the definition of g above) denotes
explicit type applications in Haskell. We will also adopt a similar notation in this paper.

1Type-checked with the GHC extensions: RankNTypes, TypeApplications and ScopedTypeVariables.

J. Zhao and B. C. d. S. Oliveira

2:5

Syntaxa, b
A, B, Cτ, σeΨType variables
Types
Monotypes
Expressions
Contexts

1 | a | ∀a. A | A → B
1|a|τ →σx | () | λx. e | e1 e2 | (e : A)
· | Ψ, a | Ψ, x : A

::=
::=
::=
::=

Ψ ` A ≤ B Declarative subtyping
a∈Ψ

≤Var

Ψ`a≤a

Ψ`τ

Ψ`1≤1
Ψ ` [τ /a]A ≤ BΨ ` ∀a. A ≤ B

Ψ ` B 1 ≤ A1≤Unit

Ψ ` A2 ≤ B 2≤→

Ψ ` A1 → A2 ≤ B 1 → B 2
Ψ, b ` A ≤ B≤∀LΨ ` A ≤ ∀b. B≤∀RΨ ` e ⇐ A e checks against input type A.
Ψ ` e ⇒ A e synthesizes output type A.
Ψ ` A • e ⇒⇒ C Applying a function of type A to e synthesizes type C.
(x : A) ∈ Ψ
Ψ`x⇒A

Ψ`e⇒A
DVar

D1I⇒

Ψ ` λx. e ⇐ A → BΨ ` e ⇐ ∀a. A

D∀I

Ψ`e⇐A
D→I

Ψ, x : σ ` e ⇐ τΨ ` λx. e ⇒ σ → τ

Ψ, a ` e ⇐ AD∀AppΨ ` ∀a. A • e ⇒⇒ C

DAnno

Ψ ` (e : A) ⇒ AΨ ` [τ /a]A • e ⇒⇒ C

Ψ, x : A ` e ⇐ BΨ`σ→τΨ`A Ψ`e⇐A
DSub

Ψ`e⇐B
Ψ`τ

Ψ ` () ⇒ 1

Ψ`A≤B

D→I⇒

Ψ ` A → C • e ⇒⇒ C
Ψ ` e1 ⇒ A

D→AppΨ ` A • e2 ⇒⇒ C

Ψ ` e1 e2 ⇒ C

D→E

Figure 1 The Dunfield and Krishnaswami Type System.

2.2

Background: The Dunfield and Krishnaswami Type System

Our declarative type system can be viewed as a variant of the DK type system. The DK
type system is predicative and supports implicit instantiation only. We review the original
type system first, before proceeding with the presentation of our work.
Syntax The syntax of DK’s declarative system is shown at the top of Figure 1. A declarative
type A is either the unit type 1, a type variable a, a universal quantification ∀a. A or afunction type A → B. Nested universal quantifiers are allowed for types, but monotypes τ do
not have any universal quantifier. Terms include a unit term (), variables x, lambda-functions
λx. e, applications e1 e2 and annotations (e : A). Contexts Ψ are sequences of type variabledeclarations and term variables with their types declared x : A.
Declarative Subtyping The middle of Figure 1 shows DK’s declarative subtyping judgment
Ψ ` A ≤ B, which was adopted from Odersky and Läufer [20]. This judgment comparesthe degree of polymorphism between types A and B in DK’s implicitly polymorphic type

ECOOP 2022

2:6

Elementary Type Inference

system. If A can always be instantiated to match any instantiation of B, then A is “at least
as polymorphic as” B. We also say that A is “more polymorphic than” B and write A ≤ B.
Subtyping rules ≤Var, ≤Unit and ≤→ handle simple cases that do not involve universal
quantifiers. The subtyping rule for function types ≤→ is standard, being covariant on the
return type and contravariant on the argument type. Rule ≤∀R states that if A is moregeneral than ∀b. B, then A must instantiate to [τ /b]B for every τ . The type variable b weintroduced in the premise is implicitly fresh. We use this convention throughout the whole
paper. The most interesting rule is ≤∀L, which is where implicit instantiation can happen.
If some instantiation of ∀a. A, [τ /a]A, is a subtype of B, then ∀a. A ≤ B. Only monotypes
τ can be used to instantiate a, which is guessed in this declarative rule.
Declarative Typing The bidirectional type system, shown at the bottom of Figure 1, has
three judgments. The checking judgment Ψ ` e ⇐ A checks expression e against the type A
in the context Ψ. The synthesis judgment Ψ ` e ⇒ A synthesizes the type A of expression ein the context Ψ. The application judgment Ψ ` A • e ⇒⇒ C synthesizes the type C of theapplication of a function of type A (which could be polymorphic) to the argument e.
Many rules are standard bidirectional type-checking rules [10], so we focus only on the
more interesting and non-standard rules. Checking an expression e against a polymorphic
type ∀a. A in the context Ψ (rule D∀I) succeeds if e checks against A in the extended context(Ψ, a). The subsumption rule DSub calls the subtyping relation, and changes the mode fromchecking to synthesis: if e synthesizes type A and A ≤ B, then e checks against B. Besides a
standard checking rule (D→I) for lambda abstractions, rule D→I⇒ synthesizes monotypes
σ → τ . Application e1 e2 is handled by rule D→E, which first synthesizes the type A of thefunction e1 . If A is a function type B → C, then rule D→App is applied. The synthesized
type of function e1 can also be polymorphic, of the form ∀a. A. In that case, we instantiate A
to [τ /a]A with a monotype τ using the rule D∀App. If [τ /a]A is a function type, rule D→App
is used; if [τ /a]A is another universal quantified type, rule D→I⇒ is recursively applied.

2.3

The Challenges of Explicit Type Applications

While explicit type applications seem like a natural extension to type systems with implicit
instantiation, the combination can break some important properties and make programs lessrobust to refactoring or inlining. In particular, in many existing type systems with implicit
instantiation, the order of type arguments being instantiated does not matter, whereas
with explicit instantiation the order does matter (at least if arguments are positional). The
design proposed by Eisenberg et al. [13] notices this difference, and distinguishes between
specified and generalized type quantification. All the GHC examples that we show in thispaper employ specified type quantification, where the programmer explicitly writes the typesignature, and the order of type arguments is relevant. However, there are other subtler
points in the design of a subtyping relation for specified type quantification that make it
hard to get certain expected properties in a language. We illustrate some concrete issues
next with GHC 8 and Eisenberg et al.’s design. We remark, however, that some other issues
with GHC 8’s approach have already been identified and GHC 9 adopts a different approachthat avoids the issues described here. A detailed discussion follows in Section 7.
Explicit Type Applications, Subsumption and Equational Reasoning The design byEisenberg et al. is based on bidirectional type-checking and supports a standard subsumption
rule, similar to the rule DSub in DK’s type system. Moreover, the subtyping relation employedin that design is essentially an extension of that in DK’s type system. The examples that weshow next involve subtyping relations that are valid in both DK’s type system, as well as the

J. Zhao and B. C. d. S. Oliveira

2:7

subtyping relation employed by Eisenberg et al. [13]. An important lemma that holds forthe DK type system is the checking subsumption lemma:
I Lemma 1 (Checking Subsumption). If Ψ ` e ⇐ A and Ψ ` A ≤ B then Ψ ` e ⇐ B
This lemma is quite similar to the subsumption rule. The difference is that the premise(Ψ ` e ⇐ A) is in checking mode, instead of synthesis mode. The lemma states that we
can always change the type of an expression being checked to a supertype. A practicalconsequence of this lemma is that changing type annotations of an expression to a supertypeis always possible, which is something that programmers would expect. For example, we
could change the type annotation of f in Section 2.1 to that of h and f would still type-check.
In contrast to DK’s type system, the work by Eisenberg et al. [13] and GHC 8 does
not have the checking subsumption property. We believe that the lack of this property isundesirable, especially for a language that promotes equational reasoning like Haskell. To
illustrate why the property is important, consider the Haskell functions:h2 :: (forall b a. b -> a -> b) -> Bool -> Int
h2 k = g k -- type checks!
h3 :: (forall b a. b -> a -> b) -> Bool -> Int
h3 k = k @Bool 3 -- rejected!

Recall the examples from Section 2.1. Function h is defined with a simple call to f, although
it has a different type. Here the new function h2 has the same type as h, which is a supertypeof the type of f and g. However, if we try to replace the call g k by its definition in h2, we
get the definition h3, which no longer type-checks. There are two important issues to noticehere. Firstly, replacing equals by equals (or inlining) results in a program that does not
type-check! The problem is that now the type argument of k in h3 instantiates the wrong
type variable. Now k has two type arguments, and the second type argument corresponds
to the first type argument of the type of the argument k in g. Because of this, the type ofk in h3 is not compatible with the use of k in the body. Secondly, the example shows thathigher-ranked type arguments that use explicit type applications can break the checking
subsumption property. There are some valid supertypes of functions that, if used insteadof the original type, will result in an ill-typed program. Even though the type of h2 is asupertype of the type of g, we cannot use that supertype to type-check g.
Explicit Type Applications in DK’s Type System A naive extension of the DK type systemwith explicit type applications would be to add the rule:Ψ ` e ⇒ ∀a. A
Ψ ` e @B ⇒ [B/a]A

DTypeApp∀

This rule first synthesizes a polymorphic type ∀a. A from e, and then outputs its instantiation[B/a]A for the explicit type application e @B. Unfortunately, this rule breaks checking
subsumption as well, for very similar reasons to those in the GHC examples. It is easy toport the previous GHC counter-examples to this extension of DK’s type system, and get
similar issues to those that we have just described.
Example 1 Now we look at a different example that illustrates the general problem of
having order-irrelevance of universally quantified type variables. Suppose that we havee = λx. x @Int 3 True, A = (∀a. ∀b. a → b → a) → Int, and B = (∀b. ∀a. a → b → a) → Int.
Both conditions of the checking subsumption lemma
λx. x @Int 3 True ⇐ (∀a. ∀b. a → b → a) → Int(∀a. ∀b. a → b → a) → Int ≤ (∀b. ∀a. a → b → a) → Int

ECOOP 2022

2:8

Elementary Type Inferencehold, yet the conclusion λx. x @Int 3 True ⇐ (∀b. ∀a. a → b → a) → Int does not hold:the type application instantiates the wrong type variable, causing the type system to reject
it. The types A and B here differ only in the order of polymorphic type variables. The
order-sensitive explicit type application is not compatible with order-irrelevant subtyping
relations, such as the one in DK’s type system, breaking the checking subsumption lemma.
Impredicative Type Applications and Stability of Subtyping So far, we have illustrated
problems that involve only monotypes (and predicative instantiation). If impredicative typeapplications are supported as well, then this brings another class of problems.
Example 2 Consider e = λx. x @C, A = (∀a. a → a) → (C → C), and B =(∀a. ∀b. b → a) → (C → C). Here we assume C = (∀a. a → a) → Int, but other polymorphic types could be used as well. Both conditions of the checking subsumption lemma:
λx. x @C ⇐ (∀a. a → a) → (C → C)(∀a. a → a) → (C → C) ≤ (∀a. ∀b. b → a) → (C → C)
hold, but not the conclusion λx. x @C ⇐ (∀a. ∀b. b → a) → (C → C). When type checking
the condition λx. x @C ⇐ (∀a. a → a) → (C → C), the type application @C is properly
applied, instantiating the universal variable a on the type of x (∀a. a → a) to C. However,when we have the conclusion λx. x @C ⇐ (∀a. ∀b. b → a) → (C → C), the type application
x @C only instantiates the type argument a, but not the type argument b. Thus the type
inferred for the application x @C is ∀b. b → C. Unfortunately, the predicative subtyping
relation rejects ∀b. b → C ≤ C → C when C is a polymorphic type like (∀a. a → a) → Int.
Thus, the conclusion λx. x @C ⇐ (∀a. ∀b. b → a) → (C → C) fails to type check.
While this problem is also an instance of checking subsumption not holding, the reason
why this example fails is different from the previous examples. The crux of the problem hereis that some instantiations with polytypes break the polymorphic subtyping relation after
instantiation. More concretely, we would like the following property to hold:
I Corollary 2 (Stability of Subtyping). If Ψ ` ∀a. A ≤ ∀a. B then Ψ ` [C/a]A ≤ [C/a]B
holds for any well-formed C (Ψ ` C).
but this property does not hold in general for polytypes in DK’s type system. DK’s typesystem has a similar property, but only for monotypes. When impredicative type applications
are present, we would like to have a more general property that holds for polytypes as well.
Problem with Unused Variables Furthermore, unused type variables in universal quantifiers
are problematic, since they can also break stability of subtyping. ∀a. ∀b. a ≤ ∀a. a is acceptedby most subtyping relations that support implicit instantiation, including DK and HM. If
we instantiate both sides of the subtyping judgment with the polytype C := ∀c. c → c, thejudgment becomes ∀b. ∀c. c → c ≤ ∀c. c → c, which is then problematic, because a second
instantiation with C 0 := ∀d. d → d would give ∀c. c → c ≤ (∀d. d → d) → (∀d. d → d), whichis rejected by predicative systems. Here the problem is not caused by a permutation or extra
type variables in polytypes. Instead, an unused variable leads to such problem.

2.4

The Problems with Subtyping with Top and Bottom Types

Besides the problems with explicit type applications, the presence of top and bottom types
raises its own class of issues.

J. Zhao and B. C. d. S. Oliveira

2:9

Polymorphic Subtyping with Top and Bottom Types To support top and bottom types in
DK’s type system, a first idea is to introduce those types, with their standard subtyping
rules and consider them to be monotypes, leading to the following syntax for monotypes:
τ ::= 1 | ⊥ | > | τ → τ | a
Unfortunately, it is known that the subtyping for a language with type variables, such as theabove, can quickly become undecidable [34]. To illustrate some of the issues, consider thesubtyping judgment ∀a. (a → a → 1) → 1 ≤ (∀b. b → b) → 1, which reduces to the following
b satisfying α
problem: find (predicative) instantiations for αb and β,b ≤ βb and βb ≤ α
b → 1.
Such a problem has infinitely many solutions, where there is no best one. If we assume thatexistential variables αb and βb are instantiated to the same type, there are infinite solutions:αb = βb = ⊥ | > → 1 | > → ⊥ | (⊥ → 1) → 1 | · · ·b Assignments
Additionally, αb = βb is not the most general unification for the judgment αb ≤ β.
bbb
like αb = β, β = β → 1 also validate the subtyping judgments.
Inference of > and ⊥ Types can Mask Type Errors A different issue is that sometimes
inferring > and ⊥ types can mask type errors. Consider the following expression:
λf. f + f 1
Such expression can be typed with the type ⊥ → Int. Since the input parameter f , having
type ⊥, can be converted to either an integer or to a function of type Int → Int. However,inferring such a type is hardly useful in practice. Instead, the programmer might have
immediately realised the bug (perhaps the argument for the first call to f is missing) if thetype inference algorithm rejects the lambda expression, rather than after it has inferred atype with ⊥. By constraining the type inference algorithm to infer types free from > and ⊥,such type is no longer be inferred, and thus the bug is reported when defining the function.
It is mentioning that, in languages like Scala, there are several reports of issues arisingbecause > and ⊥ (respectively Any and N othing in Scala) can be inferred2 . The Scalacompiler even has a flag -Xlint:infer-any that is used to warn whenever Any is inferred.

2.5

Our Solutione
The form of type-inference available in F<:
is inspired by current approaches employed inepredicative higher-ranked type inference [25, 8, 9, 20, 39]. In terms of restrictions, F<:does
not have generalization (similarly to the DK type system), and there are some restrictions
that weaken the expressive power of the polymorphic subtyping relation. However, those
restrictions mostly affect higher-ranked programs, and for many other Hindley-Milner styleprograms (with polymorphic annotations) there should be no impact from those restrictions.
e
In terms of innovations the type system of F<:
supports top and bottom types and explicit
impredicative type applications. Moreover, implicit instantiation and explicit instantiationinteroperate well and have important properties, such as checking subsumption and stabilityof subtyping. Next we show some examples that run in our implementation and illustrateethe capabilities of the F<:
type system. We note that our implementation contains someextra features that enable us to present more interesting examples. These features include
recursive let expressions, (polymorphic) lists and case expressions on lists.
2

See for instance: https://riptutorial.com/scala/example/21134/preventing-inferring-nothing.

ECOOP 2022

2:10

Elementary Type Inference

Rank-1 Polymorphism. We start with first-order polymorphism, which is the kind ofepolymorphism supported in Hindley-Milner. We can define the map function in F<:
as follows:1
2

let map :: forall a b. (a -> b) -> [a] -> [b]= \f -> \xs -> case xs of [] -> []; (x:xs) -> f x : map f xs

This definition is similar to a definition in a language with Hindley-Milner, except that wemust explicitly provide the type of the map function. An explicit type is optional in languages
elike Haskell or ML, but must be provided in F<:
for polymorphic functions like map. Like in
Hindley-Milner, when writing the body of the function we do not need to use type binders
and the recursive call implicitly instantiates the types a and b. We can use map conventionally,
as in an HM language like Haskell or ML:
1map (\x -> x + 1) [1,2,3]

or use explicit type applications if necessary or desired. For example:
1

map @Int @Top (\x -> x :: Top) [1,2,3]

which uses explicit type applications to instantiate b with the Top type. Since the bodyof the function argument uses a type annotation (x :: Top) to return a Top type, writingmap (\x -> x :: Top) [1,2,3] would fail to type-check. The problem is that Top is not a
monotype in our system and cannot be inferred during implicit instantiation.
While there is no generalization, we can still infer monotypes for lambdas. Therefore, thefollowing is allowed:
1

let succ = \x -> x + 1

The type inferred for succ is the monotype Int -> Int. However writing let id = \x -> x,
without an explicit annotation for id would fail, since generalization would be necessary toinfer a polymorphic type for the identity function.
Higher-Ranked Polymorphism. With explicit type applications, it becomes possible toperform impredicative instantiations. A simple example of this is applying the identityefunction to itself. In F<:
we can write:1

let id :: forall a. a -> a = \x -> x in id @(forall a. a -> a) id

In this case the type used to explicitly instantiate the identity function is a polymorphic
type. Implicit instantiation is not possible here, since the type argument is not a monotype.
Another example of impredicative instantiation is:1
2

let plist :: [forall a. a -> a] = [\z -> z, \z -> z]
in map @(forall a. a -> a) (\f -> f 1) plist

where the map function takes a list with polymorphic functions of type forall a. a -> a. The
function argument (\f -> f 1) of map applies a polymorphic function to 1.
Restrictions for Higher-Ranked Polymorphism. The GHC 8 definitions in Section 2.1 for fe
and g also type-check in F<::
1
2

let f :: (forall a. Int -> a -> Int) -> Bool -> Int = \k -> k 3
let g :: (forall a. Int -> a -> Int) -> Bool -> Int = \k -> k @Bool 3

However, the definition of h fails to type-check:1

let h :: (forall b. forall a. b -> a -> b) -> Bool -> Int = \k -> f k-- fails!

This definition is rejected because ∀b. ∀a. b → a → b ≤ ∀a. Int → a → Int does not hold ineF<:. Our polymorphic subtyping relation does not consider the type of k to be a subtype ofthe expected argument for f. By preventing examples such as this one we avoid the issues
discussed in Section 2.3 and we retain the checking subsumption property.
We can also type-check the expression used in our Example 2:
1\x -> x @((forall a. a -> a) -> Int)

J. Zhao and B. C. d. S. Oliveira

2:11

with a type annotation:1(forall a. a -> a) -> ((forall a. a -> a) -> Int) -> ((forall a. a -> a) -> Int)

However, using the type annotation
12(forall a. forall b. b -> a) ->((forall a. a -> a) -> Int) -> ((forall a. a -> a) -> Int)

will fail because the type in the first annotation is not a subtype of the type in the second
annotation in our polymorphic subtyping relation: the subtyping statement ∀a. ∀b. b → a ≤∀a. a → a does not hold. In the Odersky and Läufer relation, such subtyping statement
holds. As discussed in Section 2.3, accepting such subtyping statements is problematic when
impredicative instantiation is allowed, since we lose the stability of subtyping property.
e
No Inference of Top and Bottom. Finally the type system of F<:
rejects:1

let strange = \f -> f + f 1-- fails!

As discussed in Section 2.4, this definition could be type-checked if we could infer the bottom
type for f. Since bottom is not a monotype, it cannot be infered and this definition is rejected.
However, the following definition, with an explicit type annotation is allowed:
1

let strange : Bot -> Int = \f -> f + f 1

In other words, we avoid inferring top and bottom, which can type-check programs that arelikely to have type errors. However, we can always provide annotations for definitions that
can type-check with polytypes, thus allowing such definitions to type-check if desired.

2.6

Key Technical Ideas

Stable Polymorphic Subtyping We address the problems with explicit type applications
via a novel notion of polymorphic subtyping, which preserves both subsumption and stabilityof subtyping. Stable subtyping, shown in Figure 2, is a variant from DK’s subtyping withsome changes. Note that we use color to highlight new rules or changes, with respect to
DK’s type system, here and throughout the paper. The new rule ≤s refl replaces base casesin the previous system, and rule ≤s ∀ directly expresses the expected stability property. We
also forbid polymorphic types that contain unused type variables. This restriction is enforcedby the well-formedness relation (see details in Section 3.1). Rule ≤s ∀L has a side condition
to prevent overlapping with rule ≤s ∀ and has a less priority. In addition, we also have two
new (but standard) rules for top and bottom types (rules ≤s > and ≤s ⊥).
There are 3 main differences with respect to DK’s subtyping relation. Firstly, stable
subtyping does not allow instantiations out-of-order. Note that, unlike DK’s type system,
there is no rule that corresponds to ≤∀R, which removes the ability to perform such instantiations. Thus, the order of type variables becomes relevant. Secondly, types with unused typevariables, such as ∀a.1, are not allowed. Finally, top and bottom types are supported.
A Syntax-Directed System with Subtype Variables While rule ≤s ∀ directly captures
the stability property that we want, such a rule is highly declarative. Thus, an important
challenge is to find an alternative equivalent set of rules that is closer to an implementation.
Our solution to the problem relies on a new sort of variables, ã, called subtype variables,
and the following subtyping rule, which is proven to have equal effect to ≤s ∀:Ψ, ã ` [ã/a]A ≤ [ã/a]BΨ ` ∀a. A ≤ ∀a. B≤∀

The difference between a subtype variable ã and a conventional type variable a is that a
subtype variable is not a monotype, therefore it cannot be instantiated with rule ≤∀L. Thus,
a subtyping statement such as ∀a. ∀b. b → a ≤ ∀a. a → a does not hold, since it would
require instantiation with a subtype variable, which is not allowed.

ECOOP 2022

2:12

Elementary Type InferenceΨ `s A ≤ B Stable subtypingΨ `s AΨ `s A ≤ A≤s reflΨ `s A ≤ >∀C, Ψ `s C =⇒ Ψ `s [C/a]A ≤ [C/a]BΨ `s ∀a. A ≤ ∀a. B
Ψ`τ

≤s ∀

Ψ `s [τ /a]A ≤ B≤s >Ψ `s ⊥ ≤ A

Ψ ` s B 1 ≤ A1≤s ⊥

Ψ `s A2 ≤ B2

Ψ ` s A1 → A2 ≤ B 1 → B 2
B 6= ∀b.B 0Ψ `s ∀a. A ≤ B

≤s →

≤s ∀L

Figure 2 Stable Subtyping

Explicit Type Applications for Polytype Instantiations To avoid being overly restrictive,
we still support polytype instantiations via explicit type applications. Thus, while someconvenience afforded by more expressive formulations of type inference is lost, no expressive
power is lost. We can encode a variant of System F<: (without bounded quantification)
trivially using explicit type applications. We formally verify the soundness and completenesstheorems in our Abella formalization and present the results in the extended version.
Summary With stable subtyping, Corollary 2 and the subsumption lemma hold, and thesystem works smoothly with the explicit type application rules in the type system. Moreover,
we address the problems with top and bottom types by not considering top and bottom types
as monotypes. This extends a similar idea in predicative HRP, which excludes universal
types from monotypes, thus avoiding decidability issues that arise from including such types.

3

Syntax-Directed SystemeThis section introduces a syntax-directed type system for F<:, which serves as a specification
for the algorithmic version that will be presented in Section 4. The type system can beviewed as a variant of the Dunfield and Krishnaswami [8] type system, adding explicit typeapplications and abstractions, as well as > and ⊥ types. Furthermore, the type system
supports impredicativity via explicit instantiations. The subtyping relation employed in thistype system is equivalent to the stable subtyping relation introduced in Section 2.6, but itis syntax-directed and employs a special kind of type variables in the subtyping relation.
Several important properties, such as the subsumption lemma, a generalized stability lemma
for impredicative types, and transitivity of subtyping are proved.

3.1

Syntax and Well-FormednesseCompared to the syntax of the DK system presented in Figure 1, the syntax of F<::

Type variables a, b
Types
Monotypes
Expressions
Contexts

A, B, C
τ, σ
e, t
Ψ

Subtype variables
::=
::=
::=
::=

ã, b̃

1 | a | ∀a. A | A → B | ã | > | ⊥1|a|τ →σx | () | λx. e | e1 e2 | (e : A) | e @A | Λa. e : A· | Ψ, a | Ψ, x : A | Ψ, ã

J. Zhao and B. C. d. S. Oliveira

2:13

is extended in the four directions. First, types now include > and ⊥. Second, expressions
are extended with type applications (e @A). Third, type abstractions (Λa. e : A), studied
by Zhao et al. [39], are adopted as well, since they are useful to express programs withscoped type variables [24]. Note that programmers do not have to write Λ’s directly. Instead,an explicit annotation e : ∀a. A can serve as the syntactic sugar e : ∀a. A ≡ Λa.e : ∀a. A.
Finally, there is a new syntactic sort: subtype variables, ã, representing type variables thatare only used in subtyping and are not monotypes. It is worth mentioning that the definition
for monotypes is not changed. We do not treat >, ⊥, or subtype variables as monotypes.
Well-Formedness The well-formedness relation is mainly used to ensure the well-scopednessof binders. Additionally, we add special free variable checks to ensure that the polymorphic
type ∀a. A is indeed polymorphic in the following two rules:
Ψ, a ` Aa ∈ FV(A)Ψ ` ∀a. A

wfd ∀Ψ, a ` A Ψ, a ` e

a ∈ FV(A)Ψ ` Λa. e : A

wfd tLam

The motivation for the a ∈ FV(A) restriction is discussed in Section 2.3 with examples. This
has an impact on the compatibility with other systems, since we can no longer express types
like ∀a. 1. Yet we argue that such types are not very useful in practice; when a ∈/ FV(A),∀a. A is isomorphic to A in systems without explicit instantiation.

3.2

Subtyping and Typing Rules

The top of Figure 3 shows the subtyping relation. Grayed parts are F<: [2] expressions, which
are used to prove our soundness result with respect to F<: , can be ignored for the moment.
We refer the reader to the our extended version for the details of the F<: soundness result.
Most rules are inherited from Odersky and Läufer (OL) [20], yet there are several differences.
Rule ≤SVar is a new rule for subtype variables. This rule is just like the standard rule fortype variables (rule ≤Var). Rules ≤> and ≤⊥ are new (but standard) rules for > and ⊥.
Rule ≤∀ is also new. In this rule, two forall types are subtypes if their bodies are subtypes.
Importantly, the type variables in the bodies become subtype variables and are marked
as such when added to the context. Rule ≤∀L has an two additional premises to prevent
overlapping with rules ≤∀ and ≤>, respectively. The first condition B =6 ∀b. B 0 ensures that≤∀ always has priority. The second condition B =6 > can be safely omitted without changing
the expressive power, but is presented here to ensure that the system is syntax-directed.
The polymorphic subtyping relation behaves slightly differently from OL’s subtyping. Ifewe ignore > and ⊥ types, this relation is weaker than OL. In F<:, the order of polymorphic
variables is important. For example, in the OL’s system, the subtyping statement · `e∀a. ∀b. a → b → a ≤ ∀b. ∀a. a → b → a holds, but F<:
will reduce that to ã, b̃ ` ã → b̃ →ã ≤ b̃ → ã → b̃ , which does not hold. Apart from the ordering of variables, instantiation
works differently for subtyping between polymorphic types. OL’s subtyping relation acceptsethe following judgment · ` ∀a. (a → a) → (a → a) ≤ ∀a. a → a but F<:
does not, sinceã ` (ã → ã) → (ã → ã) ≤ ã → ã does not hold either.
Typing The bottom of Figure 3 shows the type system. Compared to DK’s type system,
there are 4 groups of changes:
1. Rules D> and D⊥App are introduced for the > and ⊥ types. Note that in rule D> weemploy a relation Ψ ` e that checks for the well-formedness of expressions. We omit
the definition of Ψ ` e, but it is standard, checking whether all the free variables in
e are bound in Ψ. Both rules are essential for the subsumption lemma to hold. For
example, rule D⊥App is required to type-check the expression (λx. x ()) : ⊥ → 1, where

ECOOP 2022

2:14

Elementary Type InferenceΨ ` A ≤ B ,→ E

Syntax-directed subtypingΨ ` 1 ≤ 1 ,→ λ(x : 1). x≤UnitΨ ` ⊥ ≤ A ,→ λ(x : ∀a. a). x @|A|Ψ ` A ≤ > ,→ λ(x : |A|). topa∈Ψ≤⊥Ψ ` a ≤ a ,→ λ(x : a). xã ∈ Ψ
Ψ ` ã ≤ ã ,→ λ(x : a). xΨ`τ

B 6= >Ψ ` ∀a. A ≤ B ,→ λ(x : |∀a. A|). E (x @τ )Ψ, ã ` [ã/a]A ≤ [ã/a]B ,→ EΨ ` ∀a. A ≤ ∀a. B ,→ λ(x : |∀a. A|). Λa. E (x @a)Ψ ` B1 ≤ A1 ,→ E1

≤∀L

≤∀

Ψ ` A2 ≤ B2 ,→ E2

Ψ ` A1 → A2 ≤ B1 → B2 ,→ λ(f : |A1 → A2 |). λ(x : |B1 |). E2 (f (E1 x))

Ψ ` e ⇐ A ,→ Ee checks against input type A.

Ψ ` e ⇒ A ,→ E

e synthesizes output type A.

Ψ ` A • e ⇒⇒ C ,→ Ec | EΨ ` e ⇒ A ,→ E
DVarΨ ` A ≤ B ,→ co

Ψ`σ→τ
DAnno

Ψ ` (e : A) ⇒ A ,→ E

DSubΨ, x : σ ` e ⇐ τ ,→ EΨ ` λx. e ⇒ σ → τ ,→ λ(x : σ). E

Ψ, a ` e ⇐ A ,→ E

D→I⇒

Ψ, x : A ` e ⇐ B ,→ EΨ ` e ⇐ ∀a. A ,→ Λa. E

D∀IΨ ` λx. e ⇐ A → B ,→ λ(x : A). EΨ ` e1 ⇒ A ,→ E1
D1I⇒

D→I

Ψ ` A • e2 ⇒⇒ C ,→ Ec | E2
D→E

Ψ ` e1 e2 ⇒ C ,→ (Ec E1 ) E2
Ψ ` e ⇐ A ,→ EΨ`e
Ψ ` e ⇐ > ,→ top

A 6= ∀a. A0Ψ ` e ⇐ B ,→ co EΨ ` A Ψ ` e ⇐ A ,→ E

Ψ ` () ⇒ 1 ,→ ()≤→Applying a function of type A to e synthesizes type C.

(x : A) ∈ ΨΨ ` x ⇒ A ,→ x

≤Var

≤SVar

B 6= ∀b.B 0Ψ ` [τ /a]A ≤ B ,→ E≤>D>Ψ ` A → C • e ⇒⇒ C ,→ λ(x : |A → C|). x | E

D→AppΨ ` e ⇒ ⊥ ,→ EΨ ` e @B ⇒ ⊥ ,→ E
Ψ`τ

DTA⊥

Ψ ` [τ /a]A • e ⇒⇒ C ,→ Ec | EΨ ` ∀a. A • e ⇒⇒ C ,→ λ(x : |∀a. A|). Ec (x @τ ) | E
Ψ, a ` e ⇐ A ,→ EΨ ` Λa. e : A ⇒ ∀a. A ,→ Λa. E

D∀AppΨ ` e ⇒ ∀a. A ,→ E
DSTVΨ ` e @B ⇒ [B/a]A ,→ E @|B|Ψ`e
Ψ ` ⊥ • e ⇒⇒ ⊥ ,→ λ(x : ∀a. a). x @(> → ∀a. a) | top

Figure 3 Syntax-directed System.

D⊥App

DTA∀

J. Zhao and B. C. d. S. Oliveira

2:15

the argument x has type ⊥ and the application x () synthesizes ⊥ according to the rule,
which can then check against the 1 type by rule DSub.
2. Rule DSub now requires one side-condition to prevent overlapping with Rule D∀I. In
presence of explicit type applications, this condition cannot be eliminated.
3. Rules DTA⊥ and DTA∀ infer type application expressions. If the type of e synthesizes apolymorphic type ∀a. A, then e @B has type [B/a]A. Any expression of type ⊥ will
synthesize ⊥ for any type applied.
4. Rule DSTV enables the scoped type variables [24]. This allows flexible control of typevariables by the programmer.
Note that the D> is peculiar in that it allows some ill-typed terms to type-check. Suchrules are often needed in bi-directional type systems with top types to enable properties suchas checking subsumption. For instance a similar rule is employed by Dunfield [7]. Since the
top type is the supertype of all types, all well-typed expressions should be able to type-checkunder the top type as well. For example, we should be able to change the type annotationin function λx.x : Int → Int to λx.x : >. However, there is not enough type information to
type-check the body of the later lambda. Nevertheless, we do not need to evaluate expressions
with a top type, since no information can be extracted from such type, and the elaboration
to F<: results directly in the top value for such expression, preserving type-safety.

3.3

Metatheory

The type system has several desirable properties, including subsumption and a stability oftype substitutions lemma in subtyping.
Reflexivity and Transitivity Firstly, our subtyping relation is reflexive and transitive.
I Lemma 3 (Subtyping Reflexivity). If Ψ ` A then Ψ ` A ≤ A.
I Lemma 4 (Subtyping Transitivity). If Ψ ` A ≤ B and Ψ ` B ≤ C then Ψ ` A ≤ C.
Equivalence to Stable Subtyping and Stability Secondly, the syntax-directed formulationof subtyping is sound and complete with respect to the stable subtyping relation in Section 2.6.
Subtype variables are used to provide an alternative formulation of the ≤∀ rule, bringing
subtyping closer to an algorithm. Nonetheless, syntax-directed subtyping still guesses
monotypes, thus it is not algorithmic.
I Theorem 5 (Soundness w.r.t stable subtyping). If Ψ ` A ≤ B then Ψ `s A ≤ B.
I Theorem 6 (Completeness w.r.t stable subtyping). Given Ψ ` A and Ψ ` B, if Ψ `s A ≤ B
then Ψ ` A ≤ B.
The proof works by generalizing instantiations for subtype variables and existential
variables (which represents monotypes to be guessed). We refer to the extended version
for details. A related property of the subtyping relation is stability. The following lemma
generalizes Corollary 2 by allowing the subtype variable to appear anywhere in the context.
I Lemma 7 (Stability of Subtyping, Generalized). If Ψ ` A ≤ B and Ψ ` C then Ψ `[C/ã]A ≤ [C/ã]B.
This property ensures that any subtype variable can be replaced by a polytype C in two
types A and B while preserving the subtyping relation between those two types.

ECOOP 2022

2:16

Elementary Type Inference

The Subsumption Lemma To prove the checking subsumption lemma, we first needto generalize the statement for inference and application inference judgments, as well as
introduce a context subtyping relation, Ψ ≤ Ψ0 , to state the most general form.
I Definition 8. Ψ0 ≤ Ψ Context Subtyping
Ψ0 ≤ Ψ
·≤·CS_Empty

Ψ0 , a ≤ Ψ, a
Ψ0 ≤ Ψ

Ψ0 ≤ Ψ
CS_TV

Ψ0 , ã ≤ Ψ, ã

CS_STVΨ ` A0 ≤ AΨ0 , x : A0 ≤ Ψ, x : A

CS_V

Context Ψ subsumes context Ψ0 if they bind the same variables in the same order, but thetypes of variables in Ψ0 must be subtypes of those in Ψ. The generalized lemma is:
I Lemma 9 (Subsumption). Given Ψ0 ≤ Ψ:
1. If Ψ ` e ⇐ A and Ψ ` A ≤ A0 then Ψ0 ` e ⇐ A0 ;2. If Ψ ` e ⇒ B then there exists B 0 s.t. Ψ ` B 0 ≤ B and Ψ0 ` e ⇒ B 0 ;3. If Ψ ` A • e ⇒⇒ C and Ψ ` A0 ≤ A, then ∃C 0 s.t. Ψ ` C 0 ≤ C and Ψ0 ` A0 • e ⇒⇒ C 0 .
This lemma expresses that any derivation in a context Ψ has a corresponding derivation inany context Ψ0 that it subsumes.
Relating Subtype and Type Variables The following lemma shows that we can substitutea subtype variable with a normal type variable, while preserving the subtyping relation.
I Lemma 10. If Ψ[ã] ` A ≤ B then Ψ[a] ` [a/ã]A ≤ [a/ã]B.
The reason is relatively straightforward. First, the substitution does not affect the ã ≤ ã
sub-judgments. Second, substituting ã to a increases the range of implicit instantiation,
which means that the monotypes picked in the old context are still well-formed under the newcontext. Note that the reverse statement does not hold. For example, b ` ∀a. a → a ≤ b → b
holds with the predicative instantiation a := b, but b̃ ` ∀a. a → a ≤ b̃ → b̃ does not; one
cannot instantiate a with a non-monotype, or b̃ in this case.

4

Algorithmic System

This section introduces an algorithmic system that implements the syntax-directed specificaetion of F<:. The new algorithm is based on Zhao et al.’s [39] worklist algorithm but extended
with explicit type applications and top and bottom types. In Section 5, we show that thisalgorithm is sound, complete and decidable with respect to the specification presented in
Section 3. We also use color throughout this section to highlight differences to the original
formulation by Zhao et al. [39].

4.1

Syntax and Well-FormednesseFigure 4 shows the syntax for the algorithmic version of F<:. Similarly to the syntax-directed
system, the well-formedness rules are unsurprising, ensuring well-scopedness for binders aswell as the free variable constraint on polymorphic types. We refer to the extended version
for well-formedness relations of algorithmic types, expressions, judgments, and worklists.

J. Zhao and B. C. d. S. Oliveira

2:17

a, b

Subtype variables

A, B, C::=

Judgment chainω::= A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω | A ◦ B ⇒⇒a ω

Algorithmic worklistΓ::= · | Γ, a | Γ, ã | Γ, αb | Γ, x : A | Γ

Declarative worklistΩ::= · | Ω, a | Ω, ã | Ω, x : A | Ω

Type variables
Algorithmic types

ã, b̃

Existential variables αb , βb... | αbωωFigure 4 Extended Syntax for the Algorithmic System (Extended from Figure 1)

Existential Variables The algorithmic system inherits the syntax of terms from the syntaxdirected system and extends types with a new sort of variables—existential variables. Exb are introduced to help find unknown monotypes τ that appear in
istential variables (bα , β)
multiple rules of the syntax-directed system. In the algorithmic worklist, the position where
existential variables are declared indicates the possible monotypes they can be solved to.
Formally speaking, if α
b is introduced right after Γ, then αb can only be solved to a monotype
τ where Γ ` τ . This behavior is derived from the well-formedness restriction of the rule ≤∀L.
An important remark is that subtype variables are not considered to be monotypes, therefore
no existential variable can be solved to a subtype variable.
Judgment Chains Judgment chains ω, or judgments for short, are the core componentsof our algorithmic type-checking. There are five kinds of judgments in our system. Four ofthem are inherited from [39]: subtyping (A ≤ B), checking (e ⇐ A), inference (e ⇒a ω) andapplication inference (A • e ⇒⇒a ω). Type application inference A ◦ B ⇒⇒a ω is new, and it isused to help with the inference in type application expressions (e @B). This judgment plays
a role similar to application inference for regular applications. In type application inference
judgments, the first type A is the type inferred from the expression e. The judgment is thenreduced differently depending on whether A is a polymorphic type ∀a. A0 or ⊥.
Subtyping and checking are relatively simple, since their results are only success or failure.
However, inference, application inference, and type application inference judgments return atype that is used in subsequent judgments. We use a continuation-passing-style encoding toaccomplish this, following the approach by Zhao et al. [39]. For example, the judgment chaine ⇒a (a ≤ B) contains two judgments: first we infer the type of the expression e, and thencheck if the inferred type is a subtype of B. The unknown type of e is represented by a typevariable a, which is used as a placeholder in the second judgment to denote the type of e.
Worklist Judgments Our algorithmic context Γ, or worklist, combines traditional contexts
and judgment(s) into a single sort. The worklist is an ordered collection of both variablebindings and judgments. The order captures the scope: only the objects that come aftera variable’s binding in the worklist can refer to it. For example, [·, a, x : a x ⇐ a] is avalid worklist, but [· x ⇐ a, x : a, a] is not (the underlined symbols refer to out-of-scope
variables). This property also affects how the algorithm behaves regarding solving existential
variables. By solving an existential variable α
b with any monotype that does not escape thescope of αb preserves well-formedness of the whole worklist.
Notation and Form of the Algorithmic Rules The algorithmic subtyping and typing
reduction rules, defined in Figures 5 and 6, have the form Γ −→ Γ0 . Since the worklist isa stack of variable definitions and judgment chains, the algorithm pops the first element,
processes according to the rules, and possibly pushes simplified judgments back. The syntax
Γ −→∗ Γ0 denotes multiple reduction steps. A worklist Γ is accepted by the algorithm iff

ECOOP 2022

2:18

Elementary Type InferenceΓ −→ Γ0 Γ reduces to Γ0 .
Γ, a −→1 ΓΓ

1 ≤ 1 −→5 ΓΓΓ, αb −→2 ΓΓ, ã −→3 ΓΓa ≤ a −→6 ΓΓã ≤ ã −→7 ΓΓA ≤ > −→8 ΓΓ⊥ ≤ A −→9 Γ

A1 → A2 ≤ B1 → B2 −→10 ΓΓA2 ≤ B2∀a. A ≤ B −→11 Γ, αb

Γ, x : A −→4 Γ

B1 ≤ A1[b
α /a]A ≤ B

when B 6= ∀a. B 0 and B 6= >
Γ∀a. A ≤ ∀a. B −→12 Γ, ã
Γ

Γ[b
α]

[ã/a]A ≤ [ã/a]Bαb≤αb −→13 Γαb ≤ A → B −→14 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ]

αb1 → αb2 ≤ A → B)

when αb∈/ F V (A) ∪ F V (B)
Γ[b
α]

A→B≤α
b −→15 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ]A→B≤αb1 → αb2 )when αb∈/ F V (A) ∪ F V (B)bΓ[bα ][β]bαb ≤ βb −→16 [bα /β](Γ[bα ][])bΓ[bα ][β]bβb ≤ αb −→17 [bα /β](Γ[bα ][])b
Γ[a][β]ba ≤ βb −→18 [a/β](Γ[a][])b
Γ[a][β]b
βb ≤ a −→19 [a/β](Γ[a][])

b
Γ[β]

b
1 ≤ βb −→20 [1/β](Γ[])

b
Γ[β]

b
βb ≤ 1 −→21 [1/β](Γ[])

Figure 5 Algorithmic Variable and Subtyping Rules.

Γ −→∗ ·. In other words a program successfully type-checks if all the work has been processed.
Any new variable introduced to the r.h.s of the worklist Γ0 is fresh implicitly, similarly to
how we treat them in the conditions of other rules. We also adopt the notation Γ[ΓM ] fromthe DK type system to denote the worklist ΓL , ΓM , ΓR , where Γ[•] is the worklist ΓL , •, ΓR
with a hole (•). Hole notations with the same name implicitly share the same structure ΓLband ΓR . A multi-hole notation splits the worklist into more parts. For example, Γ[bα ][β]bmeans Γ1 , α
b , Γ2 , β, Γ3 .

4.2

Garbage Collection and Algorithmic Subtyping Rules

Figure 5 defines algorithmic rules on variables (garbage collection) and subtyping. Rules
1-4 pop variable declarations that are essentially garbage. Thanks to the nature of ordered
context, those variables are no longer referred to by the remaining judgments, therefore
removing them does not break the well-formedness of the worklist.
Subtyping rules We can discern 3 groups of rules for algorithmic subtyping. The firstgroup consists of rules 5-12, where all the rules are similar to their syntax-directed systemcounterparts. The most interesting one is rule 12, which reflects the changes in our syntaxdirected system. A subtype variable ã is used to replace the bound variable in the polymorphic
types ∀a. A and ∀a. B for further reduction. Rule 11 differs from rule ≤∀L by introducing
an existential variable α
b instead of guessing the monotype τ instantiation.
The second group is about solving existential variables (rule 13) and existential variable
decomposition (rules 14 and 15). Rule 13 is one of the base cases involving existential variables.

J. Zhao and B. C. d. S. Oliveira

2:19

Rules 14 and 15 are algorithmic versions of Rule ≤→; they both partially instantiate αb tofunction types. The domain α
b1 and range α
b2 of the new function type are not determined
immediately: they are fresh existential variables with the same scope as αb . The occurs-checkcondition prevents divergence as usual. For example, without it αb≤1→αb would diverge.
The final group consists of rules 16-21, where each rule solves an existential variableagainst a basic type. Each rule removes an existential variable and substitutes it with its
solution in the remaining worklist, which preserves well-formedness in the meantime. For
example, Rule 16 solves variable α
b with βb only if βb occurs after αb . It is worth noting thatnone of these rules solves α
b to a subtype variable b̃. As we have discussed, >, ⊥ and subtype
variables are not monotypes, therefore existential variables do not unify with them.

4.3

Algorithmic Typing Rules

Figure 6 shows the algorithmic rules for typing.
Checking Judgments Rules 22-26 deal with checking judgments. Rule 22 is DSub written in
a continuation-passing-style. The side conditions e 6= λx. e0 and B 6= > prevent overlap withall other rules. Rules 23, 24 and 26 adapt their counterparts in the syntax-directed system,
where rules 23 and 26 correspond to the new/changed rules introduced in the syntax-directed
system compared to DK’s work. Rule 25 is a special case of D→I, dealing with the casewhen the input type is an existential variable, representing a monotype function as in thesyntax-directed system. The same instantiation technique as in rules 14 and 15 applies.
Inference judgments Inference judgments accept an expression and return a type. Rules
27-33 deal with type inference judgments. The algorithm uses a continuation-passing-style
encoding, where the output type is passed to the next judgment. When an inference judgment
succeeds with type A, the algorithm continues to work on the inner-chain ω by substituting
a by A in ω. Rule 27 and 30 are base cases (variable and unit), where the inferred typeis passed to its child judgment chain. Rules 28 and 29 infer an annotated expression bychanging into checking mode, therefore another judgment chain is created. Rule 29 deals
with scoped type variables; the type variable a is in scope in e, and corresponds to the rule
DTA∀. Rule 31 infers the type of a lambda expression by introducing α
b , βb as the input andoutput types of the function, respectively. Rule 32 infers the type of an application by firstly
inferring the type of the function e1 . Then the remaining work is delegated to an application
inference judgment, which passes a, representing the return type of the application, to theremainder of the judgment chain ω. Rule 33 is new: it first infers the type of e, then calls
the type application inference judgment to compute the return type.
Type Application and Application Inference Judgments Rules 34 and 35 deal with the
new type application inference judgments. Rule 34 accepts a polymorphic input ∀b. B
and produces its instantiation [C/b]B. Rule 35 returns ⊥ as it can be used as any type.
For example, if we choose to treat ⊥ as the polymorphic type ∀b. ⊥, the result after typeapplication is ⊥ according to rule 34. Finally, Rules 36-39 deal with application inference
judgments. Rules 36, 37 and 38 behave like rules D∀App, D→App and D⊥App, respectively.
Rule 39 instantiates α
b to the function type α
b1 → αb2 , just like Rules 14, 15 and 25.

5

Algorithmic Metatheory

This section presents the metatheory of the algorithmic system in Section 4. We show threemain results: soundness, completeness and decidability. Our proofs employ similar techniques
to the ones by Zhao et al. [39], so we only highlight the main results and differences.

ECOOP 2022

2:20

Elementary Type InferenceΓ −→ Γ0 (cont.) Γ reduces to Γ0 .
Γe ⇐ B −→22 Γe ⇒a a ≤ Bwhen e 6= λx. e0 and B 6= ∀a. B 0 and B 6= >e ⇐ ∀a. A −→23 Γ, a

Γ

λx. e ⇐ A → B −→24 Γ, x : AΓΓe ⇐ > −→26 ΓΓx ⇒a ω −→27 Γ([A/a]ω)(Λa. e : A) ⇒b ω −→29 ΓΓΓ

λx. e ⇒a ω −→31 Γ, αb , βbΓ

e1 e2 ⇒a ω −→32 Γ

e1 ⇒b (b • e2 ⇒⇒a ω)Γ

e @C ⇒a ω −→33 Γe ⇒b (b ◦ C ⇒⇒a ω)ΓΓ⊥ ◦ C ⇒⇒a ω −→35 ΓΓ[bα]⊥ • e ⇒⇒a ω −→38 Γe ⇐ βb[⊥/a]ω
([C/a]ω)∀a. A • e ⇒⇒a ω −→37 Γ, α
b
Γ

b
([b
α → β/a]ω),x:αb[([C/b]B)/a]ω

A → C • e ⇒⇒a ω −→36 ΓΓe⇐A[1/a]ω

∀b. B ◦ C ⇒⇒a ω −→34 ΓΓe⇐A([∀a. A/b]ω), a() ⇒a ω −→30 Γ

e⇐α
b2 )

when (x : A) ∈ Γ[A/a]ω

(e : A) ⇒a ω −→28 ΓΓe⇐B

λx. e ⇐ αb −→25 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ], x : α
b1

Γ[b
α]

Γ

e⇐A

e⇐A

[b
α /a]A • e ⇒⇒a ω[⊥/a]ω

αb • e ⇒⇒a ω −→39 [bα1 → αb2 /bα ](Γ[bα1 , αb2 ]

αb1 → αb2 • e ⇒⇒a ω)

Figure 6 Algorithmic Typing Rules

5.1

Declarative Worklist and Transfer

To aid in formalizing the correspondence between the declarative and algorithmic systems,
we use a declarative worklist Ω, defined in Figure 4. A declarative worklist Ω has the samestructure as an algorithmic worklist Γ, but does not contain any existential variables αb.
Worklist Instantiation We instantiate an algorithmic worklist Γ to the declarative worklistΩ by instantiating all existential variables α
b in Γ with well-scoped monotypes τ .
I Definition 11. ΓΩ Γ instantiates to Ω.

Ω

Ω

Ω

Ω`τ

Ω, [τ /b
α ]Γ
Ω, α
b, Γ

Ω

Ω

α
b

Rule αb replaces the first (left-most) existential variable with a well-scoped monotype andrepeats the process on the resulting worklist until no existential variable remains and thus
the algorithmic worklist has become a declarative one. In order to maintain well-scopedness,the substitution is applied to all the judgments and term variable bindings in the scope of αb.
Declarative Worklist Reduction A relation Ω −→ Ω0 is defined to reduce all judgmentsin the declarative worklists with declarative typing rules. This relation checks that every

J. Zhao and B. C. d. S. Oliveira

2:21

judgment entry in the worklist holds using a corresponding conventional declarative judgment.
The typing contexts of declarative judgments are recovered using an auxiliary erasure function
kΩk. The erasure function simply drops all judgment entries from the worklist, keeping
only variable and type variable declarations. Both definitions are available in the extended
version.

5.2

Soundness

Our algorithm is sound with respect to the declarative system. For any worklist Γ that
reduces successfully, there is a valid instantiation Ω that transfers all judgments to thedeclarative system.
I Theorem 12 (Soundness). If wf Γ and Γ −→∗ ·, then ∃Ω s.t. ΓΩ and Ω −→∗ ·.

The proof proceeds by induction on the derivation of Γ −→∗ ·. Most of the proof
follows Zhao et al. [39]. Algorithmic type application rules are the most interesting change,
because they have a different shape compared to the declarative rules. With the help of
declarative worklist reduction, we can reduce the additional form of type application syntax
and therefore indirectly build a relationship with the declarative system.

5.3

CompletenessAny derivation in the declarative system has an algorithmic counterpart:
I Theorem 13 (Completeness). If wf Γ and ΓΩ and Ω −→∗ ·, then Γ −→∗ ·.

We prove completeness by induction on the derivation of Ω −→∗ · with a similar techniqueto the one used by Zhao et al. [39]. New rules, including the ones involve subtype variables
and type applications, do not increase the difficulty of our proof significantly. It is worth
noting that our system forbids the > and ⊥ types to be instantiated by monotypes. If we
did not pose such restriction, then the following lemma would not hold anymore:
I Lemma 14 (Prune Transfer for Instantiation). If (Γ αb ≤ A → B)
and kΩk ` C ≤ A1 → B1 , then αb∈/ F V (A) ∪ F V (B).

(ΩC ≤ A1 → B1 )For example, allowing instantiations like αb := > would make the algorithmic judgment
α
b → α
b ≤ α
b derivable. This lemma is essential to follow the original proof to prove
completeness for the occurs-check condition in rules 14 and 15.

5.4

Decidability

Finally, we show that our algorithm is decidable:
I Theorem 15 (Decidability). Given wf Γ, it is decidable whether Γ −→∗ · or not.
Our decidability proof is based on a lexicographic group of induction measures:|Γ|e , |Γ|⇔ , |Γ|>⊥ , |Γ|∀ , |Γ|αb , |Γ|→ + |Γ|on the worklist Γ. Compared with the measures used by Zhao et al. [39], we introduce a newmeasure | · |>⊥ , which counts the total number of > and ⊥ occurrences. This is required
because judgments like αb ≤ > now do not solve α
b , which breaks the original proof technique.
This type of judgment now reduces the new measure by at least one. The rest of the proof
follows the approach closely. The extended version has detailed explanations of the measuresand proofs. Combining all three main results (soundness, completeness and decidability), we
conclude that the declarative system is decidable by means of our algorithm.

ECOOP 2022

2:22

Elementary Type Inference

I Corollary 16 (Decidability of Declarative Typing). Given wf Ω, it is decidable whetherΩ −→∗ · or not.

6

DiscussioneInferring Top and Bottom Types F<:
does not treat the > and ⊥ types as monotypes,
therefore these types cannot be implicitly instantiated by the type inference algorithm.
However, in certain programming languages, especially OOP languages with downcasts, the> type can be useful in certain cases and implicit instantiation would be convenient to have.
For example, the following Java program

var ns = List.of(1, 2, "3");should instantiate the generic variable A of the List<A> class to Object (note that Object
plays a similar role to > in Java) to type-check the program. Thus, the inferred type for ns
is List<Object>. In this program, because downcasts are possible in Java, it is plausible thatthe programmer intended to have a heterogeneous list of values, that could later be accessedby doing some type analysis for the elements and downcasting from Object to Integer orString. We consider such use cases to be a practical example where instantiation with thee
top type would be useful in languages like Java. In contrast, in F<:, we would need to
explicitly instantiate the type argument. Nonetheless, in a language without downcastse(such as F<:), the declaration of ns above would very likely be a programmer error, since
there would not be much that could be done with a value of type List<Object>. As we haveargued in Section 2.4, there is a tension between inferring types with top and bottom types
and hiding programmer errors: sometimes type errors that would be caught in many typesystems, are instead type-checked by inferring some types with top and bottom types. Ouredesign decision in F<:
is not to infer top and bottom types, which avoids hiding such errors
as well as avoiding the technical complexities that arise from inferring such types.
e
It is possible to have alternative designs for F<:
that infer top and bottom types aswell. For instance, if we would be aiming at covering common cases that arise in practicein languages like Java, such as the inference of the type of ns above, we could extend our
syntax-directed system and algorithmic system with the rules:Ψ ` [>/a]A ≤ B

B 6= >Ψ ` ∀a. A ≤ B
Γ∀a. A ≤ B −→ ΓDInst>[>/a]A ≤ B

when B 6= >The two rules above support simple forms of instantiation where the type variable isdirectly instantiated with the > type (a similar approach could be used for ⊥ types). Notethat these rules overlap with the current predicative instantiation rules, and thus introduce
nondeterminism. Implementing the algorithmic rule directly would require some backtracking.
From the theoretical point of view the rules are quite ad-hoc, since they cover only very
specific cases of instantiation with top types. A more theoretically appealing approach would
be to borrow ideas from approaches such as MLSub [6], which can infer types with top andbottom. However, this would be much more technically challenging. Another direction woulde
be to complement the global type inference approach of F<:
with some more local approachto attempt to infer top and bottom types. We will discuss this approach more next.
Local Impredicative Inference Implicit impredicative instantiation is an advanced feature
in modern type systems, and it is also supported by the local type inference approach [27].
Unlike top types, which can have some practical use cases in languages like Java, no existing
mainstream OOP languages support higher-ranked systems with first-class polymorphic

J. Zhao and B. C. d. S. Oliveira

2:23

functions/values. Thus, there is no need for impredicative instantiations in those languages
today. Nonetheless, future languages may support such feature and it is worthwhile considering impredicative type inference. Local type inference algorithms are designed to support
impredicative instantiations through information in the neighbor nodes of the syntax tree.
The recent work on Quick Look by [32] instantiates polymorphic types through a similar local
approach and falls back to a global Hindley-Milner-style unification afterwards. Currently,
our system only employs global unification and ignores any local information. We believe thata promising direction would be to follow the Quick Look approach, preserve the core globaleinference system of F<:, and try to employ a more local approach to infer impredicative
types as well as top and bottom types before introducing unification variables. The main
challenge in this direction is that Serrano et al.’s [32] approach relies on invariant subtyping
for function types. In contrast, we have to deal with contravariance for input types andcovariance for output types.

7

Related Work

This section discusses related work, focusing on the most closely related research on higherranked type inference and local type inference.
Hindley-Milner The Hindley-Milner (HM) type system [5, 19, 16] was a landmark achievement in type inference. The constraint-based presentation by Pottier and Rémy [29] for HM
and ML type inference has similarities with the worklist approach and it also keeps precise
scoping of variables. In HM the order of universally quantified variables is irrelevant andno annotations are required. In contrast, in our work, the order of universally quantified
variables matters, and annotations are necessary for polymorphic functions. Thus, we donot support Hindley-Milner style generalization. Nevertheless if we assume annotationsof polymorphic expressions, the order-relevance of universally quantified variables is notproblematic. Because of its support for visible type applications [13], GHC Haskell alreadydistinguishes between specified and generalized type quantification. Specified type quantificaetion refers to polymorphic expressions that have explicit type annotations. Like F<:, in GHC
type variables in specified quantification are order relevant to be compatible with explicitetype applications. In contrast to Hindley-Milner, F<:
supports higher-ranked polymorphism,
explicit impredicative type applications and top and bottom types.
Higher-Ranked Polymorphic Type Inference There has been much work extending HM
while preserving all of its expressive power. In particular, there are several extensions of
HM to System F, which support higher-ranked polymorphism. Since full type inference for
System F is undecidable [38], such extensions need some type annotations or restrictions toremain decidable. The work on type inference for higher-ranked polymorphism (HRP) can bedivided into two main lines: predicative and impredicative type systems. In predicative typesystems, only monotypes can be inferred. An advantage of predicative type systems is thatthe predicative polymorphic subtyping relation is decidable [20], which facilitates the designof such type systems and type inference algorithms. There are several predicative HRP
type systems [25, 8, 9, 20, 39]. The work in this paper is based on DK’s [8] declarative typesystem and the algorithmic formulation by Zhao et al. [39]. However, we support explicit
impredicative type applications and top and bottom types. Such features create various
challenges and, to address some of those challenges, we introduce a novel stable polymorphic
subtyping relation. In contrast, DK adopt the polymorphic subtyping relation by Odersky
and Läufer [20]. In essence, with stable subtyping, the order of type variables becomesrelevant in universal quantification. As a consequence, some forms of subtyping that are

ECOOP 2022

2:24

Elementary Type Inference

accepted by Odersky and Läufer’s relation are rejected in our type system. Nonetheless, withthose restrictions we retain important properties, such as checking subsumption and stabilityof type substitutions, in the presence of new features that are not supported by DK.
Impredicative System F allows instantiation with polymorphic types. Unfortunately, a
subtyping relation with impredicative implicit instantiation is undecidable [3, 35]. Work on
partial impredicative type inference algorithms [17, 18, 36, 33, 32, 14] navigate a variety ofdesign tradeoffs for a decidable algorithm. Ideas from Guarded Impredicative Polymorphism [33] and the Quick Look approach [32], are being adopted in GHC 9 for enabling
impredicative instantiation. They make use of local information in n-ary applications to infer
polymorphic instantiations with a relatively simple specification and unification algorithm.
Although not all impredicative instantiations can be handled well, these approaches are usefulin practice. In contrast to this line of work, we do not attempt to infer impredicative types.
Instead, all impredicative instantiations must be explicit. While explicit instantiation is lessconvenient, an advantage is flexibility. Approaches that only allow implicit impredicative
instantiation may reject some instantiations that would be possible with explicit instantiation.
Stability Besides the motivation of supporting a form of impredicative polymorphism,
another motivation for the changes in type inference in GHC 9 has been to simplify thealgorithms and address various issues surrounding subsumption. While we are not aware thatthe issues that we have described in Section 2 have been previously identified, there havebeen several discussions documenting other issues related to subsumption in GHC 8 [26].
Recently, motivated to understand what would be the best design for instantiation in GHC,
Bottu and Eisenberg [1] have compared four different approaches to instantiation. They
have identified stability properties as an important factor for language designers to take into
consideration when designing languages with implicit instantiation. Stability also plays animportant role in the Cochis calculus [31], where it ensures that the behavior of resolution(which is a mechanism employed by type classes [37] or Scala implicits [22]) is preserved aftereinstantiation. Stable subtyping in F<:
provides a high-level specification of polymorphic
subtyping, which essentially embeds a stability property into the subtyping relation.
Type Inference with Explicit Type Applications The work on visible type application(VTA) [13] adds a predicative form of explicit type application to HM and HRP type systems.
This approach has been adopted in GHC 8. As discussed in detail in Section 2, a property
that is not enforced in VTA is checking subsumption. We believe that checking subsumption
is an important property, as it ensures that a program can always be annotated with asupertype and it can prevent situations where simply inlinings of function definitions canmake a well-typed program ill-typed. The Quick Look approach [32] supports impredicative
visible type application. An important difference is that in Quick Look subtyping of functions
is invariant, whereas in the original VTA approach the standard subtyping rule is used. The
invariant subtyping rule prevents the counter-examples to checking subsumption that we
found in GHC 8, and described in Section 2. Our work shows a different way to prevent such
examples, by employing stable subtyping with a standard subtyping rule for functions. We
believe that there are merits in both approaches. The restrictions adopted by Quick Look do
not affect backward compatibility with the HM type system. In contrast, elementary type
inference does not aim at backwards compatibility with the HM type system. Instead, weare interested in backward compatibility with extensions of System F with subtyping (suchas F<: [2]). Quick Look would not preserve backward compatibility to such type systems,
which employ a standard subtyping rule for function types.
Local Type Inference While technically speaking we are closest to predicative HRP, we
are closer in spirit and in goals to local type inference [27, 21]. Like our work, local type

J. Zhao and B. C. d. S. Oliveira

2:25

inference does not aim to subsume the HM type system. Local type inference sacrificessome of the expressive power of type inference, in exchange for the ability to smoothly deal
with features such as top and bottom types and impredicative types. Pierce and Turnerconsidered a language similar to the language that we consider in our work (with top andbottom types, but no bounded quantification). Like our approach, both implicit and explicit
type applications are supported. Technically speaking, our approach is still a global inference
approach, and thus it is quite different from local type inference. In local type inference,
missing annotations are recovered using only information from adjacent nodes in the syntax
tree, and there are no long-distance constraints such as unification variables. We believe thatean advantage of F<:
is that it has simple and clear syntax-directed specifications, whereas the
specification of local type inference is more involved, and it is not obvious to programmersewhen instantiation works or not. Furthermore, F<:
allows the inference of lambda expressions
without any contextual type information, as long as the inferred type is a monotype.
Type Inference with Subtyping Another line of work is extensions of HM with subtyping.
Type systems in presence of subtyping encounter constraints that are not simply equalities
as in HM. Therefore constraint solvers used in HM, where unifications are based on equality,cannot be easily extended to support subtyping. Instead, constraints are usually collected as
subtyping relations and may delay resolution as the constraints accumulate. Some systems
that are based on constraint types [12, 11], i.e. types expressed together with a set of
constraints τ | {τ1 ≤ τ2 }. Unfortunately, such constraints can be quite large and hard tointerpret by programmers. Pottier [30] proposed three methods to simplify constraints,
aiming at improving the efficiency of type inference algorithms and improving the readabilityof the resulting types. Inspired by the simplification strategies of Pottier, MLsub [6] suggeststhat the data flow on the constraint graph can be reflected directly on types in a richer typesystem. Simple-sub [23] further simplifies the algorithm of MLsub and is implemented in
500 lines of code. While being equivalent to MLsub, it is a more efficient variant. In ourwork, we avoid subtyping constraints and do not infer types with top and bottom types. If
instantiations with such types are needed, then an explicit type application must be used.
On the other hand, we support higher-ranked polymorphism, and explicit type applications,which (as far as we know) are not supported by any extensions of HM with subtyping.

8

Conclusion

In this paper, we proposed elementary type inference: a partial form of type inference thatcan be used in languages with subtyping that combine implicit instantiation with explicit typeapplications. As type systems become more powerful, the inference problem becomes harder,
quickly leading to various undecidable problems. It is clear that some form of type-inferenceis needed in most languages to make their use practical. However, it is not necessarily truethat being able to infer more types is always better, especially if there is the possibility toresort to explicit instantiation. Attempting to infer more types may have the side-effect ofhiding programmer errors, as very general types can be inferred in the presence of advanced
type system features. Moreover, predicatibility of what can be inferred and what cannot isalso an important factor for users of the programming language. Elementary type inference
strikes a compromise. It chooses to infer only monotypes, which are always inferrable, andmakes it easy to understand when the instantiation succeeds or fails. For polytypes (which
include top and bottom), explicit type applications must be used, but no expressive power issacrificed. More work is needed to understand what is the right balance between inference,
predicatibility and usability of languages in the future.

ECOOP 2022

2:26

Elementary Type Inference

References
1

2
3

4
5

6

7
8

9

10
11

12

13

14

15
16
17

Gert-Jan Bottu and Richard A. Eisenberg. Seeking stability by being lazy and shallow:
Lazy and shallow instantiation is user friendly. In Proceedings of the 14th ACM SIGPLAN
International Symposium on Haskell, page 85–97, New York, NY, USA, 2021. Association for
Computing Machinery.
L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping.
Information and Computation, 109(1):4–56, 1994.
Jacek Chrząszcz. Polymorphic subtyping without distributivity. In Luboš Brim, Jozef Gruska,
and Jiří Zlatuška, editors, Mathematical Foundations of Computer Science 1998, pages 346–355,
Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
Maurizio Cimadamore. Jep 101: Generalized target-type inference, 2015. URL: http://
openjdk.java.net/jeps/101.
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedingsof the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’82, 1982.
Stephen Dolan and Alan Mycroft. Polymorphism, subtyping, and type inference in MLsub. In
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
POPL 2017, page 60–72, New York, NY, USA, 2017. Association for Computing Machinery.
doi:10.1145/3009837.3009882.
Jana Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133–165,
2014. doi:10.1017/S0956796813000270.
Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking
for higher-rank polymorphism. In Proceedings of the 18th ACM SIGPLAN International
Conference on Functional Programming, ICFP ’13, 2013.
Jana Dunfield and Neelakantan R. Krishnaswami. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL, (POPL),
January 2019. http://arxiv.org/abs/1601.05106.
Jana Dunfield and Neelakantan R. Krishnaswami. Bidirectional typing. ACM Comput. Surv.,
54(5), May 2021.
Jonathan Eifrig, Scott Smith, and Valery Trifonov. Sound polymorphic type inference forobjects. OOPSLA ’95, page 169–184, New York, NY, USA, 1995. Association for Computing
Machinery. doi:10.1145/217838.217858.
Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained
types and its application to OOP. Electronic Notes in Theoretical Computer Science, 1:132–153,
1995. MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. URL: https://www.sciencedirect.com/science/article/pii/S1571066104800082,
doi:https://doi.org/10.1016/S1571-0661(04)80008-2.
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible type application.
In Peter Thiemann, editor, Programming Languages and Systems, Berlin, Heidelberg, 2016.
Springer Berlin Heidelberg.
Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. Freezeml:
Complete and easy type inference for first-class polymorphism. In Proceedings of the 41st
ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI
2020, page 423–437. Association for Computing Machinery, 2020.
Andrew Gacek. The Abella interactive theorem prover (system description). In Proceedings of
IJCAR 2008, Lecture Notes in Artificial Intelligence, 2008.
Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of
the american mathematical society, 146:29–60, 1969.
Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of system F. In Proceedingsof the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP
’03, 2003.

J. Zhao and B. C. d. S. Oliveira

18
19
20

21

22

23

24
25
26

27
28
29
30
31
32
33

34

35
36

37

38

2:27

Daan Leijen. HMF: Simple type inference for first-class polymorphism. In Proceedings of the
13th ACM SIGPLAN International Conference on Functional Programming, ICFP ’08, 2008.
Robin Milner. A theory of type polymorphism in programming. Journal of computer andsystem sciences, 17(3):348–375, 1978.
Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Proceedingsof the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’96, 1996.
Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored local type inference. In
Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’01, page 41–53, New York, NY, USA, 2001. Association for Computing
Machinery.
Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects andimplicits. In Proceedings of the ACM International Conference on Object Oriented Programming
Systems Languages and Applications, OOPSLA ’10, page 341–360, 2010.
Lionel Parreaux. The simple essence of algebraic subtyping: Principal type inference with
subtyping made easy (functional pearl). Proc. ACM Program. Lang., 4(ICFP), August 2020.
doi:10.1145/3409006.
Simon Peyton Jones and Mark Shields. Lexically-scoped type variables. Draft, 2004. URL:
http://research.microsoft.com/en-us/um/people/simonpj/papers/scoped-tyvars/.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical
type inference for arbitrary-rank types. Journal of functional programming, 17(1):1–82, 2007.
Peyton Jones, Simon.
Simplify Subsumption.
GHC Proposals, 2020.
URL:
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/
0287-simplify-subsumption.rst.
Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang.
Syst., 22(1):1–44, January 2000.
Hubert Plociniczak. Decrypting Local Type Inference. PhD thesis, EPFL, 2016.
François Pottier and Didier Rémy. Advanced Topics in Types and Programming Languages,
chapter The Essence of ML Type Inference, pages 387–489. The MIT Press, 2005.
François Pottier. Type inference in the presence of subtyping: from theory to practice. PhD
thesis, INRIA, 1998.
Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. COCHIS:
Stable and coherent implicits. Journal of Functional Programming, 29:e3, 2019.
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. A quick
look at impredicativity. Proc. ACM Program. Lang., 4(ICFP), August 2020.
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. Guarded
impredicative polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI 2018, 2018.
Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. The firstorder theory of subtyping constraints. In Proceedings of the 29th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL ’02, page 203–216, New York,NY, USA, 2002. Association for Computing Machinery. doi:10.1145/503272.503292.
Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types is undecidable.
In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996.
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH: First-class polymorphism for Haskell. In Proceedings of the 13th ACM SIGPLAN International Conference
on Functional Programming, ICFP ’08, 2008.
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the
16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
’89, page 60–76, New York, NY, USA, 1989. Association for Computing Machinery.
Joe B Wells. Typability and type checking in system F are equivalent and undecidable. Annalsof Pure and Applied Logic, 98(1-3):111–156, 1999.

ECOOP 2022

2:28

Elementary Type Inference

39

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. A mechanical formalization ofhigher-ranked polymorphic type inference. Proc. ACM Program. Lang., 3(ICFP), July 2019.