Complete and decidable type inference for GADTs
Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, Dimitrios Vytiniotis · 2009
GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the principal-type property, which is necessary for modular type inference.