instance synthesis size has exponential growth

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When proving decidability of a chain of implications, the size of the term appears to grow exponentially. Consider the example:

set_option synthInstance.maxSize 45035996273704960 in

variable (a b c d e f g h i j k : Nat) in
#synth Decidable <|
      a ≠ b → a ≠ c → a ≠ d → a ≠ e → a ≠ f → a ≠ g → a ≠ h → a ≠ i → a ≠ j → a ≠ k → b ≠ c → b ≠ d → 
      b ≠ e → b ≠ f → b ≠ g → b ≠ h → b ≠ i → b ≠ j → b ≠ k → c ≠ d → c ≠ e → c ≠ f → c ≠ g → c ≠ h → 
      c ≠ i → c ≠ j → c ≠ k → d ≠ e → d ≠ f → d ≠ g → d ≠ h → d ≠ i → d ≠ j → d ≠ k → e ≠ f → e ≠ g → 
      e ≠ h → e ≠ i → e ≠ j → e ≠ k → f ≠ g → f ≠ h → f ≠ i → f ≠ j → f ≠ k → g ≠ h → g ≠ i → g ≠ j → 
      g ≠ k → h ≠ i → h ≠ j → h ≠ k → i ≠ j → i ≠ k → j ≠ k

Observe that there are 54 implications, and the maxSize counter is set to exactly 5 * 2 ^ 53. Decreasing it by even one makes the instance fail. Recall also that the default value of this counter is 2 ^ 7.

Context

I attempted to figure out what's going on here: the remainder of the "Context" section is about this.

First consider the same example but with each implication replaced by a conjunction:

set_option synthInstance.maxSize 164 in

variable (a b c d e f g h i j k : Nat) in
#synth Decidable <|
      a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ a ≠ e ∧ a ≠ f ∧ a ≠ g ∧ a ≠ h ∧ a ≠ i ∧ a ≠ j ∧ a ≠ k ∧ b ≠ c ∧ b ≠ d ∧ 
      b ≠ e ∧ b ≠ f ∧ b ≠ g ∧ b ≠ h ∧ b ≠ i ∧ b ≠ j ∧ b ≠ k ∧ c ≠ d ∧ c ≠ e ∧ c ≠ f ∧ c ≠ g ∧ c ≠ h ∧ 
      c ≠ i ∧ c ≠ j ∧ c ≠ k ∧ d ≠ e ∧ d ≠ f ∧ d ≠ g ∧ d ≠ h ∧ d ≠ i ∧ d ≠ j ∧ d ≠ k ∧ e ≠ f ∧ e ≠ g ∧ 
      e ≠ h ∧ e ≠ i ∧ e ≠ j ∧ e ≠ k ∧ f ≠ g ∧ f ≠ h ∧ f ≠ i ∧ f ≠ j ∧ f ≠ k ∧ g ≠ h ∧ g ≠ i ∧ g ≠ j ∧ 
      g ≠ k ∧ h ≠ i ∧ h ≠ j ∧ h ≠ k ∧ i ≠ j ∧ i ≠ k ∧ j ≠ k

Here a value of 164 is the smallest possible (still above the default of 128, but significantly less).
(This example takes close to a minute to compile, but the point can be equally well made with noncomputable def here).

This leads me to believe one of the instances instDecidableForall or forall_prop_decidable is at fault: both can apply. Turning instDecidableForall off (back in the original) means the smallest value of maxSize is now 5 * 2 ^ 54 - 3 so forall_prop_decidable appears the culprit. Indeed, turning this one off leads to a maxSize of 164 again.

The options

set_option trace.Meta.synthInstance.resume true in
set_option trace.Meta.synthInstance.answer true in

show where the failure occurs in the original example with value 5 * 2 ^ 53 - 1 (ie one less than the smallest size): it's in the very last resume step, where this line informs that the instance size is too large. While I'm of course not sure, I find it incredibly hard to believe that this example has an instance size that massive (Wolfram Alpha informs me that if I had 5 * 2 ^ 53 bits, I'd have more content than the digitised version of the Library of Congress).

These two data points suggest to me that there's weird interaction between forall_prop_decidable and the resume function in synthesis.

Steps to Reproduce

1. Code as above

Expected behavior: Decidable instance can be synthesized with a reasonable size limit

Actual behavior: Decidable instance requires exponentially growing size limit

Versions

live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Run the minimal reproducer with the synthesis tracing options, then read the referenced resume logic in src/Lean/Meta/SynthInstance.lean around lines 421 and 603. Compare the behavior with instDecidableForall and forall_prop_decidable disabled; done means the Decidable instance synthesizes without exponential maxSize growth.