TC performance issue when hitting maxSize

Stream: lean4

[Tomas Skrivan]

I have been dealing with curious TC performance issue. In a moderately sized computation I had to synthesize Add (K × K × K × K × K × K × K × K × K × K × K). Interestingly, synthesizing this class for 10 Ks takes ~4ms but for 11Ks it takes ~450ms. The issue is that for 11Ks the type class synthesis hits the maximum size, kills the good inference path, goes crazy and after half a second it finds an instance in some mysterious way. The issue is easily solvable just by increasing synthInstance.maxSize

My issue is that there is no warning or error letting you know that this is happening. Actually, what is the purpose of the synthInstance.maxSize. Why there is no error like when hitting synthInstance.maxHeartbeats ? Would it make sense to throw an error or a warning?

---

mwe

import Mathlib.Data.IsROrC.Basic

variable {K : Type} [IsROrC K]

set_option profiler true
set_option profiler.threshold 1


-- fast
-- 10 K
example : Add (K × K × K × K × K × K × K × K × K × K) := by infer_instance

-- slow
-- 11 K
example : Add (K × K × K × K × K × K × K × K × K × K × K) := by infer_instance

-- fast
-- 11 K
set_option synthInstance.maxSize 200 in
example : Add (K × K × K × K × K × K × K × K × K × K × K) := by infer_instance

[Eric Wieser]

What's the instance in each case? (You can check with #synth)

[Kyle Miller]

import Mathlib.Data.IsROrC.Basic

variable {K : Type} [IsROrC K]

set_option profiler true
set_option profiler.threshold 1


-- fast
-- 10 K
#synth Add (K × K × K × K × K × K × K × K × K × K)
-- Prod.instAdd

-- slow
-- 11 K
#synth Add (K × K × K × K × K × K × K × K × K × K × K)
-- Distrib.toAdd

-- fast
-- 11 K
set_option synthInstance.maxSize 200 in
#synth Add (K × K × K × K × K × K × K × K × K × K × K)
-- Prod.instAdd

[Kyle Miller]

I just wanted to experiment to see if there was an alternative to raising synthInstance.maxSize, and adding these instances does work:

namespace Prod

@[to_additive]
instance instMul_2 {M₁ M₂ N : Type*} [Mul M₁] [Mul M₂] [Mul N] : Mul (M₁ × M₂ × N) :=
  inferInstance

@[to_additive]
instance instMul_4 {M₁ M₂ M₃ M₄ N : Type*} [Mul M₁] [Mul M₂] [Mul M₃] [Mul M₄] [Mul N] :
    Mul (M₁ × M₂ × M₃ × M₄ × N) :=
  inferInstance

end Prod

You don't need both, but the second does have a measurable impact on synthesis time.

[Tomas Skrivan]

For 12 Ks it is slow again

[Tomas Skrivan]

I have built a custom version of lean which throws an error when maximum size is reached i.e. throwing on this line. The whole mathlib recompiles without a problem only in two files Mathlib/Lean/CoreM.lean and Std/CodeAction/Attr.lean the option maxSize has to be increased. Each time it is trying to synthesize instance of typeNonempty (A → ... → Y → Z).

I'm thinking about adding boolean option synthInstance.strictMaxSize. When set to true TC synthesis will throw when it reaches the maximum size. Would it make sense to make a PR?