Greedy Implicit Bounded Quantification
CHEN CUI, The University of Hong Kong, China
SHENGYI JIANG, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
Mainstream object-oriented programming languages such as Java, Scala, C#, or TypeScript have polymorphic
type systems with subtyping and bounded quantification. Bounded quantification, despite being a pervasive
and widely used feature, has attracted little research work on type-inference algorithms to support it. A
notable exception is local type inference, which is the basis of most current implementations of type inference
for mainstream languages. However, support for bounded quantification in local type inference has important
restrictions, and its non-algorithmic specification is complex.
In this paper, we present a variant of kernel 𝐹 ≤ , which is the canonical calculus with bounded quantification,with implicit polymorphism. Our variant, called 𝐹 𝑏≤ , comes with a declarative and an algorithmic formulationof the type system. The declarative type system is based on previous work on bidirectional typing forpredicative higher-rank polymorphism and a greedy approach to implicit instantiation. This allows for a clear
declarative specification where programs require few type annotations and enables implicit polymorphism
where applications omit type parameters. Just as local type inference, explicit type applications are alsoavailable in 𝐹 𝑏≤ if desired. This is useful to deal with impredicative instantiations, which would not be allowed
otherwise in 𝐹 𝑏≤ . Due to the support for impredicative instantiations, we can obtain a completeness resultwith respect to kernel 𝐹 ≤ , showing that all the well-typed kernel 𝐹 ≤ programs can type-check in 𝐹 𝑏≤ . The
corresponding algorithmic version of the type system is shown to be sound, complete, and decidable. All the
results have been mechanically formalized in the Abella theorem prover.
CCS Concepts: • Theory of computation → Type theory.
Additional Key Words and Phrases: Bounded Quantification, Mechanical Formalization, Type Inference
ACM Reference Format:
Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira. 2023. Greedy Implicit Bounded Quantification. Proc.
ACM Program. Lang. 7, OOPSLA2, Article 295 (October 2023), 29 pages. https://doi.org/10.1145/3622871

1

INTRODUCTION

Bounded quantification [Cardelli and Wegner 1985] is an extension of parametric polymorphism,
where type variables can have subtyping bounds. Mainstream object-oriented programming languages such as Java, Scala, C#, or TypeScript have polymorphic type systems with subtyping andbounded quantification. The canonical calculus for bounded quantification is 𝐹 ≤ [Cardelli et al.
1991; Cardelli and Wegner 1985; Curien and Ghelli 1992], which is an extension of System 𝐹 [Girard
1972; Reynolds 1974] with subtyping and bounded quantifiers. Like System 𝐹 , polymorphism in
𝐹 ≤ is explicit, which means that explicit type applications are necessary to instantiate the typearguments of polymorphic functions. There are two well-known variants of 𝐹 ≤ in the literature.
Authors’ addresses: Chen Cui, ccui@cs.hku.hk, The University of Hong Kong, Department of Computer Science, Hong
Kong, China; Shengyi Jiang, shengyi.jiang@outlook.com, The University of Hong Kong, Department of Computer Science,
Hong Kong, China; Bruno C. d. S. Oliveira, bruno@cs.hku.hk, The University of Hong Kong, Department of Computer
Science, Hong Kong, China.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/10-ART295
https://doi.org/10.1145/3622871
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295

295:2Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

The full variant of 𝐹 ≤ [Curien and Ghelli 1992] is the more expressive one but, unfortunately, it
is well-known that subtyping for full 𝐹 ≤ is undecidable [Pierce 1992]. The other variant is kernel 𝐹 ≤ [Cardelli and Wegner 1985], which is the most well-known and used decidable variant of 𝐹 ≤ .
Since we are interested in decidable type systems in this paper, we will focus on kernel 𝐹 ≤ .
A practical drawback of explicit polymorphism in System 𝐹 or 𝐹 ≤ is that programs require toomuch type information to type check. Therefore, to make programming languages with (bounded)parametric polymorphism practical, implicit polymorphism is needed. For System 𝐹 , there have been
many proposals for global type inference with implicit polymorphism [Dunfield and Krishnaswami
2013; Le Botlan and Rémy 2003; Leijen 2008; Odersky and Läufer 1996; Peyton Jones et al. 2007;
Serrano et al. 2018; Vytiniotis et al. 2008], typically designed as extensions of the Hindley-Milner
type system (HM) [Hindley 1969; Milner 1978]. One well-known strand of work is type systems
with predicative Higher Ranked Polymorphism (HRP). In the context of HRP, predicative meansthat instantiations can only be monotypes, which are types that are not polymorphic. This imposes a
restriction compared to System 𝐹 , where instantiations can also be polymorphic types. Nonetheless,predicative HRP has been shown to work quite well in practice for many applications since most
instantiations required in practice use monotypes.
One extension to predicative HRP is to combine implicit instantiation with explicit type applications. Eisenberg et al. [2016] proposed extensions to both HM and a predictive HRP system withpredicative explicit type applications. With explicit type applications, programmers can choose
their own instantiations by using type applications similar to System 𝐹 . A complication that arises
in combining implicit instantiation with explicit type applications is that the usual predicative
subtyping relation for HRP, due to Odersky and Läufer [1996], is incompatible with explicit typeapplications. Eisenberg et al. [2016] proposed modified subtyping relations that are compatible
with predicative explicit type applications. More recently, Zhao and Oliveira [2022] proposed toextend a predicative HRP type system, called 𝐹 ≤𝑒 , with impredicative explicit type applications. The
impredicativity of explicit type applications requires further changes to the HRP subtyping relation.
There is little work on predicative HRP type inference with bounded quantification. Zhao
and Oliveira consider a subtyping relation with top and bottom types, but 𝐹 ≤𝑒 does not havebounded quantification. Cardelli [1993] implemented a type-inference algorithm for 𝐹 ≤ , but did notformally study it. The only formal study that we are aware of supporting bounded quantification
is by Sequeira [1998], who has studied a calculus called ML∀≤ : a System 𝐹 variant with bounded
quantification. The kind of type inference supported by Sequeira’s work is quite ambitious sinceML∀ ≤ supports let generalization and the inference of principal types, just as HM. However,as Sequeira admits, his algorithm is impractical because it infers subtyping constraints without
simplification. For example, he notes that the type inferred for a quicksort algorithm has around
300 constraints. Thus, many inferred types are too large and difficult to understand for humans.
The de facto technique to deal with type inference for languages with bounded quantification
is local type inference [Odersky et al. 2001; Pierce and Turner 2000]. Unlike HM and global type
inference HRP approaches, local type inference does not employ long-distance constraints suchas unification variables and only employs a local constraint solver to infer type arguments inpolymorphic applications. This is less powerful than global approaches but, as argued by Pierce
and Turner, has the advantage of scaling up to features that are hard to deal with using global
type-inference approaches. For instance, local type inference techniques can deal with subtyping
and impredicative instantiations. Despite the technical differences, both (predicative) HRP and
local type inference target the problem of type inference for higher-rank polymorphic languages.
Moreover, local type inference complements implicit polymorphism with support for explicit typeapplications, like some predicative HRP approaches. Programmers can explicitly provide typeinstantiations when automatic (implicit) inference fails to find them.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:3

Local type inference has more modest goals regarding type inference compared to HM-styleinference and many HRP type-inference approaches. In particular, local type inference does notprovide any mechanism to infer the types of arguments for (top-level) functions and does not haveto deal with the question of finding principal types for polymorphic functions. In this way, the issues
with Sequeira’s approach are a non-issue for local type inference since all polymorphic functions
are given explicit type annotations. While local type inference has shown its value in practice, it
has some important limitations that were identified by Hosoya and Pierce [1999]; Pierce and Turner[2000]: hard-to-synthesize arguments; no best argument; and no support for interdependent bounds. In
particular, for bounded quantification Pierce and Turner did not know how to extend the algorithm
to support interdependent bounds such as ∀(𝑎 ≤ ⊤). ∀(𝑏 ≤ 𝑎). · · · where the type variable 𝑏 isbounded by another type variable 𝑎. Thus, their algorithm cannot infer such implicit instantiations.
In Section 2.2 we will discuss these limitations in more detail. Especially in the presence of bounded
quantification, local type inference requires a complex specification that makes it hard to predict
when instantiations will be successfully inferred.
In this paper, we present a variant of kernel 𝐹 ≤ , called 𝐹 ≤𝑏 , with implicit predicative polymorphism
as well as explicit impredicative type applications. The declarative type system of 𝐹 ≤𝑏 is simple
and clear. 𝐹 ≤𝑏 extends Zhao and Oliveira’s 𝐹 ≤𝑒 calculus with bounded quantification. In the designof 𝐹 ≤𝑒 , the authors follow a philosophy similar to local type inference but instead advocate for amore modest form of global type inference: i.e., no let generalization or automatic inference of(top-level) polymorphic functions is allowed. Moreover, easy (predicative) instantiations can always
be guessed automatically, but hard (impredicative) instantiations require explicit type applications.
They call this a more modest form of global type inference elementary type inference. 𝐹 ≤𝑏 adopts asimilar philosophy. Furthermore, implicit instantiations in 𝐹 ≤𝑏 support interdependent bounds anddeal with other weaknesses of local type inference, and 𝐹 ≤𝑏 can type check all kernel 𝐹 ≤ programs.
In 𝐹 ≤𝑏 , a critical question is what is a monotype? The approach for finding implicit instantiations
is greedy [Cardelli 1993]. That is, once an instantiation is found, 𝐹 ≤𝑏 commits to that instantiation,
regardless of other possible instantiations that can be found later. This greedy approach follows
previous predicative HRP approaches, which have the property that monotype subtyping implies
equality of monotypes. This ensures that if a monotype works for the first instantiation, it also
works for the subsequent instantiations. However, without care, the property easily breaks in thepresence of more expressive subtyping relations. In addition, it turns out that in 𝐹 ≤𝑏 , if all the typevariables are considered monotypes, the transitivity of subtyping is lost! Thus, while typicallymonotypes are defined in a purely syntactic way, this is not the case in 𝐹 ≤𝑏 . In particular, whether or
not type variables are considered to be monotypes depends on their bounds. With careful craftingof what constitutes a monotype, we can ensure that the greedy approach is always successful andthe transitivity of subtyping is preserved.
The algorithmic version of the type system is shown to be sound, complete, and decidable. We
introduce two new algorithmic techniques: polytype splitting and worklist substitutions. Polytype
splitting is a simple technique where functional existential (or unification) variables are only split
into two existential variables if they unify with a polytype. Polytype splitting has the property thatthe number of splits is statically determined, which helps derive a simpler measure for decidability.
Worklist substitutions simplify the presentation and proofs of the algorithmic system by dealing
with necessary reorderings that arise from widening the scope of existential variables. We also
discuss a variant with a more general notion of monotype. The declarative system of this systemstill preserves all the desirable properties, but the greedy algorithm is no longer complete. All the
results have been mechanically formalized in the Abella theorem prover.
In summary, the contributions of this paper are:Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:4

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira• A declarative bidirectional type system with predicative implicit bounded quantificationand impredicative explicit type applications. The declarative type system guesses monotypes.
Monotypes are unconventional in that they require a non-syntactic formulation due to thepresence of bounds in type variables.
• An algorithmic formulation of the type system, which is shown to be sound, complete
and decidable with respect to the declarative formulation. The algorithm employs a worklist
formulation inspired by Zhao et al. [2019]’s work.
• New algorithmic techniques: We introduce two new algorithmic techniques: polytype splitting
and worklist substitutions. Both techniques are helpful in providing a simple algorithm, and theyalso simplify some of the key proofs, in particular decidability.
• A variant of 𝐹 ≤𝑏 with monotype subtyping: In Section 5, we present a variant of 𝐹 ≤𝑏 that
deals with subtyping between monotypes during implicit instantiation. This variant has a moregeneral notion of monotypes, and infers more instantiations at the cost of completeness.
• Completeness with respect to kernel 𝐹 ≤ : 𝐹 ≤𝑏 ’s type system is shown to be complete withrespect to kernel 𝐹 ≤ . In other words, all the programs that type check in 𝐹 ≤ also type check in𝐹 ≤𝑏 .
• Mechanical formalization and implementation: All the calculi and proofs in this paper
have been mechanically formalized in the Abella theorem prover [Gacek 2008]. We also havea simple Haskell implementation, which type checks all the 𝐹 ≤𝑏 examples in this paper. The
supplementary materials, including the implementation, proofs, and the extended version of
the paper are available at: https://doi.org/10.5281/zenodo.8202095.
2

OVERVIEW

We start with a background on implicit (predicative) higher-rank polymorphic (HRP) type inference
and elementary type inference [Zhao and Oliveira 2022]. Then, we discuss the limitations oflocal type inference and its variants in dealing with languages with 𝐹 ≤ features and bounded
quantification. Finally, we illustrate the key ideas in our work that address some of these limitations
and discuss technical innovations over previous work.
2.1

Background: Predicative and Elementary Type Inference

Higher-rank polymorphism for languages à la System 𝐹 allows universal types to appear in arbitrary
positions in types, which lifts restrictions of top-level universal types in the Hindley-Milner typesystem. The 𝐹 ≤𝑒 calculus [Zhao and Oliveira 2022] additionally supports impredicative instantiation
by explicit type applications provided by the programmer, which allows it to type-check all the
programs typable in System 𝐹 . There are several important design principles of 𝐹 ≤𝑒 that are in place
to preserve properties such as subsumption and inferring all easy instantiations.
HRP subtyping and explicit type applications. The introduction of explicit type applications
invalidates some subtyping rules commonly used in predicative HRP systems, and in particular in
the well-known subtyping relation for HRP by Odersky and Läufer [1996]. The two key rules inOdersky and Läufer’s subtyping relation are:Ψ⊢𝜏Ψ ⊢ [𝜏/𝑎]𝐴 ≤ 𝐵Ψ ⊢ ∀𝑎 . 𝐴 ≤ 𝐵≤∀LΨ, 𝑏 ⊢ 𝐴 ≤ 𝐵
Ψ ⊢ 𝐴 ≤ ∀𝑏. 𝐵≤∀R

These rules enable order-irrelevant universal quantifiers. For instance, both of the following
subtyping relations hold: ∀𝑎 . ∀𝑏. 𝑎 → 𝑏 ≤ ∀𝑏. ∀𝑎. 𝑎 → 𝑏 and ∀𝑏. ∀𝑎. 𝑎 → 𝑏 ≤ ∀𝑎 . ∀𝑏. 𝑎 → 𝑏. Thus,
𝜆𝑥 . 𝑥 3 can be checked against both (∀𝑎 . ∀𝑏. 𝑎 → 𝑏) → Bool and (∀𝑏. ∀𝑎. 𝑎 → 𝑏) → Bool, by instantiating 𝑎 and 𝑏 to Int and Bool, respectively. However, explicit type applications create problems.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

Type variables 𝑎, 𝑏
Types
𝐴, 𝐵, 𝐶
Monotypes
𝜏, 𝜎Contexts
Ψ

295:5

˜ 𝑏˜
Subtype variables 𝑎,::=
1 | 𝑎 | ∀𝑎 . 𝐴 | 𝐴 → 𝐵 | 𝑎˜ | ⊤ | ⊥::=1|𝑎 |𝜏 →𝜎::=· | Ψ, 𝑎 | Ψ, 𝑥 : 𝐴 | Ψ, 𝑎˜Ψ⊢𝐴 ≤𝐵

