Refactor "unique overloads" check (#4127)

Previously, this check relied on identifying when a set of overloads
with the same key had multiple greatest / least elements. This is too
strong in the presence of Y-shaped overload sets; the solution is
instead to check that all the productions that share an overload key are
in the same connected component of the overload POSet.[^1]

Fixes an issue in the WASM semantics
(https://github.com/runtimeverification/wasm-semantics/blob/master/wasm.md?plain=1#L62-L65)
reported by @virgil-serbanuta, where a spurious warning was being
generated:
https://runtimeverification.slack.com/archives/C7E701MFG/p1711124927666709

The PR includes a reproduction of Virgil's issue, which breaks with K
`6.3.58` and is fixed by this change.

[^1]: Except for user lists, which must partition into precisely two
connected components: one for the cons case and one for the terminator.

k-distribution/tests/regression-new/checkWarns/nonUniqueOverload.k

@@ -11,8 +11,28 @@ module WARNS
   syntax Foo2 ::= "foo" Foo2 Foo2 [overload(foo), unused]
 endmodule
 
+module WASM-REPRO
+    syntax EmptyStmt
+
+    syntax Instr ::= EmptyStmt
+    syntax Defn  ::= EmptyStmt
+    syntax Stmt  ::= Instr | Defn
+ // -----------------------------
+
+    syntax EmptyStmts ::= List{EmptyStmt , ""} [overload(listStmt), terminator-symbol(".List{\"listStmt\"}"), unused]
+    syntax Instrs     ::= List{Instr     , ""} [overload(listStmt), unused]
+    syntax Defns      ::= List{Defn      , ""} [overload(listStmt), unused]
+    syntax Stmts      ::= List{Stmt      , ""} [overload(listStmt), unused]
+ // -------------------------------------------------------------
+
+    syntax Instrs ::= EmptyStmts
+    syntax Defns  ::= EmptyStmts
+    syntax Stmts  ::= Instrs | Defns
+endmodule
+
 module NOWARNS
   imports DOMAINS
+  imports WASM-REPRO
 
   syntax Exp  ::= Int | Id
 

kernel/src/main/java/org/kframework/kompile/Kompile.java

@@ -650,21 +650,29 @@ private void checkSingletonOverload(Module module) {
   }
 
   private void checkDuplicateOverloads(Module module) {
-    // Collect the set of productions that are the greatest element of an overload set, grouped
-    // by their `overload(_)` key. If any key has multiple greatest elements, then two overload sets
-    // are using the same key. This is not ambiguous from the point of view of the compiler, but may
-    // be confusing to users.
-    var partialOrderHeads =
-        module.overloads().relations().keySet().stream()
+    // Group the overloaded productions in this module by their `overload(_)` attribute, then
+    // examine each group to see if the elements in that group are connected. If elements with the
+    // same attribute are not in the same connected component, then we have two disjoint overload
+    // sets with the same name, which is potentially confusing to the user.
+    var attributeGroups =
+        module.overloads().elements().stream()
             .filter(p -> p.att().contains(Att.OVERLOAD()))
-            .collect(Collectors.groupingBy(p -> p.att().get(Att.OVERLOAD())));
-
-    partialOrderHeads.forEach(
-        (key, prods) -> {
-          var userList =
-              prods.size() == 2 && prods.stream().allMatch(p -> p.att().contains(Att.USER_LIST()));
-          if (prods.size() > 1 && !userList) {
-            for (Production prod : prods) {
+            .collect(Collectors.groupingBy(p -> p.att().get(Att.OVERLOAD())))
+            .values();
+
+    attributeGroups.forEach(
+        ps -> {
+          var userList = ps.stream().allMatch(p -> p.att().contains(Att.USER_LIST()));
+
+          var groups =
+              ps.stream()
+                  .collect(Collectors.groupingBy(module.overloads().connectedComponents()::get));
+
+          if (groups.size() > (userList ? 2 : 1)) {
+            for (var g : groups.values()) {
+              assert !g.isEmpty();
+              var prod = g.get(0);
+              var key = prod.att().get(Att.OVERLOAD());
               kem.registerCompilerWarning(
                   KException.ExceptionType.DUPLICATE_OVERLOAD,
                   errors,