Fix #3357, mark implicit arguments in Notations #668

psteckler · 2017-05-22T20:09:56Z

Notations were converting implicit arguments to explicit arguments in notations when using the NProd and NLambda constructors of notation_constr, because there was nothing in those constructors to mark implicitness.

Adding a binding_kind field for those constructors allows marking implicitness, and propagating it to the stored pattern.

The test 3357.v has the Fail removed, and the file moved to bugs/closed/.

herbelin

Looks good but there are a couple of cases to check in the function used for printing (Notation_ops.match_). See the annotated code which tells which bk must be matched again a bk in the glob_constr, which are necessaritly Explicit by construction (those which are used to catch a binder which is part of a recursive binder) and thus deserve an assert, and thus that apply only when with Explicit (the eta case).

Also, those NLambda and NProd used to catch a binder which is part of a recursive binder should conventially be written without { } (i.e. it makes no sense to write Notation "lambda {x} .. {y} => t" := ... (x binder, y binder, ...).). Thus, there should be an error if the GLambda and GProd in the aux part of compare_recursive_parts of notation_ops.ml expose a Implicit. (I could not comment on the diff since it is not in the diff.)

On a more general note, since the kernel drops Explicit/Implicit (*), a notation with a { } shall never be reused to print a term from the kernel.

(*) Maybe it should not drop them, but as it is now, it does. I always found frustrating to write thinks like

Lemma L (f:forall {A}, A -> A) : foo.

and see f : forall A, A -> A instead of f : forall {A}, A -> A in the hypotheses.

herbelin · 2017-05-22T22:01:57Z

interp/constrintern.ml

        when Name.equal na na' ->
        let subinfos,na = traverse_binder subst avoid subinfos na in
        let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
 	GProd (loc,na,Explicit,ty,aux subst' subinfos c')
-    | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
+    | NLambda (na,_,NHole(Evar_kinds.BinderType na',naming,arg),c')


In all those four cases, I would say that we should have an assertion bk = Explicit

herbelin · 2017-05-22T22:05:16Z

interp/notation_ops.ml

      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
      let alp,sigma = bind_bindinglist_env alp sigma x decls in
      match_in u alp metas sigma b termin

  (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,_,b2),termin)->


In the NBinderList cases, one should also have the assertion bk2 = Explicit

herbelin · 2017-05-22T22:05:33Z

interp/notation_ops.ml

      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
      let alp,sigma = bind_bindinglist_env alp sigma x decls in
      match_in u alp metas sigma b termin

-  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
+  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,_,b2),termin)


herbelin · 2017-05-22T22:06:33Z

interp/notation_ops.ml

      when is_bindinglist_meta id metas ->
      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
      match_in u alp metas sigma b1 b2
-  | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
+  | GProd (_,na,bk,t,b1), NProd (Name id,_,_,b2)
      when is_bindinglist_meta id metas && na != Anonymous ->


Idem for these case where the NLambda and NProd are placeholders for a sequence of binders.

herbelin · 2017-05-22T22:07:06Z

interp/notation_ops.ml

     match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) ->
+  | GProd (_,na1,_,t1,b1), NProd (na2,_,t2,b2) ->
     match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2


In those cases however, one should have the same bk on the lhs and rhs.

herbelin · 2017-05-22T22:13:42Z

interp/notation_ops.ml

@@ -1090,7 +1090,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
     otherwise how to ensure it corresponds to a well-typed eta-expansion;
     we make an exception for types which are metavariables: this is useful e.g.
     to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
-  | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+  | b1, NLambda (Name id as na,_,(NHole _ | NVar _ as t2),b2) when inner ->


For the eta-expansion, one need to match exactly an Explicit for the expansion to make sense.

Typical situation: we don't want to identify let y := fun {A} => g A in t with let y := g in t as this would break the implicit argument of y.

psteckler · 2017-05-22T22:34:24Z

Thanks, I somehow knew it wasn't that simple! I'll make these changes soon.

psteckler · 2017-05-23T16:03:09Z

I've made the changes suggested in the code comments.

Looking into the Implicit check in compare_recursive_parts.

psteckler · 2017-05-23T16:37:46Z

@herbelin I've added a check for implicit argument in the aux part of compare_recursive_parts. You should confirm it's OK.

psteckler · 2017-05-23T21:11:52Z

In fiat-crypto run by Travis, one of the new asserts failed, at line 686 in constrintern.ml. Not sure what to make of that.

JasonGross · 2017-05-23T21:33:50Z

Here is a small test-case that succeeds in v8.6 and triggers the anomaly here:

Local Notation foo := (forall {n : nat}, n = n).
Definition bar : foo := fun _ => eq_refl.
Check bar _ : _ = _.

Of course, the implicit status doesn't actually get set in v8.6, but if you're not supporting implicit status, then it should be an error message, not an anomaly.

psteckler · 2017-05-23T21:37:10Z

Currently, the check for implicit arguments is done by assertion. We could change them to errors.

JasonGross · 2017-05-23T22:20:49Z

