Allowing Set to be part of universe expressions.

Conversely, Type existential variables now (explicitly) cover the Set
case.

Similarly for Prop and SProp.

7 files changed, 91 insertions, 88 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 901a1bd342..18a036cb8c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -688,20 +688,21 @@ let hack_qualid_of_univ_level sigma l =
 
 let detype_universe sigma u =
   let fn (l, n) =
-    let qid = hack_qualid_of_univ_level sigma l in
-    (qid, n)
-  in
+    let s =
+      if Univ.Level.is_prop l then GProp else
+      if Univ.Level.is_set l then GSet else
+      GType (hack_qualid_of_univ_level sigma l) in
+    (s, n) in
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
-  | SProp -> GSProp
-  | Prop -> GProp
-  | Set -> GSet
+  | SProp -> UNamed [GSProp,0]
+  | Prop -> UNamed [GProp,0]
+  | Set -> UNamed [GSet,0]
   | Type u ->
-    GType
       (if !print_universes
        then UNamed (detype_universe sigma u)
-       else UUnknown)
+       else UAnonymous {rigid=true})
 
 type binder_kind = BProd | BLambda | BLetIn
 
@@ -710,7 +711,7 @@ type binder_kind = BProd | BLambda | BLetIn
 
 let detype_level sigma l =
   let l = hack_qualid_of_univ_level sigma l in
-  GType (UNamed l)
+  UNamed (GType l)
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 656b987942..a3a3c7f811 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -45,25 +45,27 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
-let univ_name_eq u1 u2 = match u1, u2 with
-  | UUnknown, UUnknown -> true
-  | UAnonymous, UAnonymous -> true
-  | UNamed l1, UNamed l2 ->
-    List.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n) l1 l2
-  | (UNamed _ | UAnonymous | UUnknown), _ -> false
-
-let glob_sort_eq g1 g2 = match g1, g2 with
+let glob_sort_name_eq g1 g2 = match g1, g2 with
   | GSProp, GSProp
   | GProp, GProp
   | GSet, GSet -> true
-  | GType u1, GType u2 -> univ_name_eq u1 u2
+  | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
   | (GSProp|GProp|GSet|GType _), _ -> false
 
+exception ComplexSort
+
 let glob_sort_family = let open Sorts in function
-| GSProp -> InSProp
-| GProp -> InProp
-| GSet -> InSet
-| GType _ -> InType
+  | UAnonymous {rigid=true} -> InType
+  | UNamed [GSProp,0] -> InProp
+  | UNamed [GProp,0] -> InProp
+  | UNamed [GSet,0] -> InSet
+  | _ -> raise ComplexSort
+
+let glob_sort_eq u1 u2 = match u1, u2 with
+  | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
+  | UNamed l1, UNamed l2 ->
+    List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2
+  | (UNamed _ | UAnonymous _), _ -> false
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index df902a8fa7..3995ab6a5a 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,10 +15,13 @@ open Glob_term
 
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
-val glob_sort_family : 'a glob_sort_gen -> Sorts.family
-
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
+(** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
+    contains a max, an increment, or a flexible universe *)
+exception ComplexSort
+val glob_sort_family : glob_sort -> Sorts.family
+
 val alias_of_pat : 'a cases_pattern_g -> Name.t
 
 val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 37bacbdeb2..704cddd784 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -23,23 +23,23 @@ type existential_name = Id.t
 
 (** Sorts *)
 
-type 'a glob_sort_gen =
+type glob_sort_name =
   | GSProp (** representation of [SProp] literal *)
-  | GProp (** representation of [Prop] literal *)
-  | GSet  (** representation of [Set] literal *)
-  | GType of 'a (** representation of [Type] literal *)
+  | GProp (** representation of [Prop] level *)
+  | GSet  (** representation of [Set] level *)
+  | GType of Libnames.qualid (** representation of a [Type] level *)
 
-type 'a universe_kind =
-  | UAnonymous (** a flexible universe (collapsable by minimization) *)
-  | UUnknown (** a rigid universe *)
-  | UNamed of 'a (** a named universe or a universe expression *)
+type 'a glob_sort_expr =
+  | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
+  | UNamed of 'a
 
-type level_info = Libnames.qualid universe_kind (** levels, occurring in universe instances *)
-type glob_level = level_info glob_sort_gen
-type glob_constraint = glob_level * Univ.constraint_type * glob_level
+(** levels, occurring in universe instances *)
+type glob_level = glob_sort_name glob_sort_expr
 
