Failed mixed use of compiled code and code from `evalExpr`

Stream: lean4

[Qiyuan Zhao]

I'm trying to mix the use of compiled code and code from evalExpr in a Lean project. During my experiments, I found what appears to be a bug: mixing compiled code with code obtained through evalExpr causes a stack overflow under specific conditions.

I've created a minimal reproduction project here: https://github.com/zqy1018/compilation-vs-evalExpr (OS version of my machine: MacOS 26.1 (arm64)). I've also done some testing; the result is in the README.md.

The result indicates:

1. Pure evalExpr (main1 + bycall) works fine
2. Pure compiled code (main2) works fine
3. The problem only occurs when mixing the two (main1 + byarg)
4. It only happens with the large input
5. It only affects isPrimeUsingClass and isPrimeNotUsingClass, which are relatively complicated and involve typeclass instances
6. Interestingly, whether the called function actually uses the typeclass doesn't matter (isPrimeUsingClass uses the typeclass, isPrimeNotUsingClass doesn't)

My question is: is this a bug, or is there something fundamentally wrong with my approach? More broadly, is it reasonable/supported to use evalExpr within compiled programs to dynamically generate code in this way?

Any insights would be greatly appreciated!