Merge PR #12768: Granting wish #12762: warning on duplicated catch-all pattern-matching clause with unused named variable

Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares

10 files changed, 108 insertions, 19 deletions

diff --git a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst
new file mode 100644
index 0000000000..c9e941743c
--- /dev/null
+++ b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Warning on unused variables in pattern-matching branches of
+  :n:`match` serving as catch-all branches for at least two distinct
+  patterns.
+  (`#12768 <https://github.com/coq/coq/pull/12768>`_,
+  fixes `#12762 <https://github.com/coq/coq/issues/12762>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 561262262b..3c1983ee97 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -290,6 +290,43 @@ This example emphasizes what the printing settings offer.
 
        Print snd.
 
+Conventions about unused pattern-matching variables
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Pattern-matching variables that are not used on the right-hand side of ``=>`` are
+considered the sign of a potential error. For instance, it could
+result from an undetected mispelled constant constructor. By default,
+a warning is issued in such situations.
+
+.. warn:: Unused variable @ident catches more than one case.
+
+   This indicates that an unused pattern variable :token:`ident`
+   occurs in a pattern-matching clause used to complete at least two
+   cases of the pattern-matching problem.
+
+   The warning can be deactivated by using a variable name starting
+   with ``_`` or by setting ``Set Warnings
+   "-unused-pattern-matching-variable"``.
+
+   Here is an example where the warning is activated.
+
+   .. example::
+
+      .. coqtop:: none
+
+         Set Warnings "-unused-pattern-matching-variable".
+
+      .. coqtop:: all
+
+         Definition is_zero (o : option nat) := match o with
+         | Some 0 => true
+         | x => false
+         end.
+
+      .. coqtop:: none
+
+         Set Warnings "+unused-pattern-matching-variable".
+
 Patterns
 --------
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a459229256..97218ca670 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -128,7 +128,8 @@ type 'a equation =
       rhs          : 'a rhs;
       alias_stack  : Name.t list;
       eqn_loc      : Loc.t option;
-      used         : bool ref }
+      used         : int ref;
+      catch_all_vars : Id.t CAst.t list ref }
 
 type 'a matrix = 'a equation list
 
@@ -543,11 +544,34 @@ let check_all_variables env sigma typ mat =
            error_bad_pattern ?loc env sigma cstr_sp typ)
     mat
 
+let set_pattern_catch_all_var ?loc eqn = function
+  | Name id when not (Id.Set.mem id eqn.rhs.rhs_vars) ->
+    eqn.catch_all_vars := CAst.make ?loc id :: !(eqn.catch_all_vars)
+  | _ -> ()
+
+let warn_named_multi_catch_all =
+  CWarnings.create ~name:"unused-pattern-matching-variable" ~category:"pattern-matching"
+         (fun id ->
+          strbrk "Unused variable " ++ Id.print id ++ strbrk " catches more than one case.")
+
+let wildcard_id = Id.of_string "wildcard'"
+
+let is_wildcard id =
+  Id.equal (Id.of_string (Nameops.atompart_of_id id)) wildcard_id
+
 let check_unused_pattern env eqn =
-  if not !(eqn.used) then
-    raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns)
+  match !(eqn.used) with
+  | 0 -> raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns)
+  | 1 -> ()
+  | _ ->
+    let warn {CAst.v = id; loc} =
+      (* Convention: Names starting with `_` and derivatives of Program's
+         "wildcard'" internal name deactivate the warning *)
+      if (Id.to_string id).[0] <> '_' && not (is_wildcard id)
+      then warn_named_multi_catch_all ?loc id in
+    List.iter warn !(eqn.catch_all_vars)
 
-let set_used_pattern eqn = eqn.used := true
+let set_used_pattern eqn = eqn.used := !(eqn.used) + 1
 
 let extract_rhs pb =
   match pb.mat with
@@ -1017,7 +1041,8 @@ let add_assert_false_case pb tomatch =
               it = None };
       alias_stack = Anonymous::aliasnames;
       eqn_loc = None;
-      used = ref false } ]
+      used = ref 0;
+      catch_all_vars = ref [] } ]
 
 let adjust_impossible_cases sigma pb pred tomatch submat =
   match submat with
@@ -1235,6 +1260,7 @@ let group_equations pb ind current cstrs mat =
                  let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
                  brs.(i-1) <- (args, name, rest) :: brs.(i-1)
                done;
+               set_pattern_catch_all_var ?loc:pat.CAst.loc eqn name;
                if !only_default == None then only_default := Some true
            | PatCstr (((_,i)),args,name) ->
                (* This is a regular clause *)
@@ -1602,7 +1628,8 @@ let matx_of_eqns env eqns =
     { patterns = initial_lpat;
       alias_stack = [];
       eqn_loc = loc;
-      used = ref false;
+      used = ref 0;
+      catch_all_vars = ref [];
       rhs = rhs }
   in List.map build_eqn eqns
 
@@ -1859,7 +1886,8 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
     { patterns = patl;
       alias_stack = [];
       eqn_loc = None;
-      used = ref false;
+      used = ref 0;
+      catch_all_vars = ref [];
       rhs = { rhs_env = pb_env;
               (* we assume all vars are used; in practice we discard dependent
                  vars so that the field rhs_vars is normally not used *)
@@ -1879,7 +1907,8 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
       [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl;
           alias_stack = [];
           eqn_loc = None;
-          used = ref false;
+          used = ref 0;
+          catch_all_vars = ref [];
           rhs = { rhs_env = pb_env;
                   rhs_vars = Id.Set.empty;
                   avoid_ids = avoid0;
@@ -2149,7 +2178,7 @@ let constr_of_pat env sigma arsign pat avoid =
         let name, avoid = match name with
             Name n -> name, avoid
           | Anonymous ->
-              let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
+              let id = next_ident_away wildcard_id avoid in
                 Name id, Id.Set.add id avoid
         in
         let r = Sorts.Relevant in (* TODO relevance *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 8b1ec3aba0..9a986bc14c 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -68,7 +68,8 @@ type 'a equation =
       rhs          : 'a rhs;
       alias_stack  : Name.t list;
       eqn_loc      : Loc.t option;
-      used         : bool ref }
+      used         : int ref;
+      catch_all_vars : Id.t CAst.t list ref }
 
 type 'a matrix = 'a equation list
 
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index da2fc90fc3..01564e7f25 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -178,3 +178,6 @@ match N with
 | _ => Node
 end
      : Tree -> Tree
+File "stdin", line 253, characters 4-5:
+Warning: Unused variable B catches more than one case.
+[unused-pattern-matching-variable,pattern-matching]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 262ec2b677..2d8a8b359c 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -242,3 +242,15 @@ end.
 Print stray.
 
 End Bug11231.
+
+Module Wish12762.
+
+Inductive foo := a | b | c.
+
+Definition bar (f : foo) :=
+  match f with
+  | a => 0
+  | B => 1
+  end.
+
+End Wish12762.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c3c6c96997..02f408fd85 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -139,8 +139,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | xH =>
         match m with
         | Leaf => Leaf
-        | Node Leaf o Leaf => Leaf
-        | Node l o r => Node l None r
+        | Node Leaf _ Leaf => Leaf
+        | Node l _ r => Node l None r
         end
     | xO ii =>
         match m with
diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v
index ac0323442a..144ffd59e0 100644
--- a/theories/Strings/ByteVector.v
+++ b/theories/Strings/ByteVector.v
@@ -42,7 +42,7 @@ Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) :=
 Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n :=
   match n with
   | 0 => fun _ => []
-  | S n' =>
+  | S _ =>
     fun v =>
       let (b0, v1) := uncons v in
       let (b1, v2) := uncons v1 in
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index adffa1ded4..382538875d 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -138,12 +138,12 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Fixpoint compare x y :=
     match x, y with
       | x~1, y~1 => compare x y
-      | x~1, _ => Gt
+      | _~1, _ => Gt
       | x~0, y~0 => compare x y
-      | x~0, _ => Lt
-      | 1, y~1 => Lt
+      | _~0, _ => Lt
+      | 1, _~1 => Lt
       | 1, 1 => Eq
-      | 1, y~0 => Gt
+      | 1, _~0 => Gt
     end.
 
   Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v
index fb7fbcf80b..f7a848d7a5 100644
--- a/theories/micromega/RingMicromega.v
+++ b/theories/micromega/RingMicromega.v
@@ -1122,8 +1122,8 @@ Definition simpl_cone (e:Psatz) : Psatz :=
                     end
     | PsatzMulE t1 t2 =>
       match t1 , t2 with
-        | PsatzZ      , x        => PsatzZ
-        |    x     , PsatzZ      => PsatzZ
+        | PsatzZ      , _        => PsatzZ
+        |    _     , PsatzZ      => PsatzZ
         | PsatzC c ,  PsatzC c' => PsatzC (ctimes c c')
         | PsatzC p1 , PsatzMulE (PsatzC p2)  x => PsatzMulE (PsatzC (ctimes p1 p2)) x
         | PsatzC p1 , PsatzMulE x (PsatzC p2)  => PsatzMulE (PsatzC (ctimes p1 p2)) x