Complete the relocation of contrib HVect into base as All

[mattpolzin]

Description

Per discussion in https://github.com/idris-lang/Idris2/wiki/%5BLanguage%5D-Contrib-Organisation, the Data.HVect contrib module should be deprecated (or removed, I'd argue, since we can entirely replace it with base library's All and an alias).

I moved a number of functions from contrib over to base. A few of these functions changed names or argument orders but a number more were moved with no changes beyond generalizing them to work with All instead of just HVect. Where names were changed, the name changes were motivated by matching same-purpose functions in Data.Vect or Data.Vect.Elem.

This PR will cause Frex builds to fail until frex-project/idris-frex#69 is merged.

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_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[andrevidela]

The change looks good to me but I'm curious about the upgrade path for frex. Do you mean to merge both the frex PR and this one at the same time? Or should frex be pinned to an older version for a bit? Or should we make the additive change to base only without removing contrib to make the tests pass?

[mattpolzin]

Do you mean to merge both the frex PR and this one at the same time?

that was my thought since we do that with e.g. pack and it’s the easiest option.

Or should frex be pinned to an older version for a bit?

I’m not sure now that you mention it if there’s any concept of pinning for frex; I think there might be an assumption that it always works with latest Idris. We could say/document that frex targeted 0.7.0 for now, which may as well mean we comment out the unit tests in the Idris compiler.

Or should we make the additive change to base only without removing contrib to make the tests pass?

that sounds unfortunate because then we’d have half-migrated the code, created possible ambiguity errors between base/contrib code that would only exist during that interim period, and we would be dependent on Frex merging a PR before we could complete the migration, whereas I’ve not heard any feedback on the frex PR so I dont yet know if/when that PR would be merged.

[andrevidela]

I see, probably best to get someone who has merge rights on frex to greenlight this then. I think both @gallais and @ohad qualify for this

[mattpolzin]

This process has begun. Frex merged a PR that works against this branch. Once this is merged, Frex's CI will be switched back to pointing at the main branch of Idris2.