# Zulip Chat Archive

## Stream: general

### Topic: performance issues

#### Kenny Lau (Jul 13 2019 at 09:38):

#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 (Jul 13 2019 at 09:38):

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

#### Kenny Lau (Jul 13 2019 at 10:13):

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

#### Kevin Buzzard (Jul 13 2019 at 11:06):

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

#### Kevin Buzzard (Jul 13 2019 at 11:09):

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 (Jul 13 2019 at 11:10):

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

#### Kevin Buzzard (Jul 13 2019 at 11:35):

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 (Jul 13 2019 at 11:40):

@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 (Jul 13 2019 at 11:41):

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

#### Floris van Doorn (Jul 13 2019 at 21:45):

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 (Jul 13 2019 at 21:45):

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 (Jul 13 2019 at 21:46):

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 (Jul 13 2019 at 21:49):

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 asargumentsof 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 (Jul 13 2019 at 21:49):

This guideline is definitely violated for `mv_polynomial`

, so maybe this is the same issue Kenny is facing.

#### Floris van Doorn (Jul 13 2019 at 21:51):

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.

Last updated: May 10 2021 at 18:22 UTC