Deterministic timeout

Stream: general

[Heather Macbeth]

This gives a deterministic timeout for me:

import data.polynomial.basic

variables {F : Type*} [ring F]

example (X : polynomial F) (h : (5 : polynomial F) + 3 * X * X = 0) :
  4 + 4 * X * X = 0 :=
begin
  convert h using 1,

end

Can someone reproduce it and/or explain it?

[Floris van Doorn]

Without trying to reproduce this, this is probably related to #4678, and the reason is that convert tries to apply refl (which likely fails, but causes a lot of unfolding).

[Heather Macbeth]

Thanks!