tricky failure with type-class inference

Stream: lean4

[Floris van Doorn]

I found a weird failure of type-class inference, and I am unable to minimize it, and therefore depends on Mathlib.

import Mathlib.Analysis.InnerProductSpace.Calculus
import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap

set_option trace.Meta.synthInstance true
example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace E] [OpensMeasurableSpace E]
  (f : H → E) (g : E →L[ℝ] H) : Measurable (fun x : E ↦ ‖g‖₊) := by
  -- let z : NormedAddCommGroup (E →L[ℝ] H) := by infer_instance -- this works
  refine Measurable.nnnorm ?_ -- this works, but caches a failure of `NormedSpace ℝ H`
  have : fderiv ℝ f (0 : H) = 0 := sorry -- ... which causes this to fail

The problem is that my refine succeeds, but caches a failure of NormedSpace ℝ H when trying to synthesize NormedAddCommGroup (E →L[ℝ] H). This causes the last line to fail. Commenting out the refine line fixes the error on the next line.
Making minor modifications does not cause this cached failure (see commented line). Here is the relevant part of the type-class trace. (The instance InnerProductSpace.toNormedSpace should unify, and does in the commented-out line.)
image.png