slow coercion from homomorphisms to functions

Stream: mathlib4

[David Loeffler]

I was trying to understand why some of the mathlib code for Fourier transforms takes so long to compile, and I stumbled across the following.

variable (e : ℝ →+ ℝ)

set_option profiler true in
#check e π -- takes 0.25 seconds

It seems that Lean takes 0.25 seconds to realise that ℝ →+ ℝ (bundled additive-group homomorphisms) can be coerced to functions. This seems like an eternity for such a simple term. Is there anything that I can do in my code to make this quicker, other than using "bare" functions and explicitly supplying the compatibility with addition as an explicit hypothesis when I need it (which I'd rather not do, since it's ugly)?

[Eric Wieser]

With what imports?

[Matthew Ballard]

Try it on #8386

[David Loeffler]

Eric Wieser said:

With what imports?

Fourier transforms need a lot of prerequisites, the imports were

import Mathlib.Analysis.Calculus.ParametricIntegral
import Mathlib.Analysis.Fourier.AddCircle
import Mathlib.Analysis.Fourier.FourierTransform

(and the imports inherited from these amount to pretty much all of the algebra, topology and analysis hierarchies).

Matthew Ballard said:

Try it on #8386

That certainly looks relevant, but the PR doesn't merge cleanly at the moment so it's not easy to try anything on it.

[Eric Wieser]

This speeds it up:

instance {A B} [AddZeroClass A] [AddZeroClass B] : CoeFun (A →+ B) (fun _ => A → B) where
  coe := FunLike.coe

[Eric Wieser]

We removed these instances in the port before we understood coercions; we used to have them in Lean 3

[Matthew Ballard]

set_option maxHeartbeats 30 in
#check e π

works on #8386

[David Loeffler]

I got #8386 working and it indeed drastically reduces the time to elaborate this term down to something like 0.002 sec, which seems much far reasonable. Many thanks to @Anne Baanen for #8386 – let's hope it can be merged soon!