Let definitions must not contain side-effects when reaching the kernel.

Let definitions have the same behaviour if they are ended with a Qed or a
Defined command, i.e. they are treated as if they were transparent. Indeed,
it doesn't make sense for them to be opaque as they are going to be expanded
away at the end of the section.

For an unknown reason, handling of side-effects in Let definitions considers
them as if they were opaque, i.e. the effects are inlined in the definition.

This discrepancy has bad consequences in the kernel, where one is forced to
juggle with universe constraints generated by polymorphic Let definitions.
As a first phase of cleaning, we simply enforce by typing that Let definitions
should be purified before reaching the kernel.

This has the intended side-effect to make side-effects persistent in Let
definitions, as if they were indeed truly transparent.

1 files changed, 4 insertions, 8 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 70dd6438d..761eab511 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -533,14 +533,10 @@ type side_effect_role =
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
 
-let export_side_effects mb env ce =
-  match ce with
-  | ParameterEntry e -> [], ParameterEntry e
-  | ProjectionEntry e -> [], ProjectionEntry e
-  | DefinitionEntry c ->
+let export_side_effects mb env c =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
-      let ce = DefinitionEntry { c with
+      let ce = { c with
         const_entry_body = Future.chain body
           (fun (b_ctx, _) -> b_ctx, ()) } in
       let not_exists (c,_,_,_) =
@@ -609,9 +605,9 @@ let translate_recipe env kn r =
   let hcons = DirPath.is_empty dir in
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
-let translate_local_def mb env id centry =
+let translate_local_def env id centry =
   let open Cooking in
-  let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
+  let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with