Reporting infinite projective dimension

Right now, pdim is a synonym for the length of a minimal "resolution": pdim Module := M -> length resolution minimalPresentation M. Thus if $S$ is a polynomial ring, $R=S/I$ and $M$ is an $R$-module, then you'll always be told that pdim M is $\leq \dim S+1$ (since $\dim S$ is the default LengthLimit option for resolution).

However, I think we can effectively detect when $\mathrm{pdim}\ M = \infty$ without doing any additional calculations: if $\mathrm{pdim}\ M$ were finite, we have $\mathrm{pdim}\ M\leq \mathrm{depth}\ R \leq \mathrm{dim}\ S$. Exactly two things can happen: $M$ has finite pdim and thus the length of res R (which will be $<\dim S+1$) really is pdim M, or it doesn't, in which case pdim outputs $\dim S +1$. What do people think about returning infinity if the length of the calculated resolution is $\mathrm{dim}\ S +1$? I realize that this is a trivial mental translation for the user to make, but I like the idea of a more mathematically meaningful output.

(All of the above assumes $R=S/I$ is graded, but I think that's essentially the current state of pdim anyways.)

Start by locating the implementation of pdim and how it calls minimalPresentation with the LengthLimit option; compare the returned resolution length with the proposed bound involving dim S. Review the existing behavior for res R and determine how an infinite projective dimension should be represented, then add or update coverage for the finite and boundary cases.