Fixes #11331 (unexpected level collisions between custom entries and constr).

There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).

Also fixes #9517, fixes #9519, fixes #9640 (part 3).

2 files changed, 37 insertions, 25 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 07656f9715..65a51f648e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -208,7 +208,9 @@ let assoc_eq al ar =
      Some None = NEXT
      Some (Some (n,cur)) = constr LEVEL n
          s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = let open Gramlib.Gramext in function
+let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
+(* If in a different grammar, no other choice than denoting it by absolute level *)
+  | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> Some (Some (n,true))
 (* Associativity is None means force the level *)
   | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
 (* Compute production name on the right side *)
@@ -231,7 +233,7 @@ let adjust_level assoc from = let open Gramlib.Gramext in function
     | _ -> Some None
     end
   (* None means NEXT *)
-  | (NextLevel,_) -> Some None
+  | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); Some None
 (* Compute production name elsewhere *)
   | (NumLevel n,InternalProd) ->
     if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
@@ -311,13 +313,14 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function
    | ForConstr -> entry_for_constr
    | ForPattern -> entry_for_patttern
 
-let is_self from e = match e with
+let is_self custom (custom',from) e = Notation.notation_entry_eq custom custom' && match e with
 | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
 | (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
 | _ -> false
 
-let is_binder_level from e = match e with
-| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200
+let is_binder_level custom (custom',from) e = match e with
+| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
+  custom = InConstrEntry && custom' = InConstrEntry && from = 200
 | _ -> false
 
 let make_sep_rules = function
@@ -338,11 +341,11 @@ type ('s, 'a) mayrec_symbol =
 | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
-  if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200"))
-  else if is_self from p then MayRecMay Aself
+  if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200"))
+  else if is_self custom from p then MayRecMay Aself
   else
     let g = target_entry custom forpat in
-    let lev = adjust_level assoc from p in
+    let lev = adjust_level custom assoc from p in
     begin match lev with
     | None -> MayRecNo (Aentry g)
     | Some None -> MayRecMay Anext
@@ -503,19 +506,19 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
   ExtendRule (target_entry where forpat, reinit, empty)
 
-let rec pure_sublevels' custom assoc from forpat level = function
+let rec pure_sublevels' assoc from forpat level = function
 | [] -> []
 | GramConstrNonTerminal (e,_) :: rem ->
-   let rem = pure_sublevels' custom assoc from forpat level rem in
+   let rem = pure_sublevels' assoc from forpat level rem in
    let push where p rem =
-     match symbol_of_target custom p assoc from forpat with
+     match symbol_of_target where p assoc from forpat with
      | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
      | _ -> rem in
    (match e with
    | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
    | ETProdConstr (s,p) -> push s p rem
    | _ -> rem)
-| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
@@ -530,8 +533,8 @@ let extend_constr state forpat ng =
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key custom forpat n in
   let fold (accu, state) pt =
-    let AnyTyRule r = make_ty_rule assoc n forpat pt in
-    let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
+    let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in
+    let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 0c39aba70a..ecfebec6b8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -955,18 +955,28 @@ let is_only_printing mods =
 
 (* Compute precedences from modifiers (or find default ones) *)
 
-let set_entry_type from etyps (x,typ) =
+let set_entry_type from n etyps (x,typ) =
+  let make_lev n s = match typ with
+    | BorderProd _ -> NumLevel n
+    | InternalProd ->
+      if s = InConstrEntry then NumLevel 200 else
+      user_err (strbrk "level of inner subentry " ++ quote (pr_notation_entry s) ++
+                str " cannot be inferred. It must be given explicitly.") in
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+      | ETConstr (s,bko,Some n), BorderProd (left,_) ->
           ETConstr (s,bko,(n,BorderProd (left,None)))
-      | ETConstr (s,bko,Some n), (_,InternalProd) ->
-         ETConstr (s,bko,(n,InternalProd))
+      | ETConstr (s,bko,Some n), InternalProd ->
+          ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
       | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
-      | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
+      | ETConstr (s,bko,None), _ ->
+         if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
+         else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else
+         user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++
+                   str " cannot be inferred. It must be given explicitly.")
     with Not_found ->
-      ETConstr (from,None,typ)
+      ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
 
 let join_auxiliary_recursive_types recvars etyps =
@@ -1216,14 +1226,13 @@ module SynData = struct
 end
 
 let find_subentry_types from n assoc etyps symbols =
-  let innerlevel = NumLevel 200 in
   let typs =
     find_symbols
-      (NumLevel n,BorderProd(Left,assoc))
-      (innerlevel,InternalProd)
-      (NumLevel n,BorderProd(Right,assoc))
+      (BorderProd(Left,assoc))
+      (InternalProd)
+      (BorderProd(Right,assoc))
       symbols in
-  let sy_typs = List.map (set_entry_type from etyps) typs in
+  let sy_typs = List.map (set_entry_type from n etyps) typs in
   let prec = List.map (assoc_of_type from n) sy_typs in
   sy_typs, prec