Stream: Coq devs & plugin devs

Topic: Anomaly "Signature and its instance do not match"


view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Janno (Oct 01 2020 at 09:05):

That seems to fix the problem! Thank you very much!


Last updated: Oct 16 2021 at 07:02 UTC