GADT

Type inference with type abbreviations

We study how to perform lazy expansion of type abbreviations during type inference. The goal is both efficiency of type inference, and output types in a more pertinent form. This is particular crucial in the presence of object types, which extensively uses type abbreviations, and where both efficiency and readabiliy becomes serious issues. This project started with Carine Morel's master internship and has later been extended to cope with destructive type abbreviations [ abunif.pdf].