Zulip Chat Archive

Stream: general

Topic: Type inference timing out


view this post on Zulip Devon Tuma (Nov 24 2020 at 03:19):

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

view this post on Zulip Rob Lewis (Nov 24 2020 at 03:28):

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

view this post on Zulip Devon Tuma (Nov 24 2020 at 03:43):

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

Last updated: May 13 2021 at 17:42 UTC