From 2af40ea1f8ef87664ca90a3f6077459c6579288b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Mon, 8 Dec 2025 10:41:42 +0100 Subject: [PATCH 1/2] Allow bound universe variables in the VM. We simply treat them as global levels, by clearly separating the compilation of code that is supposed to quantify over levels from the one that merely passes them around. (cherry picked from commit fe06b974cc32be9070119e433398e824a1bd71e9) --- kernel/vmbytegen.ml | 77 ++++++++++++++++++++++++++----------- kernel/vmbytegen.mli | 3 +- test-suite/bugs/bug_21405.v | 7 ++++ 3 files changed, 62 insertions(+), 25 deletions(-) create mode 100644 test-suite/bugs/bug_21405.v diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index c0e9eac2e92e..cef33cd6a45a 100644 --- a/kernel/vmbytegen.ml +++ b/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)) diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli index bd068b40a08e..45c5659f7741 100644 --- a/kernel/vmbytegen.mli +++ b/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 diff --git a/test-suite/bugs/bug_21405.v b/test-suite/bugs/bug_21405.v new file mode 100644 index 000000000000..ce08338da86c --- /dev/null +++ b/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). From eee9597b2633a44f34911ef7862d84f51c9f92bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 7 Dec 2025 13:45:53 +0100 Subject: [PATCH 2/2] Perform kernel typing after universe abstraction for polymorphic code. This is safer and will make it possible to simplify the code that pushes bound levels and sorts in the environment. We also share more hashconsing for polymorphic entries this way. This also probably fixes a bug with the relevance computation for definitions. The environment passed to the function was the one with the concrete levels, but the term argument was expected to live in the abstracted context. (cherry picked from commit 4bd12beab19887f4bc821061d67fd8f5ee5f767e) --- kernel/constant_typing.ml | 56 +++++++++++++++++++++------------------ 1 file changed, 30 insertions(+), 26 deletions(-) diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml index c8aa654d5f3b..49ad4b5339f1 100644 --- a/kernel/constant_typing.ml +++ b/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. *)