[econstr] Forbid calling `to_constr` in open terms.

We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]

Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.

Now, grepping for `~abort:false` should return the questionable
parts of the system.

Not a lot of places had to be fixed, some comments:

- problems with the interface due to `Evd/Constr` [`Evd.define` being
  the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.

A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.

3 files changed, 21 insertions, 12 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bd47a04f1..01b4fe851 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -40,7 +40,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
 val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
-val to_constr : evar_map -> t -> Constr.t
+val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
 val unsafe_eq : (t, Constr.t) eq
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
@@ -110,11 +110,16 @@ let of_constr c = c
 let unsafe_to_constr c = c
 let unsafe_eq = Refl
 
-let rec to_constr sigma c = match Constr.kind c with
+let to_constr ?(abort_on_undefined_evars=true) sigma c =
+let rec to_constr c = match Constr.kind c with
 | Evar ev ->
   begin match safe_evar_value sigma ev with
-  | Some c -> to_constr sigma c
-  | None -> Constr.map (fun c -> to_constr sigma c) c
+  | Some c -> to_constr c
+  | None ->
+    if abort_on_undefined_evars then
+      anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
+    else
+      Constr.map (fun c -> to_constr c) c
   end
 | Sort (Sorts.Type u) ->
   let u' = Evd.normalize_universe sigma u in
@@ -128,7 +133,8 @@ let rec to_constr sigma c = match Constr.kind c with
 | Construct (co, u) when not (Univ.Instance.is_empty u) ->
   let u' = Evd.normalize_universe_instance sigma u in
   if u' == u then c else mkConstructU (co, u')
-| _ -> Constr.map (fun c -> to_constr sigma c) c
+| _ -> Constr.map (fun c -> to_constr c) c
+in to_constr c
 
 let of_named_decl d = d
 let unsafe_to_named_decl d = d
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 28c9dd3c2..dac937457 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter
 
 val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 
-val to_constr : Evd.evar_map -> t -> Constr.t
-(** Returns the evar-normal form of the argument, and cast it as a theoretically
-    evar-free term. In practice this function does not check that the result
-    is actually evar-free, it is currently the duty of the caller to do so.
-    This might change in the future. *)
+val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
+(** Returns the evar-normal form of the argument. Note that this
+   function is supposed to be called when the original term has not
+   more free-evars anymore. If you need compatibility with the old
+   semantics, set [abort_on_undefined_evars] to [false].
+
+    For getting the evar-normal form of a term with evars see
+   {!Evarutil.nf_evar}. *)
 
 val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 45760c6b4..c707b37b6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -72,9 +72,9 @@ let flush_and_check_evars sigma c =
 (** Term exploration up to instantiation. *)
 let kind_of_term_upto = EConstr.kind_upto
 
-let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t)
+let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
 let whd_evar = EConstr.whd_evar
-let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c)
+let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c)
 
 let j_nf_evar sigma j =
   { uj_val = nf_evar sigma j.uj_val;