𝐴 is a subtype of 𝐵

Ψ⊢1≤1

≤Unit

𝑎˜ ∈ Ψ
Ψ ⊢ 𝑎˜ ≤ 𝑎˜Ψ⊢𝐴 ≤⊤≤SVar˜˜Ψ, 𝑎˜ ⊢ [𝑎/𝑎]𝐴≤ [𝑎/𝑎]𝐵Ψ ⊢ ∀𝑎 . 𝐴 ≤ ∀𝑎 . 𝐵

≤⊤

Ψ⊢𝜏

Ψ⊢⊥≤𝐴
Ψ ⊢ [𝜏/𝑎]𝐴 ≤ 𝐵

𝑎∈Ψ

≤⊥

Ψ⊢𝑎 ≤𝑎𝐵 is not a ∀ type

Ψ ⊢ ∀𝑎 . 𝐴 ≤ 𝐵≤∀

Ψ ⊢ 𝐵 1 ≤ 𝐴1

Ψ ⊢ 𝐴2 ≤ 𝐵 2

Ψ ⊢ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2

≤Var

≤∀L

≤→

𝑒.
Fig. 1. Declarative Syntax and Subtyping Rules of 𝐹 ≤Consider another expression with an explicit type application: 𝜆𝑥 . (𝑥 @Int 3). This expression can
be checked against (∀𝑎 . ∀𝑏. 𝑎 → 𝑏) → Bool, but 𝜆𝑥 . (𝑥 @Int 3) ⇐ (∀𝑏. ∀𝑎. 𝑎 → 𝑏) → Bool does
not hold. The problem is that the type application instantiates the wrong universal quantifier inthe latter expression.
In addition, the possibility of impredicative explicit instantiations introduces two subtler problems.
Firstly, impredicative type applications, such as 𝑓 @(∀𝑎. 𝑎 → 𝑎), also interact with the subtyping
relation. As shown by Zhao and Oliveira, some impredicative type applications break importantstability-of-type-substitutions lemma for subtyping if no restrictions are imposed. Secondly, unused
type variables in universal quantifiers (for instance, ∀𝑎. 𝐼𝑛𝑡) are equally problematic. We refer toZhao and Oliveira’s work for more details on these issues.
Subtyping in 𝐹 ≤𝑒 . To address abovementioned problems, 𝐹 ≤𝑒 imposes three restrictions compared
to Odersky and Läufer’s subtyping relation. Subtyping for 𝐹 ≤𝑒 is shown in Figure 1. The first
restriction is to replace ≤∀R with a more restrictive rule (≤∀) that only allows comparing two
universal quantifiers. This has the consequence of making the order of the universal quantifiers
relevant, forbidding subtyping statements such as ∀𝑎 . ∀𝑏. 𝑎 → 𝑏 ≤ ∀𝑏. ∀𝑎. 𝑎 → 𝑏. The second
˜ called subtype variables, which is used by the
restriction is to introduce a new sort of variables, 𝑎,
new rule ≤∀. A subtype variable is not a monotype, contrary to the conventional type variable 𝑎,therefore it cannot be instantiated with rule ≤∀L. This restriction is key to ensuring that the stabilityof type substitutions lemma for subtyping holds. The final restriction is to add two additional
checks in well-formedness, to ensure no unused variables in universal types.
Ψ, 𝑎 ⊢ 𝐴 𝑎 ∈ FV(𝐴)Ψ ⊢ ∀𝑎 . 𝐴

Ψ, 𝑎 ⊢ 𝐴

Ψ, 𝑎 ⊢ 𝑒𝑎 ∈ FV(𝐴)Ψ ⊢ Λ𝑎 . 𝑒 : 𝐴

No inference of ⊤ and ⊥. 𝐹 ≤𝑒 does not support implicit instantiation of type ⊥ and ⊤, by treatingthem as non-monotypes. There are two reasons for this. The first reason is technical: allowing
unification with ⊤ and ⊥ introduces considerable complications in the unification procedure. Evena simple 𝛼b ≤ 𝛽b and 𝛽b ≤ 𝛼b → 1, produced by ∀𝑎 . (𝑎 → 𝑎 → 1) → 1 ≤ (∀𝑏. 𝑏 → 𝑏) → 1, can haveinfinitely many solutions by picking 𝛼b = 𝛽b = ⊥ | ⊤ → 1 | ⊤ → ⊥ | · · · and no one is the best.
The second reason is practical: inference of ⊤ and ⊥ types can often mask type errors. For
instance, 𝜆𝑓 . (𝑓 + 𝑓 1) can be typed with the type ⊥ → Int, but it is likely to be a programmer’s
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:6

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveiraerror: possibly the programmer forgot an argument in the first occurrence of 𝑓 . When programmers
are certain that they need a type involving ⊤ or ⊥, they can inform the type-inference algorithm
using type annotations or explicit type applications. Section 2.2 shows more examples that illustratesome undesirable consequences of enabling the inference of ⊤ and ⊥.
𝐹 ≤𝑒 uses the same greedy solving strategy for implicit instantiation as previous predicative
HRP systems [Dunfield and Krishnaswami 2013; Odersky and Läufer 1996]. Moreover (like other
HRP systems), 𝐹 ≤𝑒 guarantees that monotype instantiations can always be inferred. There is afolklore property for such a greedy solving of implicit instantiations on predicative HRP systems
to work: subtyping between monotypes implies equality of monotypes, or formally speaking,𝜏1 ≤ 𝜏2 → 𝜏1 = 𝜏2 . This property is helpful in establishing the completeness of an algorithmic
system with respect to its declarative specification. Suppose that there are two instantiation
judgments (or unification judgments) 𝛼b ≤ 𝜏1 and 𝛼b ≤ 𝜏2 produced by the algorithm, and thedeclarative specification could guess a 𝜏 that satisfies 𝜏 ≤ 𝜏1 and 𝜏 ≤ 𝜏2 . This means that 𝜏1 = 𝜏2 andthe order of unification makes no difference. Note also that the fact that ⊥ and ⊤ are not monotypes
in 𝐹 ≤𝑒 is also crucial for this property to hold. However, this property requires a delicate definitionof monotype after bounded quantification is introduced, and we will revisit this in Section 2.3.
2.2 A Tour of Local Type Inference
Local type inference is the most widely used technique for languages with bounded quantification.
To better compare with our work, we will examine a series of examples in Scala 2, which provides
a state-of-the-art implementation of (colored) local type inference [Plociniczak 2016]. Note that theimplementation in Scala 2 contains some improvements compared to the algorithms formalizedby calculi with local type inference [Odersky et al. 2001; Pierce and Turner 2000], enabling moreprograms to type-check. We will point out such cases explicitly in the following discussion. Despite
such improvements, well-known limitations of local type inference can still be identified in Scala 21 ,including hard-to-synthesize arguments, no best argument, and no support for interdependent bounds.
For readers unfamiliar with the Scala syntax, we explain a few important pieces of syntax first. In
Scala types, => denotes the function type constructor. For instance, Int => Int denotes a function
type whose argument and output are both integers. Variables in square brackets ([A]) are universal
variables, possibly with an extra bound ([A <: Int]) for bounded quantification. At the term level,=> is part of the syntax of lambda abstractions. For instance, x => x + 1 is the syntax for thelambda abstraction that increments its argument by one.
Hard-to-synthesize arguments. Local type inference employs two techniques to synthesize types:
local type argument synthesis and bidirectional type checking. But circumstances exist when noneof them can be applied, e.g., when a higher-order function is applied to an anonymous function.
def map[A, B](f: A => B, xs: List[A]): List[B] = ...
def mapPlus1: List[Int] = map(x => 1 + x, List(1, 2, 3))// fails to type check!

To workaround this issue, the programmer can choose to provide type annotations to the function
argument (as in mapPlus2 ) or provide all the instantiations directly (as in mapPlus3).
def mapPlus2: List[Int] = map((x: Int) => 1 + x, List(1, 2, 3))
def mapPlus3: List[Int] = map[Int, Int](x => 1 + x, List(1, 2, 3))

Another more language-dependent solution is to swap the order of two arguments in thedefinition of map as shown below. Because the type-inference algorithm in Scala proceeds left-toright, the type information in the first argument helps infer the second one.
1We do not use Scala 3 because its approach to type inference [Martres 2023] seems to be a hybrid combination of local type

inference and some other techniques, which have not been formaly studied. Thus Scala 2 type inference remains morefaithful to the original work [Odersky et al. 2001; Pierce and Turner 2000].
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:7

def map2[A, B](xs: List[A], f: A => B): List[B] = ...
def map2Plus: List[Int] = map2(List(1, 2, 3), x => 1 + x)

No support for interdependent bounds. The only formalized variant of local type inference supporting bounded quantification that we are aware of is by Pierce and Turner [2000]. However, theirwork forbids the inference of type arguments with interdependent bounds because they could not
find a complete algorithm that deals with such bounds. Scala 2 does provide some basic support forinterdependent bounds instead of forbidding them, but type checking still fails frequently. Thisreveals the difficulty of achieving a complete algorithm that can always succeed in such cases. A
simple example of failing to find instantiations of interdependent bounds in Scala is:def idFun[A, B <: A => A](x: B): A => A = x
def idInt1: Int => Int = x => x
def idInt2 = idFun(idInt1) // fails to type check!

In the above example, A and B are instantiated to ⊥ (i.e. Nothing in Scala) and Int → Int. The
instantiation does not conform to the bounded quantification 𝐵 ≤ 𝐴 → 𝐴 since Int → Int ≤ ⊥ → ⊥is not true. This incorrect instantiation found by Scala causes it to reject the program.
No best argument. When the type variable to instantiate appears invariantly in the output type,but the constraints are not enough to decide a unique instantiation, local type inference fails toprovide any instantiations. Scala still infers a type in such cases, but the type can be meaningless.
For example, the type of id is inferred as ⊥ → ⊥ in Scala. Thus, id cannot be applied further.
def snd[A]: Int => A => A = x => y => ydef id = snd(1)Preference for uncurried functions. Local type inference prefers a fully uncurried style in polymorphic applications to obtain more constraints of type variables to obtain a precise instantiation.
Sometimes, type checking will fail after making the function curried.
def fst1[A, B](x: A, y: B): A = x
def idInt2: Int => Int = fst1(x => x, 4)
def fst2[A, B]: A => B => A = x => y => x
def idInt3: Int => Int = fst2(x => x)(4) // fails to type check!

Inference of ⊤ and ⊥. Local type inference can output ⊤ and ⊥ directly as a result of constraint
solving, which can often hide possible type errors. Consider:def fst3[A](x: A, y: A): A = x
def val = fst3(1, true)

The polymorphic function fst3 has type ∀𝑎 . 𝑎 → 𝑎 → 𝑎 and 𝑎 is instantiated to ⊤ (i.e. Anyin Scala) in fst3(1, true) by Scala. It enables applying the function to two values with different
types, which usually contradicts the intention of specifying two arguments with the same type 𝐴.
Inferring ⊥ may allow some programs with other possible type errors to type check. For example:
def fPlus[A](f: A => Int, g: A => Int): A => Int = x => f(x) + g(x)def useless = fPlus((x: Int) => x + 1, (y: Boolean) => 5)

The inferred type of useless is ⊥ → Int2 . Although the type of fPlus expects two functions oftype 𝐴 → Int, the application of fPlus in useless provides two functions with different domain
types. In practice, this situation could correspond to a programmer unintentionally providing two
library functions with different types to the function (perhaps because he did not recall the correct
2 To be precise, here Scala 2 infers Int & Boolean → Int, since it supports intersection types. However, this intersection

type is morally equivalent to ⊥ in Scala: we cannot build a value of that type. In a system without intersection types, wewould expect that ⊥ → Int is inferred.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:8Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

types). Note that the instantiation of A is valid here, but it is unlikely to correspond to what the
programmer would expect.
We should remark that, especially in the presence of downcasts, there are situations whereinference of ⊤ and ⊥ can be useful. So, there is also an argument for supporting the inferenceof such types. For instance, programmers may wish to build a generic container and performing
downcast when extracting its elements. In the example below, ls is inferred to type List[Any] in
Scala without any annotations.
val ls = List(1, 2, "3")Disabling the implicit inference of ⊤ would require more boilerplate in such cases, as we would
need to provide type annotations or explicit type instantiations. However, for languages without
downcasts, inference of ⊤ and ⊥ would have much more limited benefits, while hiding many
possible type errors that could be caught by other type inference disciplines (such as HindleyMilner). Thus, for languages without downcasts, forbidding inference of ⊤ and ⊥ seems quite
reasonable. Moreover, this tension between powerful type inference and early detection of errors
has even led language designers to allow programmers to disable the inference of top types. For
instance, Scala has a flag -Xlint:infer-any to disable the implicit inference of ⊤.
Higher-rank type inference. The subtyping relation employed in local type inference is basicallythe same as 𝐹 ≤ . However, this is restrictive and prohibits type-checking many programs withhigher-rank types. The definition of g is valid in Scala 3 (but not in Scala 2, which does not support
higher-rank types), but the application g(k) is still rejected by Scala 3 because it would require ≤∀Lin the subtyping relation ( Int → Int) → Int ≤ (∀(𝑎 ≤ Int). 𝑎 → 𝑎) → Int.
def k(f: (Int => Int)) = 1
def g(f: ([A <: Int] => A => A) => Int) = 1
def f = g(k) // fails to type check!

2.3

Key Ideas in our Work

Comparing Local Type Inference with 𝐹 ≤𝑏 . Table 1 shows examples in Section 2.2 that behave
differently in 𝐹 ≤𝑏 . With global type inference, 𝐹 ≤𝑏 is capable of dealing with long-distance constraints.
Therefore, 𝐹 ≤𝑏 can type the application examples mentioned in Section 2.2 without annotations,which fail in local type inference. For instance, the map example works well in 𝐹 ≤𝑏 . In addition, since𝐹 ≤𝑏 does not infer ⊤ and ⊥, the applications involving fst3 and fPlus fail. Higher-rank polymorphic
examples, such as g, are also accepted. In 𝐹 ≤𝑏 interdependent bounds are not problematic, so theapplication of idFun works and finds the correct instantiation.
A restriction in 𝐹 ≤𝑏 is that it cannot infer instantiations using type variables with monotype
bounds. The following code type checks in Scala, while it is rejected in 𝐹 ≤𝑏 :def idBnd[A <: Int](x: A) = fst1(x, x)

In 𝐹 ≤𝑏 , an explicit type application (fst1 @𝑎 𝑥 𝑥) is needed, when the instantiation is a type variable
a with the monotype bound like Int. Section 5 shows a variant of 𝐹 ≤𝑏 that can accept this program,and in general can infer more instantiations, but loses completeness. However, note that if thebound of a is Top in fst1 𝑥 𝑥, the implicit instantiation still succeeds because in that case a isconsidered to be a monotype.
In what follows we discuss the key ideas and design decisions in 𝐹 ≤𝑏 , starting by motivating its
definition of monotypes, followed by other key technical ideas.
Non-syntactic monotypes. Previous works [Dunfield and Krishnaswami 2013; Odersky and Läufer
1996; Peyton Jones et al. 2007; Zhao and Oliveira 2022] on predicative HRP determine monotypes
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:9

