Tac2externals: wrap closures to make them pure

otherwise it can be quite footgunny (even though it's hard to get a visible bug without the ltac2 compiler), for instance the current implementation of Array.set is incorrect without this.

See also SkySkimmer/coq-ltac2-compiler#17 and
https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/thunking.20and.20.60thaw.60

Close coq#18631

plugins/ltac2/tac2externals.ml

@@ -82,8 +82,11 @@ let define : type v f. _ -> (v,f) spec -> f -> unit = fun n ar v ->
     match ar with
     | S (V tr) -> tr v
     | S (F _) ->
-        let cl = Tac2val.mk_closure (arity_of ar) (interp_spec ar v) in
-        Tac2ffi.of_closure cl
+      let arity = arity_of ar in
+      let v = interp_spec ar v in
+      let v = Tac2val.purify_closure arity v in
+      let cl = Tac2val.mk_closure arity v in
+      Tac2ffi.of_closure cl
     | _ -> invalid_arg "Tac2def.define: not a pure value"
   in
   Tac2env.define_primitive n v

plugins/ltac2/tac2val.ml

@@ -123,3 +123,10 @@ let abstract n f =
 let annotate_closure fr (MLTactic (arity, fr0, f)) =
   assert (Option.is_empty fr0);
   MLTactic (arity, Some fr, f)
+
+let rec purify_closure : type a. a arity -> (unit -> a) -> a = fun arity f ->
+  match arity with
+  | OneAty -> (fun x -> Proofview.tclUNIT () >>= fun () -> f () x)
+  | AddAty a -> (fun x -> purify_closure a (fun () -> f () x))
+
+let purify_closure ar f = purify_closure ar (fun () -> f)

plugins/ltac2/tac2val.mli

@@ -57,12 +57,19 @@ val arity_one : (valexpr -> valexpr Proofview.tactic) arity
 val arity_suc : 'a arity -> (valexpr -> 'a) arity
 
 val mk_closure : 'v arity -> 'v -> closure
+(** The arrows in ['v] should be pure. Use [tclLIFT] or do
+    [tclUNIT () >>= fun () -> f args] when you need effects. *)
+
 val mk_closure_val : 'v arity -> 'v -> valexpr
 (** Composition of [mk_closure] and [ValCls] *)
 
 val annotate_closure : Tac2expr.frame -> closure -> closure
 (** The closure must not be already annotated *)
 
+val purify_closure : 'v arity -> 'v -> 'v
+(** For internal use (Tac2externals). Wraps the applications of the ['v] argument
+    to make it pure. *)
+
 val to_closure : valexpr -> closure
 
 val apply : closure -> valexpr list -> valexpr Proofview.tactic