[ design ] Should `Reasoning.Binary.Setoid setoid` be part of the public API exported by `Algebra.Properties.X`?

[jamesmckinna]

... should this be part of the API exported by Algebra.Properties.X? Do we ever invoke algebraic properties not in a context where we have access to equational reasoning wrt that algebra?

Originally posted by @jamesmckinna in #2855 (comment)

If we do this, and with #2804 in mind, we could do this right at the bottom with Algebra.Properties.Magma, and then re-export it right up through the hierarchy...

[JacquesCarette]

Interesting question. When importing Algebra.Properties.X, what are you putting in the scope? Having both tools for reasoning (over an X) as well as a bunch of properties about X does make sense. And Algebra.Properties.X are already "fat" modules, so this further broadening of the API size does not bother me so much. [Although I'll probably want to re-compose some Algebra.Properties.X from smaller pieces in the future, once findability is under control.]

[jamesmckinna]

NB. I'm not clear whether or not adding the Reasoning infrastructure would in fact be a breaking change?

[JacquesCarette]

I'd say that normally it would not be, but if doing so causes a lot of ambiguous names downstream (because now things are imported twice), then it would be.

[MatthewDaggitt]

If you exported it unopened then I don't think you'd get much savings in terms of code. If you exported it opened, I suspect that as @JacquesCarette says we would end up with a very large number of ambiguous names. Particularly, if you wanted to both open the algebraic structure of a concrete datatype (e.g. naturals) and then also wanted to perform non-standard reasoning over the structure (e.g. partial order reasoning).

[jamesmckinna]

Thanks @MatthewDaggitt I had been slowly coming to the same conclusion myself (esp. wrt the setting where you have multiple reasoning environments coexisting... such as in an algebra and in some quotient of it at the same time), so happy to close this now.
Thanks to you both for spending time thinking about it though!