Table 1. Examples used in the comparison of local type inference with 𝐹 𝑏≤

𝐹 ≤𝑏 program
let map: ∀(𝑎 ≤ ⊤). ∀(𝑏 ≤ ⊤). (𝑎 → 𝑏) → [𝑎] → [𝑏] = ...
in map (𝜆𝑥 . 𝑥 + 1) [1, 2, 3]
let idFun: ∀(𝑎 ≤ ⊤). ∀(𝑏 ≤ 𝑎 → 𝑎). 𝑏 → 𝑎 → 𝑎 = Λ𝑎 . Λ𝑏 . 𝜆𝑥 . 𝑥,
idInt: Int → Int = 𝜆𝑥 . 𝑥 in idFun idInt
let snd: ∀(𝑎 ≤ ⊤). Int → (𝑎 → 𝑎) → 𝑎 → 𝑎 = Λ𝑎 . 𝜆𝑥 . 𝜆𝑦. 𝑦in snd 1
let fst3: ∀(𝑎 ≤ ⊤). 𝑎 → 𝑎 → 𝑎 = Λ𝑎 . 𝜆𝑥 . 𝜆𝑦. 𝑥
in fst3 1 true
let fPlus: ∀(𝑎 ≤ ⊤). (𝑎 → Int) → (𝑎 → Int) → Int =Λ𝑎 . 𝜆𝑓 . 𝜆𝑔. 𝜆𝑥 . 𝑓 𝑥 + 𝑔 𝑥
in fPlus ((𝜆𝑥 . 𝑥 + 1) : Int → Int) ((𝜆𝑦. 5) : Bool → Int)
let k: (Int → Int) → Int = 𝜆𝑓 . 1,
g: ((∀(𝑎 ≤ Int). 𝑎 → 𝑎) → Int) → Int = 𝜆𝑓 . 1 in g k
let fst1: ∀(𝑎 ≤ ⊤). ∀(𝑏 ≤ ⊤). 𝑎 → 𝑏 → 𝑎 = Λ𝑎 . Λ𝑏 . 𝜆𝑥 . 𝜆𝑦. 𝑥in (Λ𝑎 . 𝜆𝑥 . fst1 𝑥 𝑥) : ∀(𝑎 ≤ Int). 𝑎 → 𝑎... in (Λ𝑎 . 𝜆𝑥 . fst1 @𝑎 𝑥 𝑥) : ∀(𝑎 ≤ Int). 𝑎 → 𝑎... in (Λ𝑎 . 𝜆𝑥 . fst1 𝑥 𝑥) : ∀(𝑎 ≤ ⊤). 𝑎 → 𝑎

Accepted or not
✓
✓
✓
✗
✗
✓
✗
✓
✓

syntactically. In particular, they treat all type variables as monotypes. Simply adopting the sameidea in a system extending the subtyping relation in Figure 1 with bounded quantification would
break subtyping transitivity. The reader can look at the subtyping relation in Figure 2, which
provides such an extension and simply assume, for the sake of our argument, that all type variables
are monotypes. A counterexample that illustrates that transitivity does not hold is described next.
Let 𝐴 = ∀(𝑎 ≤ ⊤). 𝑎, 𝐵 = 𝑏, 𝐶 = ∀(𝑐 ≤ 1). 𝑐 → 1 and Ψ = ·, 𝑏 ≤ ∀(𝑐 ≤ 1). 𝑐 → 1. Both Ψ ⊢ 𝐴 ≤ 𝐵
and Ψ ⊢ 𝐵 ≤ 𝐶 hold as shown in the following derivations. But Ψ ⊢ 𝐴 ≤ 𝐶 is invalid because thetwo bounds (⊤ and 1) are not equivalent, which is required by kernel 𝐹 ≤ when comparing bounds.
𝑏 ≤ ∀(𝑐 ≤ 1). 𝑐 → 1 ⊢ 𝑏 ≤ ⊤ 𝑏 ≤ ∀(𝑐 ≤ 1). 𝑐 → 1 ⊢ 𝑏 ≤ 𝑏by ≤ ∀L• Ψ⊢𝐴 ≤𝐵:𝑏 ≤ ∀(𝑐 ≤ 1). 𝑐 → 1 ⊢ ∀(𝑎 ≤ ⊤). 𝑎 ≤ 𝑏• Ψ ⊢ 𝐵 ≤ 𝐶 : 𝑏 ≤ ∀(𝑐 <: 1). 𝑐 → 1 ⊢ 𝑏 ≤ ∀(𝑐 <: 1). 𝑐 → 1 by ≤VarTrans• Ψ ⊢ 𝐴 ̸ ≤ 𝐶 : ∀(𝑎 ≤ ⊤). 𝑎 ̸ ≤ ∀(𝑐 <: 1). 𝑐 → 1
The reason is the interplay between rule ≤∀L and ≤VarTrans: type variables are used as monotypes for instantiation in rule ≤∀L, but they can be transformed into universal types using the≤VarTrans and used in other subtyping judgments. Similar problems happen if a type variable withbound ⊥ is used as a monotype. To avoid breaking transitivity, we need to regard type variables
with such bounds as non-monotypes to forbid instantiating such type variables with rule ≤∀L.
Can we then regard type variables with a monotype or ⊤ bound as monotypes? For transitivity,and other essential properties such as type safety and soundness of the algorithmic system, such a
definition of monotypes is fine (as shown in Section 5.1). Sadly, with greedy instantiation, monotype
bounds are still problematic for a different reason. Recall the important property to ensure thatgreedy instantiations always work: Ψ ⊢ 𝜏1 ≤ 𝜏2 implies 𝜏1 = 𝜏2 . This property is broken if we
treat type variables with a monotype bound as a monotype. The counterexample is obvious,·, 𝑎 ≤ 1 ⊢ 𝑎 ≤ 1, but 𝑎 ≠ 1. Allowing monotypes to include type variables with bounds other than ⊤results in an incomplete greedy algorithm. To solve the abovementioned issues, all type variables
with bound other than ⊤ are considered non-monotypes, i.e., they cannot be implicitly instantiatedwith rule ≤∀L. In other words, our definition of monotypes is no longer purely syntactic.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:10Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

Matching and type-application inference–judgments. An important property that our completenessresult depends on is a subsumption theorem. The proof of the subsumption theorem needs us togeneralize the lemma to all kinds of judgments first and then prove them simultaneously. With
many new cases added due to bounded quantification, the proof becomes complex. We develop two
new kinds of judgment, namely matching and type application inference, to disentangle the proof.
The matching judgment is inspired by Siek et al. [2015] to replace the application inference used by
Zhao and Oliveira [2022] and Dunfield and Krishnaswami [2013]. The type-application inference–
judgment unifies all the cases with type application and reduces the number of cases in inference
judgments. These two judgments are defined independently from checking and inference judgments,
and their metatheory can be established independently. With the help of these two judgments andtheir independently proved metatheory, our final generalized lemma for subsumption only requires
a 2-fold mutual induction with much fewer cases rather than a potential 4-fold mutual induction.
Polytype splitting and decidability. Previous works on type inference for implicit HRP [Dunfield
and Krishnaswami 2013; Zhao and Oliveira 2022; Zhao et al. 2019] adopt the following (simplified)rule when comparing an existential (unification) variable with an arrow type in subtyping: split anexistential variable into two fresh ones to solve the domain and codomain type separately.
𝛼b ≤ 𝐴 → 𝐵

reduces to

𝛼b1 → 𝛼b2 ≤ 𝐴 → 𝐵

when 𝛼b ∉ 𝐹𝑉 (𝐴 → 𝐵)

This rule poses difficulties in proving decidability because it increases the number of existential
variables by one without decreasing any other measures instantly. To solve this issue, previous
work employs concepts such as instantiation judgments 𝛼b ≤ 𝐴 and 𝐴 ≤ 𝛼b and prove (1) eachreduction procedure of these instantiation judgments is decidable because the type size decreases;(2) after an instantiation judgment is fully reduced, the overall measure will also decrease. This
intermediate decision procedure, that each instantiation judgment will reduce the overall measure
after an indefinite number of steps, creates complexity in the decidability proof.
We observe that it is unnecessary to split the existential variable when 𝐴 → 𝐵 is a monotype.
Instead, we can always solve 𝛼b using the monotype 𝐴 → 𝐵 directly, i.e., substitute every occurrenceof 𝛼b with 𝐴 → 𝐵, and split only when 𝐴 → 𝐵 is a polytype. This modification, named polytype
splitting, allows us to develop a measure | · | → to track the maximum possible number of splits ofa type statically. With the help of this new measure, the entire measure of our algorithm always
decreases after a constant number of reduction steps, so the proof of decidability is greatly simplified.
Another challenge is to combine the measure used to prove the decidability of kernel 𝐹 ≤ withthat of worklist algorithms. The weight measure for 𝐹 ≤ [Pierce 2002], is not compatible with theexistential variables in worklists: the weight could increase arbitrarily after solving an existential
with a monotype. To address this challenge, we develop a lexicographic group of four measures on
the worklist. The first three in the group are (almost) unaffected by existential-variable solving,
and the last one is a simplified version of the weight.
Worklist substitution. A complication that arises in HRP type-inference algorithms is that existential (unification) variables sometimes need to have their scope widened. However, changing
the scope of an existential variable may require changing the scope of other existential variables
recursively. To help with this process and simplify the type-inference algorithm, we employ arevised substitution procedure to deal with the variable insertion, removal, and worklist reordering
after solving an existential variable with another monotype. The rules and notations for the typeinference algorithm can be presented more concisely and clearly since the scope management forexistential variables is encapsulated within the worklist substitution. The lemmas related to thesecases in the soundness, completeness, and decidability proof can also be stated in a unified manner
to provide more intuition on the properties of our system.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

3

295:11DECLARATIVE SYSTEM

This section introduces a declarative type system for 𝐹 ≤𝑏 , which serves as a specification for thealgorithmic version that will be presented in Section 4. The type system extends Zhao and Oliveira[2022]’s 𝐹 ≤𝑒 type system by adding bounded quantification [Cardelli and Wegner 1985]. Several
important properties of the subtyping and typing relation are stated and discussed, especially thetransitivity of subtyping and the subsumption of typing, which are significantly complicated by
the addition of bounded quantification.
3.1

Syntax, Monotypes, and Well-Formedness

Type variables
𝑎, 𝑏
Types
𝐴, 𝐵, 𝐶
Expressions𝑒, 𝑡Typing contexts
Δ
Subtyping contexts Ψ

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

1 | 𝑎 | ∀(𝑎 ≤ 𝐵). 𝐴 | 𝐴 → 𝐵 | ⊤ | ⊥𝑥 | () | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2 | (𝑒 : 𝐴) | 𝑒 @𝐴 | Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴· | Δ, 𝑥 : 𝐴 | Δ, 𝑎 ≤ 𝐴
Δ | Ψ, 𝑎 ≲ 𝐴

The syntax of 𝐹 ≤𝑏 is shown above. Compared to 𝐹 ≤𝑒 , universal types ∀(𝑎 ≤ 𝐵). 𝐴 and typeabstractions Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴 now incorporate a bound 𝐵 to support bounded quantification. Typeapplication (𝑒 @𝐴) is inherited from 𝐹 ≤𝑒 . The remaining expression and type syntax is standard.
Differently from 𝐹 ≤𝑒 , there are two kinds of contexts in 𝐹 ≤𝑏 : typing context Δ and subtyping
context Ψ. This change is to enforce some expected invariants. Firstly, subtype variables should
not occur in typing and typing contexts. Secondly, only subtype variables will be added to thecontext in subtyping. Thus, a subtyping context should be a typing context prefix followed bya collection of subtype variables. Consequently, the bound of a type variable cannot depend on
a subtype variable. Despite having no major consequences for the formalization in terms of theproperties of the system, none of these invariants are enforced in 𝐹 ≤𝑒 . In contrast, they are enforced
in 𝐹 ≤𝑏 . With this new design, 𝐹 ≤𝑏 distinguishes type variables from subtype variables by the entries
in the contexts (𝑎 ≤ 𝐴 or 𝑎 ≲ 𝐴) rather than by a syntactic distinction of 𝑎 and 𝑎˜ as in 𝐹 ≤𝑒 . The
entries also keep track of the bound for (sub)type variables. For convenience, we sometimes use thenotation 𝑎 <≃ 𝐴 to represent both 𝑎 ≤ 𝐴 and 𝑎 ≲ 𝐴 entries in subtyping contexts. The key syntactic
differences to 𝐹 ≤𝑒 are marked in gray.
Monotypes. The definition of monotypes plays a central role in 𝐹 ≤𝑏 , and it requires significant
changes in comparison to previous calculi with predicative implicit instantiation [Dunfield andKrishnaswami 2013, 2019; Odersky and Läufer 1996; Peyton Jones et al. 2007]. Monotypes are nolonger defined syntactically due to the presence of bounds. Instead, we need a dedicated judgment
to decide whether a type variable is a monotype or not: only unbounded type variables (the upperbound is ⊤) are allowed. The new monotype relation needs to take the context Ψ as input to performthe bound lookup. The remaining cases of the monotype definition are standard, as shown in the
top part of Figure 2. For brevity, we will use conventional symbols 𝜏, 𝜎 to represent monotypes inΨ ⊢𝑚 𝜏 and sometimes omit Ψ when it is clear what the context is.
Well-formedness. Well-formedness (listed in the extended version of the paper) ensures the wellscopedness of binders. After adding bounded quantification, we need to check the well-formednessof the bounds in certain rules. We also inherit the free-variable checks in Zhao and Oliveira [2022]
to ensure that the polymorphic type ∀(𝑎 ≤ 𝐵). 𝐴 is indeed polymorphic. It is worth noting that if
the type variable appears in the bound of a nested universal type, it also passes the free-variablecheck, i.e., the type ∀(𝑎 ≤ ⊤). ∀(𝑏 ≤ 𝑎). 𝑏 → 𝑏 is regarded as a well-formed type in 𝐹 ≤𝑏 .
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:12Chen Cui, Shengyi Jiang, and Bruno C. d. S. OliveiraΨ ⊢𝑚 𝐴A is a monotypeΨ ⊢𝑚 1Ψ ⊢𝑚 𝐴

MUnit

Ψ ⊢𝑚 𝐵Ψ ⊢𝑚 𝐴 → 𝐵

𝑎 ≤⊤∈Ψ

M→Ψ ⊢𝑚 𝑎Ψ⊢𝐴 ≤𝐵
Ψ⊢1≤1

≤Unit

𝑎 <≃ 𝐵 ∈ ΨΨ⊢𝐴 ≤⊤

Ψ⊢𝐵 ≤𝐴Ψ⊢𝑎 ≤𝐴
Ψ⊢𝜏≤⊤≤VarTransΨ ⊢𝑚 𝜏 ≤ 𝐵

Ψ⊢⊥≤𝐴Ψ ⊢ 𝐵 1 ≤ 𝐴1

A is a subtype of B𝑎 <≃ 𝐵 ∈ Ψ≤⊥Ψ⊢𝑎 ≤𝑎Ψ ⊢ 𝐴2 ≤ 𝐵 2

Ψ ⊢ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2

Ψ ⊢ [𝜏/𝑎]𝐴 ≤ 𝐶

