> Can arity checkers detect infinite recursion? My intuition is that this is the halting problem, and therefore impossible. So removing bounds checks on stack ops leaves the door open for stack corruption and therefore very odd and unpredictable behaviour in such cases.

I'm not sure how this fits with the halting problem, but in uxntal,
the arity checker will not let you recurse if the body that you're
jumping to imbalances the stack, is that an issue you've had with
uxnbal? It validates most recursion that I've found but it's possible
that it misses some specific patterns. I have yet to implement lambdas
support, that one is a bit tricky. Right now, I just mark these jumps
as unsafe.