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

If you are using Agesen-style CPA, then it is more of a global analysis (type recovery) then type inference. I would be a bit worried about scaling, but if you've put 50kloc through it, maybe you've figured it out? I'm working on my own type-less type inference system that I'll share more about soon.

Do you have a (more or less) formal description of the type system?

They have a couple posts on their inference algorithm, but I confess I haven't read them.