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
That seems to fix the problem! Thank you very much!
Last updated: Dec 07 2023 at 09:01 UTC