-type sort_info = (Libnames.qualid * int) list universe_kind (** sorts: Prop, Set, Type@{...} *)
-type glob_sort = sort_info glob_sort_gen
+(** sort expressions *)
+type glob_sort = (glob_sort_name * int) list glob_sort_expr
+
+type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
 
 type glob_recarg = int option
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c788efda48..2d27b27cab 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -410,7 +410,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
-  | GSort gs -> PSort (Glob_ops.glob_sort_family gs)
+  | GSort gs ->
+     (try PSort (Glob_ops.glob_sort_family gs)
+      with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern."))
   | GHole _ ->
       PMeta None
   | GCast (c,_) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 48aba8edf4..be8f7215fa 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -132,7 +132,7 @@ let is_strict_universe_declarations =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level evd qid =
+let interp_known_universe_level_name evd qid =
   try
     let open Libnames in
     if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
@@ -142,7 +142,7 @@ let interp_known_universe_level evd qid =
     Univ.Level.make qid
 
 let interp_universe_level_name ~anon_rigidity evd qid =
-  try evd, interp_known_universe_level evd qid
+  try evd, interp_known_universe_level_name evd qid
   with Not_found ->
     if Libnames.qualid_is_ident qid then (* Undeclared *)
       let id = Libnames.qualid_basename qid in
@@ -164,45 +164,31 @@ let interp_universe_level_name ~anon_rigidity evd qid =
         with UGraph.AlreadyDeclared -> evd
       in evd, level
 
-let interp_universe ?loc evd = function
-  | UUnknown ->
-    let evd, l = new_univ_level_variable ?loc univ_rigid evd in
-    evd, Univ.Universe.make l
-  | UAnonymous ->
-    let evd, l = new_univ_level_variable ?loc univ_flexible evd in
-    evd, Univ.Universe.make l
-  | UNamed l ->
+let interp_universe_name ?loc evd l =
+  (* [univ_flexible_alg] can produce algebraic universes in terms *)
+  let anon_rigidity = univ_flexible in
+  let evd', l = interp_universe_level_name ~anon_rigidity evd l in
+  evd', l
+
+let interp_sort_name ?loc sigma = function
+  | GSProp -> sigma, Univ.Level.sprop
+  | GProp -> sigma, Univ.Level.prop
+  | GSet -> sigma, Univ.Level.set
+  | GType l -> interp_universe_name ?loc sigma l
+
+let interp_sort_info ?loc evd l =
     List.fold_left (fun (evd, u) (l,n) ->
-      let evd', u' =
-        let evd',u' =
-           (* [univ_flexible_alg] can produce algebraic universes in terms *)
-           let anon_rigidity = univ_flexible in
-           let evd', l = interp_universe_level_name ~anon_rigidity evd l in
-           evd', Univ.Universe.make l
-        in
-        match n with
-            | 0 -> evd', u'
-            | 1 -> evd', Univ.Universe.super u'
-            | n ->
-               user_err ?loc ~hdr:"interp_universe"
-                        (Pp.(str "Cannot interpret universe increment +" ++ int n))
+      let evd', u' = interp_sort_name ?loc evd l in
+      let u' = Univ.Universe.make u' in
+      let u' = match n with
+      | 0 -> u'
+      | 1 -> Univ.Universe.super u'
+      | n ->
+        user_err ?loc ~hdr:"interp_universe"
+          (Pp.(str "Cannot interpret universe increment +" ++ int n))
       in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
 
-let interp_known_level_info ?loc evd = function
-  | UUnknown | UAnonymous ->
-    user_err ?loc ~hdr:"interp_known_level_info"
-      (str "Anonymous universes not allowed here.")
-  | UNamed qid ->
-    try interp_known_universe_level evd qid
-    with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
-
-let interp_level_info ?loc evd : level_info -> _ = function
-  | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
-  | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
-  | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
-
 type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 
 type inference_flags = {
@@ -416,13 +402,14 @@ let interp_known_glob_level ?loc evd = function
   | GSProp -> Univ.Level.sprop
   | GProp -> Univ.Level.prop
   | GSet -> Univ.Level.set
-  | GType s -> interp_known_level_info ?loc evd s
+  | GType qid ->
+    try interp_known_universe_level_name evd qid
+    with Not_found ->
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
 
 let interp_glob_level ?loc evd : glob_level -> _ = function
-  | GSProp -> evd, Univ.Level.sprop
-  | GProp -> evd, Univ.Level.prop
-  | GSet -> evd, Univ.Level.set
-  | GType s -> interp_level_info ?loc evd s
+  | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
+  | UNamed s -> interp_sort_name ?loc evd s
 
 let interp_instance ?loc evd l =
   let evd, l' =
@@ -461,18 +448,26 @@ let pretype_ref ?loc sigma env ref us =
     let ty = unsafe_type_of !!env sigma c in
     sigma, make_judge c ty
 
-let judge_of_Type ?loc evd s =
-  let evd, s = interp_universe ?loc evd s in
+let interp_sort ?loc evd : glob_sort -> _ = function
+  | UAnonymous {rigid} ->
+    let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
+    evd, Univ.Universe.make l
+  | UNamed l -> interp_sort_info ?loc evd l
+
+let judge_of_sort ?loc evd s =
   let judge = 
     { uj_val = mkType s; uj_type = mkType (Univ.super s) }
   in
     evd, judge
 
-let pretype_sort ?loc sigma = function
-  | GSProp -> sigma, judge_of_sprop
-  | GProp -> sigma, judge_of_prop
-  | GSet -> sigma, judge_of_set
-  | GType s -> judge_of_Type ?loc sigma s
+let pretype_sort ?loc sigma s =
+  match s with
+  | UNamed [GSProp,0] -> sigma, judge_of_sprop
+  | UNamed [GProp,0] -> sigma, judge_of_prop
+  | UNamed [GSet,0] -> sigma, judge_of_set
+  | _ ->
+  let sigma, s = interp_sort ?loc sigma s in
+  judge_of_sort ?loc sigma s
 
 let new_type_evar env sigma loc =
   new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c0a95e73c6..d38aafd0e9 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -31,7 +31,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
 val clear_bidirectionality_hint : GlobRef.t -> unit
 
 val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
-  glob_level -> Univ.Level.t
+  glob_sort_name -> Univ.Level.t
 
 (** An auxiliary function for searching for fixpoint guard indexes *)