Enforce typing of external declarations

Fix coq#18553
Fix coq#18635

plugins/ltac2/tac2core.mli

@@ -44,6 +44,7 @@ module type MapType = sig
   type valmap
   val valmap_eq : (valmap, Tac2val.valexpr M.t) Util.eq
   val repr : S.elt Tac2ffi.repr
+  val typ : Tac2ffi.Types.t option
 end
 
 type ('a,'set,'map) map_tag

plugins/ltac2/tac2env.mli

@@ -157,6 +157,8 @@ val interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object
 
 (** {5 Absolute paths} *)
 
+(* TODO move this to tac2globals *)
+
 val coq_prefix : ModPath.t
 (** Path where primitive datatypes are defined in Ltac2 plugin. *)
 

plugins/ltac2/tac2externals.ml

@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Proofview
 open Tac2ffi
 
@@ -21,52 +22,52 @@ type 'a with_env = Environ.env -> Evd.evar_map -> 'a
    to be give for this type definition to be accepted. If we remove it, we get
    an error: "a type variable cannot be deduced from the type parameters". *)
 type (_, _, _) spec_aux =
-  | T : 'r to_v -> (v tactic, 'r tactic, 'r) spec_aux
-  | V : 'r to_v -> (v tactic, 'r, 'r) spec_aux
-  | E : 'r to_v -> (v tactic, 'r with_env, 'r) spec_aux
-  | G : 'r to_v -> (v tactic, Goal.t -> 'r, 'r) spec_aux
-  | F : 'a of_v * ('t, 'f, 'r) spec_aux -> (v -> 't , 'a -> 'f, 'r) spec_aux
+  | T : 'r to_v annotated -> (v tactic, 'r tactic, 'r) spec_aux
+  | V : 'r to_v annotated -> (v tactic, 'r, 'r) spec_aux
+  | E : 'r to_v annotated -> (v tactic, 'r with_env, 'r) spec_aux
+  | G : 'r to_v annotated -> (v tactic, Goal.t -> 'r, 'r) spec_aux
+  | F : 'a of_v annotated * ('t, 'f, 'r) spec_aux -> (v -> 't , 'a -> 'f, 'r) spec_aux
 
 type (_,_) spec = S : ('v,'f,'r) spec_aux -> ('v,'f) spec [@@unboxed]
 
-let tac : type r. r repr -> (v tactic, r tactic) spec = fun r ->
-  S (T (repr_of r))
+let tac : type r. r repr annotated -> (v tactic, r tactic) spec = fun r ->
+  S (T (on_fst repr_of r))
 
-let tac': type r. r to_v -> (v tactic, r tactic) spec = fun tr ->
+let tac': type r. r to_v annotated -> (v tactic, r tactic) spec = fun tr ->
   S (T tr)
 
-let ret : type r. r repr -> (v tactic, r) spec = fun r ->
-  S (V (repr_of r))
+let ret : type r. r repr annotated -> (v tactic, r) spec = fun r ->
+  S (V (on_fst repr_of r))
 
-let ret': type r. r to_v -> (v tactic, r) spec = fun tr ->
+let ret': type r. r to_v annotated -> (v tactic, r) spec = fun tr ->
   S (V tr)
 
-let eret : type r. r repr -> (v tactic, r with_env) spec = fun r ->
-  S (E (repr_of r))
+let eret : type r. r repr annotated -> (v tactic, r with_env) spec = fun r ->
+  S (E (on_fst repr_of r))
 
-let eret': type r. r to_v -> (v tactic, r with_env) spec = fun tr ->
+let eret': type r. r to_v annotated -> (v tactic, r with_env) spec = fun tr ->
   S (E tr)
 
-let gret : type r. r repr -> (v tactic, Goal.t -> r) spec = fun r ->
-  S (G (repr_of r))
+let gret : type r. r repr annotated -> (v tactic, Goal.t -> r) spec = fun r ->
+  S (G (on_fst repr_of r))
 
-let gret': type r. r to_v -> (v tactic, Goal.t -> r) spec = fun tr ->
+let gret': type r. r to_v annotated -> (v tactic, Goal.t -> r) spec = fun tr ->
   S (G tr)
 
-let (@->) : type a t f. a repr -> (t,f) spec -> (v -> t, a -> f) spec =
-  fun r (S ar) -> S (F (repr_to r, ar))
+let (@->) : type a t f. a repr annotated -> (t,f) spec -> (v -> t, a -> f) spec =
+  fun r (S ar) -> S (F (on_fst repr_to r, ar))
 
-let (@-->): type a t f. a of_v -> (t,f) spec -> (v -> t, a -> f) spec =
+let (@-->): type a t f. a of_v annotated -> (t,f) spec -> (v -> t, a -> f) spec =
   fun of_v (S ar) -> S (F (of_v, ar))
 
 let rec interp_spec : type v f. (v,f) spec -> f -> v = fun (S ar) f ->
   let open Proofview.Notations in
   match ar with
-  | T tr -> f >>= fun v -> tclUNIT (tr v)
-  | V tr -> tclUNIT (tr f)
-  | E tr -> tclENV >>= fun e -> tclEVARMAP >>= fun s -> tclUNIT (tr (f e s))
-  | G tr -> Goal.enter_one @@ fun g -> tclUNIT (tr (f g))
-  | F (tr,ar) -> fun v -> interp_spec (S ar) (f (tr v))
+  | T tr -> f >>= fun v -> tclUNIT (fst tr v)
+  | V tr -> tclUNIT (fst tr f)
+  | E tr -> tclENV >>= fun e -> tclEVARMAP >>= fun s -> tclUNIT (fst tr (f e s))
+  | G tr -> Goal.enter_one @@ fun g -> tclUNIT (fst tr (f g))
+  | F (tr,ar) -> fun v -> interp_spec (S ar) (f (fst tr v))
 
 let rec arity_of : type v f. (v,f) spec -> v Tac2val.arity = fun (S ar) ->
   match ar with
@@ -77,13 +78,23 @@ let rec arity_of : type v f. (v,f) spec -> v Tac2val.arity = fun (S ar) ->
   | F (_, ar) -> Tac2val.arity_suc (arity_of (S ar))
   | _ -> invalid_arg "Tac2def.arity_of: not a function spec"
 
+let rec type_of_spec : type v f. (v,f) spec -> Types.t = fun (S ar) ->
+  let of_annot (_,t) = Option.default Types.any t in
+  match ar with
+  | T tr -> of_annot tr
+  | V tr -> of_annot tr
+  | E tr -> of_annot tr
+  | G tr -> of_annot tr
+  | F (tr,ar) -> Types.(of_annot tr @-> type_of_spec (S ar))
+
 let define : type v f. _ -> (v,f) spec -> f -> unit = fun n ar v ->
   let v =
     match ar with
-    | S (V tr) -> tr v
+    | S (V tr) -> fst tr v
     | S (F _) ->
         let cl = Tac2val.mk_closure (arity_of ar) (interp_spec ar v) in
         Tac2ffi.of_closure cl
     | _ -> invalid_arg "Tac2def.define: not a pure value"
   in
-  Tac2env.define_primitive n None v
+  let ty = Some (Types.as_scheme @@ type_of_spec ar) in
+  Tac2env.define_primitive n ty v

plugins/ltac2/tac2externals.mli

@@ -24,36 +24,36 @@ type (_, _) spec
 (** [tac r] is the specification of a tactic (in the tactic monad sense) whose
     return type is specified (and converted into an Ltac2 value) via [r]. *)
 val tac :
-  'r repr ->
+  'r repr annotated ->
   (valexpr tactic, 'r tactic) spec
 
 (** [tac'] is similar to [tac], but only needs a conversion function. *)
 val tac' :
-  ('r -> valexpr) ->
+  ('r -> valexpr) annotated ->
   (valexpr tactic, 'r tactic) spec
 
 (** [ret r] is the specification of a pure tactic (i.e., a tactic defined as a
     pure OCaml value, not needing the tactic monad) whose return type is given
     by [r] (see [tac]). *)
 val ret :
-  'r repr ->
+  'r repr annotated ->
   (valexpr tactic, 'r) spec
 
 (** [ret'] is similar to [ret], but only needs a conversion function. *)
 val ret' :
-  ('r -> valexpr) ->
+  ('r -> valexpr) annotated ->
   (valexpr tactic, 'r) spec
 
 (** [eret] is similar to [ret], but for tactics that can be implemented with a
     pure OCaml value, provided extra arguments [env] and [sigma], computed via
     [tclENV] and [tclEVARMAP]. *)
 val eret :
-  'r repr ->
+  'r repr annotated ->
   (valexpr tactic, Environ.env -> Evd.evar_map -> 'r) spec
 
 (** [eret'] is similar to [eret], but only needs a conversion function. *)
 val eret' :
-  ('r -> valexpr) ->
+  ('r -> valexpr) annotated ->
   (valexpr tactic, Environ.env -> Evd.evar_map -> 'r) spec
 
 (** [gret] is similar to [ret], but for tactics that can be implemented with a
@@ -62,24 +62,24 @@ val eret' :
     of using an Ltac2 value defined with this specification. Indeed, the value
     of [g] is computed using [Goal.enter_one]. *)
 val gret :
-  'r repr ->
+  'r repr annotated ->
   (valexpr tactic, Goal.t -> 'r) spec
 
 (** [gret'] is similar to [gret], but only needs a conversion function. *)
 val gret' :
-  ('r -> valexpr) ->
+  ('r -> valexpr) annotated ->
   (valexpr tactic, Goal.t -> 'r) spec
 
 (** [r @-> s] extends the specification [s] with a closure argument whose type
     is specified by (and converted from an Ltac2 value via) [r]. *)
 val (@->) :
-  'a repr ->
+  'a repr annotated ->
   ('t,'f) spec ->
   (valexpr -> 't, 'a -> 'f) spec
 
 (** [(@-->)] is similar to [(@->)], but only needs a conversion function. *)
 val (@-->) :
-  (valexpr -> 'a) ->
+  (valexpr -> 'a) annotated ->
   ('t,'f) spec ->
   (valexpr -> 't, 'a -> 'f) spec
 

plugins/ltac2/tac2extffi.ml

@@ -24,7 +24,8 @@ let to_qhyp v = match Value.to_block v with
 | (1, [| id |]) -> NamedHyp (CAst.make (Value.to_ident id))
 | _ -> assert false
 
-let qhyp = make_to_repr to_qhyp
+let qhyp_ = make_to_repr to_qhyp
+let qhyp = typed qhyp_ Types.(!! Tac2globals.Types.hypothesis)
 
 let to_bindings = function
 | ValInt 0 -> NoBindings
@@ -34,10 +35,7 @@ let to_bindings = function
   ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
 | _ -> assert false
 
-let bindings = make_to_repr to_bindings
+let bindings_ = make_to_repr to_bindings
+let bindings = typed bindings_ Types.(!! Tac2globals.Types.bindings)
 
-let to_constr_with_bindings v = match Value.to_tuple v with
-| [| c; bnd |] -> (Value.to_constr c, to_bindings bnd)
-| _ -> assert false
-
-let constr_with_bindings = make_to_repr to_constr_with_bindings
+let constr_with_bindings = pair constr bindings

plugins/ltac2/tac2extffi.mli

@@ -11,8 +11,8 @@
 open Tac2ffi
 open Tac2types
 
-val qhyp : quantified_hypothesis repr
+val qhyp : quantified_hypothesis repr annotated
 
-val bindings : bindings repr
+val bindings : bindings repr annotated
 
-val constr_with_bindings : constr_with_bindings repr
+val constr_with_bindings : constr_with_bindings repr annotated