Revive work on Polymorphic Sorts

[wadoon]

Introducing Sorts with Sort-Parameters.

Type of pull request

• X New feature (non-breaking change which adds functionality)
• X Breaking change (fix or feature that would cause existing functionality to change)
• X There are changes to the (Java) code
• X There are changes to the taclet rule base

[wadoon]

Support for data types:

\sorts{\generic E;} \datatypes { List<[E]> = Nil | Cons(E obj, List<[E]> tail);

Test case fails.

[mattulbrich]

There are a number of fundamental questions to be sorted out: https://github.com/KeYProject/key/wiki/Polymorphic-types-in-KeY

[sonarqubecloud[bot]]

Quality Gate failed

Failed conditions
16 New Major Issues (required ≤ 0)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE

[mattulbrich]

Discussion at Hackeython:

• Comparison with Scala's type system: All ADT definitions in our sense must be covariant (or invariant), cannot be contravariant.
• We do not want to specify type parameters with constructors (not Cons<int>(3, Nil<int)))
• implicit upcasts may be necessary, e.g. in list_of_strings.append(list_of_objects) which should return a list<Object>. Here the receiver needs to be upcast to list<object> for this to work.
• Contravariance might be needed for co-ADTs, ... perhaps
• Java type hierarchy needs still to be accommodated. perhaps have different types for the List<T>, List<? extends T> and List<? super T> (like List_extends<T>)
• The parser should be refactored to allow for < and > to be used for type arguments! (And allow that for diamond while we are at it ...)

@TudorBalan