Merge PR coq#19337: A few corner case notation bugs in the presence o…

…f binders

Reviewed-by: proux01
Co-authored-by: proux01 <[email protected]>

interp/notation_ops.ml

@@ -1118,7 +1118,7 @@ let unify_term renaming v v' =
   match DAst.get v, DAst.get v' with
   | GHole _, _ -> v'
   | _, GHole _ -> v
-  | _, _ -> if glob_constr_eq (alpha_rename renaming v) v' then v else raise No_match
+  | _, _ -> let v = alpha_rename renaming v in if glob_constr_eq v v' then v else raise No_match
 
 let unify_opt_term alp v v' =
   match v, v' with
@@ -1134,24 +1134,24 @@ let unify_binder_upto alp b b' =
   let loc, loc' = CAst.(b.loc, b'.loc) in
   match DAst.get b, DAst.get b' with
   | GLocalAssum (na,r,bk,t), GLocalAssum (na',r',bk',t') ->
-     let alp, na = unify_name_upto alp na na' in
-     alp, DAst.make ?loc @@
+     let alp', na = unify_name_upto alp na na' in
+     alp', DAst.make ?loc @@
      GLocalAssum
        (na,
         unify_relevance_info r r',
         unify_binding_kind bk bk',
         unify_term alp.renaming t t')
   | GLocalDef (na,r,c,t), GLocalDef (na',r',c',t') ->
-     let alp, na = unify_name_upto alp na na' in
-     alp, DAst.make ?loc @@
+     let alp', na = unify_name_upto alp na na' in
+     alp', DAst.make ?loc @@
      GLocalDef
        (na,
         unify_relevance_info r r',
         unify_term alp.renaming c c',
         unify_opt_term alp.renaming t t')
   | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' ->
-     let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
-     alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp.renaming t t')
+     let alp', p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
+     alp', DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp.renaming t t')
   | _ -> raise No_match
 
 let rec unify_terms alp vl vl' =
@@ -1191,10 +1191,10 @@ let unify_term_binder renaming c = DAst.(map (fun b' ->
 let rec unify_terms_binders renaming cl bl' =
   match cl, bl' with
   | [], [] -> []
-  | c :: cl, b' :: bl' ->
+  | c :: cl', b' :: bl' ->
      begin match DAst.get b' with
-     | GLocalDef (_, _, _, t) -> unify_terms_binders renaming cl bl'
-     | _ -> unify_term_binder renaming c b' :: unify_terms_binders renaming cl bl'
+     | GLocalDef (_, _, _, t) -> b' :: unify_terms_binders renaming cl bl'
+     | _ -> unify_term_binder renaming c b' :: unify_terms_binders renaming cl' bl'
      end
   | _ -> raise No_match
 
@@ -1241,6 +1241,20 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
+let bind_singleton_bindinglist_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
+  try
+    (* If already bound to a binder, unify the term and the binder *)
+    let vars,patl' = Id.List.assoc var binderlists in
+    let patl'' = unify_terms_binders alp.renaming [c] patl' in
+    if patl' == patl'' then sigma
+    else
+      let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
+      let alp' = {alp with actualvars = Id.Set.union vars alp.actualvars} in
+      add_bindinglist_env alp' sigma var patl''
+  with Not_found ->
+    (* A term-as-binder occurs in the scope of a binder which is already bound *)
+    anomaly (Pp.str "Unbound term as binder.")
+
 let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
   let env = Global.env () in
   let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
@@ -1471,7 +1485,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_var_term r1 && is_onlybinding_strict_meta id2 metas -> raise No_match
   | r1, NVar id2 when is_var_term r1 && is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
-  | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_singleton_bindinglist_as_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)
   | r1, NList (x,y,iter,termin,revert) ->

test-suite/output/Notations3.out

@@ -97,8 +97,10 @@ fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
      : nat -> Prop
 fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
-tele (t : Type) '(y, z) (x : t0) := tt
+tele (t : Type) '(y, z) (x : t) := tt
      : forall t : Type, nat * nat -> t -> fpack
+tele (t : Type) (y := nat) (x : t) (z : y) := (y, z)
+     : forall t : Type, t -> nat -> fpack
 [fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2]
      : (nat -> nat) *
        ((nat -> nat) *
@@ -116,7 +118,7 @@ where
      : nat * (nat * nat)
 {{0, 1, 2, 3}}
      : nat * (nat * (nat * nat))
-File "./output/Notations3.v", line 178, characters 0-174:
+File "./output/Notations3.v", line 179, characters 0-174:
 Warning: Closed notations (i.e. starting and ending with a terminal symbol)
 should usually be at level 0 (default).
 [closed-notation-not-level-0,parsing,default]
@@ -149,13 +151,15 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop * Prop * Prop
 {{D 1, 2}}
      : nat * nat * (nat * nat * (nat * nat))
-File "./output/Notations3.v", line 235, characters 0-104:
+File "./output/Notations3.v", line 236, characters 0-104:
 Warning: Notations "! _ .. _ , _" defined at level 200 with arguments binder,
 constr at next level and "! _ .. _ # _ #" defined at level 200 with arguments
 binder, constr have incompatible prefixes. One of them will likely not work.
 [notation-incompatible-prefix,parsing,default]
 ! a b : nat # True #
      : Prop * (Prop * Prop)
+{{forall x : nat, x = 0, nat}}
+     : Prop * Set
 !!!! a b : nat # True #
      : Prop * Prop * (Prop * Prop * Prop)
 @@ a b : nat # a = b # b = a #

test-suite/output/Notations3.v

@@ -144,6 +144,7 @@ Notation "'tele' x .. z := b" :=
   (at level 85, x binder, z binder).
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
+Check tele (t:Type) (y:=nat) (x:t) (z:y) := (y,z).
 
 (* Checking that "fun" in a notation does not mixed up with the
    detection of a recursive binder *)
@@ -236,6 +237,7 @@ Notation "! x .. y # A #" :=
   ((forall x, x=x), .. ((forall y, y=y), A) ..)
   (at level 200, x binder).
 Check ! a b : nat # True #.
+Check ((forall x, x=0), nat). (* should not use the notation *)
 
 Notation "!!!! x .. y # A #" :=
   (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)