Move the responsibility of type-checking to the caller for tactic-in-terms.

Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.

This should be 1:1 equivalent to the previous code, we are just moving code
around.

Author: ppedrot

plugins/ltac/tacinterp.ml

@@ -2148,16 +2148,22 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval lfun poly env sigma ty tac =
+  let eval ?loc ~poly env sigma tycon tac =
+    let lfun = GlobEnv.lfun env in
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun; poly; extra; } in
     let tac = eval_tactic_ist ist tac in
     (* EJGA: We should also pass the proof name if desired, for now
        poly seems like enough to get reasonable behavior in practice
      *)
     let name = Id.of_string "ltac_gen" in
-    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, ty = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
 

pretyping/globEnv.ml

@@ -51,6 +51,8 @@ let make ~hypnaming env sigma lvar =
   }
 
 let env env = env.static_env
+let renamed_env env = env.renamed_env
+let lfun env = env.lvar.ltac_genargs
 
 let vars_of_env env =
   Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
@@ -183,10 +185,13 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju
 
 let interp_ltac_id env id = ltac_interp_id env.lvar id
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 module ConstrInterpObj =
 struct
-  type ('r, 'g, 't) obj =
-    unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+  type ('r, 'g, 't) obj = 'g obj_interp_fun
   let name = "constr_interp"
   let default _ = None
 end
@@ -195,8 +200,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
 
 let register_constr_interp0 = ConstrInterp.register0
 
-let interp_glob_genarg env poly sigma ty arg =
+let interp_glob_genarg ?loc ~poly env sigma ty arg =
   let open Genarg in
   let GenArg (Glbwit tag, arg) = arg in
   let interp = ConstrInterp.obj tag in
-  interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
+  interp ?loc ~poly env sigma ty arg

pretyping/globEnv.mli

@@ -15,11 +15,18 @@ open EConstr
 open Ltac_pretype
 open Evarutil
 
+(** Type of environment extended with naming and ltac interpretation data *)
+
+type t
+
 (** To embed constr in glob_constr *)
 
+type 'a obj_interp_fun =
+  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
+  'a -> unsafe_judgment * Evd.evar_map
+
 val register_constr_interp0 :
-  ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+  ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
 
 (** {6 Pretyping name management} *)
 
@@ -32,17 +39,15 @@ val register_constr_interp0 :
       variables used to build purely-named evar contexts
 *)
 
-(** Type of environment extended with naming and ltac interpretation data *)
-
-type t
-
 (** Build a pretyping environment from an ltac environment *)
 
 val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 
 (** Export the underlying environment *)
 
 val env : t -> env
+val renamed_env : t -> env
+val lfun : t -> unbound_ltac_var_map
 
 val vars_of_env : t -> Id.Set.t
 
@@ -85,5 +90,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
 (** Interpreting a generic argument, typically a "ltac:(...)", taking
     into account the possible renaming *)
 
-val interp_glob_genarg : t -> bool -> evar_map -> constr ->
-  Genarg.glob_generic_argument -> constr * evar_map
+val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint ->
+  Genarg.glob_generic_argument -> unsafe_judgment * evar_map

pretyping/pretyping.ml

@@ -653,12 +653,8 @@ struct
       sigma, { uj_val; uj_type }
 
     | Some arg ->
-      let sigma, ty =
-        match tycon with
-        | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
-      let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
-      sigma, { uj_val = c; uj_type = ty }
+      let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly env sigma tycon arg in
+      sigma, j
 
   let pretype_rec self (fixkind, names, bl, lar, vdef) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->

user-contrib/Ltac2/tac2core.ml

@@ -1388,24 +1388,34 @@ let () =
 (** Ltac2 in terms *)
 
 let () =
-  let interp ist poly env sigma concl (ids, tac) =
+  let interp ?loc ~poly env sigma tycon (ids, tac) =
     (* Syntax prevents bound notation variables in constr quotations *)
     let () = assert (Id.Set.is_empty ids) in
-    let ist = Tac2interp.get_env ist in
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
-    let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
-    (EConstr.of_constr c, sigma)
+    let sigma, concl = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let c, sigma = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma concl tac in
+    let j = { Environ.uj_val = EConstr.of_constr c; Environ.uj_type = concl } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
 
 let () =
-  let interp ist poly env sigma concl id =
-    let ist = Tac2interp.get_env ist in
+  let interp ?loc ~poly env sigma tycon id =
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
-    let sigma = Typing.check env sigma c concl in
-    (c, sigma)
+    let sigma, concl = match tycon with
+    | Some ty -> sigma, ty
+    | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+    in
+    let sigma = Typing.check (GlobEnv.renamed_env env) sigma c concl in
+    let j = { Environ.uj_val = c; Environ.uj_type = concl } in
+    (j, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_quotation interp