Check for repeated name of module and module types

CHANGES.md

@@ -7,6 +7,10 @@
 
 ## Improved
 
+- Check for repeated name of module and module types
+  [\#444](https://github.com/ocaml-gospel/gospel/pull/444)
+- Fix bug in creation of fresh type variables
+  [\#435](https://github.com/ocaml-gospel/gospel/pull/435)
 - Fix typing of pattern with inlined record
   [\#429](https://github.com/ocaml-gospel/gospel/pull/429)
 - Remove support for the record update syntax
@@ -46,8 +50,6 @@
 
 ## Internals
 
-- Fix bug in creation of fresh type variables
-  [\#435](https://github.com/ocaml-gospel/gospel/pull/435)
 - Fix premature parsing of specification keywords in the preprocessor.
   [\#394](https://github.com/ocaml-gospel/gospel/pull/394)
 - Fix `ls_name` of `unit` logical symbol to be `()`

src/tmodule.ml

@@ -75,8 +75,6 @@ let ns_add_xs ~allow_duplicate ns s xs =
   in
   { ns with ns_xs }
 
-(* FIXME: Adding multiple modules with the same name to the export should not be
-   allowed either. *)
 let ns_add_ns ~allow_duplicate:_ ns s new_ns =
   { ns with ns_ns = Mstr.add s new_ns ns.ns_ns }
 
@@ -107,6 +105,7 @@ let ns_find_xs ns s = ns_find (fun ns -> ns.ns_xs) ns s
 let ns_find_ns ns s = ns_find (fun ns -> ns.ns_ns) ns s
 let ns_find_tns ns s = ns_find (fun ns -> ns.ns_tns) ns s
 let ns_exists_ns ns s = Mstr.mem s ns.ns_ns
+let ns_exists_tns ns s = Mstr.mem s ns.ns_tns
 
 let rec ns_rm_ts ns = function
   | [] -> assert false

src/typing.ml

@@ -1469,6 +1469,8 @@ and process_modtype path penv muc umty =
 
 and process_mod path penv loc m muc =
   let nm = Option.value ~default:"_" m.mdname.txt in
+  (if ns_exists_ns (get_top_import muc) nm then
+     W.(error ~loc (Repeated_name (`Module_def, nm))));
   let muc = open_module muc nm in
   let muc, mty = process_modtype (path @ [ nm ]) penv muc m.mdtype in
   let decl =
@@ -1483,6 +1485,8 @@ and process_mod path penv loc m muc =
 
 and process_modtype_decl path penv loc decl muc =
   let nm = decl.mtdname.txt in
+  (if ns_exists_tns (get_top_import muc) nm then
+     W.(error ~loc (Repeated_name (`Module_type, nm))));
   let muc = open_module muc nm in
   let md_mty = Option.map (process_modtype path penv muc) decl.mtdtype in
   let muc, mty =

src/warnings.ml

@@ -37,6 +37,7 @@ type kind =
   | Pattern_redundant of string
   | Predicate_symbol_expected of string
   | Public_type_invariant of string
+  | Repeated_name of ([ `Module_def | `Module_type ] * string)
   | Return_unit_without_modifies of string
   | Symbol_not_found of string list
   | Syntax_error
@@ -147,6 +148,12 @@ let pp_kind ppf = function
         p
   | Predicate_symbol_expected s -> pf ppf "Not a predicate symbol: %s" s
   | Public_type_invariant t -> pf ppf "Invariant on public type %s" t
+  | Repeated_name (k, m) ->
+      pf ppf
+        "Multiple definition of the %s name %s.@\n\
+         Names must be unique in a given signature"
+        (match k with `Module_def -> "module" | `Module_type -> "module type")
+        m
   | Return_unit_without_modifies f ->
       pf ppf
         "The function %s returns unit@ but its specifications does not contain \

test/typechecker/dune.inc

@@ -775,6 +775,50 @@
    ; Syntax sanity check
    (run ocamlc -c %{dep:labeled_arg8.mli}))))
 
+(rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe))
+ (targets multiple_module_definition.gospel)
+ (action
+  (with-outputs-to multiple_module_definition.mli.output
+   (run %{checker} %{dep:multiple_module_definition.mli}))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff multiple_module_definition.mli multiple_module_definition.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (with-accepted-exit-codes 2
+    (run ocamlc -c %{dep:multiple_module_definition.mli})))))
+
+(rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe))
+ (targets multiple_module_type.gospel)
+ (action
+  (with-outputs-to multiple_module_type.mli.output
+   (run %{checker} %{dep:multiple_module_type.mli}))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff multiple_module_type.mli multiple_module_type.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (with-accepted-exit-codes 2
+    (run ocamlc -c %{dep:multiple_module_type.mli})))))
+
 (rule
  (deps
   %{bin:gospel}

test/typechecker/dune_gen.options

@@ -7,3 +7,7 @@ type_arity3.mli
 2
 type_arity5.mli
 2
+multiple_module_definition.mli
+2
+multiple_module_type.mli
+2

test/typechecker/multiple_module_definition.mli

@@ -0,0 +1,9 @@
+module M : sig end
+module M : sig end
+(* {gospel_expected|
+   [125] File "multiple_module_definition.mli", line 2, characters 0-18:
+         2 | module M : sig end
+             ^^^^^^^^^^^^^^^^^^
+         Error: Multiple definition of the module name M.
+                Names must be unique in a given signature.
+   |gospel_expected} *)

test/typechecker/multiple_module_type.mli

@@ -0,0 +1,9 @@
+module type S = sig end
+module type S = sig end
+(* {gospel_expected|
+   [125] File "multiple_module_type.mli", line 2, characters 0-23:
+         2 | module type S = sig end
+             ^^^^^^^^^^^^^^^^^^^^^^^
+         Error: Multiple definition of the module type name S.
+                Names must be unique in a given signature.
+   |gospel_expected} *)