Caterpillar

So yeah, type inference in the presence of recursive function calls is complicated. If you're calling yourself, then during type inference, you encounter the call to yourself before you've figured out your own type. Hence you can't figure out the type of the call, which prevents you from figuring out your own type.

The key insight to resolving this contradiction, is that a function consists of multiple branches. If all branches end up calling the function itself, then the function never returns (it diverges). I wrote a compiler pass that detects this relatively easily, using a call graph. We'll see how that holds up, once I've been using it under real conditions for a bit.

If some branches diverge while others don't, then it's possible to infer the signature of a function based on its non-diverging branches. The tricky thing is, that you need to infer those branches in the right order. So far, I've failed with a more dynamic solution to this, based on a queue. Too easy to run into endless loops. Now I'm looking into another approach based on a call graph.