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.

6 files changed, 90 insertions, 94 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 0adad1419..8781c8719 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -31,64 +31,6 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
-(** Declaration of section variables and local definitions *)
-
-type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
-
-type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-
-let cache_variable ((sp,_),o) =
-  match o with
-  | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(p,d,mk)) ->
-  (* Constr raisonne sur les noms courts *)
-  if variable_exists id then
-    alreadydeclared (Id.print id ++ str " already exists");
-
-  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty,poly),ctx) in
-      let impl = if impl then Implicit else Explicit in
-	impl, true, poly, ctx
-    | SectionLocalDef (de) ->
-      let univs = Global.push_named_def (id,de) in
-      let poly = match de.const_entry_universes with
-      | Monomorphic_const_entry _ -> false
-      | Polymorphic_const_entry _ -> true
-      in
-      Explicit, de.const_entry_opaque,
-      poly, univs in
-  Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
-  Dischargedhypsmap.set_discharged_hyps sp [];
-  add_variable_data id (p,opaq,ctx,poly,mk)
-
-let discharge_variable (_,o) = match o with
-  | Inr (id,_) ->
-    if variable_polymorphic id then None
-    else Some (Inl (variable_context id))
-  | Inl _ -> Some o
-
-type variable_obj =
-    (Univ.ContextSet.t, Id.t * variable_declaration) union
-
-let inVariable : variable_obj -> obj =
-  declare_object { (default_object "VARIABLE") with
-    cache_function = cache_variable;
-    discharge_function = discharge_variable;
-    classify_function = (fun _ -> Dispose) }
-
-(* for initial declaration *)
-let declare_variable id obj =
-  let oname = add_leaf id (inVariable (Inr (id,obj))) in
-  declare_var_implicits id;
-  Notation.declare_ref_arguments_scope (VarRef id);
-  Heads.declare_head (EvalVarRef id);
-  oname
-
-
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -195,6 +137,20 @@ let update_tables c =
   Heads.declare_head (EvalConstRef c);
   Notation.declare_ref_arguments_scope (ConstRef c)
 
+let register_side_effect (c, role) =
+  let o = inConstant {
+    cst_decl = None;
+    cst_hyps = [] ;
+    cst_kind = IsProof Theorem;
+    cst_locl = false;
+  } in
+  let id = Label.to_id (pi3 (Constant.repr3 c)) in
+  ignore(add_leaf id o);
+  update_tables c;
+  match role with
+  | Safe_typing.Subproof -> ()
+  | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+
 let declare_constant_common id cst =
   let o = inConstant cst in
   let _, kn as oname = add_leaf id o in
@@ -229,25 +185,11 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
       (** This globally defines the side-effects in the environment. We mark
           exported constants as being side-effect not to redeclare them at
           caching time. *)
