Stream: MetaCoq

Topic: Infer implicit types during unquoting


view this post on Zulip Louise Dubois de Prisque (Nov 08 2021 at 15:40):

Hello everyone,
Is there a way to let the unquote mechanism infer implicit types ? For instance, if I quote the term eq I will get a reified term applied to a tEvar but using this reified evar leads me to an error message if I try to unquote an refied equality which uses it :

MetaCoq Quote Definition eq_reif := eq.
MetaCoq Quote Definition one_reif := 1.
Definition mkEq u v := tApp eq_reif [u; v].
Definition foo_reif := mkEq one_reif one_reif.

MetaCoq Unquote Definition foo := (mkEq one_reif one_reif). (* Anomaly "Evar ?X135 was not declared." Please report at http://coq.inria.fr/bugs/.*)

Thanks in advance for your help !

view this post on Zulip Yannick Forster (Nov 08 2021 at 15:47):

Hey Louise! Yes, you can use a hole:

(* Distributed under the terms of the MIT license. *)
From MetaCoq.Template Require Import utils All.

Import MCMonadNotation.

MetaCoq Quote Definition eq_reif := @eq.
MetaCoq Quote Definition one_reif := 1.
Definition mkEq u v := tApp eq_reif [hole; u; v].
Definition foo_reif := mkEq one_reif one_reif.

MetaCoq Unquote Definition foo := (mkEq one_reif one_reif).
Print foo.

view this post on Zulip Yannick Forster (Nov 08 2021 at 15:47):

Note that I inserted an @ in front of eq in eq_reif

view this post on Zulip Louise Dubois de Prisque (Nov 08 2021 at 15:48):

Thank you very much for your help!

view this post on Zulip Yannick Forster (Nov 08 2021 at 15:55):

The reason for the @ is that eq has an implicit argument (as can be verified using About), and eq is really @eq ?evar with ?evar being an evar of type Type. In general, I would always use @ when quoting constants in MetaCoq, otherwise you can get strange behaviour

view this post on Zulip Louise Dubois de Prisque (Nov 08 2021 at 16:01):

Do you have a pointer to the evar mechanism in MetaCoq since the main article says it was not implemented at that time ? I am curious about knowing precisely why it is not possible to use the reified evar generated while quoting eq (so @eq ?evar) instead of @eq

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 16:05):

Using the evar directly would not be the expected behaviour I think. If in the future we support evar, unquoting a term with evars should just produce a term with evars don't you think?

view this post on Zulip Yannick Forster (Nov 08 2021 at 16:06):

There is no pointer, because evars are still not properly treated. I don't think anything changed w.r.t. the main article: If you end up with a tEvar after an unquote you are stuck. The only way to morally use evars is via hole

view this post on Zulip Pierre Vial (Nov 08 2021 at 16:07):

@Théo Winterhalter What do you mean "by supporting evar" ? You mean that currently, the complex mechanisms of unification for evars are not formalized in MetaCoq and that it's Coq which is used in the example given by Yannick?

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 16:08):

Yes, there is no unification in MetaCoq at all.
But beyond that, we don't even update the evar map (which collects the constraints and instantiations) I think.

view this post on Zulip Pierre Vial (Nov 08 2021 at 16:10):

Is there unification in the kernel of Coq?

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 16:11):

We're going to areas where I'm not an expert but I don't believe unification is part of the kernel but of elaboration.

view this post on Zulip Louise Dubois de Prisque (Nov 08 2021 at 16:16):

So why the evar tEvar fresh_evar_id [] which corresponds to the term hole is treated by the unquote function?

view this post on Zulip Yannick Forster (Nov 08 2021 at 16:17):

Don't look behind the hole :) It's implemented as an evar, but the right slogan to keep in mind is that evars are not implemented properly and are not treated by the quoting and unquoting mechanisms

view this post on Zulip Louise Dubois de Prisque (Nov 08 2021 at 16:19):

Okay, so if one day the evars are treated by the quoting and unquoting mechanism, I guess that hole would also be implemented differently

view this post on Zulip Yannick Forster (Nov 08 2021 at 16:20):

Yes, I would say that once they are treated properly the more ad-hoc solution with holes goes away. You could but an arbitrary evar there and then run tmUnquote in a way such that evars are solved

view this post on Zulip Meven Lennon-Bertrand (Nov 09 2021 at 13:26):

Pierre Vial said:

Is there unification in the kernel of Coq?

No, but there are evars: AFAIK you must be able to type the term without further solving those evars (so for instance the kernel would type-check refl ?evar : ?evar = ?evar but not refl tt : tt = ?evar while the second one would be treated by the elaboration by unifying tt and ?evar).

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 13:29):

no, the kernel rejects evars

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 13:29):

https://github.com/coq/coq/blob/21e199784cb8330086b815972c3639c18469d497/kernel/typeops.ml#L611

view this post on Zulip Meven Lennon-Bertrand (Nov 09 2021 at 13:29):

Ah, my bad!

view this post on Zulip Meven Lennon-Bertrand (Nov 09 2021 at 13:31):

I mixed it up with what happens/ed in Matita

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2021 at 16:10):

@Gaëtan Gilbert depends on what you call the kernel, to share code we try to be as resilient as possible w.r.t. evars in the kernel API

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2021 at 16:10):

conversion handles them as variables for instance

view this post on Zulip Enrico Tassi (Nov 12 2021 at 10:23):

Does it? It should have a reflexivity rule for them, not sure it does.


Last updated: Aug 11 2022 at 02:03 UTC