I'm not sure if "better" is appropriate in this context; in general, semi-unification is undecidable. Type checking in presence of subtypes is decidable for sim

I'm not sure if "better" is appropriate in this context; in general, semi-unification is undecidable. Type checking in presence of subtypes is decidable for simple cases (where types form a lattice), but the presence of polymorphism/generics makes it undecidable (Java [1], OCaml[2]). The type inference algorithms for subtyping are not that performant (an algorithm is described in [3]). [1] http://stackoverflow.com/questions/23939168/is-c-sharp-type-system-sound-and-decidable http://stackoverflow.com/questions/23939168/is-c-sharp-type-... [2] http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html [3] http://www.normalesup.org/~simonet/publis/simonet-aplas03.pdf http://www.normalesup.org/~simonet/publis/simonet-aplas03.pd...