Merge PR #13299: Remember universe instances of constants in notations

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

13 files changed, 91 insertions, 43 deletions

diff --git a/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh
new file mode 100644
index 0000000000..27e7cee42e
--- /dev/null
+++ b/dev/ci/user-overlays/13299-jashug-preserve-universes-notation.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13299" ] || [ "$CI_BRANCH" = "preserve-universes-notation" ]; then
+
+    elpi_CI_REF=overlay-universes-in-notations
+    elpi_CI_GITURL=https://github.com/jashug/coq-elpi
+
+fi
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 70a4ea35e9..7c63ebda3a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -244,6 +244,8 @@ let contract_curly_brackets_pat ntn (l,ll) =
 
 type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool }
 
+let empty_local_univs = { bound = Id.Map.empty; unb_univs = false }
+
 type intern_env = {
   ids: Id.Set.t;
   unb: bool;
@@ -1202,6 +1204,11 @@ let intern_sort ~local_univs s =
 let intern_instance ~local_univs us =
   Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
 
+let try_interp_name_alias = function
+  | [], { CAst.v = CRef (ref,u) } ->
+     NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u)
+  | _ -> raise Not_found
+
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   let loc = qid.loc in
@@ -1251,16 +1258,16 @@ let intern_qualid_for_pattern test_global intern_not qid pats =
   | SynDef kn ->
     let filter (vars,a) =
       match a with
