The algorithm isn't very easy to explain in a few words. We don't use any well-known algorithm. It has some bits of the cartesian-product algorithm, but just tiny bits.

There's some info here:

http://crystal-lang.org/2013/09/23/type-inference-part-1.htm... http://crystal-lang.org/2014/04/27/type-inference-rules.html

About subtyping and paramtricity, I'm not sure what's that, but the compiler just keeps track of all the types and forms unions, except in one case which is this one (a union of references with a base type): http://crystal-lang.org/docs/syntax_and_semantics/virtual_an...