Luko van der Maas (Dec 06 2023 at 09:55): Luko van der Maas (Dec 06 2023 at 09:55):I am getting an error Error: Ill-typed evar instance, I have found which term it is talking about and at what line of code it happens, but the term contains several evars and they all look good to me, so I was wondering. Is there a way to know which evar is ill-typed? Then I can try to provide more type information.
Enrico Tassi (Dec 06 2023 at 10:08):I believe this is another manifestation of the same bug we did look at. When the evar is applied to a wrong number of arguments it is inherently illtyped. Can you confirm you are in a section?
Luko van der Maas (Dec 06 2023 at 11:38):Yes I am
Luko van der Maas (Dec 07 2023 at 15:04):I was testing some more, and it also happens out of a section.
Luko van der Maas (Dec 07 2023 at 15:04):I have also removed all holes from the term and I still get the same error
Luko van der Maas (Dec 08 2023 at 15:30):it might be similar to this https://github.com/LPCIC/coq-elpi/issues/523
Luko van der Maas (Dec 13 2023 at 14:22):I was looking through the backtrace of the error and saw that it backtracked to https://github.com/coq/coq/blob/master/pretyping/evarsolve.ml#L903 Which has the following contents:
let check_evar_instance_evi unify flags env evd evi body =
let evenv = evar_env env evi in
(* FIXME: The body might be ill-typed when this is called from w_merge *)
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
Thus it might be a coq bug?
Luko van der Maas (Dec 14 2023 at 11:47):It looks like it was a bug on my end and the error message was a bit unclear
Last updated: Oct 13 2024 at 01:02 UTC