inexplicably slow type class inference

[robertylewis]

To add yet another problem to @gebner 's plate:

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))

The infer_instance is quite slow on my laptop (~2 sec) even though it succeeds with the first instance it tries. Changing infer_instance to by apply_instance, or rephrasing it to appear after the := of an example, makes the inference instant. This suggests it might have something to do with an unfrozen cache.

I really don't know where this is coming from so I'm not sure how to un-mathlib it.

Possibly related to #397

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.