Fix hashconsing of terms in the kernel.

In one case, the hashconsed type of a judgement was not used anywhere else.

In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.

5 files changed, 19 insertions, 8 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f5059cd75..a9f212393 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -191,15 +191,19 @@ let lift_univs cb subst =
       subst, Univ.UContext.make (inst,cstrs')
   else subst, cb.const_universes
 
-let cook_constant env { from = cb; info } =
+let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
+  let map c =
+    let c = abstract_constant_body (expmod c) hyps in
+    if hcons then hcons_constr c else c
+  in
   let body = on_body modlist (hyps, usubst, abs_ctx)
-    (fun c -> abstract_constant_body (expmod c) hyps)
+    map
     cb.const_body
   in
   let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index eb4073096..7d47eba23 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,7 @@ type result =
     bool * constant_universes * inline
     * Context.Named.t option
 
-val cook_constant : env -> recipe -> result
+val cook_constant : hcons:bool -> env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f147ea343..74ba73508 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -48,7 +48,10 @@ let turn_indirect dp o (prfs,odp) = match o with
       then CErrors.anomaly (Pp.str "Indirect in a different table")
       else CErrors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
-      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
+      (** Uncomment to check dynamically that all terms turned into
+          indirections are hashconsed. *)
+(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
+(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
       let id = Int.Map.cardinal prfs in
       let prfs = Int.Map.add id (d,cu) prfs in
       let ndp =
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5139cf051..3897d5e51 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,8 +28,9 @@ val empty_opaquetab : opaquetab
 (** From a [proofterm] to some [opaque]. *)
 val create : proofterm -> opaque
 
-(** Turn a direct [opaque] into an indirect one, also hashconses constr.
- *  The integer is an hint of the maximum id used so far *)
+(** Turn a direct [opaque] into an indirect one. It is your responsibility to
+  hashcons the inner term beforehand. The integer is an hint of the maximum id
+  used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 (** From a [opaque] back to a [constr]. This might use the
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eb2c040e..2eba1eb2a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -186,7 +186,8 @@ let rec unzip ctx j =
       unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
-  { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
+  (** Do not hashcons type: it is not used by the callers of this function. *)
+  { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} 
 
 let feedback_completion_typecheck =
   let open Feedback in
@@ -507,7 +508,9 @@ let translate_local_assum env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant env r)
+  let (_, dir, _) = Constant.repr3 kn in
+  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 def,typ,proj,poly,univs,inline_code,ctx =