## Stream: general

### Topic: type class slowdown: mv_polynomial algebras

#### Rob Lewis (Jul 20 2020 at 13:49):

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_ring R]
(A : Type w) [comm_ring A] [algebra R A]

set_option trace.class_instances true
#check (infer_instance : algebra R (mv_polynomial σ R))

end


The type class search here takes ~2 seconds on my laptop. It's definitely the algebra search that's slow, elaborating the type is fine. What's strange is the search succeeds in two steps. It fails to unify the target with algebra R A, and then finds the corect instance mv_polynomial.algebra. These respectively fail and succeed instantly when I try them outside of the type class search.

#### Rob Lewis (Jul 20 2020 at 13:49):

This seems to be fallout from https://github.com/leanprover-community/mathlib/commit/ce48b6ba77a02430c098f26f3fcc3c11e516179b . The search is instant before that.

#### Rob Lewis (Jul 20 2020 at 13:49):

But I can't tell why it's slow now. Any ideas?

#### Johan Commelin (Jul 20 2020 at 14:16):

This one is instant:

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_semiring R]
(A : Type w) [comm_ring A] [algebra R A]

set_option trace.class_instances true
#check (infer_instance : algebra R (mv_polynomial σ R))

end


#### Johan Commelin (Jul 20 2020 at 14:17):

The diff: comm_semiring R instead of comm_ring R

#### Sebastien Gouezel (Jul 20 2020 at 14:19):

It's really strange, because the instance search output is pretty short in any case, and for the same question apply_instance works instantaneously.

I have no clue about what's going on.

#### Rob Lewis (Jul 20 2020 at 14:25):

It's not the comm_semiring -> semiring search that's at fault. This def is instant and doesn't affect the bad search.

@[instance, priority 1000000] def csr : comm_semiring R := infer_instance


#### Rob Lewis (Jul 20 2020 at 14:25):

Which makes me suspect that some instance is taking a long time to unify or fail to unify.

#### Rob Lewis (Jul 20 2020 at 14:25):

But I'm not sure how to debug this.

#### Sebastien Gouezel (Jul 20 2020 at 14:33):

How do you explain that

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_ring R]

set_option trace.class_instances true

noncomputable lemma foo : algebra R (mv_polynomial σ R) :=
let a := (infer_instance : algebra R (mv_polynomial σ R)) in
infer_instance

end


is also instant?

#### Rob Lewis (Jul 20 2020 at 14:36):

My guess is a caching thing. The type class cache should be frozen after the :=.

#### Sebastien Gouezel (Jul 20 2020 at 14:41):

Yes, it's a cache thing:

import data.mv_polynomial

universes u v w

section

set_option trace.class_instances true

noncomputable example {σ : Type u} (R : Type v) [comm_ring R] : true :=
begin
unfreezingI {let a := (infer_instance : algebra R (mv_polynomial σ R)) },
trivial
end

end


is also slow.

#### Sebastien Gouezel (Jul 20 2020 at 14:46):

And the profiler is totally unhelpful:

set_option profiler true

lemma foo {σ : Type u} (R : Type v) [comm_ring R] : true :=
begin
unfreezingI { let a := (infer_instance : algebra R (mv_polynomial σ R)) },
trivial
end


gives the output

elaboration: tactic execution took 4.25s
num. allocated objects:  35
num. allocated closures: 117
4249ms   100.0%   tactic.to_expr
4249ms   100.0%   tactic.interactive.let._lambda_1
4249ms   100.0%   _interaction._lambda_3
4249ms   100.0%   tactic.focus1
4249ms   100.0%   tactic.step
4249ms   100.0%   tactic.unfreezing._lambda_2
4249ms   100.0%   tactic.istep._lambda_1
4249ms   100.0%   tactic.istep
4249ms   100.0%   _interaction._lambda_2
4249ms   100.0%   scope_trace
4249ms   100.0%   _interaction


#### Rob Lewis (Jul 20 2020 at 15:05):

So this is as minimal as I have it.

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [cr : comm_ring R]
include cr
noncomputable def p : semiring (mv_polynomial σ R) := infer_instance

#check (infer_instance :
@algebra R (@ mv_polynomial σ R (@comm_ring.to_comm_semiring _ cr))
(@comm_ring.to_comm_semiring _ cr) (@p σ R cr))


There's exactly one type class search in the #check. It tries to apply exactly one instance.

#### Rob Lewis (Jul 20 2020 at 15:07):

Uhm. And using by apply_instance instead of infer_instance makes it instant.Maybe because this freezes the instance cache?

#### Sebastien Gouezel (Jul 20 2020 at 15:13):

Yes, getting into tactic mode should freeze the cache.

Should we invoke @Gabriel Ebner ?

#### Rob Lewis (Jul 20 2020 at 15:16):

Poor Gabriel is too popular for his own health, hah.

#### Jannis Limperg (Jul 20 2020 at 15:26):

I should walk over and remind him that all this research business is interfering with his Lean maintenance duties. :upside_down:

#### Sebastien Gouezel (Jul 20 2020 at 15:28):

Isn't he on holidays? We should definitely not interfere with the holidays!

#### Gabriel Ebner (Jul 20 2020 at 16:04):

Is this lean#397? If not, please file an issue. I'm back from holidays but occupied by another project for the next two days.

#### Rob Lewis (Jul 20 2020 at 16:10):

It's not directly the same but could be related. I'll file it separately for when you have time. Thanks as always!

#### Floris van Doorn (Jul 20 2020 at 17:15):

Rob Lewis said:

Uhm. And using by apply_instance instead of infer_instance makes it instant.Maybe because this freezes the instance cache?

I've noticed infer_instance being worse than by apply_instance in multiple cases. I think in those cases usually infer_instance fails and by apply_instance succeeds. My personal workaround is just to never use infer_instance anymore.

#### Johan Commelin (Jul 20 2020 at 17:15):

But this is a MWE extracted from a situation where we use neither, I think

#### Johan Commelin (Jul 22 2020 at 12:23):

This is biting me again :sad:

#### Johan Commelin (Jul 22 2020 at 16:37):

@Gabriel Ebner do you think that lean#403 also fixes this issue?

I think so.

#### Johan Commelin (Jul 23 2020 at 09:32):

@Gabriel Ebner Cool! Any idea about when you want to release a new Lean? (-;

Last updated: May 10 2021 at 00:31 UTC