Yeah, an error would be better. Anomalies are for code that should be impossible to reach, not for when the user gives Coq garbage input.

Is there any reason, though, that Coq can't support this use-case?

psteckler · 2017-05-23T22:38:33Z

@JasonGross Unfortunately, my force-push deleted @herbelin 's original review comments that asked for these asserts. Maybe he can look at this particular use-case.

JasonGross · 2017-05-23T22:57:40Z

You mean #668 (comment) ? (I think you can expand the hidden review comments.)

psteckler · 2017-05-24T15:20:31Z

Yes, I meant those comments. I can see them again now, maybe the page was stale in my browser when I tried yesterday.

psteckler · 2017-05-24T15:25:33Z

I can turn any of these new asserts into errors, but maybe some of them are indeed sanity checks, rather than limitations on user input, so we should clarify which are which.

herbelin · 2017-05-24T15:48:36Z

interp/notation_ops.ml

+      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2)
+  | GProd (_,na1,bk1,t1,b1), NProd (na2,bk2,t2,b2) ->
+     (assert (bk1 = bk2);
+      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2)


Hi Paul, the anomaly comes from here presumably. These two assert should be when binding_kind_eq bk1 bk2 (but an "=" should be ok also).

@herbelin Thanks, should any of the other asserts in the diffs also be turned into guards?

Should be ok, I think.

psteckler · 2017-05-24T17:20:57Z

I've changed the assert identified by @herbelin to a guard, also the neighboring similar match-case.

There may be others to change to guards, or to errors.

JasonGross · 2017-05-24T17:27:50Z

I'd suggest also adding an output test-case in notations that makes use of implicit binders, since apparently there wasn't one before:

Notation foo := (forall {n : nat}, n = n).
Axiom f0 : foo. Check f0 _ : _ = _.
Notation "&& x .. y , B" := (forall x , .. (forall y , B) .. ) (at level 0, x binder, y binder).
Axiom f1 : && x y , (x = y :> nat). Check f1 _ _ : _ = _.
Notation "&& x .. y , B" := (forall x , .. (forall {y} , B) .. ) (at level 0, x binder, y binder).
Axiom f2 : && x y , (x = y :> nat). Check f2 _ _ : _ = _.
Notation "&& x .. y , B" := (forall {x} , .. (forall {y} , B) .. ) (at level 0, x binder, y binder).
Axiom f3 : && x y , (x = y :> nat). Check f3 _ _ : _ = _.
Notation "&& x .. y , B" := (forall {x} , .. (forall y , B) .. ) (at level 0, x binder, y binder).
Axiom f4 : && x y , (x = y :> nat). Check f4 _ _ : _ = _.

(Should that be Check f0 _ : _ = _ or Check f0 : _ = _?)

ejgallego · 2017-05-24T17:47:13Z

I'd like to have a look into this before merging if not urgent, thanks!

herbelin · 2017-05-24T17:49:43Z

interp/notation_ops.ml

+  | GLambda (_,Name x,bk1,t_x,c), GLambda (_,Name y,bk2,t_y,term)
+  | GProd (_,Name x,bk1,t_x,c), GProd (_,Name y,bk2,t_y,term) ->
+     if (bk1 = Implicit || bk2 = Implicit) then 
+       error "Implicit arguments found in recursive parts of a binder"


By the way, an improvement: one could use user_err here with the loc taken in one of the GLambda or GProd which has an Implicit.

herbelin · 2017-05-24T17:53:48Z

@JasonGross: The notations 3 to 5 should fail with an error Implicit arguments found in recursive parts of a binder (since { } is not supposed to be used in variables used to denote recursive binders).

Also, there is no support for { } in kernel, so, internally, Axiom f0 : foo is Axiom f0 : forall (n : nat), n = n.

I start to feel that we are somehow opening a can of worms. Maybe the { } status should actually be first added to the type constr before we start supporting it in notations, otherwise, we may be facing more new surprises than what we solve.

psteckler · 2017-05-26T18:40:57Z

@herbelin Worms are bad. I'll back off from this PR, unless someone really wants me to push forward.

herbelin · 2017-05-31T09:24:45Z

@pstecker: Somehow, I would eventually lean towards having implicit arguments annotations in constr (e.g. extending the Name.t field into a more informative one which would also contain Explicit and Implicit). Don't know what @mattam82, or @ppedrot (or anyone else) think, if this is an idea which they already considered.

SkySkimmer · 2017-05-31T09:49:20Z

I feel like implicits are about references rather than part of a type somehow. ie

Definition Id := forall {A}, A -> A.
Definition id : Id := fun A a => a.

If this worked would id have an implicit argument?
I would rather imagine that when defining Id there is some error like "implicit arguments in floating type", and when someone does forall (f : forall {A}, A -> A), ... the implicit information is bound to the rel f inside the forall (eg by adding a (Implicit|Explicit) list to each constructor of Context.Rel.Declaration.pt).

herbelin · 2017-05-31T10:14:33Z

@SkySkimmer: Maybe. We need to think more at where { } is expected to be meaningful.

