Janno (Jan 12 2022 at 12:24): Janno (Jan 12 2022 at 12:24):I am observing a discrepancy between Retyping.relevance_of_type on template polymorphic and properly polymorphic/monomorphic inductives applied to unbound Rels. I am using Ltac2 to trigger this but the trace shows pretty clearly that it only really concerns Retyping.relevance_of_type and nothing Ltac2-specific.
Inductive tmplpoly := .
Fail Ltac2 Eval Binder.make None (make (appL '@tmplpoly [make (Rel 1)])).
(* Uncaught exception Retyping.RetypeError(0) *)
#[universes(polymorphic)] Inductive poly (T:Type) := .
Ltac2 Eval Binder.make None (make (appL '@poly [make (Rel 1)])). (* Works fine. *)
#[universes(monomorphic)] Inductive mono (T:Type) := .
Ltac2 Eval Binder.make None (make (appL '@mono [make (Rel 1)])). (* Works fine. *)
I suspect this is a bug but I don't know what to expect from this. My code currently relies on Binder.make accepting terms with unbound Rels so to me this a bug with template polymorphic inductives. But I am wondering now how one can determine the relevance of an unbound Rel.
Gaëtan Gilbert (Jan 12 2022 at 12:27):we could make this one work, but in general unbund rels won't work out well
Janno (Jan 12 2022 at 12:34):Should I create my own alternative Binder.make version that always picks Relevant? I see that the docs mention caveats there but we don't (yet) use SProp so this might be OK for now. The alternative fix is to always extend the local environment when working under binders. That can be quite annoying in Ltac2 but maybe I just need to write some new primitives for that.
Janno (Jan 13 2022 at 10:42):How do plugins deal with the choice of relevance when generating binders? I doubt everybody writing plugin code has a solid strategy for supporting SProp, or do they?
Pierre-Marie Pédrot (Jan 13 2022 at 10:42):nope, and that's why using SProp is currently a hell
Janno (Jan 13 2022 at 10:43):Hmm
Pierre-Marie Pédrot (Jan 13 2022 at 10:43):most of the code was ported setting Relevant everywhere, which is somewhat sensible but not very correct
Pierre-Marie Pédrot (Jan 13 2022 at 10:44):the net result is that when you use SProp you get weird conversion errors here and there between terms that are literally the same
Pierre-Marie Pédrot (Jan 13 2022 at 10:45):About Ltac2, we should probably provide primitives similar to the ones we have in OCaml to manipulate terms under contexts
Janno (Jan 13 2022 at 10:45):I wonder now if maybe Ltac2 is doing the wrong thing by trying to infer relevance for binders. Why not let the user pick something? Because it seems in general the answer will have to be Relevant anyway, especially when the types involved have unbound Rels in them.
Pierre-Marie Pédrot (Jan 13 2022 at 10:47):I think that this reflects the poor API we have currently on the OCaml side, we're erring between different design choices and the current situation is not very satisfactory
Pierre-Marie Pédrot (Jan 13 2022 at 10:48):it's very unsafe to let the user pick whatever they want, so it makes sense to have something automatic by default
Pierre-Marie Pédrot (Jan 13 2022 at 10:49):there used to be an explicit API in Ltac2 as well, so everything is moving everywhere
Janno (Jan 13 2022 at 10:49):Pierre-Marie Pédrot said:
About Ltac2, we should probably provide primitives similar to the ones we have in OCaml to manipulate terms under contexts
What kind of primitives are those? I've always thought Mtac's \nu operator was very intuitive. It's a scoped addition to the context. For some reason it does named variables only but I don't see why something like that wouldn't work for Rels.
Pierre-Marie Pédrot (Jan 13 2022 at 10:49):we have map / fold under contexts notably
Pierre-Marie Pédrot (Jan 13 2022 at 10:51):I am open to proposals for extending the Ltac2 API in a palatable way, btw
Pierre-Marie Pédrot (Jan 13 2022 at 10:52):also the OCaml representation of relevance is bound (no pun intended) to change soon
Janno (Jan 13 2022 at 10:52):Do these primitives extend the local environment so that e.g. Retyping.relevance_of_type would work correctly when working under binders?
Pierre-Marie Pédrot (Jan 13 2022 at 10:52):not in OCaml but we could do that in Ltac2
Pierre-Marie Pédrot (Jan 13 2022 at 10:52):(because there is no such thing as "the local environment" in OCaml)
Janno (Jan 13 2022 at 10:53):Everything needs an env to function correctly, doesn't it? That's what I call the local environment. A bit of a misnomer I guess
Pierre-Marie Pédrot (Jan 13 2022 at 10:54):not necessarily, and there are several notions of environment in the tactic monad
Janno (Jan 13 2022 at 10:55):Ah, yes, I have suffered from picking the wrong environment. There is the one of the monad and the one of the current goal, at least, I think.
Pierre-Marie Pédrot (Jan 13 2022 at 10:55):the ones of the the current goals
Janno (Jan 13 2022 at 10:55)::)
Janno (Jan 13 2022 at 10:56):I am not sure if this just me but I see a mismatch here between the ability to unsafely create terms and the reliance on the implicit local environment on the Ltac2 side. If am free to create unbound Rels, then I really want all the rest of the API to be as resilient as possible, right?
Janno (Jan 13 2022 at 10:57):Maybe this is some kind of inherent tension between Ltac2 the tactic language and Ltac2 the metaprogramming language
Pierre-Marie Pédrot (Jan 13 2022 at 10:57):it just means we need two kinds of APIs
Pierre-Marie Pédrot (Jan 13 2022 at 10:58):one for manipulating raw untyped terms, very unsafe and you know what you're doing
Pierre-Marie Pédrot (Jan 13 2022 at 10:58):and another one for the casual user that wants high-level operators
Pierre-Marie Pédrot (Jan 13 2022 at 10:58):thankfully we have functions rather than hardwired notations in Ltac2, so it's just a matter of exposing that
Janno (Jan 13 2022 at 10:58):That does sound reasonable to me
Pierre-Marie Pédrot (Jan 13 2022 at 10:59):(you could even implement the high level one through the low-level one, if you wanted so)
Janno (Jan 13 2022 at 10:59):It also suggests that my short-term fix will be exposing a version of Binder.make that either hardcodes Relevant or lets me copy the relevance from an existing binder (which would cover most of my use cases.)
Pierre-Marie Pédrot (Jan 13 2022 at 11:00):just expose the low-level binder making function that takes an explicit relevance, as it used to be
Pierre-Marie Pédrot (Jan 13 2022 at 11:00):you might simply revert the commit that removed it...
Janno (Jan 13 2022 at 11:05):That commit also bundled the type of the binder into the binder type itself so reverting it would be a bit chaotic. In any case, I won't patch Ltac2 itself but I'll expose these old binder functions. It's much easier to get people to recompile our local development than it is to get them to recompile Coq (really just Ltac2 but it's the same opam package IIRC)
Paolo Giarrusso (Jan 13 2022 at 11:46):BTW is relevance only needed when binding (S : SProp) or members of an SProp? Or also when binding datatypes that contain SProp?
Gaëtan Gilbert (Jan 13 2022 at 11:48):for binding x : P : SProp
Last updated: Apr 20 2024 at 08:02 UTC