[uconstr]: use a closure instead of eager substitution.

This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine.

As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.

5 files changed, 32 insertions, 31 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d682574779..27986eab6c 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -44,7 +44,7 @@ let instantiate_tac n (ist,rawc) ido =
     let evi = Evd.find sigma evk in
     let filtered = Evd.evar_filtered_env evi in
     let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
-    let sigma' = w_refine (evk,evi) ((constrvars, ist.Geninterp.lfun),rawc) sigma in
+    let sigma' = w_refine (evk,evi) ((constrvars,Names.Id.Map.empty, ist.Geninterp.lfun),rawc) sigma in
     tclEVARS sigma' gl
   end
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a7d95c5e89..214db580a0 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -359,12 +359,14 @@ let refine_red_flags =
 
 let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
 
-let refine_tac c =
+let refine_tac {Glob_term.closure=closure;term=term} =
     let c = Goal.Refinable.make begin fun h ->
       Goal.bind Goal.concl (fun concl ->
         let flags = Pretyping.all_no_fail_flags in
         let tycon = Pretyping.OfType concl in
-        Goal.Refinable.constr_of_raw h tycon flags Id.Map.(empty,empty) c)
+        Goal.Refinable.constr_of_raw h tycon flags
+          Glob_term.(closure.typed,closure.untyped,Id.Map.empty) term
+      )
     end in
     Proofview.Goal.lift c begin fun c ->
       Proofview.tclSENSITIVE (Goal.refine c) <*>
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 2937d42731..c1f9fe30d9 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -150,10 +150,9 @@ let coerce_to_constr env v =
 let coerce_to_uconstr env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_uconstr) then
-    Lazy.lazy_from_val (out_gen (topwit wit_uconstr) v)
+    out_gen (topwit wit_uconstr) v
   else
-    let (_ctx,c) = coerce_to_constr env v in
-    lazy (Detyping.detype false [] [] c)
+    raise (CannotCoerceTo "an untyped term")
 
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 171269f929..7b278996e0 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -37,8 +37,8 @@ sig
 
   val of_constr : constr -> t
   val to_constr : t -> constr option
-  val of_uconstr : Glob_term.glob_constr -> t
-  val to_uconstr : t -> Glob_term.glob_constr option
+  val of_uconstr : Glob_term.closed_glob_constr -> t
+  val to_uconstr : t -> Glob_term.closed_glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
@@ -58,7 +58,7 @@ val coerce_to_int : Value.t -> int
 
 val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
 
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr Lazy.t
+val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
 
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 95752c99a8..9ec486c1c3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -457,39 +457,36 @@ let interp_fresh_id ist env l =
 
 (* Extract the uconstr list from lfun *)
 let extract_ltac_uconstr_values ist env =
-  let fold id v accu =
+  let open Glob_term in
+  let fold id v ({typed;untyped} as accu) =
     try
       let c = coerce_to_uconstr env v in
-      Id.Map.add id c accu
-    with CannotCoerceTo _ -> accu
+      { typed ; untyped = Id.Map.add id c untyped }
+    with CannotCoerceTo _ -> try
+      let c = coerce_to_constr env v in
+      { typed = Id.Map.add id c typed ; untyped }
+    with CannotCoerceTo _ ->
+      accu
   in
-  Id.Map.fold fold ist.lfun Id.Map.empty
+  Id.Map.fold fold ist.lfun { typed = Id.Map.empty ; untyped = Id.Map.empty }
 
 (** Significantly simpler than [interp_constr], to interpret an
-    untyped constr, it suffices to substitute any bound Ltac variables
-    while redoing internalisation. *)
-let subst_in_ucconstr subst =
-  let rec subst_in_ucconstr = function
-  | Glob_term.GVar (_,id) as x ->
-      begin try Lazy.force (Id.Map.find id subst)
-      with Not_found -> x end
-  | c -> Glob_ops.map_glob_constr subst_in_ucconstr c
-  in
-  subst_in_ucconstr
-
+    untyped constr, it suffices to adjoin a closure environment. *)
 let interp_uconstr ist env = function
-  | (c,None) -> subst_in_ucconstr (extract_ltac_uconstr_values ist env) c
+  | (term,None) ->
+      { closure = extract_ltac_uconstr_values ist env ; term }
   | (_,Some ce) ->
+      let ( {typed ; untyped } as closure) = extract_ltac_uconstr_values ist env in
       let ltacvars = {
-        Constrintern.ltac_vars = Id.Set.empty;
+        Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
-        ltac_subst = extract_ltac_uconstr_values ist env;
+        ltac_subst = Id.Map.empty;
       } in
-      intern_gen WithoutTypeConstraint ~ltacvars env ce
+      { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_values ist env in
-  let vars = (constrvars, ist.lfun) in
+  let vars = (constrvars, Id.Map.empty, ist.lfun) in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1189,8 +1186,11 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
       GTac.raw_enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        let c_glob = interp_uconstr ist env c in
-        let (sigma,c_interp) = Pretyping.understand_tcc sigma env c_glob in
+        let {closure;term} = interp_uconstr ist env c in
+        let vars = closure.typed , closure.untyped , ist.lfun in
+        let (sigma,c_interp) =
+          Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term
+        in
         Proofview.V82.tclEVARS sigma <*>
         GTac.return (Value.of_constr c_interp)
       end