Success is not monotone in `synthInstance.maxSize`

Stream: lean4

[Eric Wieser]

I'm in a situation where synthInstance.maxSize = 128 fails, but both 127 and 130 work. Wouldn't the expected behavior be that for any given problem, it succeeds until a certain limit, then fails everywhere below it?

import Mathlib

open Nat

set_option synthInstance.maxSize 128 -- the default; change to 127 and it works

abbrev broken := ∀ n : ℕ,
  let bin := [1] ++ (digits 2 n) ++ [1];
  Decidable <|
    ∀ i j : Fin bin.length, i < j → bin.get i = 1 → bin.get j = 1 →
      (∀ k, i < k → k < j → bin.get k = 0) → Even ((j : ℕ) - (i : ℕ) - 1)

#synth broken

(cc @George Tsoukalas whose code this is extracted from)

[Eric Wieser]

Frustratingly it seemingly becomes monotone just after the default limit!

run_meta do
  let fails ← (List.range 500).filterM fun x => do
    withOptions (fun o => Lean.Meta.synthInstance.maxSize.set o x) do
      let s ← getThe Meta.State
      try
        return ! (←succeeds (synthInstanceQ q(broken)))
      finally
        set s  -- ensure the result isn't cached
  Lean.logInfo m!"{fails}"
  guard <| fails = List.range 22 ++ List.range' 30 6 ++ List.range' 63 4 ++ List.range' 128 2