Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.

We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.

2 files changed, 29 insertions, 1 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4fc0c164e3..59a64658dc 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1010,10 +1010,34 @@ end
 module Refine =
 struct
 
+  let extract_prefix env info =
+    let ctx1 = List.rev (Environ.named_context env) in
+    let ctx2 = List.rev (Evd.evar_context info) in
+    let rec share l1 l2 accu = match l1, l2 with
+    | d1 :: l1, d2 :: l2 ->
+      if d1 == d2 then share l1 l2 (d1 :: accu)
+      else (accu, d2 :: l2)
+    | _ -> (accu, l2)
+    in
+    share ctx1 ctx2 []
+
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
+    (** Typecheck the hypotheses. *)
+    let type_hyp (sigma, env) (na, body, t as decl) =
+      let evdref = ref sigma in
+      let _ = Typing.sort_of env evdref t in
+      let () = match body with
+      | None -> ()
+      | Some body -> Typing.check env evdref body t
+      in
+      (!evdref, Environ.push_named decl env)
+    in
+    let (common, changed) = extract_prefix env info in
+    let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+    let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+    (** Typecheck the conclusion *)
     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
 
diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v
new file mode 100644
index 0000000000..4b2aae0c7b
--- /dev/null
+++ b/test-suite/bugs/closed/4412.v
@@ -0,0 +1,4 @@
+Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
+Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
+  intros.
+  Fail rewrite Bool.andb_true_iff in H.