Fix "singleton overload" check for user lists

[Baltoli]

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¹ 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.

Footnotes

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. ↩

[Baltoli]

Related: #1278