Relaxing again the test on types of replacements in tactic change

(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).

It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.

  Goal @eq Type nat nat.
  change nat with (@id Type nat).

which is a correct replacement, even if (id Type nat) is in a higher sort.

Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)

2 files changed, 37 insertions, 13 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 26b05c68e..f66c18822 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -464,36 +464,55 @@ let e_change_in_hyp redfun (id,where) gl =
 
 type change_arg = env -> evar_map -> evar_map * constr
 
-let weak_check env sigma deep newc origc =
+let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
-  if deep then
+  if deep then begin
     let t2 = Retyping.get_type_of env sigma origc in
     let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in
-      snd (infer_conv ~pb:Reduction.CUMUL env sigma t1 t2)
+    if not (snd (infer_conv ~pb:Reduction.CUMUL env sigma t1 t2)) then
+      if
+        isSort (whd_betadeltaiota env sigma t1) &&
+        isSort (whd_betadeltaiota env sigma t2)
+      then
+        mayneedglobalcheck := true
+      else
+        errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
+  end
   else
-    isSort (whd_betadeltaiota env sigma t1)
+    if not (isSort (whd_betadeltaiota env sigma t1)) then
+      errorlabstrm "convert-check-hyp" (str "Not a type.")
 
 (* Now we introduce different instances of the previous tacticals *)
-let change_and_check cv_pb deep t env sigma c =
+let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   let sigma, t' = t env sigma in
-  let b = weak_check env sigma deep t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+  check_types env sigma mayneedglobalcheck deep t' c;
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
   if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   sigma, t'
 
-let change_and_check_subst cv_pb subst t env sigma c =
+let change_and_check_subst cv_pb mayneedglobalcheck subst t env sigma c =
   let t' env sigma = 
     let sigma, t = t env sigma in
       sigma, replace_vars (Id.Map.bindings subst) t 
-  in change_and_check cv_pb true t' env sigma c
+  in change_and_check cv_pb mayneedglobalcheck true t' env sigma c
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t = function
-  | None -> change_and_check cv_pb deep t
+let change_on_subterm cv_pb deep t where env sigma c =
+  let mayneedglobalcheck = ref false in
+  let sigma,c = match where with
+  | None -> change_and_check cv_pb mayneedglobalcheck deep t env sigma c
   | Some occl ->
-    e_contextually false occl
-      (fun subst -> change_and_check_subst Reduction.CONV subst t)
+      e_contextually false occl
+        (fun subst ->
+          change_and_check_subst Reduction.CONV mayneedglobalcheck subst t)
+        env sigma c in
+  if !mayneedglobalcheck then
+    begin
+      try ignore (Typing.type_of env sigma c)
+      with e when catchable_exception e ->
+        error "Replacement would lead to an ill-typed term."
+    end;
+  sigma,c
 
 let change_in_concl occl t =
   e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index f775f818a..cd2dd77f9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -45,3 +45,8 @@ Abort.
 Goal True.
 change ?x with x.
 Abort.
+
+(* Check typability after change of type subterms *)
+Goal nat = nat :> Set.
+Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
+Abort.