pith. sign in

arxiv: 2511.10343 · v2 · submitted 2025-11-13 · 💻 cs.PL

Omnidirectional type inference for ML: principality any way

Alistair O'Brien , Didier R\'emy , Gabriel Scherer This is my paper

Pith reviewed 2026-05-17 22:08 UTC · model grok-4.3

classification 💻 cs.PL
keywords type inferenceprincipalityMLDamas-Hindley-Milnersuspended constraintsincremental instantiationOCamlfirst-class polymorphism
0
0 comments X

The pith

Omnidirectional type inference restores principality for fragile ML constructs by solving constraints in dynamic order.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that omnidirectional type inference can recover the principal type property in ML systems even when fragile features like static overloading or first-class polymorphism are added. Instead of requiring a fixed order for propagating known types, constraints are solved in any order and suspended until the required information arrives. This is made to work with ML's let-generalization by allowing partial type schemes to be instantiated and then updated incrementally as more information is found. Demonstrations on two OCaml features show the resulting algorithm accepts more programs while still producing a unique most general type.

Core claim

By replacing fixed-order propagation with suspended match constraints and incremental instantiation, the Damas-Hindley-Milner system can be extended to handle dynamic ordering of type information without sacrificing principality, yielding a principal inference algorithm that is strictly more expressive than OCaml's current typechecker for both static overloading of labels and constructors and semi-explicit first-class polymorphism.

What carries the argument

Suspended match constraints that pause solving until needed type information becomes available, together with incremental instantiation that allows partially solved type schemes to be used and later refined.

If this is right

  • Principal type inference becomes possible for static overloading of record labels and datatype constructors.
  • Semi-explicit first-class polymorphism can be handled with a principal and more expressive algorithm than the current OCaml checker.
  • The same framework applies to other fragile extensions such as GADTs without forcing a rigid inference order.
  • Type inference remains predictable because a unique most general type is still guaranteed whenever a program is accepted.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could be tested on additional fragile features such as dependent types or linear types to see whether principality is recovered without new machinery.
  • Implementations in other ML-family languages might become simpler by removing the need for separate bidirectional passes.
  • Error reporting could improve because the solver can continue from multiple directions rather than stopping at the first missing annotation.

Load-bearing premise

That suspended match constraints combined with incremental instantiation preserve principality and soundness when the core Damas-Hindley-Milner system is extended to support dynamic ordering and partial generalization.

What would settle it

A concrete program using record label overloading or semi-explicit first-class polymorphism that receives a principal type under the omnidirectional algorithm but is rejected by OCaml's existing typechecker.

Figures

Figures reproduced from arXiv: 2511.10343 by Alistair O'Brien, Didier R\'emy, Gabriel Scherer.

