more possible type class caching opportunities

[robertylewis]

There were some amazing performance increases earlier this year from improved instance caching. I just noticed another situation where redundant searches are performed. Note that I don't really know the implementation details here, so maybe there are reasons the cache can't be preserved here, but it seems plausible.

In the code below, add_comm assumes an add_comm_semigroup instance. The search from add_comm_group to add_comm_semigroup is repeated twice.

import algebra.group

set_option trace.class_instances true 
example {α} [add_comm_group α] (a b c : α) : (a + b) + c = c + (b + a) :=
begin 
  rw [add_comm, add_comm a],
end

Prerequisites

• [ ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.