[ add ] Data.List.Base.foldMap and refactor

[jamesmckinna]

Fix the remaining (second and third) items in #3016 in line with my most recent comment on #2553

DONE:

• fix up metavariables so that foldMap-congruent typechecks
• fix up definitions so that foldr-congruent become an instance of foldMap-congruent

NB. does not yet refactor/redefine definitions in Data.Bool.ListAction etc. for the time being!

[jamesmckinna]

Thanks @JacquesCarette for continuing to comment on a DRAFT.
I think that this ready for review, although the Foldable proofs are definitely a lot gnarlier than I might have hoped, esp. wrt rewrite steps, but I just can't face doing more work on them now. Suggest that they be improved in a downstream PR, once it's (perhaps) a bit clearer how best to proceed.

Everything typechecks, but I have the feeling that the new definitions and properties are all still at present ... suboptimal. Certainly when trying to apply them to the intended refactorings of Data.Bool.ListAction etc. Sigh.

[jamesmckinna]

Everything typechecks, but I just have the feeling that the new definitions and properties are all still at present suboptimal... so maybe let this one lie for a bit before pursuing further?

[jamesmckinna]

I've taken #3016 off the docket as being fixed by this PR, because there's currently no refactoring to allow eg and-++ simply to be derived as an instance of the foldMap homomorphism theorem etc.... TODO!

[JacquesCarette]

Indeed, I would want to have all those proofs be properly equational. And some of the new reasoning combinators can be used to shorten some of the proofs you do have.

[jamesmckinna]

Thanks @gallais for the approval, but I do think that various things should be tidied up, even if the refactoring of Data.*.ListAction should wait for a downstream PR... and I haven't had the energy in the last few days to return to this one, and not quite sure when I can switch threads to do so.