Introduce an efficient typing rule for let-bindings in Typeops.

When the expand_let typing flag is set in the environment, we change
the kernel typing rule for let-bindings from

let x := t in u : T{x := t}

to

let x := t in u : let x := t in T.

We cannot do this by default since it may change the inferred type for
some expressions, which is returned when the expected type is not
provided. To work around this, we statically set the flag in expressions
for which the precise inferred type is not relevant. For now there is
no user-facing flag that would allow setting this option in a more
fine-grained way though, but it is easy to fix.

This is a revival of #13606 and a partial fix of #11838. The latter still
suffers from superlinear blowups in unrelated parts of the kernel, namely
VM and native compilation.

Author: ppedrot

checker/checkFlags.ml

@@ -23,6 +23,7 @@ let set_local_flags flags env =
     share_reduction = flags.share_reduction;
     unfold_dep_heuristic = flags.unfold_dep_heuristic;
     allow_uip = flags.allow_uip;
+    expand_let = flags.expand_let;
     (* These flags may not *)
     enable_VM = envflags.enable_VM;
     enable_native_compiler = envflags.enable_native_compiler;

checker/values.ml

@@ -357,7 +357,7 @@ let v_typing_flags =
   v_tuple "typing_flags"
     [|v_bool; v_bool; v_bool; v_bool;
       v_oracle; v_bool; v_bool;
-      v_bool; v_bool; v_bool; v_bool; v_bool; v_bool|]
+      v_bool; v_bool; v_bool; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 1 [|[|v_abs_context|]|]
 

kernel/constant_typing.ml

@@ -24,6 +24,12 @@ open UVars
 
 module NamedDecl = Context.Named.Declaration
 
+(** Use this function when typing terms where the precise value of the inferred
+    type from the equivalence class of conversion does not matter. It makes it
+    more efficient. *)
+let unset_let_expansion env =
+  Environ.set_typing_flags { (Environ.typing_flags env) with expand_let = false } env
+
 (* Checks the section variables for the body.
    Returns the closure of the union with the variables in the type.
 *)
@@ -174,7 +180,8 @@ 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
+  (* Inferred type is not returned *)
+  let j = Typeops.infer (unset_let_expansion env) symb_entry_type in
   let r = Typeops.assumption_of_judgment env j in
   {
     const_hyps = [];
@@ -196,7 +203,8 @@ 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 typ = Vars.subst_univs_level_constr usubst entry.parameter_entry_type in
-  let j = Typeops.infer env typ in
+  (* Inferred type is not returned *)
+  let j = Typeops.infer (unset_let_expansion env) typ in
   let r = Typeops.assumption_of_judgment env j in
   let typ = j.uj_val in
   let undef = Undef entry.parameter_entry_inline_code in
@@ -217,7 +225,9 @@ let infer_definition ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.definition_entry_universes 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
+  (* When the expected type is provided, don't care about the inferred type *)
+  let jenv = if Option.is_empty entry.definition_entry_type then env else unset_let_expansion env in
+  let j = Typeops.infer_hconstr jenv hbody in
   let typ = match entry.definition_entry_type with
     | None ->
       j.uj_type
@@ -284,7 +294,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
   (* 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
+    (* Inferred type is not returned *)
+    let j = Typeops.infer_hconstr (unset_let_expansion eff_env) eff_body in
     let () = assert (HConstr.self eff_body == j.uj_val) in
     let j = { uj_val = HConstr.self hbody; uj_type = j.uj_type } in
     Typeops.check_cast eff_env j DEFAULTcast tyj
@@ -302,12 +313,15 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
 (*s Global and local constant declaration. *)
 
 let infer_local_assum env t =
-  let j = Typeops.infer env t in
+  (* Inferred type is not returned *)
+  let j = Typeops.infer (unset_let_expansion env) t in
   let t = Typeops.assumption_of_judgment env j in
     j.uj_val, t
 
 let infer_local_def env _id { secdef_body; secdef_type; } =
-  let j = Typeops.infer env secdef_body in
+  (* When the expected type is provided, don't care about the inferred type *)
+  let jenv = if Option.is_empty secdef_type then env else unset_let_expansion env in
+  let j = Typeops.infer jenv secdef_body in
   let typ = match secdef_type with
     | None -> j.uj_type
     | Some typ ->

kernel/declarations.mli

@@ -89,6 +89,9 @@ type typing_flags = {
   unfold_dep_heuristic : bool;
   (** If [true], use dependency heuristic when unfolding constants during conversion *)
 
+  expand_let : bool;
+  (** Whether to infer [let x := t in u : T{x := t}] or [let x := t in u : let x := t in T]  *)
+
   enable_VM : bool;
   (** If [false], all VM conversions fall back to interpreted ones *)
 

kernel/declareops.ml

@@ -27,6 +27,7 @@ let safe_flags oracle = {
   conv_oracle = oracle;
   share_reduction = true;
   unfold_dep_heuristic = false;
+  expand_let = true;
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;

kernel/environ.ml

@@ -577,6 +577,7 @@ let same_flags {
      indices_matter;
      share_reduction;
      unfold_dep_heuristic;
+     expand_let;
      enable_VM;
      enable_native_compiler;
      impredicative_set;
@@ -591,6 +592,7 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   unfold_dep_heuristic == alt.unfold_dep_heuristic &&
+  expand_let == alt.expand_let &&
   enable_VM == alt.enable_VM &&
   enable_native_compiler == alt.enable_native_compiler &&
   impredicative_set == alt.impredicative_set &&

kernel/typeops.ml

@@ -733,7 +733,7 @@ and execute_aux tbl env cstr =
       let () = check_cast env c1 c1t DEFAULTcast c2 in
       let env1 = push_rel (LocalDef (name,c1,c2)) env in
       let c3t = execute tbl env1 c3 in
-      subst1 c1 c3t
+      if (Environ.typing_flags env).expand_let then subst1 c1 c3t else mkLetIn (name, c1, c2, c3t)
 
     | Cast (c,k,t) ->
       let ct = execute tbl env c in
@@ -919,7 +919,9 @@ let infer_type env constr =
   let () = check_wellformed_universes env constr in
   let hconstr = HConstr.of_constr env constr in
   let constr = HConstr.self hconstr in
-  let t = execute env hconstr in
+  (* Returned j_type is not observable *)
+  let tenv = Environ.set_typing_flags { (Environ.typing_flags env) with expand_let = false } env in
+  let t = execute tenv hconstr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}