The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Thu, Aug 18, 2016 at 9:12 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

It's more likely to be failing unifications that take a long time indeed. It's easy to check which it is using Set Typeclasses Depth 0 which will make resolution fail immediately. Maybe using Hint Opaque foo : rewrite. for a few constants you don't want to unfold during unification of the lemma would help (these hints are used by setoid_rewrite).

Matthieu,

Thanks for the hints. I tried setting depth to 0 and `setoid_rewrite` fails immediately showing bunch of unsatisfied evars. Does that mean that the problem is not in unification?

Interestingly setting the depth to 4 makes it work! This is not the first time I am having this problem. I just want to understand the mechanics of all this to be able to debug and avoid such problems in future.

This case is a particularly good example to study the problem because:

1. It is using very simple lemma to rewrite (`comp_assoc` does not have any additional typeclass constraints) 

2. It uses Leibniz equality, so I am sure I am not missing any `Proper` instances.

I am going to collect debug logs for depth 4 when it works and larger depth where it gets stuck, to see what branch of search tree it stucks in. Any other ideas on what to look at or to try to get to the bottom on this issue are very welcome!

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060