(I hope this is right here, if not I'd be thankful if someone moved it to Coq users)

For a plugin I'm writing I need to generate a match statement generalized by the corresponding equality like Program does, as part of constructing a larger term. I haven't found any existing matching mechanism that I can use (at least I don't think I can use constrexpr's since I'm working with EConstr.constr terms and there doesn't seem to be a way to reference them inside constrexprs), so I'm attempting to manually compile them.

However, when generating even a small match with an inferred evars I get an error message I don't understand.

e.g. when matching on a natural number:

match ?n as H return (?n = H -> nat) with

| 0 => fun _ : ?y1 => 0

| S _ => fun _ : ?y => 0

end

If I annotate ?y1 explicitly it works, but if I let it be inferred, I get

Error: In pattern-matching on term "?n" the branch for constructor

"S" has type "nat -> ?T -> nat" which should be

"forall H : nat, ?n = S H -> nat".

Why does the inference fail here? Do I need to do something special while generating the evars? After all it works if one defines the term with these holes in Coq itself.

I get "unknown existential variable" on `Check (your code)`

, do you have an actual example?

I probably should have mentioned that I was printing the term using Printer.pr_econstr.

Do you want the ocaml code I used to generate the example term? I'm not sure how best to share it.

Maybe I'm just confused about how Coq does its type inference.

I thought this:

Check (fun n => match n as H return (n = H -> nat) with

| 0 => fun _ => 0

| S _ => fun _ => 0

end). (which works without issue)

would insert existential variables like if I generate them using Evarutil.new_evar. Is this not the case?

I've attached both a file containing just the code to generate the failing example and a zip of it embedded into the coq plugin template so that it can be run directly with dune build

matchtest.ml matchtest.zip

it seems you generate all evars in the global env, meaning they don't have access to the variables from the context. this is a problem for the S branch: as the error indirectly tells you by printing one side as an arrow and the other as a forall `?y`

needs access to the nat from the S

Ah, yes, that's it, thank you very much!

Daniel Kuhse has marked this topic as resolved.

Last updated: Nov 29 2023 at 17:01 UTC