exponential growth when synthesizing type instances

Stream: lean4

[Ted Hwa]

Consider the following code

-- creates a chain P → P → ... → P
@[reducible]
def imp_chain (P: Prop) (n: Nat) :=
    match n with
    | Nat.zero => P
    | Nat.succ m => P → imp_chain P m

set_option trace.Meta.synthInstance.newAnswer true in
example (P: Prop) [Decidable P]: imp_chain P 6  := by
  apply Decidable.byContradiction   -- 3, 9, 21, 45, 93, 95

The number you get from the trace are 3, 9, 21, 45, 93, 95. The numbers are 3 * (2^n - 1) (exponentia), but then it slows down at 95. If you increase 6 to 7 in the example, it becomes 97. So it seems like it has hit linear growth after 93.

But actually, this is because synthInstance.maxSize has a default value of 128. If you increase synthInstance.maxSize to 256, then you do see the next number 189:

set_option synthInstance.maxSize 256 in
set_option trace.Meta.synthInstance.newAnswer true in
example (P: Prop) [Decidable P]: imp_chain P 6  := by
  apply Decidable.byContradiction    -- 3, 9, 21, 45, 93, 189

and now if you go to P 7, you get 191.

It seems like the size grows exponentially until it hits the limit synthInstance.maxSize, then it becomes linear. Why does it do that? Why is it exponential at all?