-      | NRef g ->
+      | NRef (g,_) ->
         (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
         test_global g;
         let () = assert (List.is_empty vars) in
         Some (g, Some [], pats)
-      | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
+      | NApp (NRef (g,_),[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
         test_global g;
         let () = assert (List.is_empty vars) in
         Some (g, None, pats)
-      | NApp (NRef g,args) ->
+      | NApp (NRef (g,_),args) ->
         (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
         test_global g;
         let nvars = List.length vars in
@@ -1330,7 +1337,7 @@ let interp_reference vars r =
   let r,_ =
     intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false;
-       local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *)
+       local_univs = empty_local_univs;(* <- doesn't matter here *)
        tmp_scope = None; scopes = []; impls = empty_internalization_env;
        binder_block_names = None}
       Environ.empty_named_context_val
@@ -1784,10 +1791,10 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
           if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
             anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
       end
-    | NRef g ->
+    | NRef (g,_) ->
       ensure_kind test_kind ?loc g;
       DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true false [] args)
-    | NApp (NRef g,ntnpl) ->
+    | NApp (NRef (g,_),ntnpl) ->
       ensure_kind test_kind ?loc g;
       let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in
       let no_impl =
@@ -2554,7 +2561,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize env
       {ids; unb = false;
-       local_univs = { bound = Id.Map.empty; unb_univs = false };
+       local_univs = empty_local_univs;
        tmp_scope = None; scopes = []; impls; binder_block_names = None}
       false (empty_ltac_sign, vl) a
   in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f92a54e23f..65b63962d0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -150,6 +150,10 @@ val interp_constr_pattern :
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
 val intern_reference : qualid -> GlobRef.t
 
+(** For syntactic definitions: check if abbreviation to a name
+    and avoid early insertion of maximal implicit arguments *)
+val try_interp_name_alias : 'a list * constr_expr -> notation_constr
+
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> qualid -> glob_constr
 
diff --git a/interp/notation.ml b/interp/notation.ml
index f2d113954b..33d96f0439 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -400,12 +400,12 @@ let cases_pattern_key c = match DAst.get c with
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
-  | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
+  | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
+  | NList (_,_,NApp (NRef (ref,_),args),_,_)
+  | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
-  | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
-  | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+  | NRef (ref,_) -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (NList (_,_,NApp (NRef (ref,_),args),_,_), args') ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
   | NApp (NList (_,_,NApp (_,args),_,_), args') ->
       Oth, AppBoundedNotation (List.length args + List.length args')
@@ -2353,8 +2353,8 @@ let browse_notation strict ntn map =
 
 let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
   match c with
-  | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
-  | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
+  | NRef (ref,_) when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
+  | NApp (NRef (ref,_), l) when head || List.for_all isNVar_or_NHole l && test ref ->
       Some (on_parsing,on_printing,ntn,sc,ref)
   | _ -> None
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0e7f085bde..ea5e2a1ad4 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -43,6 +43,28 @@ let cast_type_iter2 f t1 t2 = match t1, t2 with
    in NList and NBinderList, since the iterator has its own variable *)
 let replace_var i j var = j :: List.remove Id.equal i var
 
+(* compare_glob_universe_instances true strictly_lt us1 us2 computes us1 <= us2,
+   compare_glob_universe_instances false strictly_lt us1 us2 computes us1 = us2.
+   strictly_lt will be set to true if any part is strictly less. *)
+let compare_glob_universe_instances lt strictly_lt us1 us2 =
+  match us1, us2 with
+  | None, None -> true
+  | Some _, None -> strictly_lt := true; lt
+  | None, Some _ -> false
+  | Some l1, Some l2 ->
+     CList.for_all2eq (fun u1 u2 ->
+         match u1, u2 with
+         | UAnonymous {rigid=true}, UAnonymous {rigid=true} -> true
+         | UAnonymous {rigid=false}, UAnonymous {rigid=false} -> true
+         | UAnonymous _, UAnonymous _ -> false
+         | UNamed _, UAnonymous _ -> strictly_lt := true; lt
+         | UAnonymous _, UNamed _ -> false
+         | UNamed _, UNamed _ -> glob_level_eq u1 u2) l1 l2
+
+(* Compute us1 <= us2, as a boolean *)
+let compare_glob_universe_instances_le us1 us2 =
+  compare_glob_universe_instances true (ref false) us1 us2
+
 (* When [lt] is [true], tell if [t1] is a strict refinement of [t2]
    (this is a partial order, so returning [false] does not mean that
    [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the
@@ -93,7 +115,7 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
   | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> ()
   | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> ()
   | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true
-  | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> ()
+  | NRef (gr1,u1), NRef (gr2,u2) when GlobRef.equal gr1 gr2 && compare_glob_universe_instances lt strictly_lt u1 u2 -> ()
   | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *)
   | _, NHole (_, _, _) when lt -> strictly_lt := true
   | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
@@ -377,7 +399,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
   | NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k)
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
-  | NRef x -> GRef (x,None)
+  | NRef (x,u) -> GRef (x,u)
   | NInt i -> GInt i
   | NFloat f -> GFloat f
   | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty)
@@ -612,7 +634,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GHole (w,naming,arg) ->
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
-  | GRef (r,_) -> NRef r
+  | GRef (r,u) -> NRef (r,u)
   | GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty)
   | GEvar _ | GPatVar _ ->
       user_err Pp.(str "Existential variables not allowed in notations.")
@@ -706,10 +728,10 @@ let rec subst_pat subst pat =
 
 let rec subst_notation_constr subst bound raw =
   match raw with
-  | NRef ref ->
+  | NRef (ref,u) ->
       let ref',t = subst_global subst ref in
       if ref' == ref then raw else (match t with
-          | None -> NRef ref'
+          | None -> NRef (ref',u)
           | Some t ->
             fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
 
@@ -1344,7 +1366,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> sigma
-  | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
+  | GRef (r1,u1), NRef (r2,u2) when (GlobRef.equal r1 r2) && compare_glob_universe_instances_le u1 u2 -> sigma
   | GApp (f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
@@ -1570,10 +1592,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
   | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
-  | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when Construct.CanOrd.equal r1 r2 ->
+  | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2,None) when Construct.CanOrd.equal r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
       sigma,(false,0,l)
-  | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
+  | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2,None),l2)
       when Construct.CanOrd.equal r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
@@ -1597,9 +1619,9 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
-  | NRef (GlobRef.IndRef r2) when Ind.CanOrd.equal ind r2 ->
+  | NRef (GlobRef.IndRef r2,None) when Ind.CanOrd.equal ind r2 ->
       sigma,(false,0,pats)
-  | NApp (NRef (GlobRef.IndRef r2),l2)
+  | NApp (NRef (GlobRef.IndRef r2,None),l2)
       when Ind.CanOrd.equal ind r2 ->
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index c541a19bfd..2979447cf8 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -21,7 +21,7 @@ open Glob_term
 
 type notation_constr =
   (* Part common to [glob_constr] and [cases_pattern] *)
-  | NRef of GlobRef.t
+  | NRef of GlobRef.t * glob_level list option
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 274d3655d3..07160dcf6f 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -71,10 +71,10 @@ let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
 let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
-  | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
-  | NRef ref -> RefKey(canonical_gr ref), None
+  | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), Some (List.length args)
+  | NList (_,_,NApp (NRef (ref,_),args),_,_)
+  | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
+  | NRef (ref,_) -> RefKey(canonical_gr ref), None
   | _ -> Oth, None
 
 let cache_reserved_type (_,(id,t)) =
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 46baa00c74..91d05f7317 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -26,7 +26,7 @@ let global_of_extended_global_head = function
   | SynDef kn ->
       let _, syn_def = search_syntactic_definition kn in
       let rec head_of = function
-        | NRef ref -> ref
+        | NRef (ref,None) -> ref
         | NApp (rc, _) -> head_of rc
         | NCast (rc, _) -> head_of rc
         | NLetIn (_, _, _, rc) -> head_of rc
@@ -37,8 +37,8 @@ let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
   match search_syntactic_definition kn with
-  | [],NRef ref -> ref
-  | [],NApp (NRef ref,[]) -> ref
+  | [],NRef (ref,None) -> ref
+  | [],NApp (NRef (ref,None),[]) -> ref
   | _ -> raise Not_found
 
 let locate_global_with_alias ?(head=false) qid =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f3ad3546ff..39e628883a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -40,7 +40,7 @@ let load_syntax_constant i ((sp,kn),(_local,syndef)) =
   Nametab.push_syndef (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
-  | _,NRef ref ->
+  | _,NRef (ref,_) ->
       let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
       DirPath.is_empty dir && Id.equal id (basename sp)
   | _ ->
diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml
index 89d757a72a..0e7640f430 100644
--- a/plugins/syntax/number.ml
+++ b/plugins/syntax/number.ml
@@ -387,10 +387,10 @@ let locate_global_inductive allow_params qid =
     | Globnames.TrueGlobal _ -> raise Not_found
     | Globnames.SynDef kn ->
     match Syntax_def.search_syntactic_definition kn with
-    | [], Notation_term.(NApp (NRef (GlobRef.IndRef i), l)) when allow_params ->
+    | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params ->
        i,
        List.map (function
-           | Notation_term.NRef r -> Some r
+           | Notation_term.NRef (r,None) -> Some r
            | Notation_term.NHole _ -> None
            | _ -> raise Not_found) l
     | _ -> raise Not_found in
diff --git a/test-suite/bugs/closed/bug_6157.v b/test-suite/bugs/closed/bug_6157.v
new file mode 100644
index 0000000000..cd24e4c7ee
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6157.v
@@ -0,0 +1,15 @@
+(* Check that universe instances of refs are preserved *)
+
+Section U.
+Set Universe Polymorphism.
+Definition U@{i} := Type@{i}.
+
+Section foo.
+Universe i.
+Fail Check U@{i} : U@{i}.
+Notation Ui := U@{i}. (* syndef path *)
+Fail Check Ui : Type@{i}.
+Notation "#" := U@{i}. (* non-syndef path *)
+Fail Check # : Type@{i}.
+End foo.
+End U.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e6244ee3b5..2fe402ff08 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1793,15 +1793,9 @@ let remove_delimiters local scope =
 let add_class_scope local scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
 
-(* Check if abbreviation to a name and avoid early insertion of
-   maximal implicit arguments *)
-let try_interp_name_alias = function
-  | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
-  | _ -> raise Not_found
-
 let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
   let acvars,pat,reversibility =
-    try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
+    try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
     with Not_found ->
       let fold accu id = Id.Map.add id NtnInternTypeAny accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 0fc6c7f87b..79a0cdf8d1 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -947,7 +947,7 @@ let print_about_any ?loc env sigma k udecl =
   [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
     let () = match Syntax_def.search_syntactic_definition kn with
-    | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
+    | [],Notation_term.NRef (ref,_) -> Dumpglob.add_glob ?loc ref
     | _ -> () in
       v 0 (
       print_syntactic_def env kn ++ fnl () ++