Proofview refiner is now type-safe by default.

In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).

This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.

5 files changed, 37 insertions, 21 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d2fddabdc..1485b7701 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -263,11 +263,10 @@ and execute_recdef env evdref (names,lar,vdef) =
 
 and execute_array env evdref = Array.map (execute env evdref)
 
-let check env evd c t =
-  let evdref = ref evd in
+let check env evdref c t =
   let j = execute env evdref c in
   if not (Evarconv.e_cumul env evdref j.uj_type t) then
-    error_actual_type env j (nf_evar evd t)
+    error_actual_type env j (nf_evar !evdref t)
 
 (* Type of a constr *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 8700df52a..1d651e0c1 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -25,7 +25,7 @@ val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 val sort_of : env -> evar_map ref -> types -> sorts
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
-val check   : env -> evar_map -> constr -> types -> unit
+val check   : env -> evar_map ref -> constr -> types -> unit
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c3d7e13e2..e9b194c67 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -920,7 +920,7 @@ end
 
 module Refine =
 struct
-  type handle = Evd.evar_map * goal list
+  type handle = Evd.evar_map * Evar.t list
 
   let new_evar (evd, evs) env typ =
     let src = (Loc.ghost, Evar_kinds.GoalEvar) in
@@ -928,7 +928,7 @@ struct
     let evd = Typeclasses.mark_unresolvables 
       ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
     let (evk, _) = Term.destEvar ev in
-    let h = (evd, build_goal evk :: evs) in
+    let h = (evd, evk :: evs) in
     (h, ev)
 
   let fresh_constructor_instance (evd,evs) env construct =
@@ -943,29 +943,46 @@ struct
     in
     (evd,evs) , j'.Environ.uj_val
 
-  let refine f = Goal.raw_enter begin fun gl ->
+  let typecheck_evar ev env sigma =
+    let info = Evd.find sigma ev in
+    let evdref = ref sigma in
+    let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
+    let _ = Typing.sort_of env evdref (Evd.evar_concl info) in
+    !evdref
+
+  let typecheck_proof c concl env sigma =
+    let evdref = ref sigma in
+    let () = Typing.check env evdref c concl in
+    !evdref
+
+  let refine ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
     let sigma = Goal.sigma gl in
+    let env = Goal.env gl in
+    let concl = Goal.concl gl in
     let handle = (sigma, []) in
     let ((sigma, evs), c) = f handle in
+    (** Check that the introduced evars are well-typed *)
+    let fold accu ev = typecheck_evar ev env accu in
+    let sigma = if unsafe then sigma else List.fold_left fold sigma evs in
+    (** Check that the refined term is typesafe *)
+    let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+    (** Proceed to the refinement *)
     let sigma = partial_solution sigma gl.Goal.self c in
-    let modify start = { solution = sigma; comb = undefined sigma (List.rev evs); } in
-    Proof.modify modify
+    let comb = undefined sigma (List.rev_map build_goal evs) in
+    Proof.set { solution = sigma; comb; }
   end
 
-  let refine_casted f = Goal.raw_enter begin fun gl ->
+  let refine_casted ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
-    let f h =
-      let (h,c) = f h in
-      with_type h env c concl
-    in
-    refine f
+    let f h = let (h, c) = f h in with_type h env c concl in
+    refine ~unsafe f
   end
 
   let update (evd, gls) f =
     let nevd, ans = f evd in
     let fold ev _ accu =
-      if not (Evd.mem evd ev) then build_goal ev :: accu else accu
+      if not (Evd.mem evd ev) then ev :: accu else accu
     in
     let gls = Evd.fold_undefined fold nevd gls in
     (nevd, gls), ans
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0f976d2f3..357b1f4d7 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -437,13 +437,13 @@ module Refine : sig
       [fst (f evd)] should be an extension of [evd]. New evars generated by [f]
       are turned into goals. Use with care. *)
 
-  val refine : (handle -> handle * Constr.t) -> unit tactic
+  val refine : ?unsafe:bool -> (handle -> handle * Constr.t) -> unit tactic
   (** Given a term with holes that have been generated through {!new_evar}, this
       function fills the current hole with the given constr and creates goals
       for all the holes in their generation order. Exceptions raised by the
       function are caught. *)
 
-  val refine_casted : (handle -> handle * Constr.t) -> unit tactic
+  val refine_casted : ?unsafe:bool -> (handle -> handle * Constr.t) -> unit tactic
   (** Like {!refine} except the refined term is coerced to the conclusion of the
       current goal. *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 77876e626..932bfc5fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -783,7 +783,7 @@ let cut c =
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = local_strong whd_betaiota sigma c in
-      Proofview.Refine.refine begin fun h ->
+      Proofview.Refine.refine ~unsafe:true begin fun h ->
         let (h, f) = Proofview.Refine.new_evar h env (mkArrow c (Vars.lift 1 concl)) in
         let (h, x) = Proofview.Refine.new_evar h env c in
         let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
@@ -1404,7 +1404,7 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let new_exact_no_check c =
-  Proofview.Refine.refine (fun h -> (h, c))
+  Proofview.Refine.refine ~unsafe:true (fun h -> (h, c))
 
 let exact_check c =
   Proofview.Goal.raw_enter begin fun gl ->
@@ -1446,7 +1446,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.V82.tclEVARS sigma) <*>
-	Proofview.Refine.refine (fun h -> (h, mkVar id))
+	Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id))
     else arec gl only_eq rest
   in
   let assumption_tac gl =