-      let cd, export = Global.export_private_constants ~in_section cd in
-      export, ConstantEntry (PureEntry, cd)
+      let de, export = Global.export_private_constants ~in_section de in
+      export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
-  let iter_eff (c, role) =
-    let o = inConstant {
-      cst_decl = None;
-      cst_hyps = [] ;
-      cst_kind = IsProof Theorem;
-      cst_locl = false;
-    } in
-    let id = Label.to_id (pi3 (Constant.repr3 c)) in
-    ignore(add_leaf id o);
-    update_tables c;
-    match role with
-    | Safe_typing.Subproof -> ()
-    | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
-  in
-  let () = List.iter iter_eff export in
+  let () = List.iter register_side_effect export in
   let cst = {
     cst_decl = Some decl;
     cst_hyps = [] ;
@@ -265,6 +207,65 @@ let declare_definition ?(internal=UserIndividualRequest)
     declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
+(** Declaration of section variables and local definitions *)
+
+type section_variable_entry =
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+
+type variable_declaration = DirPath.t * section_variable_entry * logical_kind
+
+let cache_variable ((sp,_),o) =
+  match o with
+  | Inl ctx -> Global.push_context_set false ctx
+  | Inr (id,(p,d,mk)) ->
+  (* Constr raisonne sur les noms courts *)
+  if variable_exists id then
+    alreadydeclared (Id.print id ++ str " already exists");
+
+  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ((ty,ctx),poly,impl) ->
+      let () = Global.push_named_assum ((id,ty,poly),ctx) in
+      let impl = if impl then Implicit else Explicit in
+        impl, true, poly, ctx
+    | SectionLocalDef (de) ->
+      let (de, eff) = Global.export_private_constants ~in_section:true de in
+      let () = List.iter register_side_effect eff in
+      let univs = Global.push_named_def (id,de) in
+      let poly = match de.const_entry_universes with
+      | Monomorphic_const_entry _ -> false
+      | Polymorphic_const_entry _ -> true
+      in
+      Explicit, de.const_entry_opaque,
+      poly, univs in
+  Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
+  add_section_variable id impl poly ctx;
+  Dischargedhypsmap.set_discharged_hyps sp [];
+  add_variable_data id (p,opaq,ctx,poly,mk)
+
+let discharge_variable (_,o) = match o with
+  | Inr (id,_) ->
+    if variable_polymorphic id then None
+    else Some (Inl (variable_context id))
+  | Inl _ -> Some o
+
+type variable_obj =
+    (Univ.ContextSet.t, Id.t * variable_declaration) union
+
+let inVariable : variable_obj -> obj =
+  declare_object { (default_object "VARIABLE") with
+    cache_function = cache_variable;
+    discharge_function = discharge_variable;
+    classify_function = (fun _ -> Dispose) }
+
+(* for initial declaration *)
+let declare_variable id obj =
+  let oname = add_leaf id (inVariable (Inr (id,obj))) in
+  declare_var_implicits id;
+  Notation.declare_ref_arguments_scope (VarRef id);
+  Heads.declare_head (EvalVarRef id);
+  oname
+
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5150ad411..fa984515a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -383,8 +383,7 @@ let safe_push_named d env =
 
 let push_named_def (id,de) senv =
   let open Entries in
-  let trust = Term_typing.SideEffects senv.revstruct in
-  let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in
+  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
   let poly = match de.Entries.const_entry_universes with
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a30bb37e6..fbc398a2a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer
+  Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
@@ -106,8 +106,8 @@ type exported_private_constant =
   Constant.t * private_constant_role
 
 val export_private_constants : in_section:bool ->
-  private_constants Entries.constant_entry ->
-  (unit Entries.constant_entry * exported_private_constant list) safe_transformer
+  private_constants Entries.definition_entry ->
+  (unit Entries.definition_entry * exported_private_constant list) safe_transformer
 
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
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
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 55da4197e..c771452a1 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,7 +18,7 @@ type _ trust =
 | Pure : unit trust
 | SideEffects : structure_body -> side_effects trust
 
-val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
+val translate_local_def : env -> Id.t -> unit definition_entry ->
   constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types
@@ -62,8 +62,8 @@ type exported_side_effect =
  * be pushed in the safe_env by safe typing.  The main constant entry
  * needs to be translated as usual after this step. *)
 val export_side_effects :
-  structure_body -> env -> side_effects constant_entry ->
-    exported_side_effect list * unit constant_entry
+  structure_body -> env -> side_effects definition_entry ->
+    exported_side_effect list * unit definition_entry
 
 val translate_mind :
   env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/library/global.mli b/library/global.mli
index 324181e79..2a646386e 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,11 +32,11 @@ val set_typing_flags : Declarations.typing_flags -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t
+val push_named_def   : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t
 
 val export_private_constants : in_section:bool ->
-  Safe_typing.private_constants Entries.constant_entry ->
-  unit Entries.constant_entry * Safe_typing.exported_private_constant list
+  Safe_typing.private_constants Entries.definition_entry ->
+  unit Entries.definition_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t