Merge PR #8104: Warnings on coercions used without being Imported

4 files changed, 38 insertions, 7 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c0c4539564..23cbd76eda 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -325,6 +325,12 @@ Coercions and Modules
    This option makes it possible to recover the behavior of the versions of
    |Coq| prior to 8.3.
 
+.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
+
+          This warning is emitted when typechecking relies on a coercion
+          contained in a module that has not been explicitely imported. It helps
+          migrating code and stop relying on the option above.
+
 Examples
 --------
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 542fb5456c..52e02c87fd 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -118,6 +118,9 @@ let class_tab =
 let coercion_tab =
   ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
+let coercions_in_scope =
+  ref Refset_env.empty
+
 module ClPairOrd =
 struct
   type t = cl_index * cl_index
@@ -131,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd)
 let inheritance_graph =
   ref (ClPairMap.empty : inheritance_path ClPairMap.t)
 
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
+let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
 
-let unfreeze (fcl,fco,fig) =
+let unfreeze (fcl,fco,fig,in_scope) =
   class_tab:=fcl;
   coercion_tab:=fco;
-  inheritance_graph:=fig
+  inheritance_graph:=fig;
+  coercions_in_scope:=in_scope
 
 (* ajout de nouveaux "objets" *)
 
@@ -445,9 +449,16 @@ let load_coercion _ o =
   if !automatically_import_coercions then
     cache_coercion (Global.env ()) Evd.empty o
 
+let set_coercion_in_scope (_, c) =
+  let r = c.coercion_type in
+  coercions_in_scope := Refset_env.add r !coercions_in_scope
+
 let open_coercion i o =
-  if Int.equal i 1 && not !automatically_import_coercions then
-    cache_coercion (Global.env ()) Evd.empty o
+  if Int.equal i 1 then begin
+    set_coercion_in_scope o;
+    if not !automatically_import_coercions then
+      cache_coercion (Global.env ()) Evd.empty o
+  end
 
 let subst_coercion (subst, c) =
   let coe = subst_coe_typ subst c.coercion_type in
@@ -492,7 +503,9 @@ let inCoercion : coercion -> obj =
     open_function = open_coercion;
     load_function = load_coercion;
     cache_function = (fun objn ->
-        let env = Global.env () in cache_coercion env Evd.empty objn
+        let env = Global.env () in
+        set_coercion_in_scope objn;
+        cache_coercion env Evd.empty objn
       );
     subst_function = subst_coercion;
     classify_function = classify_coercion;
@@ -553,3 +566,6 @@ let hide_coercion coe =
     let coe_info = coercion_info coe in
     Some coe_info.coe_param
   else None
+
+let is_coercion_in_scope r =
+  Refset_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index af00c0a8dc..dc193c4e74 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list
 (** [hide_coercion] returns the number of params to skip if the coercion must
    be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
 val hide_coercion : coe_typ -> int option
+
+val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5e3821edf1..e15c00f7dc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -363,12 +363,20 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
+let warn_coercion_not_in_scope =
+  CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
+    Pp.(fun r -> str "Coercion used but not in scope: " ++
+              Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
+              ++ str "this coercion, please Import the module that contains it.")
+
 (* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
       List.fold_left
         (fun (ja,typ_cl,sigma) i ->
+           if not (is_coercion_in_scope i.coe_value) then
+             warn_coercion_not_in_scope i.coe_value;
            let isid = i.coe_is_identity in
            let isproj = i.coe_is_projection in
            let sigma, c = new_global sigma i.coe_value in
@@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl =
       (hj,typ_cl,sigma) p
     in evd, j
   with NoCoercion as e -> raise e
-  | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.")
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =