Okay, so. Now coming back to the general case.
What if we made it possible to express depth in terms of the parameters to the function?
For example, in your snippet:
/* Original code */
// Some external module that I cannot modify.
@compilerEvaluable(recursionLimit = 5)
func factorial(_ n: Int) > Int {
return n == 0 ? 1 : n * factorial(n  1)
}
/* Depth depends on function parameter */
// Some external module that I cannot modify.
@compilerEvaluable(recursionLimit = n + 2)
func factorial(_ n: Int) > Int {
return n == 0 ? 1 : n * factorial(n  1)
}
I think that's what I wanted when I thought of #3, but now I was able to formalize it in a (maybe) practical way.
The cool thing about this is that it doesn't change the syntax for normal functions. Only users of the @compilerEvaluable
attribute would need to know about this feature.
Now. Can we guarantee the depth to be polynomial? In a nonobstrusive way? I think we can. Let's see:
We could limit the syntax of the depth formula to this:

UInt
parameters and results.
 Allow for constants (n + 2)
 Allow for the 4 basic arithmetic operators:
+, , *, /
// Semantics: anything less than or equal to 0 will be turned into 1.
And that's it. No exponentiation, no ifs, no binary expressions. Although some of those could be added as well (like ternary operators, which are technically ifthenelse).
But this syntax, as a proof of concept, prohibits exponential depth.