Prevent double definition of Ltac2 constructors inside a module; Fix #11046

4 files changed, 48 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v
new file mode 100644
index 0000000000..c73fa78473
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11046.v
@@ -0,0 +1,19 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Type t := [..].
+Ltac2 Type t ::= [A(int)].
+
+(* t cannot be extended with two constructors with the same name *)
+Fail Ltac2 Type t ::= [A(bool)].
+Fail Ltac2 Type t ::= [B | B(bool)].
+
+(* constructors cannot be shadowed in the same module *)
+Fail Ltac2 Type s := [A].
+
+(* constructors with the same name can be defined in distinct modules *)
+Module Other.
+  Ltac2 Type t ::= [A(bool)].
+End Other.
+Module YetAnother.
+  Ltac2 Type t' := [A].
+End YetAnother.
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index b8853f3755..bcc5f54505 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -410,6 +410,14 @@ let register_typedef ?(local = false) isrec types =
         in
         List.iter check_uppercase_ident cs
       in
+      let () =
+        let check_existing_ctor (id, _) =
+          let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
+          if Tac2env.mem_constructor qid
+          then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+        in
+        List.iter check_existing_ctor cs
+      in
       ()
     | CTydRec ps ->
       let same_name (id1, _, _) (id2, _, _) = Id.equal id1 id2 in
@@ -490,6 +498,21 @@ let register_open ?(local = false) qid (params, def) =
   match def with
   | CTydOpn -> ()
   | CTydAlg def ->
+    let () =
+      let same_name (id1, _) (id2, _) = Id.equal id1 id2 in
+      let () = match List.duplicates same_name def with
+        | [] -> ()
+        | (id, _) :: _ ->
+          user_err (str "Multiple definitions of the constructor " ++ Id.print id)
+      in
+      let check_existing_ctor (id, _) =
+        let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
+        if Tac2env.mem_constructor qid
+        then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+      in
+      let () = List.iter check_existing_ctor def in
+      ()
+    in
     let intern_type t =
       let tpe = CTydDef (Some t) in
       let (_, ans) = intern_typedef Id.Map.empty (params, tpe) in
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 5f9dc3798a..b0a910f10e 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -196,6 +196,11 @@ let shortest_qualid_of_constructor kn =
   let sp = KNmap.find kn tab.tab_cstr_rev in
   KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
 
+let mem_constructor qid =
+  let tab = !nametab in
+  try ignore (KnTab.locate qid tab.tab_cstr) ; true
+  with Not_found -> false
+
 let push_type vis sp kn =
   let tab = !nametab in
   let tab_type = KnTab.push vis sp kn tab.tab_type in
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 670c8735ee..effb9f705a 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -83,6 +83,7 @@ val locate_extended_all_ltac : qualid -> tacref list
 val shortest_qualid_of_ltac : tacref -> qualid
 
 val push_constructor : visibility -> full_path -> ltac_constructor -> unit
+val mem_constructor : qualid -> bool
 val locate_constructor : qualid -> ltac_constructor
 val locate_extended_all_constructor : qualid -> ltac_constructor list
 val shortest_qualid_of_constructor : ltac_constructor -> qualid