Somehow fixing a side-effect bug in tactics-in-terms.

Before this patch, when tactics-in-terms were relying on the ugly environment-
modifying primitives such as tclABSTRACT, the returned term was ill-typed
because the resulting effects were just dropped. Now we modify the returned
term on the fly, effectively getting rid of the effects it may depend on.

Yet, this is not completely satisfactory, because the tactic may solve some
goals at distance (I would have said by side-effect, but this is ambiguous
here). If ever the resulting terms are depending on the side-effects of the
tactic, then we are still unsound.

This patch should handle most of the use-cases gracefully. To really solve this
issue, we should rewrite the pretyper in the new monad, which is easier said
than done.

1 files changed, 18 insertions, 0 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d34972fb5..39070436e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2328,6 +2328,12 @@ let _ =
     if has_type arg (glbwit wit_tactic) then
       let tac = out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
+      (** Save the initial side-effects to restore them afterwards. We set the
+          current set of side-effects to be empty so that we can retrieve the
+          ones created during the tactic invocation easily. *)
+      let eff = Evd.eval_side_effects sigma in
+      let sigma = Evd.drop_side_effects sigma in
+      (** Start a proof *)
       let prf = Proof.start sigma [env, ty] in
       let (prf, _) =
         try Proof.run_tactic env tac prf
@@ -2337,11 +2343,23 @@ let _ =
           let e = Backtrace.app_backtrace ~src ~dst:e in
           raise e
       in
+      (** Plug back the retrieved sigma *)
       let sigma = Proof.in_proof prf (fun sigma -> sigma) in
       let ans = match Proof.initial_goals prf with
       | [c, _] -> c
       | _ -> assert false
       in
+      (** [neff] contains the freshly generated side-effects *)
+      let neff = Evd.eval_side_effects sigma in
+      (** Reset the old side-effects *)
+      let sigma = Evd.drop_side_effects sigma in
+      let sigma = Evd.emit_side_effects eff sigma in
+      (** Get rid of the fresh side-effects by internalizing them in the term
+          itself. Note that this is unsound, because the tactic may have solved
+          other goals that were already present during its invocation, so that
+          those goals rely on effects that are not present anymore. Hopefully,
+          this hack will work in most cases. *)
+      let ans = Term_typing.handle_side_effects env ans neff in
       ans, sigma
     else
       failwith "not a tactic"