Failing to halt and going into an infinite loop are not the same thing.

I'd appreciate some explanation on that, to see if you're saying something I haven't heard before or if we're talking past each-other. I don't just include while(true); under "infinite loop", I also include infinitely-expanding recursions that cannot be characterized as coinductive stepwise computations. Basically, anything that would evaluate to the \Bot type in type-theory counts for "infinite loop" here, just plain computational divergence.