leanprover
Configuration option for `synthPendingDepth`
Currently there is the following in Lean.Meta.SynthInstance
/- TODO: use a configuration option instead of the hard-coded limit `1`. -/
if (← read).synthPendingDepth > 1 then
trace[Meta.synthPending] "too many nested synthPending invocations"
return false
There have been multiple places where Mathlib has butted up against this; the most recent is leanprover-community/mathlib4#12150.
There are also workaround instances in Mathlib.Analysis.NormedSpace.OperatorNorm and a thread on Zulip discussing this.
Given the labeling as a TODO, I assume such a change is desired. If indeed so but bandwidth is limited, conveying specifics as to implementation (should it look like other such ones? etc...) would help in getting a solution.
Added references for failures in OperatorNorm in leanprover-community/mathlib4#12188
What happens if you just increase this to 2? (I don't know what, if anything, we will want to do about this yet.)
It broke things pretty badly when I bumped the hardcoded bound from 0 to 1.