Omnidirectional type inference for ML: principality any way

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. Yet, principality is fragile : many extensions of ML—GADTs, higher-rank polymorphism, and static overloading—break it 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 in a fixed order—type the let-bound expression first, generalize its type, and then type the let-body. 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.