[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.

11 files changed, 60 insertions, 40 deletions

diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index a97ccb270..359aab0d8 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -50,7 +50,7 @@ val wit_constr_may_eval :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
   constr) genarg_type
 
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.glob_constr) genarg_type
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
   (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index d37955225..ec27aab33 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -72,3 +72,13 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
+
+(** A globalised term together with a closure representing the value
+    of its free variables. Intended for use when these variables are taken
+    from the Ltac environment. *)
+type closure = {
+  typed: Pattern.constr_under_binders Id.Map.t ;
+  untyped:closed_glob_constr Id.Map.t }
+and closed_glob_constr = {
+  closure: closure;
+  term: glob_constr }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fe9646b9d..f18aa364b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -46,8 +46,9 @@ open Misctypes
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
+type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
 type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
-type ltac_var_map = var_map * unbound_ltac_var_map
+type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
@@ -236,7 +237,7 @@ let protected_get_type_of env sigma c =
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
-let pretype_id loc env evdref (lvar,unbndltacvars) id =
+let pretype_id pretype loc env evdref (lvar,globvar,unbndltacvars) id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
@@ -249,6 +250,13 @@ let pretype_id loc env evdref (lvar,unbndltacvars) id =
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
 	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
+    with Not_found -> try
+       let {closure;term} = Id.Map.find id globvar in
+       (* spiwack: I'm catching [Not_found] potentially too eagerly
+          here, as the call to the main pretyping function is caught
+          inside the try but I want to avoid refactoring this function
+          too much for now. *)
+       pretype env evdref (closure.typed,closure.untyped,unbndltacvars) term
     with Not_found ->
         (* Check if [id] is a ltac variable not bound to a term *)
 	(* and build a nice error message *)
@@ -366,7 +374,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 
   | GVar (loc, id) ->
     inh_conv_coerce_to_tycon loc env evdref
-      (pretype_id loc env evdref lvar id)
+      (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
       tycon
 
   | GEvar (loc, evk, instopt) ->
@@ -402,7 +410,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
         | Some ty -> ty
         | None ->
           new_type_evar evdref env loc in
-      let ist = snd lvar in
+      let ist = Util.pi3 lvar in
       let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
@@ -899,7 +907,7 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let empty_lvar : ltac_var_map = (Id.Map.empty, Id.Map.empty)
+let empty_lvar : ltac_var_map = (Id.Map.empty, Id.Map.empty, Id.Map.empty)
 
 let on_judgment f j =
   let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 72e9971d6..4a80226bd 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -28,8 +28,9 @@ val search_guard :
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = Pattern.constr_under_binders Id.Map.t
+type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
 type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
-type ltac_var_map = var_map * unbound_ltac_var_map
+type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8c2776789..4746177ac 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -64,6 +64,6 @@ let instantiate_pf_com evk com sigma =
   let evi = Evd.find sigma evk in
   let env = Evd.evar_filtered_env evi in
   let rawc = Constrintern.intern_constr env com in
-  let ltac_vars = (Id.Map.empty, Id.Map.empty) in
+  let ltac_vars = (Id.Map.empty, Id.Map.empty, Id.Map.empty) in
   let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
   sigma'
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d68257477..27986eab6 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 a7d95c5e8..214db580a 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 2937d4273..c1f9fe30d 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 171269f92..7b278996e 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 95752c99a..9ec486c1c 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
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b66a24653..7c42d7a8f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1173,7 +1173,7 @@ let explain_ltac_call_trace last trace loc =
   | Proof_type.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
               (Tacexpr.TacAtom (Loc.ghost,te)))
-  | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
+  | Proof_type.LtacConstrInterp (c,(vars,_,unboundvars)) ->
       quote (pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++