[ 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.

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.

[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.)

[JacquesCarette]

I would much prefer singleton.