[ refactor ] v2.4-admissible version of #2952

[jamesmckinna]

Cf. #2952 (comment)
NB. This is based off #2952 but without the fieldame change, so any review comments there should carry over here, mutatis mutandis...

This PR attacks the first part of #2845:

• introduces the agreed new name _≈?_ for (instances of) DecidableEquality, as an alias for the field name _≟_
• importantly does no deprecations of the latter (the proliferations of warnings needed for such a change would be prohibitive)
• continues to export the old name as public, but now uses it nowhere except to construct new Relation.Binary.Structures
• but does most of the heavy lifting of [ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence #2952 in using the new name everywhere else
• gives enough hint in the CHANGELOG as to what is to come

Further: (and this could form part of the husk of a now hollwed-out #2952 )

• plumbs in, in commented out code, the path to v3.0 deprecation of _≟_
• leaving only the actual fieldname change to make

Aim:

• the hard part of reviewing has already been done (thanks @JacquesCarette !), so hopefully this can be merged without too much controversy
• the v3.0 step in this cycle of renaming/deprecation should now be 'straightforward'
• better to get this stage done for v2.4

Comments welcome!

[jamesmckinna]

Gonna do @gallais 's trick of close and re-open to kick-start rechecking the various haskell failing versions?

[JacquesCarette]

187 files, yikes. I've put that on my next stdlib pass. I have otherwise caught up with my backlog.

[jamesmckinna]

187 files, yikes. I've put that on my next stdlib pass. I have otherwise caught up with my backlog.

No, you did the bulk of this already on #2952 this PR is based off that one but doesn't make the breaking change of fieldname...

[JacquesCarette]

Unfortunately github can't seem to see that, so is asking me to review all of them again. But now that I know, I might be able to figure out what exactly is new here.

[jamesmckinna]

Unfortunately github can't seem to see that, so is asking me to review all of them again. But now that I know, I might be able to figure out what exactly is new here.

Apologies. This doubtless down to my clumsy use of hit and GitHub. I'd had the thought that having a v2.4 version would get the worst of the use changes out of the way, (and that you'd already surveyed), and the rename+deprecate cycle proper can begin in the v3.x product line...

[Taneb]

There's a subtle issue with this change: in the definition of _∈?_, the needle is on the left of the _≟_/_≈?_, but the old version you're replacing here has the needle on the right of the _≟_. I think this is an OK change to make, and being more consistent with the rest of the library is a worthy goal, but this should be a change we're making deliberately

[gallais]

Why did we use 1 as an index in the name for the decision procedure for a non-indexed relation?

[gallais]

This is called _≡ᵇ_ in Data.Nat.Base. We should probably fix that (maybe in a different PR?)