𝐶 is not a ∀ type

Ψ ⊢ ∀(𝑎 ≤ 𝐵). 𝐴 ≤ 𝐶
Ψ ⊢ 𝐵1 ≤ 𝐵2

Ψ ⊢ 𝐵2 ≤ 𝐵1

Ψ, 𝑎 ≲ 𝐵 2 ⊢ 𝐴1 ≤ 𝐴2

Ψ ⊢ ∀(𝑎 ≤ 𝐵 1 ). 𝐴1 ≤ ∀(𝑎 ≤ 𝐵 2 ). 𝐴2

MTVar

≤Var

≤→

≤∀L

≤∀

Fig. 2. Declarative Monotype and Subtyping

3.2

Subtyping

Figure 2 shows the rules of subtyping relation. Most rules are inherited from 𝐹 ≤𝑒 . Rules ≤⊤, ≤⊥and ≤→ are standard subtyping rules for calculi with ⊤, ⊥ and function types. Rule ≤Var is
the reflexivity rule for (sub)type variables. The remaining rules are key to supporting bounded
quantification. Rule ≤∀L states that a universal type is a subtype of another (non-universal) type 𝐶
as long as we can find a monotype 𝜏 that satisfies the bound 𝐵, such that the instantiated body isthe subtype of 𝐶. This rule differs from previous rules in the literature [Dunfield and Krishnaswami
2013; Zhao and Oliveira 2022] in that the monotype is not only required to be well-formed but
also a subtype of the bound 𝐵. By checking that Ψ ⊢ 𝜏 ≤ 𝐵, we prevent incorrect instantiations
that do not satisfy the bounds. Rule ≤∀ states that two universal types are subtypes if their bodies
are subtypes and their bounds are mutual subtypes of each other. This rule is adopted from theequivalent type variant of kernel 𝐹 ≤ [Pierce 2002; Zhou et al. 2023] to support more flexible boundcomparison. Since we include bottom types, the subtyping relation is not antisymmetric like theoriginal 𝐹 ≤ , e.g., a type variable with a bottom bound and the bottom type are subtypes of eachother. Thus, the rule used here is more adequate. The extra condition “𝐶 is not a ∀ type” in rule≤∀L ensures that rule ≤∀ always takes priority when both sides are universal types. Finally, rule
≤VarTrans allows comparing a (sub)type variable with a type 𝐴 as long as its bound 𝐵 can becompared with this type. It is a standard rule in a type system with bounded quantification. The
reflexivity and transitivity property hold for this subtyping relation:
Theorem 3.1 (Subtyping Reflexivity). Given Ψ ⊢ 𝐴, Ψ ⊢ 𝐴 ≤ 𝐴.
Theorem 3.2 (Subtyping Transitivity). Given Ψ ⊢ 𝐴, Ψ ⊢ 𝐵, and Ψ ⊢ 𝐶, if Ψ ⊢ 𝐴 ≤ 𝐵, andΨ ⊢ 𝐵 ≤ 𝐶 then Ψ ⊢ 𝐴 ≤ 𝐶.
3.3

Typing

The top part of Figure 3 shows the declarative type system with the checking and inference judgments. Most rules are standard in existing bidirectional type systems with higher-rank predicative
type inference [Dunfield and Krishnaswami 2013]. However, there are a few differences.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:13Firstly, we do not include a rule that checks against a universal type:Δ, 𝑎 ⊢ 𝑒 ⇐ 𝐴
Δ ⊢ 𝑒 ⇐ ∀𝑎 . 𝐴
Here, we omit bounded quantification for a clearer comparison with previous work. Such a rule iscommon in previous work [Dunfield and Krishnaswami 2013; Zhao and Oliveira 2022]. It allows
implicit definitions of polymorphic functions, where type variables do not need to be explicitly
bound at the term level. We drop this checking rule because it seems more appropriate for typesystems where the order of bound universal variables is irrelevant, which is not the case in 𝐹 ≤𝑏 .
Consider the following checking judgment that holds with the above rule:· ⊢ Λ𝑎 .(Λ𝑏 .(𝜆𝑥 . 𝜆𝑦. .𝑥) : ∀𝑏 .𝑎 → 𝑏 → 𝑎) : ∀𝑎 .∀𝑏 .𝑎 → 𝑏 → 𝑎 ⇐ ∀𝑏 .∀𝑎 .𝑎 → 𝑏 → 𝑎
However, ∀𝑏 .∀𝑎 .𝑎 → 𝑏 → 𝑎 is not a subtype of ∀𝑎 .∀𝑏 .𝑎 → 𝑏 → 𝑎 according to the subtyping relation since the order of the binders matters in 𝐹 ≤𝑏 . In 𝐹 ≤𝑏 , explicit type abstractions (Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴)
are the only way to define polymorphic functions, aligning better with calculi with local type
inference and with languages like Scala or Java. The consequence of removing this rule is that
lambda expressions annotated with a forall type are no longer accepted, e.g., 𝜆𝑥 . 𝑥 : ∀𝑎 . 𝑎 → 𝑎.
Programmers must explicitly convert such expressions to Λ expressions. Since explicit type abstraction is more powerful than the implicit one by allowing scoped type variables [Peyton Jones andShields 2004; Zhao et al. 2019], no expressivity is lost.
Secondly, rule ⇐→⊤ is added to check a lambda expression against ⊤. In 𝐹 ≤𝑒 , there is a rule thatallows any well-formed expression to check against the top type. So, some peculiar expressions,which seem nonsensical, e.g. () () : ⊤, can also be type checked. The 𝐹 ≤𝑒 rule is type safe, since no
information can be extracted from an expression annotated with ⊤. However, we believe it is moreintuitive to completely reject any nonsensical expressions in 𝐹 ≤𝑏 . Therefore, in rule ⇐→⊤, we use
the greatest function type in the subtyping lattice (⊥ → ⊤) to type-check the lambda expression.
This allows us to prevent nonsensical lambda expressions from being accepted when checkedagainst ⊤. Checking the remaining expressions against ⊤, including (), 𝑥, 𝑒 : 𝐴, Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴,and 𝑒 1 𝑒 2 is now handled by the subsumption rule.
Finally, there are two new judgments. The inference of application depends on the matching
judgment Δ ⊢ 𝐴 ⊲ 𝐵 → 𝐶. Note that this judgment differs from the judgment used in 𝐹 ≤𝑒 or Dunfield
and Krishnaswami [2013]. In addition, the inference of type applications is unified into a single
rule ⇒TApp and depends on the new type-application inference–judgment Δ ⊢ 𝐴 ◦ 𝐵 ⇒⇒ 𝐶. Bothof these judgments are discussed next.
Matching. The matching judgment Δ ⊢ 𝐴 ⊲ 𝐵 → 𝐶 in Figure 3 states that a type 𝐴 can be regarded
as an arrow type 𝐵 → 𝐶, and thus a term of type 𝐴 can be applied to another term of type 𝐵 andhave the result type be 𝐶. It was first proposed by Siek et al. [2015] and extended to polymorphic
types [Xie et al. 2019] by guessing instantiations until reaching an arrow type. The rules ⊲∀ and⊲→ are similar to those in Xie et al. [2019]. In rule ⊲∀, a monotype 𝜏 that satisfies the bound isguessed, and the judgment is applied to the instantiated universal type recursively.
Rule ⊲⊥ and ⊲Var are newly added to support ⊥ and bounded quantification. Since a term oftype ⊥ can be applied to any well-typed term, and the result type is still ⊥, ⊥ should match ⊤ → ⊥,the least function type in the subtyping lattice, as stated in ⊲⊥. With bounded quantification, it isalso possible for type variables to match an arrow type. This case is dealt with by rule ⊲Var, whichstates that as long as the bound of a type variable can match an arrow type, the type variable itself
can match this arrow type.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:14

Chen Cui, Shengyi Jiang, and Bruno C. d. S. OliveiraΔ⊢𝑒 ⇔𝐴𝑒 is checked against/infers 𝐴(𝑥 : 𝐴) ∈ Δ

Δ⊢𝑒 ⇒𝐴⇒Var

Δ⊢𝑥 ⇒𝐴Δ⊢𝜎 →𝜏

Δ⊢𝑒 ⇐𝐵Δ, 𝑥 : 𝜎 ⊢ 𝑒 ⇐ 𝜏

Δ ⊢ 𝜆𝑥 . 𝑒 ⇒ 𝜎 → 𝜏
Δ, 𝑥 : ⊥ ⊢ 𝑒 ⇐ ⊤Δ ⊢ 𝜆𝑥 . 𝑒 ⇐ ⊤Δ⊢𝐴 ≤𝐵⇐→⊤Δ ⊢ () ⇒ 1

Δ ⊢ 𝑒1 ⇒ 𝐴

Δ ⊢ (𝑒 : 𝐴) ⇒ 𝐴
Δ ⊢ 𝜆𝑥 . 𝑒 ⇐ 𝐴 → 𝐵

Δ, 𝑎 ≤ 𝐵 ⊢ 𝑒 ⇐ 𝐴
Δ ⊢ 𝑒2 ⇐ 𝐵

Δ ⊢ 𝑒1 𝑒2 ⇒ 𝐶
Δ ⊢ 𝐴 ◦ 𝐵 ⇒⇒ 𝐶Δ⊢𝐵

Δ ⊢𝑒 @𝐵 ⇒𝐶
Δ ⊢𝐴⊲𝐵 →𝐶⇐→𝑎 ∈ FV(𝐴)

⇒Λ

⇒App

⇒TApp

A matches an arrow type 𝐵 → 𝐶
Δ⊢⊥⊲⊤→⊥Δ⊢𝜏 ≤𝐵Δ⊢𝐵⇒Anno

Δ ⊢ Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴 ⇒ ∀(𝑎 ≤ 𝐵). 𝐴

Δ ⊢𝐴⊲𝐵 →𝐶Δ⊢𝑒 ⇒𝐴Δ⊢𝑒 ⇐𝐴Δ, 𝑥 : 𝐴 ⊢ 𝑒 ⇐ 𝐵⇒→Mono

⇒Unit

Δ⊢𝐴

⇐Sub

Δ⊢𝜏

⊲⊥

Δ ⊢𝐴 → 𝐵 ⊲𝐴 → 𝐵

Δ ⊢ [𝜏/𝑎]𝐴 ⊲ 𝐶 → 𝐷

Δ ⊢ ∀(𝑎 ≤ 𝐵). 𝐴 ⊲ 𝐶 → 𝐷

𝑎 ≤𝐶 ∈Δ⊲∀

Δ ⊢ 𝐴 ◦ 𝐵 ⇒⇒ 𝐶⊲→

Δ ⊢𝐶 ⊲𝐴 → 𝐵⊲Var

Δ ⊢𝑎 ⊲𝐴 → 𝐵

A type-applied to B infers CΔ ⊢ ⊥ ◦ 𝐴 ⇒⇒ ⊥Δ ⊢𝐶 ≤ 𝐵◦⇒⇒⊥

Δ ⊢ ∀(𝑎 ≤ 𝐵). 𝐴 ◦ 𝐶 ⇒⇒ [𝐶/𝑎]𝐴𝑎 ≤𝐶 ∈Δ

Δ ⊢ 𝐶 ◦ 𝐴 ⇒⇒ 𝐵

Δ ⊢ 𝑎 ◦ 𝐴 ⇒⇒ 𝐵◦⇒⇒∀◦⇒⇒VarFig. 3. Matching and Type-Application Inference.

The key reason to use matching instead of the application-inference judgment, Δ ⊢ 𝐴 • 𝑒 ⇒⇒ 𝐶
due to Dunfield and Krishnaswami [2013], is that the matching judgment is a pure type-level
relation and, thus, independent of the checking and inference rules. On the contrary, the application
inference judgment, which is also used in 𝐹 ≤𝑒 , is mutually defined together with the checking
and inference judgments. Unfortunately, in a system with bounded quantification, this becomesproblematic as properties such as subsumption become much more entangled with other properties,
making proofs difficult. By decoupling matching from inference and checking, we are able to prove
many properties for matching independently, greatly simplifying our proofs.
Type application inference. The type-application inference–judgment Δ ⊢ 𝐴 ◦ 𝐵 ⇒⇒ 𝐶 at thebottom of Figure 6 states that a type 𝐴 can be regarded as a universal or ⊥ type so that it can be
type-applied to type 𝐵, and the result type is 𝐶. This judgment generalizes the two rules ⊥ @ 𝐴 ⇒ ⊥and ∀𝑎 .𝐴 @ 𝐵 ⇒ [𝐵/𝑎]𝐴 used by Zhao and Oliveira [2022]. It can be easily extended to support
new cases, i.e. rule ◦⇒⇒Var, that is added due to bounded quantification. This rule allows type-levelvariables to be type-applied when their bounds can be type-applied. Type-application inference isalso a pure type-level relation independent of checking and inference rules.
Checking subsumption. An important property that holds for the typing relation is:
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:15

Theorem 3.3 (Checking Subsumption). Given ∆ ⊢ B, if ∆ ⊢ e ⇐ A and ∆ ⊢ A ≤ B, then ∆ ⊢ e ⇐ B.
3.4

Metatheory

In this section, we discuss the most interesting aspects of the metatheory of the declarative typesystem. In particular, we discuss the challenges that emerge after the introduction of bounded
quantification.
Subtyping Transitivity. The proof of subtyping transitivity proceeds by induction on the firstsubtyping relation. The tricky case is the ≤∀ rule, i.e. Ψ ⊢ ∀(𝑎 ≤ 𝐷 1 ). 𝐴 ≤ ∀(𝑎 ≤ 𝐷 2 ). 𝐵 ≤ 𝐶. When
𝐶 is also a universal type ∀(𝑎 ≤ 𝐷 3 ). 𝐶 ′ , a subtyping narrowing lemma is required to replace thebound 𝐷 2 with the equivalent type 𝐷 3 in the ≤∀ derivation Ψ, 𝑎 ≲ 𝐷 2 ⊢ 𝐴 ≤ 𝐵. This is similar to thetransitivity proof in the algorithmic version of full 𝐹 <: without a built-in transitivity rule [Pierce
2002]. When 𝐶 is not a universal type, with the rule ≤∀L, there exists 𝜏 s.t. Ψ ⊢ 𝜏 ≤ 𝐷 3 andΨ ⊢ [𝜏/𝑎]𝐵 ≤ 𝐶, and thus we need a subtyping stability lemma to substitute 𝑎 with 𝜏 in the above≤∀ derivation. Both the narrowing and stability lemmas are mutually dependent on the transitivity
lemma and must be proven simultaneously. In the proofs of both lemmas, the transitivity has to be
applied when 𝐴 is a subtype variable due to the rule ≤VarTrans.
Lemma 3.4 (Subtyping Narrowing and Stability). Given all types and contexts well-formed,(1) If Ψ1, a ≲ D, Ψ2 ⊢ A ≤ B and Ψ1 ⊢ C ≤ D, then Ψ1, a ≲ C, Ψ2 ⊢ A ≤ B.
(2) If Ψ1, a ≲ D, Ψ2 ⊢ A ≤ B and Ψ1 ⊢ C ≤ D, then Ψ1, [C/a]Ψ2 ⊢ [C/a]A ≤ [C/a]B.
Subsumption. To prove the subsumption lemma, we first prove the subsumption lemmas formatching and the type-application inference–judgment independently.
Lemma 3.5 (Matching and Type-Application Inference–Subsumption). Given all types andcontexts well-formed,(1) If ∆ ⊢ A ⊲ B → C and ∆ ⊢ A′ ≤ A, then ∃B′, C ′ s.t. Δ ⊢ 𝐴′ ⊲ 𝐵 ′ → 𝐶 ′ and ∆ ⊢ B′ → C ′ ≤ B → C.
(2) If ∆ ⊢ A ◦ B ⇒⇒ C and ∆ ⊢ A′ ≤ A, then ∃C ′ s.t. ∆ ⊢ A′ ◦ B ⇒⇒ C ′ and ∆ ⊢ C ′ ≤ C.
With the above two lemmas proved, we then adopt the proof technique used by Zhao et al. toprove the subsumption lemma, which generalizes the subsumption theorem by (1) extending theproperty to both checking and inference judgments; (2) introducing a sub-context relation Δ′ <: Δ.
The sub-context is defined on typing context only and requires the bound of corresponding typevariables in Δ and Δ′ to be the same.
Δ′ <: Δ

