Just a quick status update. As my 'user' program has become larger, the type solver has begun to slow down horribly. I'm on the wrong end of some horrible O(x) where x is probably n^4 or worse.
So I decided to try an experiment, going back to the classic algorithm W. This only took a couple of days! However. One thing I didn't realize I was getting for 'free' from the constraint-based solver was recursive types. Now I'm forced to actually understand the concept.
I see two potential outcomes: 1) I grok recursive types well enough to fix my unifier, and the compiler gets much much faster; or 2) I rewrite the constraint solver to be more efficient. It's possible that I understand things well enough now to be able to do so.
If anyone out there can explain how to do unification with equirecursive types, I'd love to have the help!