Fix "singleton overload" check for user lists (#4129)

When working on #4045, I identified a case in the C Semantics where an
overload set was flagged as being singletons (that is, that the
productions in the set were not actually overloads of one another).
Despite this warning, removing the `overload(_)` attributes broke
compilation by producing a parsing ambiguity.

It turns out that the issue was a difference between the main module and
the _disambiguation module_ produced during the inner parsing process.
The disambiguation module adds an additional production
```
Es ::= E
```
for user list sorts `Es` that subsorts the list element sort into the
list sort. This means that two productions
```
S ::= f(Es)
T ::= f(E)
```
can be overloads of one another.

However, this check was only using the overloads induced by the main
module and not those used by the disambiguation module. The fix is
simply to compute the disambiguation module[^1] and use its overloads
for the checks. Doing so requires some changes to the plumbing; the
subsorting production is previously only added when `RULE-LISTS` is
imported, but we need to short-circuit that code path in this context.

This PR includes a regression test minimised from the original example.

[^1]: I tried a cheaper fix that just checks parameters of
overload-attributed productions to see if they appear in a user list,
but this isn't sufficiently general in the case where the overload
parameter is actually a sub-/supersort of the user list element, as
happens in the C semantics.

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

@@ -1,11 +1,32 @@
 module SINGLETONOVERLOAD-SYNTAX
 endmodule
 
-module SINGLETONOVERLOAD
+module WARNS
   imports ID
 
   syntax LVal ::= L() [unused]
                 | LVal "." Id [unused, overload(_.)]
   syntax Exp  ::= LVal
                 | Exp  "." Id [unused, overload(_._)]
 endmodule
+
+module NOWARNS
+  imports BOOL
+
+  syntax Foo  ::= "foo" | "bar"
+  syntax Foos ::= List{Foo, ","}
+
+  syntax Bool ::= test(Foo)   [function, overload(test)]
+                | test(Foos)  [function, overload(test)]
+
+  rule test(foo) => true
+  rule test(bar) => false
+
+  rule test(F, Rest) => test(F) andBool test(Rest)
+  rule test(.Foos) => true
+endmodule
+
+module SINGLETONOVERLOAD
+  imports WARNS
+  imports NOWARNS
+endmodule

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

@@ -3,7 +3,6 @@
 
 import static org.kframework.Collections.*;
 import static org.kframework.definition.Constructors.*;
-import static org.kframework.kore.KORE.*;
 
 import com.google.inject.Inject;
 import java.io.File;
@@ -634,12 +633,23 @@ public void structuralChecks(
   }
 
   private void checkSingletonOverload(Module module) {
-    var withOverload = module.productions().filter(p -> p.att().contains(Att.OVERLOAD())).toSeq();
+    // When disambiguating, an extra production `Es ::= E` is added for every user list
+    // sort `Es`.
+    //
+    // This means that productions that reference a user list sort (or the child sort of
+    // one) can behave as overloads at disambiguation, even if they look like singletons
+    // from the perspective. We therefore need to use the disambiguation module to implement this
+    // check.
+    //
+    // See `RuleGrammarGenerator::getCombinedGrammarImpl`.
+    var disambMod = RuleGrammarGenerator.getCombinedGrammarImpl(module, false, false, true)._2();
+    var withOverload =
+        disambMod.productions().filter(p -> p.att().contains(Att.OVERLOAD())).toSeq();
 
     stream(withOverload)
         .forEach(
             p -> {
-              if (!module.overloads().elements().contains(p)) {
+              if (!disambMod.overloads().elements().contains(p)) {
                 kem.registerCompilerWarning(
                     KException.ExceptionType.SINGLETON_OVERLOAD,
                     errors,

kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java

@@ -167,7 +167,7 @@ public Module getExtensionModule() {
     Module extM = extensionModule;
     if (extM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extM = mods._1();
       disambModule = mods._2();
       parsingModule = mods._3();
@@ -180,7 +180,7 @@ public Module getParsingModule() {
     Module parseM = parsingModule;
     if (parseM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extensionModule = mods._1();
       disambModule = mods._2();
       parseM = mods._3();
@@ -193,7 +193,7 @@ public Module getDisambiguationModule() {
     Module disambM = disambModule;
     if (disambM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extensionModule = mods._1();
       disambM = mods._2();
       parsingModule = mods._3();

kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -333,8 +333,25 @@ public static ParseInModule getCombinedGrammar(
         partialParseDebug);
   }
 
+  /**
+   * Generate the derived extension, disambiguation and parsing modules from a user module.
+   *
+   * <p>When performing different parts of the compilation pipeline, we need to use derived modules
+   * with different properties to the user-supplied source module. This method adds additional
+   * syntax to the user module to do so.
+   *
+   * <p>TODO: analysis of the properties of these modules: K Issue #1278
+   *
+   * @param mod The user module to transform.
+   * @param isBison If true, modules with the `not-lr1` attribute will be dropped.
+   * @param forGlobalScanner If false, only the public signature of the user module is considered
+   *     (i.e. private imports are dropped).
+   * @param subsortUserLists If true, a subsorting production `Es ::= E` is added to the
+   *     disambiguation module for each user list sort `Es`.
+   * @return A tuple `(extension, disambiguation, parsing)` of derived modules.
+   */
   public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
-      Module mod, boolean isBison, boolean forGlobalScanner) {
+      Module mod, boolean isBison, boolean forGlobalScanner, boolean subsortUserLists) {
     Set<Sentence> prods = new HashSet<>();
     Set<Sentence> extensionProds = new HashSet<>();
     Set<Sentence> disambProds;
@@ -730,7 +747,7 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
       parseProds = res;
     }
 
-    if (mod.importedModuleNames().contains(RULE_LISTS)) {
+    if (mod.importedModuleNames().contains(RULE_LISTS) || subsortUserLists) {
       Set<Sentence> res = new HashSet<>();
       for (UserList ul : UserList.getLists(parseProds)) {
         Production prod1;