Add (++) for List variation of All

[joelberkeley]

Description

This exists in Data for SnocList and Vect but not for List for some reason. I copied it verbatim from src

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[joelberkeley]

I don't understand why this is failing. It's unable to disambiguate between the version in src and that I've added here in base. But src isn't imported in base. More importantly, src isn't importable by clients of base afaik, so I'd like to put this in base

[mattpolzin]

Correct that src isn't imported into base, but rather the other way around: base is imported into the compiler source code -- specifically on a module by module basis, but the module of base that you added the new function to is imported upstream of the locations where ambiguity is occurring.

This is a good PR IMO, but you'll need to explicitly use the library definition of (++) in the source code to disambiguate for now. Once we release the next version of the compiler, it will be safe to bump the minimum required compiler version and remove the src version of the function in favor of the base version.

[mattpolzin]

I'd leave a note in the compiler source code about the future desire to remove the src version of the function (after the next release).

[joelberkeley]

thank @mattpolzin, is the current compiler version 0.7.0?

[mattpolzin]

is the current compiler version 0.7.0?

Yeah. And for reference, this is the sort of TODO that I'd leave for future us: https://github.com/idris-lang/Idris2/pull/3174/files#diff-458f49aa263db28859e440611f0e9e49e4cbbef7393c4215580029d938980c24L5

[joelberkeley]

all done

[mattpolzin]

You actually won't need to disambiguate where you did in the latest changes. Within base, this is the only (++) for the List.Quantifiers.All scope. You'll need to make a similar change within src (https://github.com/idris-lang/Idris2/blob/main/src/Libraries/Data/List/Quantifiers/Extra.idr#L20), though. That's where you need to indicate that the compiler code should be using Extra.(++) for now.

[buzden]

Could you please change the wording to something like "delete this function after 0.7.1 is released" because wording "next release after 0.7.0" proved to be really confusing (well, at least for me, doing cleanups). I think wording mentioning 0.7.1 is okay even if next release would be 0.8.0.

[joelberkeley]

done. All good?

[mattpolzin]

Thanks!