Type inference timing out

Stream: general

[Devon Tuma]

I've come across an issue where having adding is_prime I to the context causes lean to timeout. This only became an issue after merging the latest master branch, and used to build just fine. This should be close to a MWE, when I uncomment the is_prime instance I get a (deterministic) timeout:

example {R : Type*} [comm_ring R] (I : ideal (polynomial R)) --[is_prime I]
  : R :=
begin
  let R' : subring I.quotient := ((quotient.mk I).comp C).range,
  letI : comm_ring R' := subring.to_comm_ring R',
  letI : comm_ring (polynomial R') := polynomial.comm_ring, -- timeout here
  exact 0,
end

[Rob Lewis]

What's the full MWE with imports and open namespaces?

[Devon Tuma]

Sorry, this should be a full example:

import ring_theory.ideal.over

namespace ideal
open polynomial

example {R : Type*} [comm_ring R] (I : ideal (polynomial R)) --[is_prime I]
  : R :=
begin
  let R' : subring I.quotient := ((quotient.mk I).comp C).range,
  letI : comm_ring R' := subring.to_comm_ring R',
  letI : comm_ring (polynomial R') := polynomial.comm_ring, -- timeout here
  exact 0,
end

end ideal