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].