performance issues

Stream: general

[Kenny Lau]

#check (by apply_instance : comm_ring α) -- _inst_7
#check (by apply_instance : comm_ring (mv_polynomial σ α)) -- mv_polynomial.comm_ring
#check (by apply_instance : _root_.algebra α (mv_polynomial σ α)) -- algebra.mv_polynomial α σ
set_option pp.implicit true
#check (@«Kähler».add_comm_group α (mv_polynomial σ α) _inst_7 mv_polynomial.comm_ring (algebra.mv_polynomial α σ))
/-
@«Kähler».add_comm_group α (@mv_polynomial σ α (@comm_ring.to_comm_semiring α _inst_7)) _inst_7
  (@mv_polynomial.comm_ring α σ (λ (a b : σ), _inst_6 a b) (λ (a b : α), _inst_8 a b) _inst_7)
  (@algebra.mv_polynomial α _inst_7 (λ (a b : α), _inst_8 a b) σ (λ (a b : σ), _inst_6 a b)) :
  add_comm_group
    (@«Kähler» α (@mv_polynomial σ α (@comm_ring.to_comm_semiring α _inst_7)) _inst_7
       (@mv_polynomial.comm_ring α σ (λ (a b : σ), _inst_6 a b) (λ (a b : α), _inst_8 a b) _inst_7)
       (@algebra.mv_polynomial α _inst_7 (λ (a b : α), _inst_8 a b) σ (λ (a b : σ), _inst_6 a b)))
-/
#check («Kähler».add_comm_group α (mv_polynomial σ α))
/-
@«Kähler».add_comm_group α (@mv_polynomial σ α (@comm_ring.to_comm_semiring α _inst_7)) _inst_7
  (@mv_polynomial.comm_ring α σ (λ (a b : σ), _inst_6 a b) (λ (a b : α), _inst_8 a b) _inst_7)
  (@algebra.mv_polynomial α _inst_7 (λ (a b : α), _inst_8 a b) σ (λ (a b : σ), _inst_6 a b)) :
  add_comm_group
    (@«Kähler» α (@mv_polynomial σ α (@comm_ring.to_comm_semiring α _inst_7)) _inst_7
       (@mv_polynomial.comm_ring α σ (λ (a b : σ), _inst_6 a b) (λ (a b : α), _inst_8 a b) _inst_7)
       (@algebra.mv_polynomial α _inst_7 (λ (a b : α), _inst_8 a b) σ (λ (a b : σ), _inst_6 a b)))
-/

[Kenny Lau]

given that the first four checks are quick, why is the last one slow?

[Kenny Lau]

@Kevin Buzzard this is making me unable to do anything related to A^n

[Kevin Buzzard]

@Floris van Doorn is this anything to do with the timeouts I was having in Amsterdam?

[Kevin Buzzard]

Making instances for structures is an art and it definitely helps if you know how lean is filling in instances. Unification can struggle when presented with two defeq but not syntactically equal instances because its defeq detector might not try hard enough. This means that if you make a new object like one forms or kaehler or whatever you want to call them, you should make sure that the instances that type class inference knows about are such that it has very little chance of getting into such a mess

[Kevin Buzzard]

Floris taught me this in Amsterdam but I don't know if it's your problem

[Kevin Buzzard]

I had more instances than I needed and this was messing things up. Floris fixed it by changing the priority of some of the easier ones to something lower than the default

[Kevin Buzzard]

@Kenny Lau if you look at the type class trace can you see explicitly which instance is being found? Is it syntactically equal to the one you use when it's quick? In other words, is it taking a long time to find syntactically the right instance, or a short time to find a defeq but not syntactically equal instance?

[Kevin Buzzard]

If the latter then you can meddle with the instance priorities, or make some instances local instances, to change the behaviour

[Floris van Doorn]

This might be the same problem.
My suspicion in the 5th #check maybe some implicit (type-class) arguments are different when doing the type-class search (compared to the first 4 checks), which causes trouble for Lean.

[Floris van Doorn]

The problem I had with Kevin in the Perfectoid Project was that we needed to synthesize that some function f : α → β in their project was a group homomorphism. There was an instance f.is_group_hom saying exactly that, except that the instance that β was a group was different in the instance and in the type class problem. In the existing instance it was comm_group.to_group β.comm_group and in the type class problem we had is was comm_group.to_group (linear_ordered_comm_group.to_comm_group β.linear_ordered_comm_group). Here linear_ordered_comm_group is a new class in their project, extending comm_group, with the old structure command turned on. Now the instance of β.linear_ordered_comm_group was defined extending β.comm_group, which means that the equality linear_ordered_comm_group.to_comm_group β.linear_ordered_comm_group = β.comm_group holds definitionally. However, the only way to establish this definitional equality is to establish the definitional equality of all fields. I don't know exactly why, but this was really hard for Lean during type class resolution. It caused a deterministic time-out.

[Floris van Doorn]

The reasons I know/suspect that this was the problem:

• The timeout disappeared when we explicitly gave this (and only this) instance
• The type class trace showed that the instance f.is_group_hom is tried, but never said failed is_def_eq. I think that indicates the timeout happened while this instance was checked.

[Floris van Doorn]

Therefore I think we should adhere to the following guideline, if possible:

If you prove instA : classA X and instB : classB X and classB extends classA then instA should not be an instance. If the instA instance is used, it can cause extra unnecessary unification work during type class inference (if those instances are used as arguments of other definitions/instances). This can cause (deterministic) timeouts. It is especially bad with the old structure command option, and it even happens when both possible instances of classA are definitionally equal.

One problem is that this is not always possible: maybe instA needs fewer or weaker hypotheses. But we should be aware of this potential problem.

[Floris van Doorn]

This guideline is definitely violated for mv_polynomial, so maybe this is the same issue Kenny is facing.

[Floris van Doorn]

As an aside, the reason we were in this mess was that I advised Kevin to use the old structure command for linear_ordered_comm_group, to be more in the mathlib style, and this caused the problem. With the new structure command the issue didn't exist, presumably because the definitional equality linear_ordered_comm_group.to_comm_group β.linear_ordered_comm_group = β.comm_group is really easy in that case (since linear_ordered_comm_group.to_comm_group is then a field of the structure.