more possible type class caching opportunities

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.

Start with the embedded Lean reproducer in issue #467 and run it with set_option trace.class_instances true to confirm the repeated search. Then trace the type-class instance lookup implementation, which the issue does not identify, and determine whether preserving the cache is safe. Done means a validated caching approach with evidence that the redundant searches no longer occur.