Dot notation mysteriously speeds up elaborator

Stream: general

[Anne Baanen]

I came across the following interesting performance issue on branch#fun_like:

import analysis.complex.basic
open complex

set_option profiler true

-- master: 10-20 ms
-- to_fun: 10-20 ms
lemma foo {α} (f : α → ℂ) (c : ℂ) (h : has_sum f c) :
  has_sum (λ x, (f x).re) c.re :=
re_clm.has_sum h

-- master: 2 s
-- to_fun: 25 s
lemma foo' {α} (f : α → ℂ) (c : ℂ) (h : has_sum f c) :
  has_sum (λ x, (f x).re) c.re :=
continuous_linear_map.has_sum re_clm h

-- master: 2s
-- to_fun: 25s
lemma bar {α} (f : α → ℂ) (c : ℂ) (h : has_sum f c) :
  has_sum (λ x, (f x).re) c.re :=
h.mapL re_clm

-- master: 2s
-- to_fun: 25s
lemma bar' {α} (f : α → ℂ) (c : ℂ) (h : has_sum f c) :
  has_sum (λ x, (f x).re) c.re :=
has_sum.mapL re_clm h

Looking at the defeq trace, the slow paths try to unify has_sum (λ (x : α), (f x).re) c.re =?= has_sum (λ (b : ?m_2), ⇑?m_12 (?m_13 b)) (⇑?m_12 ?m_14), and because the RHS is so underdetermined get stuck at (f b).re =?= has_coe_to_fun.coe ?m_9 (?m_10 b), because they want to unify re =?= continuous_linear_map.to_fun.