Support universe instances on the literal Type

Fixes BZ#5726.

2 files changed, 50 insertions, 0 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 61b33aa415..1dc7f325fa 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -836,6 +836,18 @@ let intern_reference ref =
   in
   Smartlocate.global_of_extended_global r
 
+let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+  match info with
+  | Misctypes.UAnonymous -> None
+  | Misctypes.UUnknown -> None
+  | Misctypes.UNamed id -> Some (id, 0)
+
+let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+  match level with
+  | Misctypes.GProp -> Misctypes.GProp
+  | Misctypes.GSet -> Misctypes.GSet
+  | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
@@ -867,6 +879,10 @@ let intern_qualid loc qid intern env lvar us args =
           DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
         | _ -> err ()
         end
+      | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+      | Some [_old_level], GSort _new_sort ->
+        (* TODO: add old_level and new_sort to the error message *)
+        user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
       | Some _, _ -> err ()
       in
       c, projapp, args2
diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v
new file mode 100644
index 0000000000..53ef473572
--- /dev/null
+++ b/test-suite/bugs/closed/5726.v
@@ -0,0 +1,34 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Module GlobalReference.
+
+  Definition type' := Type.
+  Notation type := type'.
+  Check type@{Set}.
+
+End GlobalReference.
+
+Module TypeLiteral.
+
+  Notation type := Type.
+  Check type@{Set}.
+  Check type@{Prop}.
+
+End TypeLiteral.
+
+Module ExplicitSort.
+  Monomorphic Universe u.
+  Notation foo := Type@{u}.
+  Fail Check foo@{Set}.
+  Fail Check foo@{u}.
+
+  Notation bar := Type.
+  Check bar@{u}.
+End ExplicitSort.
+
+Module PropNotationUnsupported.
+  Notation foo := Prop.
+  Fail Check foo@{Set}.
+  Fail Check foo@{Type}.
+End PropNotationUnsupported.