The point isn't that there is an infinite loop of types that is rejected, the point is that there must be a finite loop of types that is rejected because it is

The point isn't that there is an infinite loop of types that is rejected, the point is that there must be a finite loop of types that is rejected because it is indistinguishable from an infinite loop of types. (I think the person you replied to is exaggerating the significance of this, though: it's obviously not a big deal in practice.)