Singleton types here, singleton types there, singleton types everywhere
Stefan Monnier, David Haguenauer · 2010
Singleton types are often considered a poor man's substitute for dependent types. But their generalization in the form of GADTs has found quite a following. The main advantage of singleton types and GADTs is to preserve the so-called phase distinction, which seems to be so important to make use of the usual compilation techniques.