International Conference on Functional Programming edition:14 location:Edinburgh, UK date:31 August - 2 September 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.
We present a novel and simplified type inference approach for local type
assumptions from GADT pattern matches. Our approach is complete and decidable,
while more liberal than previous such approaches.