Merge PR #18005: Fixes #18004: linearity check before inner disjuncti…

…ve patterns

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

doc/changelog/02-specification-language/17857-master+fix17854-too-late-duplicate-var-check-pattern-matching.rst

@@ -1,5 +1,5 @@
 - **Fixed:**
   Anomaly in the presence of duplicate variables within a disjunctive pattern
-  (`#17857 <https://github.com/coq/coq/pull/17857>`_,
-  fixes `#17854 <https://github.com/coq/coq/issues/17854>`_,
+  (`#17857 <https://github.com/coq/coq/pull/17857>`_ and `#18005 <https://github.com/coq/coq/pull/18005>`_,
+  fixes `#17854 <https://github.com/coq/coq/issues/17854>`_ and `#18004 <https://github.com/coq/coq/issues/18004>`_,
   by Hugo Herbelin).

interp/constrintern.ml

@@ -1476,10 +1476,9 @@ let rec adjust_to_down l l' default =
 let loc_of_multiple_pattern pl =
  Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl))
 
-let check_linearity mpl ids =
+let check_linearity loc ids =
   match List.duplicates (fun id1 id2 -> Id.equal id1.v id2.v) ids with
   | id::_ ->
-      let loc = loc_of_multiple_pattern mpl in
       Loc.raise ?loc (InternalizationError (NonLinearPattern id.v))
   | [] ->
       ()
@@ -1970,6 +1969,7 @@ let rec intern_pat genv ntnvars aliases pat =
       let pl' = List.map (intern_pat genv ntnvars aliases) pl in
       let (idsl,pl') = List.split pl' in
       let ids = List.hd idsl in
+      List.iter2 check_linearity (List.map (fun x -> x.CAst.loc) pl) idsl;
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
@@ -2422,7 +2422,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     let mpl' = List.map (intern_multiple_pattern env n) mpl in
     let (idsl,mpl') = List.split mpl' in
     let ids = List.hd idsl in
-    List.iter2 check_linearity mpl idsl;
+    List.iter2 check_linearity (List.map loc_of_multiple_pattern mpl) idsl;
     check_or_pat_variables loc ids (List.tl idsl);
     (ids,List.flatten mpl')
 

test-suite/output/bug_17854.out

@@ -4,3 +4,6 @@ The variable a is bound several times in pattern.
 File "./output/bug_17854.v", line 9, characters 11-31:
 The command has indeed failed with message:
 The variable a is bound several times in pattern.
+File "./output/bug_17854.v", line 27, characters 12-21:
+The command has indeed failed with message:
+The variable n is bound several times in pattern.

test-suite/output/bug_17854.v

@@ -15,3 +15,17 @@ Definition f b :=
          | true as a as a, true as b => true
          | _, _ => false
          end.
+
+Module Bug18002.
+
+(* Non linearity to be checked first also at the level of inner
+   disjunctive patterns *)
+
+Inductive U := p :nat->nat->U.
+
+Fail Check  match p 1 2 with
+ | (p n 0 | p n (S n)) => 0
+ | _ => 1
+ end.
+
+End Bug18002.