I'm having trouble with recursive types in my type reconstruction (type inference) algorithm, some kind of combinatorial explosion. I think there are multiple triggers for this: at each call to unify(), I'm running a complete apply-subst(), rather than a level at a time. For the massive types generated by my OO code, this means lots of wasted, repeated work.
But of course there's even more going on. I think my code that detects recursive types is not working as well as it should, and I think the cause is the lack of 'sharing'. Remy/Pottier use a different style of unification, that involves preserving shared elements of types, and I think this where I'm screwing up: because parts of types are being copied, I'm missing links between identical parts of the graph.
I found a nice presentation from Remy describing "Core ML", that explains this in (accented) English, rather than a relentless flurry of LaTeX: "Using, Understanding, and Unraveling The OCaml Language: From Practice to Theory and vice versa".
The constraint-oriented solver gave me recursive types for free, (because its output types are naturally graphs), but I'm really hoping to avoid going back to that code, because it's much slower and I frankly don't understand it as well as I'd like. Maybe I can pull out just the multi-equation unification stuff, and get back recursive types.