[ refactor ] make Data.List.Base.[_] a pattern synonym

[jamesmckinna]

As previously discussed, eg. #3073 (comment) .

The surprising thing is that I had expected this to break a lot of code, but... it doesn't, and those breakages arise from ambiguity of the name pure, ... so one solution would be not to introduce that name for the function-associated-with-the-pattern-synonym. UPDATED the change from pure to singleton simplifies this analysis, but at the cost of a non-uniformity of concept with the use of singleton as a definition under Data.Tree.*.

Another is to do a another round of more invasive weeding of imports in favour of qualified imports, and avoiding hiding directives. Currently, this PR does the bare minimum necessary (actually, it might be sufficient to do even slightly less... ;-))

Other similar definitions presumably falls to a corresponding analysis: (thanks to @gallais for the prompt)

• Data.Vec.Base.[_]
• Data.List.NonEmpty.Base.[_]
• Data.List.Fresh.NonEmpty.[_] (is this replaceable with a pattern synonym?)
• Data.DifferenceList.Base.[_] (this probably should only be replaced by a syntax declaration)
• what else?

[gallais]

Should we also do it in other places where it's a constructor? E.g.

src/Data/List/NonEmpty/Base.agda:[_] : A → List⁺ A
src/Data/List/Fresh/NonEmpty.agda:[_] : A → List#⁺ A R

[jamesmckinna]

Yes, but doing this for List was a prologue/warm-up to such other changes, but it really needs/needed to get widespread buy-in before I would continue with 'all the others'. But I would argue for that course of action, indeed have done in discussion elsewhere.

UPDATED I just did them all, for the listlike ones at least.

[JacquesCarette]

Were we to do this, should it be one giant PR, or a bunch of smaller ones?

I am all in favour of explicit using and avoiding hiding as much as possible. Qualified imports are a different thing. I do love them, but would rather use them only when I am trying to be clear about provenance (or dealing with explicit clashes).

(On naming, I left a comment / question on #3073 about that.)

[jamesmckinna]

Re: "one giant PR" I can't find much more to change than the above task list.
I'm uncommitted as regards leaf singletons for Data.Tree.*, but for sure they could be considered, but downstream? Subject to singleton having slightly different pragmatics for key, value dictionaries...