Formalizing GADT constraint reasoning in Scala

Generalized algebraic data types (GADTs) are a powerful tool allowing to express invariants leveraging the type system. Scala 3 considerably improves the support of GADTs with respect to its predecessor Scala 2. A unique feature of Scala 3, compared to languages integrating GADTs, is the ability to define variant GADTs. While Scala 3 GADTs support is satisfactory, some use-cases could benefit from extending it further. In this work, we lay out the necessary tools to help us understand and reason about the GADT inference problem. We propose an algorithm that incrementally refines the accumulated knowledge about the type variables and prove its soundness. We also show some examples where the proposed algorithm is able to infer interesting properties that the current Scala 3 compiler misses.