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.
Do you build yourself an instance of the existential? (the instance is the substitutution of all hypothesis of the evar (minus lets IIRC))
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.
I think @Pierre-Marie Pédrot could see if the recent changes in the representation of evars might have affected this code
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.
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
That seems to fix the problem! Thank you very much!
Last updated: Dec 07 2023 at 09:01 UTC