Add inverse of resolve_overloads & Check types

[GeorgeR227]

With the merging of the SymbolicUtils interoperability branch into DiagrammaticEquations we want to remove the user-allowed typing of DEC operators in the Decapode. For example, a user using d₁ instead of the generic d. While this typing is still critical during the code generation phase, in order to differentiate which matrix implementations of d to use for example, for the purposes of type inference/rewriting it is increasingly adding to the overall complexity of the code without providing much benefit.

To remedy this, we should instead only work with generic operators on the user-side, so things like d₁ are no longer viewed as a valid DEC operator and only d is. Then, for code generation only, we take the operator's name and it's surrounding type information to generate its type-specific name there for implementation differentiation.

[lukem12345]

... without providing much benefit.

To clarify, annotations enforce the selection of particular versions of operators. Some DEC equations are ambiguous (there may exist multiple valid typings) in terms of which operators to use, and different versions of operators will exhibit different (non-trivial) numerical properties.

I am wary of removing features for the sake of simplifying internal code, especially when the simplifications consist of removing error checks and input validation. The usual sorts of error checks that a developer should write to help catch bugs in and verify internal logic should also be capable of handling bugs introduced in pre-processing phases, whether they came from an automated type-inference algorithm, or manual.

It sounds like another solution, which wouldn't restrict the scope of user input, is to add a check is_well_typed, which internal functions can call if it is too cumbersome to check for errors inline.

[GeorgeR227]

Yes this is true. I guess the intention here was to remove the ability for the user to do this but maybe instead we want to resolve the operator names to something that is "as generic as possible". Like in the case for d, given the type information, the d can be resolved to one and only one specific operator. So internally, it makes some sense to remove other name annotations / resolve to a canon name to simplify internal code since we're not losing information in this case. I guess what I'm getting at is this is stronger canonicalization, where not just bespoke aliases but typing info can be used to resolve to a canon name.

Currently we do not do any type inference / type checking based on specific operator types, although PR #84 could definitely fit that in scope. This is for ACSets though and on the Symbolic side we actually type even specific types the same as the general, so d_0 given a :Form1 and returning :Form2 passes but erroneously so. I agree that this kind of type checking ability should be added although on what side (ACSet/Symbolic) I'm not sure.