Test Rocq PR #21405

kernel/constant_typing.ml

@@ -103,10 +103,10 @@ let process_universes env = function
   | Entries.Polymorphic_entry uctx ->
     (** [ctx] must contain local universes, such that it has no impact
         on the rest of the graph (up to transitivity). *)
-    let env = Environ.push_context ~strict:false uctx env in
     let inst, auctx = UVars.abstract_universes uctx in
+    let env = Environ.push_context ~strict:false (AbstractContext.repr auctx) env in
     let usubst = UVars.make_instance_subst inst in
-    env, usubst, inst, Polymorphic auctx
+    env, usubst, UVars.make_abstract_instance auctx, Polymorphic auctx
 
 let check_primitive_type env op_t u t =
   let inft = Typeops.type_of_prim_or_type env u op_t in
@@ -143,12 +143,12 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
       in
       univs, typ
 
-    | Some (typ,univ_entry) ->
+    | Some (typ, univ_entry) ->
       let univ_entry = adjust_primitive_univ_entry p auctx univ_entry in
       let env, usubst, u, univs = process_universes env univ_entry in
+      let typ = Vars.subst_univs_level_constr usubst typ in
       let typ = (Typeops.infer_type env typ).utj_val in
       let () = check_primitive_type env p u typ in
-      let typ = Vars.subst_univs_level_constr usubst typ in
       univs, typ
   in
   let body = match p with
@@ -172,17 +172,17 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
 
 let infer_symbol env { symb_entry_universes; symb_entry_unfold_fix; symb_entry_type } =
   let env, usubst, _, univs = process_universes env symb_entry_universes in
+  let symb_entry_type = Vars.subst_univs_level_constr usubst symb_entry_type in
   let j = Typeops.infer env symb_entry_type in
   let r = Typeops.assumption_of_judgment env j in
-  let t = Vars.subst_univs_level_constr usubst j.uj_val in
   {
     const_hyps = [];
     const_univ_hyps = Instance.empty;
     const_body = Symbol symb_entry_unfold_fix;
-    const_type = t;
+    const_type = j.uj_val;
     const_body_code = ();
     const_universes = univs;
-    const_relevance = UVars.subst_sort_level_relevance usubst r;
+    const_relevance = r;
     const_inline_code = false;
     const_typing_flags = Environ.typing_flags env;
   }
@@ -194,9 +194,10 @@ let make_univ_hyps = function
 
 let infer_parameter ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.parameter_entry_universes in
-  let j = Typeops.infer env entry.parameter_entry_type in
+  let typ = Vars.subst_univs_level_constr usubst entry.parameter_entry_type in
+  let j = Typeops.infer env typ in
   let r = Typeops.assumption_of_judgment env j in
-  let typ = Vars.subst_univs_level_constr usubst j.uj_val in
+  let typ = j.uj_val in
   let undef = Undef entry.parameter_entry_inline_code in
   let hyps = used_section_variables env entry.parameter_entry_secctx None typ in
   {
@@ -206,25 +207,27 @@ let infer_parameter ~sec_univs env entry =
     const_type = typ;
     const_body_code = ();
     const_universes = univs;
-    const_relevance = UVars.subst_sort_level_relevance usubst r;
+    const_relevance = r;
     const_inline_code = false;
     const_typing_flags = Environ.typing_flags env;
   }
 
 let infer_definition ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.definition_entry_universes in
-  let hbody = HConstr.of_constr env entry.definition_entry_body in
+  let body = Vars.subst_univs_level_constr usubst entry.definition_entry_body in
+  let hbody = HConstr.of_constr env body in
   let j = Typeops.infer_hconstr env hbody in
   let typ = match entry.definition_entry_type with
     | None ->
-      Vars.subst_univs_level_constr usubst j.uj_type
+      j.uj_type
     | Some t ->
+      let t = Vars.subst_univs_level_constr usubst t in
       let tj = Typeops.infer_type env t in
       let () = Typeops.check_cast env j DEFAULTcast tj in
-      Vars.subst_univs_level_constr usubst tj.utj_val
+      tj.utj_val
   in
