Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class

5 files changed, 53 insertions, 13 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 15a55d9e72..882798205b 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -260,6 +260,12 @@ preorder can be used instead. This is very similar to the coercion
 mechanism of ``Structure`` declarations. The implementation simply
 declares each projection as an instance.
 
+.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class
+
+   Using this ``:>`` syntax with a right-hand-side that is not itself a Class
+   has no effect (apart from emitting this warning). In particular, is does not
+   declare a coercion.
+
 One can also declare existing objects or structure projections using
 the Existing Instance command to achieve the same effect.
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 18c9650bd1..d732544c5c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -427,28 +427,40 @@ let remove_instance i =
   Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
   remove_instance_hint i.is_impl
 
-let declare_instance info local glob =
+let warning_not_a_class =
+  let name = "not-a-class" in
+  let category = "typeclasses" in
+  CWarnings.create ~name ~category (fun (n, ty) ->
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      Pp.(str "Ignored instance declaration for “"
+          ++ Nametab.pr_global_env Id.Set.empty n
+          ++ str "”: “"
+          ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
+          ++ str "” is not a class")
+    )
+
+let declare_instance ?(warn = false) info local glob =
   let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
       assert (not (isVarRef glob) || local);
       add_instance (new_instance tc info (not local) glob)
-    | None -> ()
+    | None -> if warn then warning_not_a_class (glob, ty)
 
 let add_class cl =
   add_class cl;
   List.iter (fun (n, inst, body) ->
-	     match inst with
-	     | Some (Backward, info) ->
-	       (match body with
-	       | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
-	       | Some b -> declare_instance (Some info) false (ConstRef b))
-	     | _ -> ())
-  cl.cl_projs
+      match inst with
+      | Some (Backward, info) ->
+        (match body with
+         | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
+         | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b))
+      | _ -> ())
+    cl.cl_projs
 
 
-      
 (*
  * interface functions
  *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 8bdac0a575..d00195678b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
+(** Declares the given global reference as an instance of its type.
+    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
+    when said type is not a registered type class. *)
+val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v
new file mode 100644
index 0000000000..c1fdd04a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9014.v
@@ -0,0 +1,19 @@
+(* A type, not a class *)
+Variant T := mkT.
+
+(* In records, :> declares a coercion *)
+Record R := { t_of_r :> T }.
+Check forall r : R, r = r :> T.
+
+(* A class *)
+Class A := { p : Prop }.
+(* A sub-class *)
+Class B := { a_of_b :> A ; t_of_b :> T }.
+(* The sub-instance is automatically inferred due to :> for a_of_b *)
+Check forall b : B, p.
+(* No coercion is introduced by :> in t_of_b *)
+Fail Check forall b : B, b = b :> T.
+
+(* Using :> when the RHS is not a class produces a “not-a-class” warning. *)
+Set Warnings "+not-a-class".
+Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }.
diff --git a/vernac/record.ml b/vernac/record.ml
index 81b33c2e11..f6dbcb5291 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -458,7 +458,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
+let declare_class def cum ubinders univs id idbuild paramimpls params arity
     template fieldimpls fields ?(kind=StructureComponent) coers priorities =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records =
     in
     let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
     let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
-    declare_class finite def cum ubinders univs id.CAst.v idbuild
+    declare_class def cum ubinders univs id.CAst.v idbuild
       implpars params arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in