Jacob Salzberg (Jan 02 2024 at 23:39): Jacob Salzberg (Jan 02 2024 at 23:39):Hi, I tried using Coq on nested instances here, and it out of memories when I try to Check the type of the final lemma:
https://paste.rs/XJ4jF
Is there any workaround? Thanks :-)
Ike Mulder (Jan 03 2024 at 08:40):If you Set Typeclasses Debug., you'll notice that Check transitive_pair. actually starts typeclass instance search. And this search looks quite bad: it looks for an instance of DecEq ?T with ?T an evar, and applies the i_beq_pair instance.
This unifies ?T with a pair ?T1 * ?T2 (which is probably not what you want), but it also recursively starts two new typeclass instances searches for DecEq ?T1 and DecEq ?T2. This process then repeats and never terminates.
In this case, you should add a Hint Mode to DecEq, instructing typeclass search that the type ?T is an input to the search. Concretely, adding Global Hint Mode DecEq ! : typeclass_instances. makes Check return immediately. See also here.
Pierre Courtieu (Jan 03 2024 at 08:45):Nothing to add, except a small hint: To see the type of a constant without triggering instance search you can either do Check @constant or better: About constant.
Karl Palmskog (Jan 03 2024 at 09:10):typically, diverging typeclass search is "caused" by lack of proper hint modes for some class declaration. See for example here: https://github.com/damien-pous/coinduction/pull/14
Last updated: Oct 13 2024 at 01:02 UTC