qvar_irrelevant in default_evar_handler: assert that the qvar is known

kernel/cClosure.ml

@@ -130,11 +130,13 @@ type 'constr evar_handler = {
   qvar_irrelevant : Sorts.QVar.t -> bool;
 }
 
-let default_evar_handler = {
+let default_evar_handler env = {
   evar_expand = (fun _ -> assert false);
   evar_repack = (fun _ -> assert false);
   evar_irrelevant = (fun _ -> assert false);
-  qvar_irrelevant = (fun _ -> false);
+  qvar_irrelevant = (fun q ->
+      assert (Sorts.QVar.Set.mem q env.env_qualities);
+      false);
 }
 
 (** Reduction cache *)
@@ -1637,7 +1639,8 @@ let whd_stack infos tab m stk = match m.mark with
   in
   k
 
-let create_infos i_mode ?univs ?(evars=default_evar_handler) i_flags i_env =
+let create_infos i_mode ?univs ?evars i_flags i_env =
+  let evars = Option.default (default_evar_handler i_env) evars in
   let i_univs = Option.default (Environ.universes i_env) univs in
   let i_share = (Environ.typing_flags i_env).Declarations.share_reduction in
   let i_cache = {i_env; i_sigma = evars; i_share; i_univs; i_mode} in

kernel/cClosure.mli

@@ -128,7 +128,7 @@ type 'constr evar_handler = {
   qvar_irrelevant : Sorts.QVar.t -> bool;
 }
 
-val default_evar_handler : 'constr evar_handler
+val default_evar_handler : env -> 'constr evar_handler
 val create_conv_infos :
   ?univs:UGraph.t -> ?evars:constr evar_handler -> reds -> env -> clos_infos
 val create_clos_infos :

kernel/conversion.ml

@@ -924,7 +924,7 @@ let () =
   in
   CClosure.set_conv conv
 
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler) t1 t2 =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 =
   let univs = Environ.universes env in
   let b =
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2
@@ -938,7 +938,7 @@ let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=defaul
 let conv = gen_conv CONV
 let conv_leq = gen_conv CUMUL
 
-let generic_conv cv_pb ~l2r reds env ?(evars=default_evar_handler) univs t1 t2 =
+let generic_conv cv_pb ~l2r reds env ?(evars=default_evar_handler env) univs t1 t2 =
   let graph = Environ.universes env in
   let (s, _) =
     clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2

kernel/genlambda.ml

@@ -55,8 +55,8 @@ and 'v fix_decl = Name.t Context.binder_annot array * 'v lambda array * 'v lambd
 type evars =
   { evars_val : constr CClosure.evar_handler }
 
-let empty_evars =
-  { evars_val = CClosure.default_evar_handler }
+let empty_evars env =
+  { evars_val = CClosure.default_evar_handler env }
 
 (** Printing **)
 

kernel/genlambda.mli

@@ -52,7 +52,7 @@ and 'v fix_decl = Name.t Context.binder_annot array * 'v lambda array * 'v lambd
 type evars =
   { evars_val : constr CClosure.evar_handler }
 
-val empty_evars : evars
+val empty_evars : Environ.env -> evars
 
 (** {5 Manipulation functions} *)
 

kernel/nativecode.ml

@@ -2247,7 +2247,7 @@ let compile_deps env sigma prefix init t =
   aux env 0 init t
 
 let compile_constant_field env con acc cb =
-    let gl = compile_constant env empty_evars con cb in
+    let gl = compile_constant env (empty_evars env) con cb in
     gl@acc
 
 let compile_mind_field mp l acc mb =

kernel/typeops.ml

@@ -387,7 +387,7 @@ let check_cast env c ct k expected_type =
     | DEFAULTcast ->
       default_conv CUMUL env ct expected_type
     | NATIVEcast ->
-      let sigma = Genlambda.empty_evars in
+      let sigma = Genlambda.empty_evars env in
       Nativeconv.native_conv CUMUL sigma env ct expected_type
   with NotConvertible ->
     error_actual_type env (make_judge c ct) expected_type

kernel/vconv.ml

@@ -222,7 +222,7 @@ let vm_conv cv_pb env t1 t2 =
     let state = (univs, checked_universes) in
     let _ : UGraph.t =
       NewProfile.profile "vm_conv" (fun () ->
-          vm_conv_gen cv_pb Genlambda.empty_evars env state t1 t2)
+          vm_conv_gen cv_pb (Genlambda.empty_evars env) env state t1 t2)
         ()
     in
     ()

kernel/vmbytegen.ml

@@ -963,7 +963,7 @@ 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 body in
+          let res = compile ~fail_on_error ~universes:instance_size env (empty_evars env) body in
           Option.map (fun (code, fv) -> BCdefined (code, fv)) res
 
 (* Shortcut of the previous function used during module strengthening *)