Use new warning API to provide nicer printer for bad relevance warning

Author: SkySkimmer

kernel/typeops.ml

@@ -57,26 +57,37 @@ let infer_assumption env t ty =
   with TypeError _ ->
     error_assumption env (make_judge t ty)
 
-type bad_relevance =
-| BadRelevanceBinder of Sorts.relevance * rel_declaration
-| BadRelevanceCase of Sorts.relevance * Constr.t
+type ('constr,'types) bad_relevance =
+| BadRelevanceBinder of Sorts.relevance * ('constr,'types) Context.Rel.Declaration.pt
+| BadRelevanceCase of Sorts.relevance * 'constr
 
 let warn_bad_relevance_name = "bad-relevance"
-let warn_bad_relevance =
-  CWarnings.create ~name:warn_bad_relevance_name ~default:CWarnings.AsError
-    Pp.(function
-        | BadRelevanceCase _ ->  str "Bad relevance in case annotation."
-        | BadRelevanceBinder (_, na) -> str "Bad relevance for binder " ++ Name.print (RelDecl.get_name na) ++ str ".")
 
-let warn_bad_relevance_case ?loc env rlv case = match CWarnings.get_status ~name:warn_bad_relevance_name with
+let bad_relevance_warning =
+  CWarnings.create_warning ~name:warn_bad_relevance_name ~default:CWarnings.AsError ()
+
+let bad_relevance_msg = CWarnings.create_msg bad_relevance_warning ()
+
+let default_print_bad_relevance = function
+  | BadRelevanceCase _ -> Pp.str "Bad relevance in case annotation."
+  | BadRelevanceBinder (_, na) ->
+    Pp.(str "Bad relevance for binder " ++ Name.print (RelDecl.get_name na) ++ str ".")
+
+(* used eg in the checker *)
+let () = CWarnings.register_printer bad_relevance_msg
+    (fun (_env,b) -> default_print_bad_relevance b)
+
+let warn_bad_relevance_case ?loc env rlv case =
+  match CWarnings.warning_status bad_relevance_warning with
 | CWarnings.Disabled | CWarnings.Enabled ->
-  warn_bad_relevance ?loc (BadRelevanceCase (rlv, mkCase case))
+  CWarnings.warn bad_relevance_msg ?loc (env, BadRelevanceCase (rlv, mkCase case))
 | CWarnings.AsError ->
   error_bad_case_relevance env rlv case
 
-let warn_bad_relevance_binder ?loc env rlv bnd = match CWarnings.get_status ~name:warn_bad_relevance_name with
+let warn_bad_relevance_binder ?loc env rlv bnd =
+  match CWarnings.warning_status bad_relevance_warning with
 | CWarnings.Disabled | CWarnings.Enabled ->
-  warn_bad_relevance ?loc (BadRelevanceBinder (rlv, bnd))
+  CWarnings.warn bad_relevance_msg ?loc (env, BadRelevanceBinder (rlv, bnd))
 | CWarnings.AsError ->
   error_bad_binder_relevance env rlv bnd
 

kernel/typeops.mli

@@ -124,12 +124,15 @@ val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> t
 val warn_bad_relevance_name : string
 (** Allow the checker to make this warning into an error. *)
 
-val warn_bad_relevance_binder
-  : ?loc:Loc.t
-  -> Environ.env
-  -> Sorts.relevance
-  -> Constr.rel_declaration
-  -> unit
+val bad_relevance_warning : CWarnings.warning
+(** Also used by the pretyper to define a message which uses the evar map. *)
+
+type ('constr,'types) bad_relevance =
+| BadRelevanceBinder of Sorts.relevance * ('constr,'types) Context.Rel.Declaration.pt
+| BadRelevanceCase of Sorts.relevance * 'constr
+
+val bad_relevance_msg : (env * (constr,types) bad_relevance) CWarnings.msg
+(** Used by the higher layers to register a nicer printer than the default. *)
 
 val should_invert_case : env -> case_info -> bool
 (** We have case inversion exactly when going from irrelevant nonempty

pretyping/typing.ml

@@ -375,10 +375,13 @@ let judge_of_array env sigma u tj defj tyj =
   in
   sigma, j
 
-let warn_bad_relevance_binder ?loc env sigma rlv bnd = match CWarnings.get_status ~name:Typeops.warn_bad_relevance_name with
+let bad_relevance_msg = CWarnings.create_msg Typeops.bad_relevance_warning ()
+(* no need for default printer, pretyping is always linked with himsg in practice *)
+
+let warn_bad_relevance_binder ?loc env sigma rlv bnd =
+  match CWarnings.warning_status Typeops.bad_relevance_warning with
 | CWarnings.Disabled | CWarnings.Enabled ->
-  let bnd = Rel.Declaration.map_constr_het EConstr.Unsafe.to_constr bnd in
-  Typeops.warn_bad_relevance_binder ?loc env rlv bnd
+  CWarnings.warn bad_relevance_msg ?loc (env,sigma,Typeops.BadRelevanceBinder (rlv, bnd))
 | CWarnings.AsError ->
   CErrors.anomaly (CErrors.print (PretypeError (env, sigma, TypingError (Type_errors.BadBinderRelevance (rlv, bnd)))))
 

pretyping/typing.mli

@@ -70,3 +70,5 @@ val checked_applist : env -> evar_map -> constr -> constr list -> evar_map * con
 
 (** hack *)
 val recheck_against : Environ.env -> evar_map -> constr -> constr -> evar_map * types
+
+val bad_relevance_msg : (Environ.env * evar_map * (constr, types) Typeops.bad_relevance) CWarnings.msg

vernac/himsg.ml

@@ -808,6 +808,23 @@ let explain_bad_case_relevance env sigma rlv case =
     strbrk " but was expected to be " ++ pr_relevance sigma rlv ++
     spc () ++ str "(maybe a bugged tactic)."
 
+let explain_bad_relevance env sigma = function
+  | Typeops.BadRelevanceCase (r,c) -> explain_bad_case_relevance env sigma r c
+  | BadRelevanceBinder (r,d) -> explain_bad_binder_relevance env sigma r d
+
+let ecast_bad_relevance = let open Typeops in function
+  | BadRelevanceCase (r,c) -> BadRelevanceCase (r, EConstr.of_constr c)
+  | BadRelevanceBinder (r,d) -> BadRelevanceBinder (r, RelDecl.map_constr_het EConstr.of_constr d)
+
+let () =
+  CWarnings.register_printer Typeops.bad_relevance_msg
+    (fun (env, b) ->
+       let sigma = Evd.from_env env in
+       explain_bad_relevance env sigma (ecast_bad_relevance b))
+
+let () = CWarnings.register_printer Typing.bad_relevance_msg
+    (fun (env, sigma, b) -> explain_bad_relevance env sigma b)
+
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."