Figure 1
Figure 1. Figure 1: Syntax and typing rules for polytypes from PolyML [ [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Syntax and explicit, robust typing rules of OmniML. [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Typing rules for fragile, implicitly typed extensions. [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Selected cases of the erasure of 𝑒. All other cases are homomorphic [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Selected syntax and semantics of constraints. [PITH_FULL_IMAGE:figures/full_fig_p019_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Patterns for OmniML. unicity for 𝛽 holds, since the context now includes 𝛽 = bool. We can therefore apply Match-Ctx to eliminate the final match constraint. This example demonstrates that suspended constraints must be resolved in a dependency￾respecting order: attempting to resolve a match constraint too early may result in unsatisfiability. Example 4.8. Let us consider a constraint with a cyclic dependenc… view at source ↗
Figure 7
Figure 7. Figure 7: The constraint generation translation for OmniML. [PITH_FULL_IMAGE:figures/full_fig_p024_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Unification: syntax, semantics, and the rewriting-based solver [PITH_FULL_IMAGE:figures/full_fig_p027_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Syntax and semantics of region-based let and incremental instantiation constraints. never appear in generated constraints, but are introduced internally by the solver to manage generalization and incremental instantiation. These administrative constraints enable the solver to represent and refine partial type schemes as solving progresses, capturing intermediate generalization states and tracking how insta… view at source ↗
Figure 10
Figure 10. Figure 10: Basic rewriting rules 𝐶1 −→ 𝐶2. solved multi-equations followed by a residual constraint—typically an instantiation, let-binding, or suspended constraint. OmniML-specific constraints, such as the label and polytype instantiation constraints (𝑡 .ℓ ≤ 𝜏1 → 𝜏2, 𝑠 ≤ 𝜏, etc.), require no special treatment in our solver. Once their pattern variables are substituted—after solving a match constraint—they are desug… view at source ↗
Figure 11
Figure 11. Figure 11: Solving rules for let-constraints and instantiations. [PITH_FULL_IMAGE:figures/full_fig_p032_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Rewriting rules for suspended match constraints. [PITH_FULL_IMAGE:figures/full_fig_p033_12.png] view at source ↗
read the original abstract

The Damas-Hindley-Milner (ML) type system owes its success to principality, the property that every well-typed expression has a unique most general type. This makes inference predictable and efficient. Unfortunately, many extensions of ML (GADTs, higher-rank polymorphism, and static overloading) endanger princpality by introducing _fragile_ constructs that resist principal inference. Existing approaches recover principality through directional inference algorithms, which propagate _known_ type information in a fixed (or static) order (e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a static inference order often causes otherwise well-typed programs to be rejected. We propose _omnidirectional_ type inference, where type information flows in a dynamic order. Typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using _suspended match constraints_. This approach is straightforward for simply typed systems, but extending it to ML is challenging due to let-generalization. Existing ML inference algorithms type let-bindings (let x = e1 in e2) in a fixed order: type e1, generalize its type, and then type e2. To overcome this, we introduce _incremental instantiation_, allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined. Omnidirectionality provides a general framework for restoring principality in the presence of fragile features. We demonstrate its versatility on two fundamentally different features of OCaml: static overloading of record labels and datatype constructors and semi-explicit first-class polymorphism. In both cases, we obtain a principal type inference algorithm that is more expressive than OCaml's current typechecker.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes omnidirectional type inference for ML to restore principality for fragile constructs such as static overloading of record labels/datatype constructors and semi-explicit first-class polymorphism. It replaces fixed-order let-generalization with suspended match constraints and incremental instantiation of partially-solved schemes, allowing type information to flow in dynamic order while claiming a principal inference algorithm more expressive than OCaml's current typechecker.

Significance. If the central mechanisms are shown to preserve principality and soundness, the work supplies a general framework for handling fragile features in ML without sacrificing expressiveness or predictability, with concrete demonstrations on two distinct OCaml extensions.

major comments (2)
  1. [Abstract and §4] The manuscript provides no derivations, proofs, or concrete examples showing that suspended match constraints combined with incremental instantiation preserve principality when let-generalization is replaced by partial schemes (see abstract and §4). This is load-bearing for the central claim that any solution order yields the same principal type.
  2. [§5.1] §5.1: The interaction between the instance-update rule and the generalization rule is not shown to commute for programs containing suspended constraints resolved from use sites; without this, the claim that omnidirectionality restores principality for overloading and first-class polymorphism remains unestablished.
minor comments (2)
  1. [§3] Notation for suspended match constraints is introduced without a clear grammar or example derivation in the early sections.
  2. The paper should include a small, fully-worked example of incremental instantiation on a let-binding with overloading to illustrate the dynamic order.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. The points raised identify gaps in the formal support for our central claims about principality. We respond to each major comment below and will revise the manuscript to address them.

read point-by-point responses

  1. Referee: [Abstract and §4] The manuscript provides no derivations, proofs, or concrete examples showing that suspended match constraints combined with incremental instantiation preserve principality when let-generalization is replaced by partial schemes (see abstract and §4). This is load-bearing for the central claim that any solution order yields the same principal type.

    Authors: We agree that the current manuscript lacks explicit derivations, proofs, or concrete examples demonstrating principality preservation for suspended match constraints and incremental instantiation of partial schemes. While §4 describes the mechanisms and states the claim that any solution order yields the same principal type, it does not supply the supporting formal argument. In the revised manuscript we will add a new subsection to §4 containing a proof sketch of principality together with several worked examples that illustrate convergence to the same principal type under different solving orders. revision: yes

  2. Referee: [§5.1] §5.1: The interaction between the instance-update rule and the generalization rule is not shown to commute for programs containing suspended constraints resolved from use sites; without this, the claim that omnidirectionality restores principality for overloading and first-class polymorphism remains unestablished.

    Authors: The referee correctly observes that commutativity of the instance-update rule and the generalization rule is not shown for programs whose suspended constraints are resolved from use sites. This interaction is essential to the principality claims for both static overloading and semi-explicit first-class polymorphism. We will revise §5.1 to include a formal argument establishing the required commutativity, supported by examples drawn from the two OCaml extensions presented in the paper. revision: yes

Circularity Check

0 steps flagged

No circularity: new mechanisms for dynamic constraint solving are defined independently of the target result

full rationale

The paper defines omnidirectional inference via suspended match constraints and incremental instantiation as fresh constructs that replace fixed-order let-generalization. These are presented as direct extensions of simply-typed omnidirectional typing to ML, with principality claimed to follow from the new update rules rather than from any self-definition, fitted parameter, or self-citation chain. No equations or steps in the abstract reduce the final principal type to a renaming or re-use of the input constraints; the derivation therefore remains self-contained against external benchmarks of soundness and principality.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The proposal rests on standard ML type system assumptions and introduces two new mechanisms to enable dynamic ordering.

axioms (1)
  • domain assumption Damas-Hindley-Milner type system has principality for the core language without fragile constructs
    Invoked when discussing how extensions endanger principality and how omnidirectionality restores it.
invented entities (2)
  • suspended match constraints no independent evidence
    purpose: Allow constraint solving to pause until required type information becomes available
    New construct introduced to support dynamic order of inference.
  • incremental instantiation no independent evidence
    purpose: Permit instantiation and later refinement of partially solved type schemes during let-generalization
    New mechanism to handle generalization under omnidirectional solving.

pith-pipeline@v0.9.0 · 5624 in / 1192 out tokens · 31753 ms · 2026-05-17T22:08:11.326374+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages

  1. [1]

    The Simple Essence of Overloading. (2025). Arthur Charguéraud, Martin Bodin, Jana Dunfield, and Louis Riboulet

    work page 2025

  2. [2]

    Extending Type Inference to Variational Programs.ACM Transactions on Programming Languages and Systems36, 1 (March 2014), 1–54. https://doi.org/10.1145/2518190 16Although the undecidability of semi-unification already implied the existence of such examples, the specific class of examples of non-terminating cases was only characterized later [Figueiredo an...

    work page doi:10.1145/2518190 2014

  3. [3]

    InProceedings of the 9th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages(Albuquerque, New Mexico)(POPL ’82)

    Principal type-schemes for functional programs. InProceedings of the 9th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages(Albuquerque, New Mexico)(POPL ’82). Association for Computing Machinery, New York, NY, USA, 207–212. https://doi.org/10.1145/582153.582176 Lucilia Figueiredo and Carlos Camarao

    work page doi:10.1145/582153.582176

  4. [4]

    Semi-unification and Periodicity of Turing Machines. (2004). https://www.researchgate.net/profile/Carlos-Camarao/publication/268426611_Semi-unification_and_Periodicity_of_ Turing_Machines Jacques Garrigue

    work page arXiv 2004

  5. [5]

    http://www.springerlink.com/content/m303472288241339/ A preliminary version appeared in TACS’97

    Extending ML with Semi-Explicit Higher-Order Polymorphism.Information and Computation155, 1/2 (1999), 134–169. http://www.springerlink.com/content/m303472288241339/ A preliminary version appeared in TACS’97. Jacques Garrigue and Didier Rémy

    work page 1999

  6. [6]

    InProgramming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11,

    Ambivalent Types for Principal Type Inference with GADTs. InProgramming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11,

    work page 2013

  7. [7]

    Model-Based Reconstructions for Quantitative Imaging in Photoacous- tic Tomography

    Proceedings (Lecture Notes in Computer Science, Vol. 8301), Chung-chieh Shan (Ed.). Springer, 257–272. https://doi.org/10.1007/978-3- 319-03542-0_19 Adam Gundry

    work page doi:10.1007/978-3-

  8. [8]

    https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/ 0023-overloaded-record-fields.rst GHC proposal/RFC

    Overloaded Record Fields. https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/ 0023-overloaded-record-fields.rst GHC proposal/RFC. Fritz Henglein. 1989.Polymorphic Type Inference and Semi-Unification. PhD. New York University. Fritz Henglein

    work page 1989

  9. [9]

    Type inference with polymorphic recursion.ACM Trans. Program. Lang. Syst.15, 2 (April 1993), 253–289. https://doi.org/10.1145/169701.169692 Roger Hindley

    work page doi:10.1145/169701.169692 1993

  10. [10]

    Gérard Huet

    The principal type-scheme of an object in combinatory logic.Transactions of the american mathematical society146 (1969), 29–60. Gérard Huet

    work page 1969

  11. [11]

    A unification algorithm for typed𝜆-calculus.Theoretical Computer Science1, 1 (1975). Mark P. Jones. 1995a.Qualified types: theory and practice. Cambridge University Press. Mark P. Jones. 1995b. A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism.J. Funct. Program.5, 1 (1995), 1–35. https://doi.org/10.1017/S0956796800001210 ...

    work page doi:10.1017/s0956796800001210 1975

  12. [12]

    https://doi.org/10.1006/inco.1993.1003 Didier Le Botlan and Didier Rémy

    The Undecidability of the Semi-unification Problem.Information and Computation102, 1 (1993), 83–101. https://doi.org/10.1006/inco.1993.1003 Didier Le Botlan and Didier Rémy

    work page doi:10.1006/inco.1993.1003 1993

  13. [13]

    https: //doi.org/10.1016/j.ic.2008.12.006 Oukseh Lee and Kwangkeun Yi

    Recasting MLF.Information and Computation207, 6 (2009), 726–785. https: //doi.org/10.1016/j.ic.2008.12.006 Oukseh Lee and Kwangkeun Yi

    work page doi:10.1016/j.ic.2008.12.006 2009

  14. [14]

    https://doi.org/10.1145/291891.291892 Daan Leijen and Wenjia Ye

    Proofs about a folklore let-polymorphic type inference algorithm.ACM Transactions on Programming Languages and Systems20, 4 (July 1998), 707–723. https://doi.org/10.1145/291891.291892 Daan Leijen and Wenjia Ye

    work page doi:10.1145/291891.291892 1998

  15. [15]

    InPLDI’25

    Principal Type Inference under a Prefix. InPLDI’25. ACM, 1–24. https://www.microsoft. com/en-us/research/publication/principal-type-inference-under-a-prefix/ Backup Publisher: ACM SIGPLAN. Brad Lushman and Gordon V Cormack. 2008.Constraint-Based Typing for ML via Semiunification. Technical Report CS-2008-10. University of Waterloo, Ontario, Canada. 49 pag...

    work page 2008

  16. [16]

    InLogic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991, Koichi Furukawa (Ed.)

    Unification of Simply Typed Lamda-Terms as Logic Programming. InLogic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991, Koichi Furukawa (Ed.). MIT Press, 255–269. Robin Milner, Robert Harper, David MacQueen, and Mads Tofte. 1997.The Definition of Standard ML. The MIT Press. https://doi.org/10.7551/mitpress/23...

    work page doi:10.7551/mitpress/2319.001.0001 1991

  17. [17]

    InConference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St

    Putting Type Annotations to Work. InConference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 54–67. https://doi.org/10.1145/237721.237729 Martin Odersky, ...

    work page doi:10.1145/237721.237729 1996

  18. [18]

    https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4 Atsushi Ohori

    Type inference with constrained types.Theory and Practice of Object Systems5, 1 (1999), 35–55. https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4 Atsushi Ohori

    work page doi:10.1002/(sici)1096-9942(199901/03)5:1 1999

  19. [19]

    A Polymorphic Record Calculus and Its Compilation.ACM Trans. Program. Lang. Syst.17, 6 (1995), 844–895. https://doi.org/10.1145/218570.218572 Benjamin C. Pierce and David N. Turner

    work page doi:10.1145/218570.218572 1995

  20. [20]

    InPOPL ’98, Proceedings of the 25th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998, David B

    Local Type Inference. InPOPL ’98, Proceedings of the 25th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998, David B. MacQueen and Luca Cardelli (Eds.). ACM, 252–265. https://doi.org/10.1145/268946.268967 François Pottier

    work page doi:10.1145/268946.268967 1998

  21. [21]

    A Versatile Constraint-Based Type Inference System.Nord. J. Comput.7, 4 (2000), 312–347. François Pottier

    work page 2000

  22. [22]

    InProceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Austin, Texas, USA)(POPL ’89)

    Type checking records and variants in a natural extension of ML. InProceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Austin, Texas, USA)(POPL ’89). Association for Computing Machinery, New York, NY, USA, 77–88. https://doi.org/10.1145/75277.75284 Didier Rémy. 1990.Algèbres Touffues. Application au Typage Polymorph...

    work page doi:10.1145/75277.75284 1990

  23. [23]

    1992.Extending ML Type System with a Sorted Equational Theory

    Didier Rémy. 1992.Extending ML Type System with a Sorted Equational Theory. Research Report

    work page 1992

  24. [24]

    Objective ML: A Simple Object-Oriented Extension of ML. InConference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 40–53. https://doi.org/10.1145/263699.263707 Andreas Rossberg

    work page doi:10.1145/263699.263707 1997

  25. [25]

    Complete and decidable type inference for GADTs. InProceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, Graham Hutton and Andrew P. Tolmach (Eds.). ACM, 341–352. https://doi.org/10.1145/1596550.1596599 Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, ...

    work page doi:10.1145/1596550.1596599 2009

  26. [26]

    ACM Program

    A quick look at impredicativity.Proc. ACM Program. Lang.4, ICFP (2020), 89:1–89:29. https://doi.org/10.1145/3408971 Wenhao Tang, Shengyi Jiang, Bruno C. d. S. Oliveira, and Sam Lindley

    work page doi:10.1145/3408971 2020

  27. [27]

    ACM22, 2 (1975), 215–225

    Efficiency of a Good But Not Linear Set Union Algorithm.J. ACM22, 2 (1975), 215–225. https://doi.org/10.1145/321879.321884 Dimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, and Martin Sulzmann

    work page doi:10.1145/321879.321884 1975

  28. [28]

    OutsideIn(X) Modular type inference with local assumptions.J. Funct. Program.21, 4-5 (2011), 333–412. https://doi.org/10.1017/S0956796811000098 Philip Wadler and Stephen Blott

    work page doi:10.1017/s0956796811000098 2011

  29. [29]

    https://doi.org/10.1145/75277.75283 Mitchell Wand

    ACM Press, 60–76. https://doi.org/10.1145/75277.75283 Mitchell Wand

    work page doi:10.1145/75277.75283

  30. [30]

    https://doi.org/10.1109/LICS.1989.39162 Leo White

    IEEE Computer Society, 92–97. https://doi.org/10.1109/LICS.1989.39162 Leo White

    work page doi:10.1109/lics.1989.39162 1989

  31. [31]

    (sep 2023)

    Semi-explicit polymorphic parameters. (sep 2023). Presentation at the Higher-order, Typed, Inferred, Strict: ML Family workshops. Xu Xue and Bruno C. d. S. Oliveira

    work page 2023

  32. [32]

    permuted down

    Contextual Typing.Proc. ACM Program. Lang.8, ICFP (2024), 880–908. https: //doi.org/10.1145/3674655 42 Alistair O’Brien, Didier Rémy, and Gabriel Scherer Organization of appendices Reference appendix.§A gives a full reference for all definitions, grammars and figures in the paper, including all cases (even those omitted from the main paper for reasons of ...

    work page doi:10.1145/3674655 2024

  33. [33]

    Lemma C.8 Subcase=⇒. 𝜙⊢𝑖(𝛼){𝛾 1 ∧𝑖(𝛼){𝛾 2 Premise 𝜙⊢𝑖(𝛼){𝛾 1 Simple inversion 𝜙⊢𝑖(𝛼){𝛾 2 ′′ 𝜙(𝛾 1)=𝜙(𝑖) (𝛼) ′′ 𝜙(𝛾 2)=𝜙(𝑖) (𝛼) ′′ 𝜙(𝛾 1)=𝜙(𝛾 2)Above 𝜙⊢𝛾 1 =𝛾 2 ByUnif Z𝜙⊢𝑖(𝛼){𝛾 1 ∧𝛾 1 =𝛾 2 ByConj Subcase⇐=. Symmetric argument. Case let𝑥 𝛼[ ¯𝛼]= ¯𝜖∧𝐶in𝒞[𝑖 𝑥 (𝛼 ′){𝛾] ∀𝛼′.∃𝛼, ¯𝛼 . ¯𝜖≡true𝛼 ′ ∈𝛼, ¯𝛼 𝛼 ′ # 𝐶 𝑖(𝛼 ′) # insts(𝒞)𝑥 # bv(𝒞) let𝑥 𝛼[ ¯𝛼]= ¯𝜖∧𝐶in𝒞[true...

    work page 2005

  34. [34]

    internal

    Otherwise, we consider cases where𝐶 1 is solved or stuck. If𝐶 1 is solved, then it must be of the form ¯𝜖. There are two cases: –∃𝛼, ¯𝛼 . ¯𝜖≡true . As 𝛼 ′ does not appear in the head position of any multi-equation in¯𝜖, it must be polymorphic. Thus ∀𝛼′.∃𝛼, ¯𝛼\𝛼 ′. ¯𝜖≡true . So we can apply S-Inst-Poly. –∃𝛼, ¯𝛼 . ¯𝜖.true. ApplyS-Exists-Lower(using the same...

    work page 2005

  35. [35]

    𝐶, then𝜗[𝛼:=𝜏]is a unifier of𝐶for some𝜏

    •For simple𝐶, if𝜗is a unifier of∃𝛼 . 𝐶, then𝜗[𝛼:=𝜏]is a unifier of𝐶for some𝜏. •For simple𝐶, if𝜗is a unifier of∀𝛼 . 𝐶, then𝜗is a unifier of𝐶. Proof.Follows by simple inversion.□ Lemma D.9.If 𝜗 unifies ∃𝛼 . 𝐶, then there exists a unifier 𝜗 ′ that extends 𝜗 with 𝛼, where 𝜗 ′ is most general unifier of∃𝜗∧𝐶. Then 𝜆𝛼 . 𝐶 is equivalent to 𝜆𝛼 . 𝜎≤𝛼 under 𝜗, where...

    work page 2005