Add a warning about abstract after being a no-op

As per https://github.com/coq/coq/pull/8064#discussion_r209875616

I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.

3 files changed, 30 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 50425c8a5d..2f7a7d42c1 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1499,6 +1499,10 @@ Numeral notations
 
        Check 90000.
 
+  .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type.
+
+    As noted above, the :n:`(abstract after @num)` directive has no
+    effect when :n:`@ident__2` lands in an :g:`option` type.
 
 .. _TacticNotation:
 
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index a097adec24..fceb0b961f 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -66,6 +66,14 @@ let warn_abstract_large_num =
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
       Printer.pr_constant (Global.env ()) f ++ strbrk ".")
 
+let warn_abstract_large_num_no_op =
+  CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
+    (fun f ->
+      strbrk "The 'abstract after' directive has no effect when " ++
+      strbrk "the parsing function (" ++
+      Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++
+      strbrk "option type.")
+
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
     A bit nasty, but not critical: only used to decide when a
     number is considered as large (see warnings above). *)
@@ -468,6 +476,9 @@ let vernac_numeral_notation ty f g scope opts =
             num_ty = ty;
             warning = opts }
   in
+  (match opts, to_kind with
+   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
+   | _ -> ());
   (* TODO: un hash suffit-il ? *)
   let uid = Marshal.to_string o [] in
   let i = Notation.(
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 907ec32671..2072fbbf62 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -160,3 +160,18 @@ Module Test9.
     Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
   End with_let.
 End Test9.
+
+Module Test10.
+  (* Test that it is only a warning to add abstract after to an optional parsing function *)
+  Definition to_uint (v : unit) := Nat.to_uint 0.
+  Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Decimal.uint) := tt.
+  Delimit Scope unit_scope with unit.
+  Delimit Scope unit2_scope with unit2.
+  Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1).
+  Local Set Warnings Append "+abstract-large-number-no-op".
+  (* Check that there is actually a warning here *)
+  Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1).
+  (* Check that there is no warning here *)
+  Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
+End Test10.