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

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|]|]
 

dev/ci/user-overlays/21678-ppedrot-preserve-let-in-kernel-the-return.sh

@@ -0,0 +1 @@
+overlay fiat_crypto https://github.com/ppedrot/fiat-crypto preserve-let-in-kernel-the-return 21678

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}