Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside a module

Reviewed-by: ppedrot

6 files changed, 75 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/bug_10097.v b/test-suite/bugs/closed/bug_10097.v
new file mode 100644
index 0000000000..12f2d4cc58
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10097.v
@@ -0,0 +1,14 @@
+From Ltac2 Require Import Ltac2.
+
+(* #10097 *)
+Ltac2 Type s := [X(int)].
+Fail Ltac2 Type s.
+Fail Ltac2 Type s := [].
+
+Ltac2 Type r := [..].
+Fail Ltac2 Type r := [].
+
+Module Other.
+  Ltac2 Type s.
+  Ltac2 Type r := [].
+End Other.
diff --git a/test-suite/bugs/closed/bug_10196.v b/test-suite/bugs/closed/bug_10196.v
index e2d6be56e9..d003ab323d 100644
--- a/test-suite/bugs/closed/bug_10196.v
+++ b/test-suite/bugs/closed/bug_10196.v
@@ -17,10 +17,10 @@ Fail Ltac2 Eval notUppercased2.
 
 (* And the same for open types*)
 Ltac2 Type open_type := [ .. ].
-Fail Ltac2 Type open_type ::= [ notUppercased ].
-Ltac2 Type open_type ::= [ Uppercased ].
+Fail Ltac2 Type open_type ::= [ notUppercased3 ].
+Ltac2 Type open_type ::= [ Uppercased3 ].
 
-Fail Ltac2 Eval notUppercased.
-Ltac2 Eval Uppercased.
+Fail Ltac2 Eval notUppercased3.
+Ltac2 Eval Uppercased3.
 
 Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].
diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v
new file mode 100644
index 0000000000..528cc4c8ff
--- /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 92bc49346f..bcc5f54505 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -374,6 +374,15 @@ let register_typedef ?(local = false) isrec types =
   | ({loc;v=id}, _) :: _ ->
     user_err ?loc (str "Multiple definition of the type name " ++ Id.print id)
   in
+  let () =
+    let check_existing_type ({v=id},_) =
+      let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
+      try let _ = Tac2env.locate_type qid in
+        user_err (str "Multiple definition of the type name " ++ pr_qualid qid)
+      with Not_found -> ()
+    in
+    List.iter check_existing_type types
+  in
   let check ({loc;v=id}, (params, def)) =
     let same_name {v=id1} {v=id2} = Id.equal id1 id2 in
     let () = match List.duplicates same_name params with
@@ -401,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
@@ -481,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