Sub-context
Δ <: Δ′· <: ·

Δ , 𝑎 ≤ 𝐴 <: Δ, 𝑎 ≤ 𝐴′

Δ <: Δ′Δ⊢𝐴 ≤𝐵Δ , 𝑥 : 𝐴 <: Δ, 𝑥 : 𝐵′

The most general form of the subsumption lemma is:
Lemma 3.6 (Checking and Inference Subsumption). Given ∆′ <: ∆(1) if ∆ ⊢ e ⇐ A, ∆ ⊢ A′ , and ∆ ⊢ A ≤ A′ , then ∆′ ⊢ e ⇐ A′ ;(2) if ∆ ⊢ e ⇒ A, then ∃A′ s.t. ∆ ⊢ A′ ≤ A and ∆′ ⊢ e ⇒ A′ .
It is not hard to observe that if Δ′ <: Δ, any matching and type application judgment that holds
in Δ also holds in Δ′ and vice versa since the changes in the bound of variables 𝑥 do not affect thesetwo pure type-level judgments. Thus, the subsumption proved for matching and type-application
inference can be used in the proof this generalized lemma with the premise Δ′ <: Δ.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:16

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

The form of our subsumption lemmas is simpler than that used by Dunfield and Krishnaswami[2013]; Zhao and Oliveira [2022]. The primary source of simplification comes from the use of thematching judgment, inspired by the work of [Xie et al. 2019]. The metatheory of the matching
judgment can be developed independently of checking and inference. We initially tried to use thesame approach as Zhao and Oliveira, but the proof became too intricate due to several mutual
dependencies between various lemmas.
Type Safety and Completeness to kernel 𝐹 ≤ . The type safety of our type system is derived via anelaboration to System 𝐹 by taking a coercive interpretation [Breazu-Tannen et al. 1991]: a proof ofsubtyping relation 𝑝 : 𝐴 ≤ 𝐵 is elaborated into a term 𝑒 : |𝐴| → |𝐵| (| · | indicates type translation).
The translation of types and contexts to mitigate the syntax gap is adopted from Curien and Ghelli[1992]. Specifically, ∀(𝑎 ≤ 𝐵). 𝐴 is translated to ∀𝑎 . (𝑎 → |𝐵|) → |𝐴|, and 𝑎 ≤ 𝐵 in Ψ is translated
to two entries 𝑎 and 𝑐 : |𝑎 | → |𝐵| in |Ψ|. We also prove that all kernel 𝐹 ≤ programs can type checkin our system after adjusting the annotations.
The extended version of the paper contains the detailed definition of elaboration, translation,
and annotation decoration, and discussion.
Theorem 3.7 (Type Soundness by Elaboration to System 𝐹 ). If ∆ ⊢ e ⇔ A ↩→ 𝑒 ′ then|∆| ⊢F e′ : |A|
Theorem 3.8 (Type completeness w.r.t. kernel 𝐹 ≤ ). If ∆ ⊢F ≤ e : A then ∃e′ , s.t. ⌊e⌋ = ⌊e′ ⌋, i.e.,e and e′ only differ on annotations, and ∆ ⊢ e′ ⇒ A.
4

ALGORITHMIC SYSTEM

This section introduces an algorithmic system that implements the specification of 𝐹 ≤𝑏 presented in
Section 3 using the worklist approach [Zhao et al. 2019]. This algorithmic system is proven to besound and complete with respect to the declarative system and is decidable.
4.1

Syntax, Well-Formedness, and Notation

Type variables
Algorithmic types
Judgment

Existential variables 𝛼b, 𝛽b::=
1 | 𝑎 | ∀(𝑎 ≤ 𝐵). 𝐴 | 𝐴 → 𝐵 | ⊤ | ⊥ | 𝛼b::=
𝐴 ≤ 𝐵 | 𝑒 ⇐ 𝐴 | 𝑒 ⇒𝑎 𝜔 | 𝐴 ◦ 𝐵 ⇒⇒𝑎 𝜔 | 𝐴 ⊲𝑎,𝑏 𝜔 |𝐴 → 𝐵 • 𝑒 ⇒⇒𝑎 𝜔
Algorithmic worklist Γ::=· | Γ, 𝑎 <≃ 𝐴 | Γ, 𝛼b | Γ, 𝑥 : 𝐴 | Γ ⊩ 𝜔Compared with the declarative syntax, the syntax of algorithmic expressions remains unchanged.
b
The syntax of algorithmic types is extended with a new sort of variable: existential variables (b𝛼 , 𝛽).
Existential variables are used as placeholders for monotype guesses in several rules and will be
unified with another monotype during the reduction of the worklist. Existential variables arealso regarded as monotypes. The (sub)type variables in the worklist are modified to incorporate
a bound, similar to the modifications made to the declarative context. The syntactic differences
to 𝐹 ≤𝑒 are marked with gray shades. A worklist Γ is an ordered collection of both (type) variabledeclarations (with bindings) and judgments, so it combines traditional contexts and judgment into asingle sort. The ordered nature helps with precise scope management, which simplifies mechanicalformalization. Unlike the declarative system, there is only one kind of worklist that deals with both
subtyping and typing judgments.
𝑎, 𝑏
𝐴, 𝐵, 𝐶𝜔

Judgments. There are six kinds of judgments in the algorithmic system. Four of them are inheritedfrom 𝐹 ≤𝑒 : subtyping (𝐴 ≤ 𝐵), checking (𝑒 ⇐ 𝐴), inference (𝑒 ⇒𝑎 𝜔) and type-application inference(𝐴 ◦ 𝐵 ⇒⇒𝑎 𝜔). The matching judgment (𝐴 ⊲𝑎,𝑏 𝜔) and its accompanying application inference
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:17

Substitute 𝛼b by 𝜏 in Γ

{𝜏/b
𝛼 }Γ
{𝜏/b
𝛼 }(Γ, 𝛼b)b{𝜏/b𝛼 }(Γ, 𝛽)b{𝜏/b𝛼 }(Γ1, 𝛼b, Γ2, 𝛽)<{𝜏/b𝛼 }(Γ, 𝑏 ≃ 𝐴)
{𝜏/b𝛼 }(Γ, 𝑥 : 𝐴){𝜏/b𝛼 }(Γ ⊩ 𝜔)

