type class slowdown: mv_polynomial algebras

Stream: general

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Johan Commelin]

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]

The diff: comm_semiring R instead of comm_ring R

[Sebastien Gouezel]

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]

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]

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

[Rob Lewis]

But I'm not sure how to debug this.

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

Now I have a headache...

[Sebastien Gouezel]

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]

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]

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

[Sebastien Gouezel]

Yes, getting into tactic mode should freeze the cache.

Should we invoke @Gabriel Ebner ?

[Rob Lewis]

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

[Jannis Limperg]

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

[Sebastien Gouezel]

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

[Gabriel Ebner]

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]

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]

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]

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

[Johan Commelin]

This is biting me again :sad:

[Johan Commelin]

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

[Gabriel Ebner]

I think so.

[Johan Commelin]

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