Canonical form for a type.

dannywillems / RML

ML modules and functors as first-class citizens by unifying ML modules and ML records with path dependent types and subtyping.

36 stars 3 forks source link

Open dannywillems opened 7 years ago

dannywillems commented 7 years ago

Instead of \mu(x : T) \inter \mu(y : U), transform it in \mu(z : T \inter U) immediately.
Use best bound on x.A.

Not a good idea to apply to each call because UN-REFL-TYP is not caught.