-  let body = Vars.subst_univs_level_constr usubst j.uj_val in
-  let hbody = if body == j.uj_val then Some hbody else None in
+  let body = j.uj_val in
+  let hbody = Some hbody in
   let def = Def body in
   let hyps = used_section_variables env entry.definition_entry_secctx (Some body) typ in
   hbody, {
@@ -242,10 +245,11 @@ let infer_definition ~sec_univs env entry =
 (** Definition is opaque (Qed), so we delay the typing of its body. *)
 let infer_opaque ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.opaque_entry_universes in
-  let typj = Typeops.infer_type env entry.opaque_entry_type in
+  let typ = Vars.subst_univs_level_constr usubst entry.opaque_entry_type in
+  let typj = Typeops.infer_type env typ in
   let context = TyCtx (env, typj, entry.opaque_entry_secctx, usubst, univs) in
   let def = OpaqueDef () in
-  let typ = Vars.subst_univs_level_constr usubst typj.utj_val in
+  let typ = typj.utj_val in
   let hyps = used_section_variables env (Some entry.opaque_entry_secctx) None typ in
   {
     const_hyps = hyps;
@@ -254,7 +258,7 @@ let infer_opaque ~sec_univs env entry =
     const_type = typ;
     const_body_code = ();
     const_universes = univs;
-    const_relevance = UVars.subst_sort_level_relevance usubst @@ Sorts.relevance_of_sort typj.utj_type;
+    const_relevance = Sorts.relevance_of_sort typj.utj_type;
     const_inline_code = false;
     const_typing_flags = Environ.typing_flags env;
   }, context
@@ -269,13 +273,14 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
        assert (UVars.is_empty_sort_subst usubst);
        push_context_set uctx env, Opaqueproof.PrivateMonomorphic uctx
     | Polymorphic _ ->
-       assert (Int.equal valid_signatures 0);
-       push_subgraph uctx env,
-       let private_univs = on_snd (subst_univs_level_constraints (snd usubst)) uctx in
-       Opaqueproof.PrivatePolymorphic private_univs
+       let () = assert (Int.equal valid_signatures 0) in
+       let uctx = on_snd (fun cst -> subst_univs_level_constraints (snd usubst) cst) uctx in
+       push_subgraph uctx env, Opaqueproof.PrivatePolymorphic uctx
   in
-  (* Note: non-trivial trusted side-effects only in monomorphic case *)
+  (* Note: non-trivial usubst only in polymorphic case *)
+  let body = Vars.subst_univs_level_constr usubst body in
   let hbody = HConstr.of_constr env body in
+  (* Note: non-trivial trusted side-effects only in monomorphic case *)
   let () =
     let eff_body, eff_env = skip_trusted_seff valid_signatures hbody env in
     let j = Typeops.infer_hconstr eff_env eff_body in
@@ -289,9 +294,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
   in
   let declared' = check_section_variables env declared (Some body) tyj.utj_val in
   let () = assert (Id.Set.equal declared declared') in
-  (* Note: non-trivial usubst only in polymorphic case *)
-  let def = Vars.subst_univs_level_constr usubst (HConstr.self hbody) in
-  let hbody = if def == HConstr.self hbody then Some hbody else None in
+  let def = HConstr.self hbody in
+  let hbody = Some hbody in
   hbody, def, univs
 
 (*s Global and local constant declaration. *)

kernel/vmbytegen.ml

@@ -139,9 +139,13 @@ type comp_env = {
        reallocate the stack if we lack space. *)
   }
 
+type uinstance =
+| Global (* Treat all levels as globally bound *)
+| Bound of (int * int) (** Size of the local universe instance *)
+
 type glob_env = {
   env : Environ.env;
-  uinst_len : int * int; (** Size of the toplevel universe instance *)
+  uinstance : uinstance;
   mutable fun_code : instruction list; (** Code of closures *)
 }
 
@@ -319,16 +323,43 @@ let pos_instance r sz =
     in
     Kenvacc (r.offset + pos)
 
-let is_toplevel_inst env u =
-  UVars.eq_sizes env.uinst_len (UVars.Instance.length u)
+let is_toplevel_inst env u = match env.uinstance with
+| Global -> false
+| Bound inst  ->
+  UVars.eq_sizes inst (UVars.Instance.length u)
   && let qs, us = UVars.Instance.to_array u in
   Array.for_all_i (fun i q -> Sorts.Quality.equal q (Sorts.Quality.var i)) 0 qs
   && Array.for_all_i (fun i l -> Univ.Level.equal l (Univ.Level.var i)) 0 us
 
-let is_closed_inst u =
+let is_closed_inst env u = match env.uinstance with
+| Global -> true
+| Bound (qlen, ulen) ->
   let qs, us = UVars.Instance.to_array u in
-  Array.for_all (fun q -> Option.is_empty (Sorts.Quality.var_index q)) qs
-  && Array.for_all (fun l -> Option.is_empty (Univ.Level.var_index l)) us
+  let check len = function
+  | None -> true
+  | Some j ->
+    let () = assert (j < len) in
+    false
+  in
+  Array.for_all (fun q -> check qlen (Sorts.Quality.var_index q)) qs
+  && Array.for_all (fun l -> check ulen (Univ.Level.var_index l)) us
+
+let is_closed_sort env s = match env.uinstance with
+| Global -> true
+| Bound (qlen, ulen) ->
+  let check len = function
+  | None -> true
+  | Some j ->
+    let () = assert (j < len) in
+    false
+  in
+  match s with
+  | Sorts.Set | Sorts.Prop | Sorts.SProp -> true
+  | Sorts.Type u ->
+    Univ.Universe.for_all (fun (l, _) -> check ulen (Univ.Level.var_index l)) u
+  | Sorts.QSort (q, u) ->
+    check qlen (Sorts.QVar.var_index q)
+    && Univ.Universe.for_all (fun (l, _) -> check ulen (Univ.Level.var_index l)) u
 
 (*i  Examination of the continuation *)
 
@@ -574,19 +605,11 @@ let rec compile_lam env cenv lam sz cont =
     (* We represent universes as a global constant with local universes
        passed as the local universe instance, where we will substitute (after
        evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *)
-    let has_var = match s with
-    | Sorts.Set | Sorts.Prop | Sorts.SProp -> false
-    | Sorts.Type u ->
-      Univ.Universe.exists (fun (l, _) -> Option.has_some (Univ.Level.var_index l)) u
-    | Sorts.QSort (q, u) ->
-      Option.has_some (Sorts.QVar.var_index q)
-      || Univ.Universe.exists (fun (l, _) -> Option.has_some (Univ.Level.var_index l)) u
-    in
     let compile_instance cenv () sz cont =
       let () = set_max_stack_size cenv sz in
       pos_instance cenv sz :: cont
     in
-    if not has_var then
+    if is_closed_sort env s then
       compile_structured_constant cenv (Const_sort s) sz cont
     else
       comp_app compile_structured_constant compile_instance cenv
@@ -836,7 +859,7 @@ and compile_instance env cenv u sz cont =
   if is_toplevel_inst env u then
     (* Optimization: do not reallocate the same instance *)
     pos_instance cenv sz :: cont
-  else if is_closed_inst u then
+  else if is_closed_inst env u then
     (* Optimization: allocate closed instances globally *)
     compile_structured_constant cenv (Const_univ_instance u) sz cont
   else
@@ -897,7 +920,7 @@ let skip_suffix l =
   in
   match aux l with None -> [] | Some l -> l
 
-let compile ?universes:(universes=(0,0)) env sigma c =
+let compile ~uinstance env sigma c =
   Label.reset_label_counter ();
   let lam = lambda_of_constr env sigma c in
   let params, body = decompose_Llam lam in
@@ -909,10 +932,14 @@ let compile ?universes:(universes=(0,0)) env sigma c =
     Array.of_list @@ skip_suffix mask
   in
   let cont = [Kstop] in
+  let uclosed = match uinstance with
+  | Global -> true
+  | Bound univ -> UVars.eq_sizes (0, 0) univ
+  in
     let cenv, init_code, fun_code =
-      if UVars.eq_sizes universes (0,0) then
+      if uclosed then
         let cenv = empty_comp_env () in
-        let env = { env; fun_code = []; uinst_len = (0,0) } in
+        let env = { env; fun_code = []; uinstance } in
         let cont = compile_lam env cenv lam 0 cont in
         let cont = ensure_stack_capacity cenv cont in
         cenv, cont, env.fun_code
@@ -924,7 +951,7 @@ let compile ?universes:(universes=(0,0)) env sigma c =
         let full_arity = arity + 1 in
         let r_fun = comp_env_fun ~univs:true arity in
         let lbl_fun = Label.create () in
-        let env = { env; fun_code = []; uinst_len = universes } in
+        let env = { env; fun_code = []; uinstance } in
         let cont_fun = compile_lam env r_fun body full_arity [Kreturn full_arity] in
         let cont_fun = ensure_stack_capacity r_fun cont_fun in
         let () = push_fun env (add_grab full_arity lbl_fun cont_fun) in
@@ -947,8 +974,8 @@ let warn_compile_error =
   CWarnings.create ~name:"bytecode-compiler-failed-compilation" ~category:CWarnings.CoreCategories.bytecode_compiler
     Vmerrors.pr_error
 
-let compile ~fail_on_error ?universes env sigma c =
-  try NewProfile.profile "vm_compile" (fun () -> Some (compile ?universes env sigma c)) ()
+let compile ~fail_on_error ~uinstance env sigma c =
+  try NewProfile.profile "vm_compile" (fun () -> Some (compile ~uinstance env sigma c)) ()
   with Vmerrors.CompileError msg as exn ->
     let exn = Exninfo.capture exn in
     if fail_on_error then
@@ -978,9 +1005,13 @@ let compile_constant_body ~fail_on_error env univs = function
       match alias with
       | Some kn -> Some (BCalias kn)
       | _ ->
-        let res = compile ~fail_on_error ~universes:instance_size env (empty_evars env) body in
+        let uinstance = Bound instance_size in
+        let res = compile ~fail_on_error ~uinstance env (empty_evars env) body in
         Option.map (fun (mask, code, patch) -> BCdefined (mask, code, patch)) res
 
+let compile ~fail_on_error env sigma c =
+  compile ~fail_on_error ~uinstance:Global env sigma c
+
 (* Shortcut of the previous function used during module strengthening *)
 
 let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn))

kernel/vmbytegen.mli

@@ -13,9 +13,8 @@ open Constr
 open Declarations
 open Environ
 
-(** Should only be used for monomorphic terms *)
 val compile :
-  fail_on_error:bool -> ?universes:int*int ->
+  fail_on_error:bool ->
   env -> Genlambda.evars -> constr ->
   (bool array * to_patch * patches) option
 

test-suite/bugs/bug_21405.v

@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+
+Definition T@{u} : Set := unit.
+Definition U@{u} : Type@{u+1} := Type@{u}.
+
+Definition anomaly := (tt <: T).
+Definition anomaly' := (Type <: U).