maximedenes · 2017-06-15T20:32:02Z

@ejgallego do you still plan to have a look at this?

psteckler · 2017-06-15T20:41:03Z

@maximedenes From the discussion, it doesn't look like there's a consensus on how to handle the issue in 3357. If @ejgallego is planning to re-work the Notation machinery, anyway, maybe it's best to give up on this PR.

ejgallego · 2017-06-15T23:25:38Z

Hey @maximedenes I'd like to but I am a bit busy, what does @herbelin think ? Is the bug really critical or we could live with it. My limited understanding of the issue is that it seems a bit complicated; @psteckler my plans for notations are not going well in the sense that I am far from satisfied with the current status of my ideas, so don't count on them for now.

herbelin · 2017-06-17T14:46:34Z

The bug is not critical and we could resolve it by issuing a warning when a {x:A} is found in a notation.

Even, if I feel that in the longer term, something remains to be done. The {x:A} syntax is pretty appealing to indicate an inferable argument and it is somehow frustrating that it does not survive beyond parsing.

ejgallego · 2018-04-24T13:29:52Z

So this PR is actually orphaned.

One question, as briefly discussed in CEP#19 , notation unfolding and implicit resolution could be seen as a separate phase, however as @silene has pointed out in the past one has to be careful of capturing the proper "implicit" closure when unfolding notations.

So, my question is, do we have a written specification of how internatilization is supposed to work? If not, should we try to come up with a more or less complete description on what the interaction between notations and implicits should be before we continue to work in this PR?

ejgallego · 2018-09-02T23:19:04Z

@herbelin should we close this PR?

herbelin · 2018-09-03T05:58:13Z

@herbelin should we close this PR?

As far as I'm concerned, it can be closed (orphaned and requiring more thinking time).

ejgallego · 2018-09-03T08:29:39Z

Ok, closed, noted left in #3357 so if someone ever tackles the bug again they can track it.

psteckler changed the title ~~Fix bug #3357, mark implicit types in Notations~~ Fix bug #3357, mark implicit arguments in Notations May 22, 2017

herbelin reviewed May 22, 2017

View reviewed changes

Fix bug coq#3357, add binding kind to lambda, prod in notation_constr

2224839

psteckler force-pushed the bug-3357-fix branch from 3b70523 to 2224839 Compare May 23, 2017 15:58

add check for implicit arguments in binder

c8a65d6

ejgallego self-requested a review May 23, 2017 23:12

herbelin reviewed May 24, 2017

View reviewed changes

change asserts to guards

ee6b7e0

herbelin reviewed May 24, 2017

View reviewed changes

maximedenes added the needs: progress Work in progress: awaiting action from the author. label May 28, 2017

maximedenes added this to the 8.6.1 milestone Jun 2, 2017

maximedenes modified the milestones: 8.7, 8.6.1 Jun 16, 2017

maximedenes modified the milestones: 8.8, 8.7 Jun 20, 2017

Zimmi48 added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 18, 2017

psteckler changed the title ~~Fix bug #3357, mark implicit arguments in Notations~~ Fix BZ#3357, mark implicit arguments in Notations Sep 26, 2017

Zimmi48 changed the base branch from v8.6 to master November 9, 2017 17:49

maximedenes removed this from the 8.8+beta1 milestone Mar 7, 2018

Zimmi48 changed the title ~~Fix BZ#3357, mark implicit arguments in Notations~~ Fix #3357, mark implicit arguments in Notations Apr 24, 2018

Zimmi48 added kind: fix This fixes a bug or incorrect documentation. part: notations The notation system. labels Apr 24, 2018

coqbot mentioned this pull request Sep 3, 2018

Notation expansion ignores curly braces #3357

Open

ejgallego closed this Sep 3, 2018

Fix #3357, mark implicit arguments in Notations #668

Fix #3357, mark implicit arguments in Notations #668

Conversation

psteckler commented May 22, 2017 • edited

herbelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

psteckler commented May 22, 2017

psteckler commented May 23, 2017

psteckler commented May 23, 2017

psteckler commented May 23, 2017

JasonGross commented May 23, 2017

psteckler commented May 23, 2017

JasonGross commented May 23, 2017

psteckler commented May 23, 2017

JasonGross commented May 23, 2017

psteckler commented May 24, 2017

psteckler commented May 24, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

psteckler commented May 24, 2017

JasonGross commented May 24, 2017

ejgallego commented May 24, 2017

Choose a reason for hiding this comment

herbelin commented May 24, 2017

psteckler commented May 26, 2017

herbelin commented May 31, 2017

SkySkimmer commented May 31, 2017

herbelin commented May 31, 2017

maximedenes commented Jun 15, 2017

psteckler commented Jun 15, 2017

ejgallego commented Jun 15, 2017

herbelin commented Jun 17, 2017

ejgallego commented Apr 24, 2018

ejgallego commented Sep 2, 2018

herbelin commented Sep 3, 2018

ejgallego commented Sep 3, 2018

psteckler commented May 22, 2017 •

edited