Fix coq#6323: stronger restrict universe context vs abstract.

In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.

Universes of a monomorphic reference [c] are considered to appear in
the term [c].

API/API.mli

@@ -2057,7 +2057,7 @@ end
 
 module Univops :
 sig
-  val universes_of_constr : Constr.constr -> Univ.LSet.t
+  val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t
   val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
 end
 

engine/eConstr.ml

@@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
-let universes_of_constr sigma c =
+let universes_of_constr env sigma c =
   let open Univ in
+  let open Declarations in
   let rec aux s c =
     match kind sigma c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
     | Sort u ->
        let sort = ESorts.kind sigma u in
        if Sorts.is_small sort then s

engine/eConstr.mli

@@ -203,7 +203,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
    type of evars appearing in it. *)
-val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
 
 (** {6 Substitutions} *)
 

engine/uState.ml

@@ -22,6 +22,7 @@ type uinfo = {
 type t =
  { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
+   uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.LSet.t; 
@@ -34,6 +35,7 @@ type t =
 let empty =
   { uctx_names = UNameMap.empty, Univ.LMap.empty;
     uctx_local = Univ.ContextSet.empty;
+    uctx_seff_univs = Univ.LSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_universes = UGraph.initial_universes;
@@ -60,6 +62,7 @@ let union ctx ctx' =
   else if is_empty ctx' then ctx
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
+    let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in
     let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
                                (Univ.ContextSet.levels ctx.uctx_local) in
@@ -70,6 +73,7 @@ let union ctx ctx' =
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
         uctx_local = local;
+        uctx_seff_univs = seff;
         uctx_univ_variables = 
           Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
         uctx_univ_algebraic = 
@@ -365,12 +369,21 @@ let check_univ_decl ~poly uctx decl =
   ctx
 
 let restrict ctx vars =
+  let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
+let demote_seff_univs entry uctx =
+  let open Entries in
+  match entry.const_entry_universes with
+  | Polymorphic_const_entry _ -> uctx
+  | Monomorphic_const_entry (univs, _) ->
+    let seff = Univ.LSet.union uctx.uctx_seff_univs univs in
+    { uctx with uctx_seff_univs = seff }
+
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
@@ -552,7 +565,8 @@ let refresh_undefined_univ_variables uctx =
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
-               uctx_local = ctx'; 
+               uctx_local = ctx';
+               uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
                uctx_initial_universes = initial } in
@@ -569,7 +583,8 @@ let normalize uctx =
       Universes.refresh_constraints uctx.uctx_initial_universes us'
     in
       { uctx_names = uctx.uctx_names;
-        uctx_local = us'; 
+        uctx_local = us';
+        uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *)
         uctx_univ_variables = vars'; 
         uctx_univ_algebraic = algs';
         uctx_universes = universes;

engine/uState.mli

@@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 val restrict : t -> Univ.LSet.t -> t
 
+val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
+
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)

engine/univops.ml

@@ -9,12 +9,25 @@
 open Univ
 open Constr
 
-let universes_of_constr c =
+let universes_of_constr env c =
+  let open Declarations in
   let rec aux s c = 
     match kind c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) -> 
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels u) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
+    | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c

engine/univops.mli

@@ -9,7 +9,8 @@
 open Constr
 open Univ
 
-(** Shrink a universe context to a restricted set of variables *)
+(** The universes of monomorphic constants appear. *)
+val universes_of_constr : Environ.env -> constr -> LSet.t
 
-val universes_of_constr : constr -> LSet.t
+(** Shrink a universe context to a restricted set of variables *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t

plugins/setoid_ring/newring.ml

@@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let vars = Univops.universes_of_constr c in
+  let env = Global.env () in
+  let vars = Univops.universes_of_constr env c in
   let univs = Univops.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 

proofs/pfedit.ml

@@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
+    let univs = UState.demote_seff_univs const univs in
     const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in

proofs/proof_global.ml

@@ -348,21 +348,17 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	    nf t
 	  else t
         in
-        let used_univs_body = Univops.universes_of_constr body in
-        let used_univs_typ = Univops.universes_of_constr typ in
-        (* Universes for private constants are relevant to the body *)
-        let used_univs_body =
-          List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us)
-            used_univs_body (Safe_typing.universes_of_private eff)
-        in
+        let env = Global.env () in
+        let used_univs_body = Univops.universes_of_constr env body in
+        let used_univs_typ = Univops.universes_of_constr env typ in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
              the body.  So we keep the two sets distinct. *)
-	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
           let univs = UState.check_mono_univ_decl ctx_body universe_decl in
           (initunivs, typ), ((body, univs), eff)

test-suite/bugs/closed/6323.v

@@ -0,0 +1,9 @@
+Goal True.
+  simple refine (let X : Type := _ in _);
+    [ abstract exact Set using Set'
+    | let X' := (eval cbv delta [X] in X) in
+      clear X;
+      simple refine (let id' : { x : X' | True } -> X' := _ in _);
+      [ abstract refine (@proj1_sig _ _) | ]
+    ].
+Abort.

vernac/classes.ml

@@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst =
 
 let declare_instance_constant k info global imps ?hook id decl poly evm term termtype =
   let kind = IsDefinition Instance in
-  let evm = 
-    let levels = Univ.LSet.union (Univops.universes_of_constr termtype) 
-				 (Univops.universes_of_constr term) in
+  let evm =
+    let env = Global.env () in
+    let levels = Univ.LSet.union (Univops.universes_of_constr env termtype)
+                                 (Univops.universes_of_constr env term) in
     Evd.restrict_universe_context evm levels 
   in
   let uctx = Evd.check_univ_decl ~poly evm decl in

vernac/command.ml

@@ -105,7 +105,7 @@ let interp_definition pl bl poly red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
         let () = evdref := Evd.restrict_universe_context !evdref vars in
         let uctx = Evd.check_univ_decl ~poly !evdref decl in
         imps1@(Impargs.lift_implicits nb_args imps2),
@@ -130,8 +130,8 @@ let interp_definition pl bl poly red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
-        let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+        let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
+        let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in
         let vars = Univ.LSet.union bodyvars tyvars in
         let () = evdref := Evd.restrict_universe_context !evdref vars in
         let uctx = Evd.check_univ_decl ~poly !evdref decl in
@@ -315,7 +315,7 @@ let do_assumptions kind nl l =
   let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
-      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
@@ -1188,7 +1188,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+    let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
@@ -1221,7 +1221,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Univops.universes_of_constr (List.hd fixdecls) in
+    let env = Global.env () in
+    let vars = Univops.universes_of_constr env (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in

vernac/obligations.ml

@@ -477,7 +477,10 @@ let declare_definition prg =
   let fix_exn = Hook.get get_fix_exn () in
   let typ = nf typ in
   let body = nf body in
-  let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in
+  let env = Global.env () in
+  let uvars = Univ.LSet.union
+      (Univops.universes_of_constr env typ)
+      (Univops.universes_of_constr env body) in
   let uctx = UState.restrict prg.prg_ctx uvars in
   let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in