ftrans applies incorrect rule

[lecopivo]

ftrans fails in the following example with the error

failed to synthesize
   SemiInnerProductSpace K (X → X)

which is indication that is has to be applying incorrect rule

example
  (f : Y → Z) (g : X → Y) 
  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
  : revDerivUpdate K (fun x : X => f (g x))
    = 
    fun x =>
      let ydg := revDerivUpdate K g x
      let zdf := revDerivUpdate K (fun x' => f (ydg.1 + semiAdjoint K (ydg.2 · 1 0) (x' - x))) x
      zdf := 
by
  have ⟨_,_⟩ := hf
  have ⟨_,_⟩ := hg
  unfold revDerivUpdate
  funext _; 
  ftrans -- error