Norm instance on continuous linear maps slow to synthesize

Stream: mathlib4

[Etienne Marion]

Hi! I noticed that this is slow, and it times out in the web editor.

import Mathlib.Topology.Algebra.Module.LinearMap
import Mathlib.Analysis.Normed.Operator.Basic
import Mathlib.Analysis.RCLike.Basic

open ContinuousLinearMap

variable {ι : Type*} [Fintype ι] [DecidableEq ι] {𝕜 : Type*} {E : ι → Type*}
  [∀ i, NormedAddCommGroup (E i)]
  [RCLike 𝕜] [∀ i, NormedSpace 𝕜 (E i)]
  (L : (i : ι) → StrongDual 𝕜 (E i) →L[𝕜] StrongDual 𝕜 (E i) →L[𝕜] 𝕜)
  (i : ι)

#synth Norm (StrongDual 𝕜 (E i) →L[𝕜] StrongDual 𝕜 (E i) →L[𝕜] 𝕜)

I don't know how to investigate/solve this kind of issue, does anyone have any idea please?

[Matthew Ballard]

set_option maxSynthPendingDepth 3 (or something close to that)

[Etienne Marion]

Thanks, this explains why it failed in the editor. So the slowness issue I have in my code comes from somewhere else.