Generic sort in problem definition leads to broken sequent

[WolframPfeifer]

Description

If a generic sort is used inside a problem definition (in a .key file), this leads to a broken sequent.

Reproducible

always

Steps to reproduce

Load a .key file containing the following:

\sorts {
    \generic S;
}

\functions {
    boolean S::test(int);
}

\problem {
    S::test(5) = TRUE
}

KeY loads the file without error message. However, in the sequent S does not occur anymore. Instead, "null" is printed. The sequent looks like this:

Expected behavior

Some context on generic sorts (that was at least not completely clear to me before a discussion with @mattulbrich): Generic sorts are placeholders that are to be instantiated with existing sorts "at verification time". They are allowed to appear in taclets (to express a family of rules), but not in the problem. The latter would result in a parameterized proof, which could be instantiated for concrete sorts (something that is possible in Isabelle for example, but not in KeY).

To avoid name clashes between the generic sorts and Java classes, the generic sorts are erased from the namespaces before starting the proof. It looks like this erasure happens before starting the proof (the resulting "null" probably stems from a toString() call where the sort object is null ...), but after parsing the problem. Thus, no error is thrown.

Additional information

The existing issues about generic sorts (#355, #720) seem to be outdated. It may be worth to investigate and close them if possible.