=1 Γ
=2 {𝜏/b𝛼 }Γ, 𝛽bb 𝛼b, Γ2 )=3 {𝜏/b𝛼 }(Γ1, 𝛽,
𝛼 ]𝐴=4 {𝜏/b𝛼 }Γ, 𝑏 <≃ [𝜏/b=5 {𝜏/b𝛼 }Γ, 𝑥 : [𝜏/b𝛼 ]𝐴
=6 {𝜏/b𝛼 }Γ ⊩ [𝜏/b𝛼 ]𝜔when 𝛽b ∉ 𝐹𝑉 (𝜏)when 𝛽b ∈ 𝐹𝑉 (𝜏)when 𝑏 ∉ 𝐹𝑉 (𝜏)Fig. 4. Worklist Substitution

judgment (𝐴 → 𝐵 • 𝑒 ⇒⇒𝑎 𝜔) are new. The syntax of subtyping and checking judgments is simple
since they either succeed or fail. The syntax of inference, type-application inference, matching,
and application-inference judgments is represented using a continuation-passing style [Zhao et al.
2019] (i.e., with a subsequent judgment 𝜔 and a subscript type variable 𝑎). These judgments returna type that will be used in subsequent judgments 𝜔, but the type may still be unknown when 𝜔is created, so the type variable 𝑎 serves as a placeholder in the subsequent judgment and will be
substituted to a concrete type once it is known.
Miscellaneous rules and notations.
• There are several well-formedness judgments. Firstly, ⊢ Γ checks that worklist Γ is well-formed.
Secondly, Γ ⊢ 𝐴 checks that the type 𝐴 is well-formed in Γ. Finally, Γ ⊢ 𝜔 checks that judgment 𝜔is well-formed in Γ. The well-formedness definitions are mostly standard, but they also enforce
the distinctions between subtyping and typing contexts discussed in Section 3. The detailed rules
can be found in the extended version of the paper.
• Worklist reduction Γ −→ Γ ′ : pops the last entry in the worklist Γ, processes according to therules, and possibly pushes multiple simplified judgments back to get a new worklist Γ ′ . Γ −→∗ Γ ′denotes multiple reduction steps, and a worklist Γ is accepted by the algorithm iff the worklist
processes all the work until nothing is left (Γ −→∗ ·).
• Worklist substitution {𝜏/b𝛼 }Γ, replaces all the references to the existential variable 𝛼b in theworklist Γ with a monotype 𝜏 and removes the existential variable 𝛼b. The existential variablesin 𝜏 need to be moved before the original position of 𝛼b to maintain the well-formedness of
the worklist. Figure 4 shows the algorithmic procedure. It traverses the worklist from head to
tail until the declaration of 𝛼b is reached. Rule 1 is the base case where the declaration of 𝛼b isreached, and 𝛼b is removed to finish the worklist substitution. Rules 2 and 3 deal with reachingexistential variables different from 𝛼b. If 𝛽b does not appear in 𝜏, we continue the substitution
on the remaining worklist. If 𝛽b appears in 𝜏, we need to move 𝛽b to the front of 𝛼b to keep thewell-formedness of 𝜏 in the remaining substitution. Rule 4 deals with reaching (sub)type variables.
Unlike existential variables, (sub)type variables cannot be moved [Dunfield and Krishnaswami
2013]. So, we need to check that the current (sub)type variable does not appear in 𝜏. Rules 5 and6 deal with variables and judgments by replacing every reference to 𝛼b with 𝜏 and continuing on
the remaining worklist.
4.2

Algorithmic Rules

All the reduction rules are defined in a single relation but for clarity of presentation, we separate
them into three parts: garbage collection, subtyping, and typing. Compared with the declarative
rules, there are two general differences in the algorithmic reduction rules:
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:18

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira• All the well-formedness checks of types in the declarative rules are dropped since we instead
require the input worklist to be well-formed, which guarantees that the algorithm only deals
with well-formed expressions and type annotations. Note that every reduction rule preserves
the well-formedness of the worklist.
• In the declarative system, if a declarative rule has multiple judgments as premises, they arechecked separately. These judgments are pushed into a single worklist and reduced jointly inthe algorithmic system. The order of pushing these judgments is deterministic for each rule,though the order may sometimes make no difference.
Garbage Collection (Rules 1-3). The scoping mechanism of the ordered worklist ensures that if
the worklist is well-formed, these variables can never be referred to by any entries that appear
before them. Thus, it is safe to remove them if they are the last entry in the worklist.
Γ, 𝑎 ≤ 𝐴 −→1 ΓΓ, 𝛼b −→2 ΓΓ, 𝑥 : 𝐴 −→3 Γ

The garbage collection of (type) variables is intuitive. The garbage collection of the existential
variable 𝛼b means that this existential variable is under-constrained and can be solved to any
monotype (and trivially, to 1).
Subtyping (Rules 4-16, Figure 5). These 13 rules can be classified into two categories, where thefirst contains rules 4-12, and the second contains rules 13-16.
Rules in the first category are similar to their declarative counterparts. Rule 6 is added since wehave a new sort of variables in the algorithmic system. The side conditions 𝐵 ≠ ⊤, 𝐵 ≠ 𝑎 and 𝐴 ≠ ⊤in rule 7 prevent the overlapping with rules 5, 8 and 14, respectively. The most significant changes
are in rule 11, where an existential variable 𝛼b is introduced instead of guessing the monotype 𝜏
instantiation in its declarative counterpart rule ≤∀L. The subtyping judgment Ψ ⊢ 𝜏 ≤ 𝐵, whichtests if the monotype satisfies the bounds, is also transformed accordingly to 𝛼b ≤ 𝐵, then added
to the worklist. In rules 10, 11, and 12, multiple new entries are pushed back to the worklist. The
side-condition 𝐶 ≠ ⊤ in rule 11 prevents the overlapping with the rule 8. Though in rule 12, 𝐵 1 and𝐵 2 are pushed back after 𝑏 ≲ 𝐵 1 , the solving scope of the existential variables in them does notchange because subtype variables are not monotypes, and cannot be used in implicit instantiation.
Another subtle difference is that the idea of “equivalent type” is enriched in rule 12 compared to rule≤∀ in that two types that contain existential variables can also be equivalent but not syntacticallyequal, e.g., 𝛼b1 → 1 and (1 → 1) → 𝛼b2 with 𝛼b1 and 𝛼b2 finally solved to 1 → 1 and 1.
The rules in the second category solve the existential variables. This set of rules is quite different
from those used in previous work [Zhao and Oliveira 2022; Zhao et al. 2019] where: (1) they only
solve existential variables to a basic monotype (i.e., another existential variable, type variable,
and unit type); (2) they always split an existential variable into two fresh existential variables
when it is compared with an arrow type. This new set of rules solves existential variables toarbitrary monotypes by employing polytype splitting: existential variables are only split into twowhen compared with a polytype (or non-monotype) arrow type. Since 𝛼b1 and 𝛼b2 are fresh, theconsequence of the worklist substitution in rules 15 and 16 is equivalent to inserting 𝛼b1, 𝛼b2 before
𝛼b, replacing every reference to 𝛼b in Γ by 𝛼b1 → 𝛼b2 , and removing 𝛼b. The occurs-check condition
in all four rules prevents the possible non-termination of the algorithm caused by judgments like𝛼b ≤ 1 → 𝛼b. In rules 13 and 14, this check also prevents overlapping with rule 6 since 𝛼b ≤ 𝛼b fails
such a check. The side condition 𝜏 ≠ 𝛽b in rule 14 ensures that rule 13 takes priority when comparing
two different existential variables. Compared with the rules of 𝐹 ≤𝑒 , the new formulation has fewer
rules and simplifies the proof of decidability, which will be discussed in detail in the Section 4.3.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:19Γ ⊩ 1 ≤ 1 −→4 ΓΓ ⊩ 𝑎 ≤ 𝑎 −→5 ΓΓ ⊩ 𝛼b ≤ 𝛼b −→6 ΓΓ ⊩ 𝑎 ≤ 𝐵 −→7 Γ ⊩ 𝐴 ≤ 𝐵 when 𝑎 <≃ 𝐴 ∈ Γ ∧ 𝐴 ≠ ⊤ ∧ 𝐵 ≠ ⊤ ∧ 𝐵 ≠ 𝑎Γ ⊩ 𝐴 ≤ ⊤ −→8 ΓΓ ⊩ ⊥ ≤ 𝐴 −→9 ΓΓ ⊩ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2 −→10 Γ ⊩ 𝐴2 ≤ 𝐵 2 ⊩ 𝐵 1 ≤ 𝐴1
Γ ⊩ ∀(𝑎 ≤ 𝐵). 𝐴 ≤ 𝐶 −→11 Γ, 𝛼b ⊩ 𝛼b ≤ 𝐵 ⊩ [b𝛼 /𝑎]𝐴 ≤ 𝐶
when 𝐶 is not a ∀ type ∧ 𝐶 ≠ ⊤Γ ⊩ ∀(𝑎 ≤ 𝐵 1 ). 𝐴1 ≤ ∀(𝑎 ≤ 𝐵 2 ). 𝐴2 −→12 Γ, 𝑎 ≲ 𝐵 1 ⊩ 𝐵 2 ≤ 𝐵 1 ⊩ 𝐵 1 ≤ 𝐵 2 ⊩ 𝐴1 ≤ 𝐴2
Γ ⊩ 𝛼b ≤ 𝜏 −→13 {𝜏/b𝛼 }Γwhen Γ ⊢𝑚 𝜏 ∧ 𝛼b ∉ 𝐹𝑉 (𝜏)Γ ⊩ 𝜏 ≤ 𝛼b −→14 {𝜏/b𝛼 }Γwhen Γ ⊢𝑚 𝜏 ∧ 𝛼b ∉ 𝐹𝑉 (𝜏) ∧ 𝜏 ≠ 𝛽b

Γ ⊩ 𝛼b ≤ 𝐴 → 𝐵 −→15 {b𝛼 1 → 𝛼b2 /b𝛼 }(Γ, 𝛼b1, 𝛼b2 ) ⊩ 𝛼b1 → 𝛼b2 ≤ 𝐴 → 𝐵

when Γ ⊬𝑚 (𝐴 → 𝐵) ∧ 𝛼b ∉ 𝐹𝑉 (𝐴 → 𝐵)Γ ⊩ 𝐴 → 𝐵 ≤ 𝛼b −→16 {b𝛼 1 → 𝛼b2 /b𝛼 }(Γ, 𝛼b1, 𝛼b2 ) ⊩ 𝐴 → 𝐵 ≤ 𝛼b1 → 𝛼b2

when Γ ⊬𝑚 (𝐴 → 𝐵) ∧ 𝛼b ∉ 𝐹𝑉 (𝐴 → 𝐵)

Fig. 5. Reduction Rules of Algorithmic Subtyping

Typing (Rules 17-36, Figure 6). Rules 17-20 deal with checking, rules 21-26 deal with inference,rules 28-32 deal with application inference and rules 34-36 deal with type inference judgments.
Rules 17-19 are the algorithmic counterparts of ⇐Sub, ⇐→ and ⇐→⊤. The premise of theinference judgment in ⇐Sub is modified to the continuation-passing style. The side condition𝑒 ≠ 𝜆𝑥 . 𝑒 ′ in 17 prevents the overlapping with the rule 19. Rule 20 is added for existential variables.
An existential variable can be used to check a lambda expression iff it can finally be resolved toan arrow type, so we split it into two fresh existential variables and process the worklist with theworklist substitution.
Rules 21-27 are the algorithmic counterparts of ⇒Var, ⇒Anno, ⇒Λ, ⇒Unit, ⇒App, ⇒TApp and⇒→Mono. Rules 21-24 are the base cases where the type is fully determined from the expression,so we replace the placeholder 𝑎 in 𝜔 with the type. Rules 22 and 23 also push 𝑒 ⇐ 𝐴 to theworklist to check the expression 𝑒 has type 𝐴. Rules 25 and 26 infer the result of (type) application
by inferring the type of 𝑒 1 and leaving the remaining work to matching and (type) applicationinference judgments. Rule 27 creates two fresh existential variables 𝛼b, 𝛽b to solve the unknown
monotype of the lambda expression by replacing the placeholder 𝑎 with 𝛼b → 𝛽b in 𝜔 and checkingb
the body against 𝛽.
Rules 28-31 are the algorithmic counterparts of ⊲→, ⊲∀, ⊲⊥, and ⊲Var. Rules 28 and 29 are twobase cases where an arrow type is known (by viewing ⊥ as ⊤ → ⊥). The placeholder 𝑎, 𝑏 in 𝜔is then replaced with the domain and codomain of this known arrow type. The modification ofrule 30 of introducing an existential variable 𝛼b is similar to that of rule 11. This 𝛼b will finally be
unified with a monotype that satisfies the bound. Rule 32 is added for existential variables. Since
this existential variable must match an arrow type, we split it into two fresh variables and process
the worklist with the worklist substitution. Rule 33 checks whether an expression of the arrow
type 𝐴 → 𝐵 solved by the matching can be applied to another expression 𝑒 by adding a checking
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:20

Chen Cui, Shengyi Jiang, and Bruno C. d. S. OliveiraΓ ⊩ 𝑒 ⇐ 𝐵 −→17 Γ ⊩ 𝑒 ⇒𝑎 𝑎 ≤ 𝐵when 𝑒 ≠ 𝜆𝑥 . 𝑒 ′Γ ⊩ 𝜆𝑥 . 𝑒 ⇐ 𝐴 → 𝐵 −→18 Γ, 𝑥 : 𝐴 ⊩ 𝑒 ⇐ 𝐵Γ ⊩ 𝜆𝑥 . 𝑒 ⇐ ⊤ −→19 Γ, 𝑥 : ⊥ ⊢ 𝑒 ⇐ ⊤Γ ⊩ 𝜆𝑥 . 𝑒 ⇐ 𝛼b −→20 {b𝛼 1 → 𝛼b2 /b𝛼 }(Γ, 𝛼b1, 𝛼b2 ⊩ 𝜆𝑥 . 𝑒 ⇐ 𝛼b)Γ ⊩ 𝑥 ⇒𝑎 𝜔 −→21 Γ ⊩ [𝐴/𝑎]𝜔

when 𝑥 : 𝐴 ∈ ΓΓ ⊩ 𝑒 : 𝐴 ⇒𝑎 𝜔 −→22 Γ ⊩ [𝐴/𝑎]𝜔 ⊩ 𝑒 ⇐ 𝐴
Γ ⊩ (Λ(𝑎 ≤ 𝐵). 𝑒 : 𝐴) ⇒𝑏 𝜔 −→23 Γ ⊩ ( [∀(𝑎 ≤ 𝐵). 𝐴/𝑏]𝜔), 𝑎 ≤ 𝐵 ⊩ 𝑒 ⇐ 𝐴
Γ ⊩ () ⇒𝑎 𝜔 −→24 Γ ⊩ [1/𝑎]𝜔
Γ ⊩ 𝑒 1 𝑒 2 ⇒𝑎 𝜔 −→25 Γ ⊩ 𝑒 1 ⇒𝑏 (𝑏 ⊲𝑐,𝑑 (𝑐 → 𝑑 • 𝑒 2 ⇒⇒𝑎 𝜔))Γ ⊩ 𝑒 @𝐴 ⇒𝑎 𝜔 −→26 Γ ⊩ 𝑒 ⇒𝑏 (𝑏 ◦ 𝐴 ⇒⇒𝑎 𝜔)bΓ ⊩ 𝜆𝑥 . 𝑒 ⇒𝑎 𝜔 −→27 Γ, 𝛼b, 𝛽b ⊩ ( [b𝛼 → 𝛽/𝑎]𝜔),𝑥 : 𝛼b ⊩ 𝑒 ⇐ 𝛽b

Γ ⊩ 𝐴 → 𝐵 ⊲𝑎,𝑏 𝜔 −→28 Γ ⊩ [𝐴/𝑎, 𝐵/𝑏]𝜔

Γ ⊩ ⊥ ⊲𝑎,𝑏 𝜔 −→29 Γ ⊩ [⊤/𝑎, ⊥/𝑏]𝜔Γ ⊩ ∀(𝑎 ≤ 𝐵). 𝐴 ⊲𝑎,𝑏 𝜔 −→30 Γ, 𝛼b ⊩ 𝛼b ≤ 𝐵 ⊩ [b𝛼 /𝑎]𝐴 ⊲𝑎,𝑏 𝜔Γ ⊩ 𝑎 ⊲𝑏,𝑐 𝜔 −→31 Γ ⊩ 𝐴 ⊲𝑏,𝑐 𝜔when 𝑎 ≤ 𝐴 ∈ ΓΓ ⊩ 𝛼b ⊲𝑏,𝑐 𝜔 −→32 {b𝛼 1 → 𝛼b2 /b𝛼 }(Γ, 𝛼b1, 𝛼b2 ⊩ 𝛼b ⊲𝑏,𝑐 𝜔)Γ ⊩ 𝐴 → 𝐵 • 𝑒 ⇒⇒𝑎 𝜔 −→33 Γ ⊩ [𝐵/𝑎]𝜔 ⊩ 𝑒 ⇐ 𝐴Γ ⊩ ∀(𝑏 ≤ 𝐵). 𝐴 ◦ 𝐶 ⇒⇒𝑎 𝜔 −→34 Γ ⊩ 𝐶 ≤ 𝐵 ⊩ [( [𝐶/𝑏]𝐴)/𝑎]𝜔Γ ⊩ ⊥ ◦ 𝐴 ⇒⇒𝑎 𝜔 −→35 Γ ⊩ [⊥/𝑎]𝜔Γ ⊩ 𝑎 ◦ 𝐵 ⇒⇒𝑎 𝜔 −→36 Γ ⊩ 𝐴 ◦ 𝐵 ⇒⇒𝑎 𝜔

when 𝑎 ≤ 𝐴 ∈ Γ

Fig. 6. Reduction Rules of Algorithmic Typing

judgment 𝑒 ⇐ 𝐴 to the worklist, and then replacing the placeholder 𝑎 in 𝜔 with the result of theapplication 𝐵. The reintroduction of the application-inference judgments in this rule is because
the matching output 𝑐 and 𝑑 in rule 25 are used in two separate judgments: 𝑐 in 𝑒 2 ⇐ 𝑐, and 𝑑 in[𝑑/𝑎]𝜔. Since the inner judgment 𝜔 can only pass the information about the placeholder 𝑎 in ourcontinuation passing syntax, an extra judgment is necessary to distribute 𝑐 and 𝑑.
Rules 34-36 are the algorithmic counterparts of ◦⇒⇒∀, ◦⇒⇒⊥, and ◦⇒⇒Var respectively. Rules
34 and 35 are two base cases where the result of the type application can be fully determined, so
we replace the placeholder 𝑎 in 𝜔 with this known result type. There is no new rule for existential
variables because a monotype can never be type-applied under the monotype definition.
4.3

Metatheory

To help formalize the correspondence between the declarative and algorithmic systems, we adopt
the approach used by Zhao et al. [2019], which adds another intermediate system defined by a setof reduction rules on the declarative worklist Ω. The syntax of Ω is the same as the algorithmic
worklist except all types in its judgments and variable declarations are declarative types. Similar to
the notations in the algorithmic worklist, ⊢ Ω, Ω ⊢ 𝐴 and Ω ⊢ 𝜔 denote the well-formedness.
There are two sets of reduction rules for this intermediate system, declarative reduction Ω −→ Ω ′and declarative worklist reduction Ω −→𝑎 Ω ′ , for soundness and completeness proofs, respectively.
Ω −→ Ω ′ is a rephrasing of the declarative judgments using the worklist style, while Ω −→𝑎 Ω ′Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:21

mimics the algorithmic reduction rules but still guesses the monotype 𝜏 instead of introducing
existential variables. The detailed rules of well-formedness and reduction of the declarative worklist
can be found in the extended version of this paper. Ω −→∗ · and Ω −→𝑎∗ · are proved equivalent:
Theorem 4.1 (Eqivalence of Declarative Reduction). ∀Ω, if ⊢ Ω, then Ω −→∗ · iff Ω −→∗a ·.
Soundness and Completeness. Soundness and completeness are built on worklist instantiation [Zhaoet al. 2019], which converts an algorithmic worklist Γ to a declarative worklist Ω by replacing all
existential variables 𝛼b in Γ with a well-formed monotype 𝜏 in Ω.
Ω is instantiated to Γ

Γ⇝Ω
Ω⇝Ω

⇝Ω

Ω ⊢𝜏

Ω, [𝜏/b𝛼 ]Γ ⇝ ΩΩ, 𝛼b, Γ ⇝ Ω⇝b𝛼Their formal statement is standard as described in the following two theorems. The quantifier inthe two lemmas is different because worklist instantiation is a non-deterministic relation.
Theorem 4.2 (Soundness). If ⊢ Γ and Γ −→∗ ·, then ∃Ω, s.t. Γ ⇝ Ω and Ω −→∗ ·.
Theorem 4.3 (Completeness). If Ω −→∗a ·, then ∀Γ, if ⊢ Γ and Γ ⇝ Ω, then Γ −→∗ ·.
The proof proceeds by induction of the derivation of Γ −→∗ · and Ω −→𝑎∗ ·, respectively.
Compared with the previous proof, there are two differences. First, existential-variable solving is all
dealt with by worklist substitution. The corresponding cases on the proof are unified, all dependingon the instantiation-consistency lemma that worklist substitution preserves instantiation. We prove
the lemma by induction on an equivalent tail-recursive version of the worklist substitution.
Lemma 4.4 (Instantiation Consistency).
(1) If {𝜏/b𝛼 }Γ ⇝ Ω, then Γ ⇝ Ω;(2) If Γ ⊩ 𝛼b ≤ 𝜏 ⇝ Ω ⊩ 𝜏 ′ ≤ 𝜏 ′ or Γ ⊩ 𝜏 ≤ 𝛼b ⇝ Ω ⊩ 𝜏 ′ ≤ 𝜏 ′ , then {𝜏/b𝛼 }Γ ⇝ Ω.
Secondly, the case ≤→ of the completeness proof relies on a property to ensure the occurrencecheck condition in rules 13-16 is satisfied, enabling the reduction on the algorithmic worklist tocontinue. The proof of this lemma in 𝐹 ≤𝑒 was based on the contradiction between the following
two properties (1) if 𝐴 → 𝐵 contains 𝛼b, 𝐴1 → 𝐵 1 contains strictly more arrows that 𝐶 and (2) ifΩ ⊩ 𝜏 ≤ 𝐴, 𝜏 has more arrows than 𝐴. Fortunately, the above two properties still hold in 𝐹 ≤𝑏 by justcounting the arrows in bounds (the number of arrows of a (sub)type variable is still zero).
Lemma 4.5 (Prune Transfer for Instantiation). If (Γ ⊩ 𝛼b ≤ A → B) ⇝ (Ω ⊩ C ≤ A1 → B1 )and Ω ⊢ C ≤ A1 → B1 , then 𝛼b ∉ FV (A) ∪ FV (B).
Confluence and Determinism. To demonstrate the greedy nature of the algorithmic approach (i.e.,
it always picks the first instantiation and does not backtrack), we show that the algorithmic system
is confluent and deterministic. These properties suggest that the algorithm can be implemented inan efficient way.
Theorem 4.6 (Algorithmic-Reduction Determinism). Given ⊢ Γ, if Γ −→ Γ1 and Γ −→ Γ2 ,then Γ1 = Γ2 (up to 𝛼-equivalance).
Corollary 4.7 (Confluence). Given ⊢ Γ, if Γ −→∗ Γ1 and Γ −→∗ Γ2 , then ∃Γ3 , Γ4 s.t. Γ1 −→∗ Γ3
and Γ2 −→∗ Γ4 and Γ3 = Γ4 (up to 𝛼-equivalance).
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:22

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

Confluence is a direct corollary of Lemma 4.6, proved by induction on the derivation of Γ −→∗ Γ1 .
Removing some side-conditions would make the algorithm non-deterministic, but could still retain
confluence. Most of the restrictions that can be dropped, while retaining confluence, are checks thata type cannot be ⊤. For instance, we do not need 𝐵 ≠ ⊤ in rule 7 or 𝐶 ≠ ⊤ in rule 11. Besides, 𝜏 ≠ 𝛽b
in rule 14 can also be dropped. The more interesting restriction that we believe can be dropped isthe monotype restriction in rules 15 and 16. All the other conditions seem necessary not to get into
any stuck state. We conjecture that the removal of restrictions preserves confluence (while losing
determinism), but we did not formally study that version of the algorithm.
Decidability. The decidability proof is based on a lexicographic group of four measures on theworklist Γ: |Γ|𝑒 , |Γ|𝜔 , 2|Γ| → + |Γ| ∀ + |Γ|𝛼b, |Γ| 𝑤 . |Γ|𝑒 , |Γ|𝜔 , |Γ| → , |Γ| ∀ , |Γ|𝛼b, |Γ| 𝑤 are the term size,
number of judgments, number of splits, number of ∀, number of existential-variable declarations,and a simplified version of weight, of the worklist, respectively. Compared with the measure used
by 𝐹 ≤𝑒 , the key innovation is |Γ| → , which statically computes the number of maximum splits of a
type 𝐴, assuming it is compared with an existential variable in subtyping. All the detailed measuredefinitions are in the extended version of this paper. The |·| → and |·| ∀ measures enjoy the desirable
property of remaining unchanged after substituting an existential variable with any monotype,
implying that both existential-variable solving and worklist instantiation will not affect them.
Using |·| → enables us to reduce the number of measures required for the decidability proof. In
𝐹 ≤𝑒 , a tuple of 6 different measures (instead of 4) is needed. It also solves the complication in thedecidability proof when comparing existential variables with an arrow type in subtyping. Zhao
et al. uses an instantiation decidability lemma to state that their measure will finally decrease after
an indefinite number of steps after they split an existential variable by observing how worklist
reduction behaves on instantiation judgments. Instead, in our rules 15 and 16, |Γ| → decreases by
one, and |Γ|𝛼b increases by one after a two-step reduction, so the whole measure decreases.
The most interesting case in our decidability proof is the rule 12, where the rebounding happensΓ to |𝐴 | Γ,𝑎 ≲𝐵 1 . To proceed with the proof,
for the 𝑎 in 𝐴2 during the reduction from |∀(𝑎 ≤ 𝐵 2 ). 𝐴2 | →2 →we need to first find some connections between the measures before and after the rebounding
based on the condition that 𝐵 1 and 𝐵 2 are equivalent.
Γ , we can prove that if two declarative types 𝐴 and 𝐵 are
According to the definition of |·| →ΩΩΩequivalent, then |𝐴| → = |𝐵| → and |𝐴| Ω∀ = |𝐵| ∀ both hold.
Lemma 4.8 (| · | → and | · | ∀ Eqality of Eqivalent Declarative Type).
ΩΩΩGiven ⊢ Ω ⊩ A ≤ B ⊩ B ≤ A, if Ω ⊩ A ≤ B ⊩ B ≤ A −→∗ ·, then |A| Ω→ = |B| → and |A| ∀ = |B| ∀ .
Using soundness, completeness, and the property that |·| → and |·| ∀ remains unchanged underworklist instantiation, we can transfer this property to the algorithmic system.
Lemma 4.9 (| · | → and | · | ∀ Eqality of Eqivalent Algorithmic Type).
Given ⊢ Γ ⊩ A ≤ B ⊩ B ≤ A, if Γ ⊩ A ≤ B ⊩ B ≤ A −→∗ ·, then |A| Γ→ = |B| Γ→ and |A| Γ∀ = |B| Γ∀ .
Then, we apply the induction hypothesis on Γ1 : Γ, 𝑎 ≲ 𝐵 1 ⊩ 𝐵 2 ≤ 𝐵 1 ⊩ 𝐵 1 ≤ 𝐵 2 to get that Γ1
reduces or not. If Γ1 does not reduce, based on the algorithmic-reduction weakening–lemma (++is the worklist concatenation), Γ1 ⊩ 𝐴1 ≤ 𝐴2 does not reduce either. The algorithmic-reduction
weakening–lemma is also proved by transferring the declarative-reduction weakening–lemmausing soundness and completeness.
Lemma 4.10 (Algorithmic-Reduction Weakening). Given ⊢ Γ1 ++ Γ2 , if Γ1 ++ Γ2 −→∗ ·, then
Γ1 −→∗ ·Otherwise, if Γ1 reduces, we can now utilize the equality property of | · | → and | · | ∀ to know
these two measures of the body 𝐴2 are not affected by the rebounding on equivalent types and theProc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:23overall measure decreases. For the remaining cases, the measures are also guaranteed to decrease
after a constant number of steps, so the decidability proof of our system can be finalized in astraightforward manner. We can now establish the decidability theorem for both algorithmic anddeclarative systems.
Theorem 4.11 (Algorithmic Decidability). Given ⊢ Γ, it is decidable whether Γ −→∗ · or not.
Corollary 4.12 (Declarative Decidability). Given ⊢ Ω, it is decidable whether Ω −→∗ · or not.
One remark is that the dependence of the decidability proof on soundness and completenesslimits the applicability of the proof technique to other variants or extensions of the system wherecompleteness is lost. We discuss one such variant in Section 5. The dependence on the measureequality of algorithmic types can be possibly removed by modifying the algorithm to avoid rebounding in the first place. However, such a change to the algorithm seems non-trivial. Anotherchoice is to prove the equality properties directly on the algorithmic system. The dependence on
the algorithmic-reduction weakening is difficult to remove and proving the lemma directly seems
to require a simultaneous proof with the decidability itself. Abella’s lack of handy mathematicalreasoning already resulted in a complicated decidability proof, so we did not attempt a direct
proof for either of the properties. Exploring solutions to simplifying the proof and removing thedependence on soundness and completeness is left for future work.
5

EXPLORING THE DESIGN SPACEIn this section, we revisit some design decisions of 𝐹 ≤𝑏 and present a sound variant of 𝐹 ≤𝑏 that
supports subtyping between monotypes, at the cost of completeness.
5.1

𝐹 ≤𝑏 with Monotype Subtyping

The inference algorithm of 𝐹 ≤𝑏 , as presented in the earlier sections of the paper, relies on theequality of monotypes. Consequently, implicit instantiation cannot employ subtyping between
monotypes, which can be limiting, since subtyping between monotypes is pervasive in objectoriented languages. Equality of monotypes is basically imposed by the desire to obtain a complete
type-inference algorithm, and the choice of greedy instantiation. Gladly, it is possible to generalize
our definition of monotypes to allow for monotype subtyping, while still having a sound type
inference algorithm.
More inference without completeness. We can broaden our definition of monotypes to get more
type inference. We consider type variables bounded by monotypes to be themselves monotypes in
our new variant of 𝐹 ≤𝑏 . This is achieved by adding the following rule to the definition of monotypes
in Figure 2:𝑎 ≤𝐴∈ΨΨ ⊢𝑚 𝐴Ψ ⊢𝑚 𝑎MTVarRec

With this rule, we can accept more programs where implicit instantiation can use type variables
with (monotype) bounds. This rule also makes the definition of monotypes even less syntactic as
now we need to recursively analyze the bounds of type variables to determine whether a typevariable is a monotype or not. In this design, we still obtain a sound algorithm with respect tothe declarative specification, but completeness is lost. The algorithmic system behaves similarly
to the implementation by Cardelli [1993], where the success or failure of type inference becomesless predictable. An example that illustrates the loss of completeness is the subtyping judgment·, 𝑏 ≤ 1 ⊩ ∀(𝑎 ≤ 1). 𝑎 → 𝑎 → 𝑎 ≤ 1 → 𝑏 → 𝑏, which is accepted by the new declarative system by
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:24

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

instantiating 𝑎 with 𝑏 (as b is regarded as a monotype in the new definition). However, it is rejectedby algorithmic reduction because the algorithm will solve 𝛼b to 1 after a two-step reduction.
·, 𝑏 ≤ 1 ⊩ ∀(𝑎 ≤ 1). 𝑎 → 𝑎 → 𝑎 ≤ 1 → 𝑏 → 𝑏 −→∗ ·, 𝑏 ≤ 1, 𝛼b ⊩ 𝛼b → 𝛼b ≤ 𝑏 → 𝑏 ⊩ 1 ≤ 𝛼b
Nominal subtyping. The previous example hints for how our algorithm can be extended to deal
with nominal subtyping, which is common in OOP languages. In mainstream OOP languages, classhierarchies can be defined, introducing subtyping relations between classes. For instance we can
add Circle and Shape classes, where Circle <: Shape. Here Circle and Shape would be twomonotypes, and it would be desirable to account for the subtyping relation between those types toenable implicit instantiation.
We can emulate what would happen after extending the calculus with nominal subtyping via
bounded quantification. With the new MTVarRec rule, we can model examples involving a Circle
and Shape type with a subtyping relation between them. For instance, consider the following two
subtyping statements:(1) ·, Shape ≤ ⊤, Circle ≤ Shape ⊩ ∀(𝑎 ≤ Shape). 𝑎 → 𝑎 → 𝑎 ≤ Shape → Circle → Shape(2) ·, Shape ≤ ⊤, Circle ≤ Shape ⊩ ∀(𝑎 ≤ Shape). 𝑎 → 𝑎 → 𝑎 ≤ Circle → Shape → ShapeBy viewing Shape and Circle just as regular (bounded) type variables, the first statement succeeds
as greedy instantiation picks Shape, leading to Shape → Shape → Shape ≤ Shape → Circle →Shape, which is valid. In contrast, the second statement fails as greedy instantiation results inCircle → Circle → Circle ≤ Circle → Shape → Shape, which is invalid. This behavior
closely parallels the behavior of instantiation in Scala 2 concerning curried functions:trait Shape
trait Circle extends Shapedef poly2[A] : A => A => A = x => y => x
def ex1 = poly2 (new Shape {}) (new Circle{})def ex2 = poly2 (new Circle{}) (new Shape{})// Accepted// Fails: instantiation picks Circle

In Scala 2, ex1 is accepted, while ex2 fails, since Scala (greedily) picks Circle for the instantiationof A. This example illustrates the left-to-right bias of Scala 2 type inference. Scala 3 seems to employ
a hybrid algorithm that combines local type inference with other techniques and can accept ex2.
Unfortunately, this algorithm is undocumented, and it is hard to make a precise comparison against
it. The behavior in Scala 2 should be consistent with local type inference and algorithms employedin other OOP languages. Of course, for uncurried functions, Scala 2 employs local type inferencetechniques, which collect subtyping constraints for all the arguments. Thus, both of the examples
with uncurried functions below succeed:
def poly[A](x : A, y : A) : A = x
def ex3 = poly(new Shape {}, new Circle{})def ex4 = poly(new Circle{}, new Shape {})// Accepted// Accepted

The primary limitation of our greedy algorithm, compared to the algorithms employed in Scala2, is the absence of specialized support for uncurried functions. This limitation is still important,given that mainstream OOP languages use uncurried functions by default. However, it is worth
mentioning that many implicit instantiations should still work correctly with our algorithm, evenwith uncurried functions.
Metatheory results and practicality. The algorithmic rules of this variant are the same, exceptthat the side condition 𝐴 ≠ ⊤ in rule 7 is changed to (Γ ⊬𝑚 𝑎) ∨ (𝐵 is not a existential variable)
for determinism. We have formalized this variant and proved all the same results that we havepresented for 𝐹 ≤𝑏 , except for completeness and decidability. Completeness does not hold, as ourearlier example shows. We conjecture that the algorithm will terminate, but since our current proof
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:25of decidability relies on the completeness, we cannot adapt it to obtain a proof of termination
for the algorithm. Despite being incomplete, we believe that this variant of 𝐹 ≤𝑏 would work wellin practice. Cardelli [1993] has observed that his greedy algorithm works well in practice, andother researchers [Mercer et al. 2022; Pierce and Turner 2000] corroborated Cardelli’s opinion
on the greedy approach. In fact, Scala’s type-inference algorithm is itself (partly) greedy, and the“left-to-right” bias of Scala in doing type inference and instantiation is well-known. Seasoned Scala
programmers are aware of the left-to-right bias of the algorithm and exploit it in the design of
Scala programs3 . Thus, we think that this variant of 𝐹 ≤𝑏 could work well, without causing much
confusion to programmers, despite its bias in the instantiation order.
5.2

Other Possible Extensions

Complete type inference with monotype subtyping. One alternative way to obtain more type
inference while preserving completeness would be to use a non-greedy algorithm instead. The
greediness of our algorithm shows up in rules such as:Γ ⊩ 𝛼b ≤ 𝜏 −→13 {𝜏/b𝛼 }Γwhen 𝛼b ∉ 𝐹𝑉 (𝜏)Here, once an existential variable is found to be a subtype of a monotype 𝜏, we immediately solve itto that monotype by substituting 𝛼b by 𝜏 in the remaining worklist. A non-greedy algorithm cannot
employ substitution directly and should, instead, collect subtyping constraints. For instance, insteadof an entry Γ, 𝛼b in the worklist, we could have, Γ, 𝐴 ≤ 𝛼b ≤ 𝐵, where 𝐴 and 𝐵 are lower and upperbounds, respectively, of 𝛼b. In a rule such as the above, instead of substituting 𝛼b by 𝜏, we would need
to update the upper bound of 𝛼b in the worklist. This change in the algorithm would be non-trivial
and require many modifications, as well as changes in the metatheory. With this change, we would
be able to delay instantiation until all the constraints have been collected. In turn, this would avoid
the bias of the (incomplete) greedy algorithm in Section 5.1. We are interested in exploring thisidea in the future, but have not developed an algorithm and metatheory yet.
Let polymorphism. Another way to get more inference with the current design of 𝐹 ≤𝑏 is to add
let polymorphism. We believe that 𝐹 ≤𝑏 has interesting properties that would make this easier thanprevious designs attempting to add HM-style type inference in languages with subtyping. Ourdefinition of monotypes in Figure 2 forbids all bounded type variables (i.e., the bound can only be ⊤).
While this is quite conservative for some programs with subtyping, it does have some advantages.
If generalization is applied to a monotype containing existential type variables, then all thoseexistential type variables would have to be unbounded if generalized. This would mean that no
simplification of polymorphic constraints would be needed, since there could be no bounds forgeneralized type variables.
A problem in adapting this idea to 𝐹 ≤𝑏 is that, in the current design, the order of type variables inuniversal quantification is relevant. But, for let generalization, we should have order-irrelevant
universal quantification. Fortunately, Eisenberg et al. [2016] has studied a related problem andproposed a solution that enables both order-relevant quantifiers (which can use explicit typeapplications), as well as order-irrelevant quantifiers, which enable HM-style let polymorphism (butcannot use explicit type applications). Eisenberg et al.’s approach is currently implemented in the
GHC Haskell compiler. We believe that a similar design could be adopted for 𝐹 ≤𝑏 .
6

RELATED WORK

Local type inference. Local type inference has been shown to work in the presence of bounded
quantification by Pierce and Turner [2000], albeit with some limitations as discussed in Section 2.
3 See, for example: https://discuss.daml.com/t/scala-inference-rules-of-thumb/2242.

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:26

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

Despite its success and impact, local type inference has only been studied formally in restrictedsettings, which are basically variants of System 𝐹 and 𝐹 ≤ . Many of the extensions of local type
inference used in practical implementations have not been formally studied. Colored local type
inference [Odersky et al. 2001] enables the propagation of partial type information by coloring
inherited and synthesized types according to their directions of propagation in the syntax tree. The
algorithm was also adopted by Plociniczak [2016] to analyze the type errors and it is the basis of
the type-inference algorithm in Scala 2. Section 2 gives an extensive overview of (colored) local
type inference, and compares it to 𝐹 ≤𝑏 .
The treatment of curried applications is limited in local type inference, possibly hindering
its usability for (functional) languages where curried applications are common. Spine-local type
inference [Jenkins and Stump 2018] takes an approach that utilizes the type information from theapplication spine to address this limitation, improving type inference for curried applications. An
example that illustrates this limitation of local type inference, due to Jenkins and Stump, is:pair : ∀𝑎. ∀𝑏. 𝑎 → 𝑏 → (𝑎 × 𝑏) ⊩ pair (𝜆𝑥 .𝑥) 0 : (Int → Int) × Int ⇒ (Int → Int) × Int
Even if full types (Int → Int) × Int are provided in a type annotation, the above program fails to
type-check with classic local type inference because the type of the first argument 𝜆𝑥 .𝑥 cannot be
inferred. Jenkins and Stump propose a form of contextual type-argument inference, which allows
the propagation of constraints in curried-function applications, accepting the above example. 𝐹 ≤𝑏treats curried and uncurried applications uniformly with existential variables, naturally solvingb which later will be instantiated tothe problem. In the above example, 𝐹 ≤𝑏 will generate 𝛼b and 𝛽,
Int → Int and Int during constraint solving. In addition, in 𝐹 ≤𝑏 , even the expression without
the annotation (pair (𝜆𝑥 .𝑥) 0) can type-check due to 𝐹 ≤𝑏 ’s global approach to type-inference.
In contrast, without type annotations, pair (𝜆𝑥 .𝑥) 0 would be rejected using (spine) local type
inference approaches. However, since 𝐹 ≤𝑏 only solves existential variables to monotypes, spine-local
type inference accepts some examples that are rejected in 𝐹 ≤𝑏 :pair : ∀𝑎. ∀𝑏. 𝑎 → 𝑏 → (𝑎 × 𝑏) ⊩ pair (𝜆𝑥 .𝑥) 0 : (∀𝑎. 𝑎 → 𝑎) × Int ⇒ (∀𝑎. 𝑎 → 𝑎) × Int𝐹 ≤𝑏 requires explicit instantiation for the above example since the type that should be inferred
is a polytype, ∀𝑎. 𝑎 → 𝑎. Mercer et al. [2022] proposed a local type-inference algorithm for an
impredicative polarized call-by-push-value variant of System 𝐹 . The proposed algorithm is formally
proved to be decidable. Quick Look [Serrano et al. 2020], adopted in GHC 9, provides impredicative
inference, but subtyping of function types is treated invariantly.
Unlike our work, these recent developments adopting ideas of local type inference focus on
traditional System 𝐹 , and do not consider bounded quantification or top and bottom types.
Global type inference with bounded quantification. Global type inference employs long-distanceconstraints via unification variables. Cardelli [1993]’s 𝐹 ≤ implementation provides a heuristic
global type-inference algorithm that is not formally studied. It introduces unification variables
to support long-distance constraints. Impredicative instantiation is implemented by unifying theunification variable with the first type constraint it encounters. In other words, Cardelli adopts agreedy approach, like our work. Type variables are directly instantiated to their bounds. However,
the algorithm is not complete in the sense that the success of its greedy solving scheme depends
on the order of candidate instantiations. On the other hand, 𝐹 ≤𝑏 is guaranteed to find the correct
solution meeting our declarative specification, yielding a more predictable behavior. 𝐹 ≤𝑏 achieves
this by distinguishing monotypes, which can always be guessed, from more general polytypes that
require explicit type applications.
Sequeira [1998] studied a predicative variant of System 𝐹 with bounded quantification, named
𝑀𝐿 ∀ ≤ . ML∀ ≤ is not an extension of 𝐹 ≤ and employs some different rules. In particular, there
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:27are at least two important restrictions. Firstly, ML∀ ≤ is predicative and does not support explicit
type applications. Thus, it cannot encode impredicative instantiations of 𝐹 ≤ . Secondly, the bounds
for type variables are restricted to monotypes, whereas 𝐹 ≤ supports unrestricted bounds. 𝑀𝐿 ∀≤is more ambitious than our work in the sense that it aims at complete Hindley-Milner styleinference, whereas we do not support let generalization or inference of principal types. Anotherimportant issue, which was left unsolved in 𝑀𝐿 ∀ ≤ , is that it does not address the issue of simplifying
constraints. This results in an impractical system where the inferred types can be too hard forhumans to understand due to the number of constraints on types.
Type inference with subtyping and MLSub. The conventional approach to tackle type inferencein HM extended with subtyping is collecting the constraint set and simplifying it using finite
automata [Eifrig et al. 1995a,b; Pottier 1998]. 𝑀𝐿 𝐹 [Rémy and Yakobowski 2008] extends the syntax
of System 𝐹 with flexible quantification ∀(𝑎 ≥ 𝐵). 𝐴 and rigid quantification ∀(𝑎 = 𝐵). 𝐴 to help
track the information for possible instantiations, requiring annotations on variables with divergent
impredicative instantiations only. Similarly to Quick Look, HMF [Leijen 2008] also restricts thesubtyping of the function type to be invariant. MLsub [Dolan and Mycroft 2017; Parreaux 2020] has
the more ambitious goal to have complete inference of principal types with (first-order, or rank-1)
polymorphic functions. To obtain the principality of inference and subsumption in the presenceof subtyping, MLsub builds an initial distributive lattice over type with a specific group of type
constructors: equi-recursive, union, and intersection types. MLstruct [Parreaux and Chau 2022]
extends MLsub by supporting first-class union and intersection types with a new boolean algebra
over types. 𝐹 ≤𝑏 , has more modest goals in terms of type inference. Full inference for System 𝐹 and𝐹 ≤ without type annotations, is undecidable, so the techniques of MLsub and its variants cannot be
used directly. More generally MLsub/struct address first-order polymorphism only, whereas 𝐹 ≤𝑏deals with higher-order polymorphism, and also supports impredicative explicit type applications.
Nevertheless, we expect that several of the techniques developed in MLSub/struct will prove to be
useful in the future to improve partial type inference methods.
7

CONCLUSION

Type inference is vital in polymorphic programming languages to alleviate the burden of writing
type annotations everywhere. However, it remains controversial how to balance the expressivenessof the language and the ability to obtain a practical and effective type inference algorithm. In thispaper, we propose 𝐹 ≤𝑏 , which extends elementary type inference and 𝐹 ≤𝑒 to bounded quantification,and inherits 𝐹 ≤𝑒 ’s modest approach to global type inference. With a careful design of what should be
regarded as monotypes, we obtain a predictable and easy-to-implement algorithm that is sound andcomplete with respect to the declarative system. Meanwhile, instantiations involving polytypes arestill available using explicit type applications. Thus, 𝐹 ≤𝑏 can express all kernel 𝐹 ≤ programs. We also
study a variant of 𝐹 ≤𝑏 that can infer types for more programs at the cost of completeness. This variant
supports monotype subtyping, and has a left-to-right bias with respect to instantiation, which issimilar to the bias that exists in languages like Scala. Thus we believe that, despite incompleteness,this variant can be used in practical type-inference algorithms.
ACKNOWLEDGMENTS
We are grateful to the anonymous reviewers for their valuable comments, to Yaoda Zhou for his
helpful feedback on the draft, and especially to Jinxu Zhao for his help in the earlier designs of 𝐹 ≤𝑏 .
The research is supported by the Practical Type Inference with Bounded Quantification and Unionand Intersection Types collaboration project (TC20230508031) between Huawei and The Universityof Hong Kong and project number 17209821 of Hong Kong Research Grants Council.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

295:28

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira

REFERENCES
Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991. Inheritance as implicit coercion. Information
and Computation 93, 1 (1991), 172–221. https://doi.org/10.1016/0890-5401(91)90055-7 Selections from 1989 IEEE
Symposium on Logic in Computer Science.
Luca Cardelli. 1993. An Implementation of 𝐹 <: . Technical Report. SRC Research Reports, Digital Equipment Corporation.
Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An Extension of System F with Subtyping. In
Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS ’91). Springer-Verlag, Berlin,
Heidelberg, 750–770.
Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv.
17, 4 (dec 1985), 471–523. https://doi.org/10.1145/6041.6042
Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of subsumption, minimum typing and type-checking in F≤.
Mathematical Structures in Computer Science 2, 1 (1992), 55–91. https://doi.org/10.1017/S0960129500001134
Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In Proceedings of the44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL 2017). Association for
Computing Machinery, New York, NY, USA, 60–72. https://doi.org/10.1145/3009837.3009882
Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-rank
Polymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13).
Jana Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and Complete Bidirectional Typechecking for Higher-Rank
Polymorphism with Existentials and Indexed Types. PACMPL POPL (Jan. 2019). http://arxiv.org/abs/1601.05106.
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995a. Sound Polymorphic Type Inference for Objects (OOPSLA ’95).
Association for Computing Machinery, New York, NY, USA, 169–184. https://doi.org/10.1145/217838.217858
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995b. Type Inference for Recursively Constrained Types and its
Application to OOP. Electronic Notes in Theoretical Computer Science 1 (1995), 132–153. https://doi.org/10.1016/S15710661(04)80008-2 MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference.
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. 2016. Visible Type Application. In European Symposiumon Programming (ESOP). 229–254.
Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). In Proceedings of IJCAR 2008 (Lecture
Notes in Artificial Intelligence).
Jean-Yves Girard. 1972. Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur. Thèsed’état. Université de Paris 7.
Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematicalsociety 146 (1969), 29–60.
Haruo Hosoya and Benjamin C. Pierce. 1999. How Good is Local Type Inference? Technical Report MS-CIS-99-17. Universityof Pennsylvania.
Christopher Jenkins and Aaron Stump. 2018. Spine-Local Type Inference. In Proceedings of the 30th Symposium on Implementation and Application of Functional Languages (Lowell, MA, USA) (IFL 2018). Association for Computing Machinery,
New York, NY, USA, 37–48. https://doi.org/10.1145/3310232.3310233
Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the Power of System F. In Proceedings of the Eighth ACM
SIGPLAN International Conference on Functional Programming (ICFP ’03).
Daan Leijen. 2008. HMF: Simple Type Inference for First-class Polymorphism. In Proceedings of the 13th ACM SIGPLAN
International Conference on Functional Programming (ICFP ’08).
Guillaume André Fradji Martres. 2023. Type-Preserving Compilation of Class-Based Languages. (2023), 153. https://doi.org/10.5075/epfl-thesis-8218
Henry Mercer, Cameron Ramsay, and Neel Krishnaswami. 2022. Implicit Polarized F: local type inference for impredicativity.
arXiv:2203.01835 [cs.PL]
Robin Milner. 1978. A theory of type polymorphism in programming. Journal of computer and system sciences 17, 3 (1978),348–375.
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL ’96).
Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored Local Type Inference. In Proceedings of the 28th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’01). Association for Computing
Machinery, New York, NY, USA, 41–53.
Lionel Parreaux. 2020. The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy
(Functional Pearl). Proc. ACM Program. Lang. 4, ICFP, Article 124 (Aug. 2020), 28 pages. https://doi.org/10.1145/3409006
Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types.
Proc. ACM Program. Lang. 6, OOPSLA2, Article 141 (oct 2022), 30 pages. https://doi.org/10.1145/3563304
Simon Peyton Jones and Mark Shields. 2004. Lexically scoped type variables. (March 2004). Draft.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.

