deterministic timeout with ideal.quotient.mk

Stream: general

[Aditya Agarwal]

I am getting a deterministic timeout when I try to state ideal.quotient.mk (ideal.span (singleton (C r))) p = 0 in the context of an integral domain.
@Scott Morrison has constructed a minimal example here : https://github.com/chocolatier/theoremproving/blob/master/src/timeout-mwe.lean , And done some debugging work.

variables {α : Type} [integral_domain α]
lemma timeout {p : polynomial α} {r : α} : ideal.quotient.mk (ideal.span (singleton (C r))) p = 0 := sorry

times out, but replacing integral_domain αwith comm_ring αmakes it work. Setting trace.class_instances true shows that the type class resolution is going crazy in the integral domain case.

Specifically, it is trying to find an instance of has_zero but it gets stuck in the path that searches for @no_zero_divisors.to_has_zero, and never tries any other branch.

I'm not sure why this is happening or how to fix it.

[Mario Carneiro]

did you try increasing the instance depth?

[Aditya Agarwal]

I've tried

set_option class.instance_max_depth 1000000

but it still times out.

[Scott Morrison]

Hi @Chris Hughes and @Kenny Lau, do you know what could be going on here?

[Kenny Lau]

does ideal.span take two arguments?

[Kenny Lau]

what is singleton?

[Scott Morrison]

There's a gist of the typeclass resolution for 0 on the rhs going nuts here: https://gist.githubusercontent.com/semorrison/fc7fd83ee0da4a875db083c01ef7a0fc/raw/80e4adb669a5be6a9b4e602972e48d0d054bae1d/gistfile1.txt

[Kenny Lau]

I'm half convinced that ideal isn't the problem, polynomial is

[Kenny Lau]

I have no idea why it doesn't work