Janno (Sep 30 2020 at 17:54): Janno (Sep 30 2020 at 17:54):Mtac2 calls Evd.existential_type on goal evars (generated by typeclass search) and I am getting Error: Anomaly "Signature and its instance do not match." for the first time. Any hints on what to look for? If I am reading the debug output correctly the goal is of type Z and it is a dependent goal that was shelved during TC search.
Matthieu Sozeau (Sep 30 2020 at 18:38):Do you build yourself an instance of the existential? (the instance is the substitutution of all hypothesis of the evar (minus lets IIRC))
Janno (Sep 30 2020 at 19:28):Yes, I think that is what happens. The code is in https://github.com/Mtac2/Mtac2/blob/master/src/run.ml#L153 but this is the first time I have ever looked at it so I cannot pretend to understand what is going on.
Matthieu Sozeau (Sep 30 2020 at 23:54):I think @Pierre-Marie Pédrot could see if the recent changes in the representation of evars might have affected this code
Janno (Oct 01 2020 at 08:07):Ah, I should have been more specific: this is not on coq/master but rather 8.11 (I know, old stuff..). So I am executing the same code just on a different (TC search) problem. It's very likely that the Mtac2 code is wrong.. I just don't know how to go about debugging it.
Gaëtan Gilbert (Oct 01 2020 at 08:44):I think you may want evar_filtered_hyps instead of evar_hyps here https://github.com/Mtac2/Mtac2/blob/1a5b29321b5574ffe50b4d8aaefbcaad7804d051/src/run.ml#L157
compare https://github.com/coq/coq/blob/1c919ed6fa476f0f7a16d69e58989f3d75104910/engine/proofview.ml#L1094
Janno (Oct 01 2020 at 09:05):That seems to fix the problem! Thank you very much!
Last updated: Dec 07 2023 at 09:01 UTC