Greedy Implicit Bounded Quantification

295:29Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitraryrank types. Journal of functional programming 17, 1 (2007), 1–82.
Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Proceedings of the 19th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (Albuquerque, New Mexico, USA) (POPL ’92). Association for
Computing Machinery, New York, NY, USA, 305–315. https://doi.org/10.1145/143165.143228
Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.
Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000),
1–44.
Hubert Plociniczak. 2016. Decrypting Local Type Inference. Ph. D. Dissertation. EPFL.
François Pottier. 1998. Type inference in the presence of subtyping: from theory to practice. Ph. D. Dissertation. INRIA.
Didier Rémy and Boris Yakobowski. 2008. From ML to MLF: Graphic Type Constraints with Efficient Type Inference. In
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (Victoria, BC, Canada) (ICFP’08). Association for Computing Machinery, New York, NY, USA, 63–74. https://doi.org/10.1145/1411204.1411216
John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, B. Robinet (Ed.). Springer Berlin
Heidelberg, Berlin, Heidelberg, 408–425.
Dilip Sequeira. 1998. Type inference with bounded quantification. Ph. D. Dissertation. University of Edinburgh.
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A Quick Look at Impredicativity.
Proc. ACM Program. Lang. 4, ICFP, Article 89 (Aug. 2020), 29 pages.
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded Impredicative Polymorphism.
In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018).
Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In
1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 32), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.). Schloss
Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 274–293. https://doi.org/10.4230/LIPIcs.SNAPL.2015.274
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell. In
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08).
Ningning Xie, Xuan Bi, Bruno C. D. S. Oliveira, and Tom Schrijvers. 2019. Consistent Subtyping for All. ACM Trans. Program.
Lang. Syst. 42, 1, Article 2 (nov 2019), 79 pages. https://doi.org/10.1145/3310339
Jinxu Zhao and Bruno C. d. S. Oliveira. 2022. Elementary Type Inference. In 36th European Conference on Object-Oriented
Programming (ECOOP 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222), Karim Ali and Jan Vitek(Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2:1–2:28. https://doi.org/10.4230/LIPIcs.
ECOOP.2022.2
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A Mechanical Formalization of Higher-Ranked Polymorphic
Type Inference. Proc. ACM Program. Lang. 3, ICFP, Article 112 (July 2019).
Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira. 2023. Recursive Subtyping for All. Proc. ACM Program. Lang. 7, POPL,
Article 48 (jan 2023), 30 pages. https://doi.org/10.1145/3571241

Received 2023-04-14; accepted 2023-08-27

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 295. Publication date: October 2023.