[ add ] commentary explaining the IsXRing design problem (issues #1617 and #2771)

[jamesmckinna]

So maybe this warrants a comment in the file, so that future maintainers don't end up tripping on the same issue?

Originally posted by @JacquesCarette in #2771

This PR precisely attempts to offer such commentary in Algebra.Structures, but it's not clear that this is the right place to do it, nor that the 'first' instance of the phenomenon, IsNearSemiring, is where users will find such explanation useful.

Meta-issue: when we have a substantive library-design issue such as #1617, and its resolution in #1684 , how/where should we document it beyond the comment trail on GitHub?

[JacquesCarette]

That Meta-issue why I'm keen to start on the stdlib design paper! We do have some design documentation in doc/README/Design/*.

The 'real' solution to this problem would have us pull out the Setoid over which the structures are defined as a parameter instead of the 'raw' approach we're taking now. More generally, I think support for what others are calling "displayed algebra" will become necessary. No idea if @AndrasKovacs is working on that now, but he's certainly one of the leading candidates!

[jamesmckinna]

I did look in the README.Design.* tree, and couldn't really find what I needed. But perhaps the text I've written here should be moved there? Ironically (sic), I find I increasingly don't bother to read the READMEs, and as they aren't re-generated by make test, although they are re-checked at least (?), there is the risk that their contents drifts from our current internal mental model of what is/should be going on...?

[JacquesCarette]

I'd say copied there rather than moved. There are times when redundancy is good.

[jamesmckinna]

I'll convert to DRAFT while I do the copying over to README?
UPDATED: turns out a lot more material was needed in order to be able to typecheck the Hierarchies module!
Now, I'll ping again and then we can get this off the docket provided you're both still happy.