Previously this option was thought to be necessary to avoid infinite recursion, but it actually isn't, since the check evaluation isn't fed back into the module fixed-point.
