Error instead of renaming section variable mentioned through a global

Fix #12304

Author: SkySkimmer

engine/evarutil.mli

@@ -199,6 +199,8 @@ type unification_pb = conv_pb * env * constr * constr
     Put it at the end of the list if [tail] is true, by default it is false. *)
 val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
 
+val vars_of_global : env -> evar_map -> GlobRef.t -> Id.Set.t
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 

kernel/context.ml

@@ -377,8 +377,8 @@ struct
     let set_id id =
       let set x = {x with binder_name = id} in
       function
-      | LocalAssum (s, x, ty) -> LocalAssum (s, set x, ty)
-      | LocalDef (s, x, v, ty) -> LocalDef (s, set x, v, ty)
+      | LocalAssum (_, x, ty) -> LocalAssum (ProofVar, set x, ty)
+      | LocalDef (_, x, v, ty) -> LocalDef (ProofVar, set x, v, ty)
 
     (** Return [true] iff a given declaration is a local assumption. *)
     let is_local_assum = function
@@ -414,6 +414,7 @@ struct
     let map_id f x =
       let id = get_id x in
       let id' = f id in
+      (* XXX use Id.equal? *)
       if id == id' then x else set_id id' x
 
     (** Map all terms in a given declaration. *)

kernel/context.mli

@@ -248,7 +248,7 @@ sig
 
     val get_relevance : ('c, 't, 'r) pt -> 'r
 
-    (** Set the identifier that is bound by a given declaration. *)
+    (** Set the identifier that is bound by a given declaration. status becomes [ProofVar]. *)
     val set_id : Id.t -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt
 
     (** Return [true] iff a given declaration is a local assumption. *)
@@ -267,7 +267,8 @@ sig
     val equal : ('r -> 'r -> bool) -> ('c -> 'c -> bool) ->
       ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt -> bool
 
-    (** Map the identifier bound by a given declaration. *)
+    (** Map the identifier bound by a given declaration.
+        Status becomes [ProofVar] if the id changes (physical equality). *)
     val map_id : (Id.t -> Id.t) -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt
 
     (** Map all terms in a given declaration. *)

pretyping/evarsolve.ml

@@ -571,7 +571,8 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
         | Some (RelAlias n) -> if n >= depth+1 then fv_rels := Int.Set.add (n-depth) !fv_rels
         | None -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        fv_ids := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids
+        (* XXX should be Evarutil.vars_of_global to handle abstracted constants? *)
+        fv_ids := Id.Set.union (Environ.vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids
     | _ ->
         iter_with_full_binders env sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))

tactics/hints.ml

@@ -858,6 +858,7 @@ let with_uid c = { obj = c; uid = fresh_key () }
 
 let secvars_of_idset s =
   Id.Set.fold (fun id p ->
+      (* XXX how can vars_of_global return non secvars? *)
       if is_section_variable (Global.env ()) id then
         Id.Pred.add id p
       else p) s Id.Pred.empty

tactics/tactics.ml

@@ -217,6 +217,74 @@ let move_hyp id dest =
     end
   end
 
+let error_renaming_implicit_dependency ?loc env where ids gr =
+  CErrors.user_err ?loc @@
+  fmt "Cannot rename section variable %t@ because it is used implicitly through %t@ in %t."
+    (fun () -> Id.print (Id.Set.choose ids))
+    (fun () -> pr_global_env env gr)
+    (fun () -> match where with
+       | None -> str "the conclusion"
+       | Some h -> fmt "hypothesis %t" (fun () -> Id.print h))
+
+let check_renaming ~src ~dst env sigma concl =
+  let sign = named_context_val env in
+  (* Check that we do not mess variables *)
+  let vars = ids_of_named_context_val sign in
+  let () =
+    if not (Id.Set.subset src vars) then
+      let hyp = Id.Set.choose (Id.Set.diff src vars) in
+      raise (RefinerError (env, sigma, NoSuchHyp hyp))
+  in
+  let mods = Id.Set.diff vars src in
+  let () =
+    try
+      let elt = Id.Set.choose (Id.Set.inter dst mods) in
+      TacticErrors.already_used elt
+    with Not_found -> ()
+  in
+  let secvars =
+    Id.Set.filter (fun id ->
+        match NamedDecl.get_status (lookup_named id env) with
+        | SecVar -> true
+        | ProofVar -> false)
+      src
+  in
+  let checked = ref GlobRef.Set_env.empty in
+  let check_constr where c =
+    let rec aux c =
+      match EConstr.destRef sigma c with
+      | VarRef _, _ ->
+        (* we only refuse implicit dependencies, because they can't be substituted *)
+        ()
+      | gr, _ ->
+        if GlobRef.Set_env.mem gr !checked then ()
+        else begin
+          let deps = Evarutil.vars_of_global env sigma gr in
+          let bad = Id.Set.inter deps secvars in
+          let () =
+            if not @@ Id.Set.is_empty bad then
+              error_renaming_implicit_dependency env where bad gr
+          in
+          checked := GlobRef.Set_env.add gr !checked
+        end
+      | exception DestKO -> EConstr.iter sigma aux c
+    in
+    aux c
+  in
+  let () =
+    if Id.Set.is_empty secvars then
+      (* not renaming any secvars -> no problem *)
+      ()
+    else
+      let () = check_constr None concl in
+      let () =
+        List.iter (fun d -> NamedDecl.iter_constr (check_constr (Some (NamedDecl.get_id d))) d)
+          (named_context env)
+      in
+      ()
+  in
+  ()
+
 let rename_hyp repl =
   let fold accu (src, dst) = match accu with
   | None -> None
@@ -238,30 +306,16 @@ let rename_hyp repl =
     Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let env = Proofview.Goal.env gl in
-      let sign = named_context_val env in
       let sigma = Proofview.Goal.sigma gl in
       let relevance = Proofview.Goal.relevance gl in
-      (* Check that we do not mess variables *)
-      let vars = ids_of_named_context_val sign in
-      let () =
-        if not (Id.Set.subset src vars) then
-          let hyp = Id.Set.choose (Id.Set.diff src vars) in
-          raise (RefinerError (env, sigma, NoSuchHyp hyp))
-      in
-      let mods = Id.Set.diff vars src in
-      let () =
-        try
-          let elt = Id.Set.choose (Id.Set.inter dst mods) in
-          TacticErrors.already_used elt
-        with Not_found -> ()
-      in
+      let () = check_renaming ~src ~dst env sigma concl in
       (* All is well *)
       let make_subst (src, dst) = (src, mkVar dst) in
       let subst = List.map make_subst repl in
       let subst c = Vars.replace_vars sigma subst c in
       let replace id = try List.assoc_f Id.equal id repl with Not_found -> id in
       let map decl = decl |> NamedDecl.map_id replace |> NamedDecl.map_constr subst in
-      let ohyps = named_context_of_val sign in
+      let ohyps = EConstr.named_context env in
       let nhyps = List.map map ohyps in
       let nconcl = subst concl in
       let nctx = val_of_named_context nhyps in

test-suite/bugs/bug_12304.v

@@ -0,0 +1,11 @@
+Section S.
+Variable a:nat.
+Definition b:=a.
+Goal b=b.
+Proof.
+  Fail rename a into c.
+  generalize b. intros b.
+  rename a into c.
+  Fail unfold b.
+Abort.
+End S.