Modern mainstream programming languages, such as TypeScript, Flow, and Scala, have polymorphic type systems enriched with intersection and union types. These languages implement variants of \emph{bidirectional higher-rank polymorphic} type inference, which was previously studied mostly in the context of functional programming. However, existing type inference implementations lack solid theoretical foundations when dealing with non-structural subtyping and intersection and union types, which were not studied before.

In this paper, we study bidirectional higher-rank polymorphic type inference algorithms with intersection and union types. We introduce both a bidirectional specification and algorithmic versions of the type system. We first study a type inference algorithm that has good theoretical properties: it is sound, complete, and decidable with respect to the corresponding bidirectional specification. This is helpful to identify a class of types that can always be inferred. We also explore algorithmic variants that are sound but not necessarily complete. These variants incorporate practical features, such as handling records, which align with real-world implementations. These variants enable inference for a broader range of types, enhancing the expressiveness of the type systems. Our findings provide insights for improving current implementations and inspire the design of novel type inference algorithms. To ensure rigor, all results are formalized in the Coq proof assistant.