[ refactor ] change type of `Data.Vec.Base.{truncate|padRight}`

[jamesmckinna]

The types of these two operations (introduced in #1640 ) are too strict in their m ≤ n argument, when this could be made irrelevant:

------------------------------------------------------------------------
-- Operations involving ≤

-- Take the first 'm' elements of a vector.
truncate : .(m ≤ n) → Vec A n → Vec A m
truncate {m = zero}  _  _        = []
truncate {m = suc _} le (x ∷ xs) = x ∷ truncate (s≤s⁻¹ le) xs

-- Pad out a vector with extra elements.
padRight : .(m ≤ n) → A → Vec A m → Vec A n
padRight {n = n}     _  a []       = replicate n a
padRight {n = suc _} le a (x ∷ xs) = x ∷ padRight (s≤s⁻¹ le) a xs

A non-breaking change, because every existing call site will have the same form as now, even though the type is strictly more constrained?

So: should we make it for v2.x, in view of #2769 or wait for v3.0?

[JacquesCarette]

Maybe we'll end up with a v2.4 after all? Might be a small bump though.

[jamesmckinna]

Notwithstanding the efforts on #2769 I think this is worth doing sooner rather than later.

I realise I'm partly responsible for perpetuating the v2.x track of versions, mostly in my case because there's still plenty that can be (more or less easily) done now, despite our wish to crack on with larger scale breaking changes for v3.0... and I think this issue falls outside the v3.0 remit?

[JacquesCarette]

As long as worthwhile, not-really-breaking improvements keep coming in, we should release them.

[jamesmckinna]

See also #2785 and ... whatever we end up deciding about Data.Fin.Base.punchOut...

[jamesmckinna]

@MatthewDaggitt do you regard this (and #2787 ) as v3.0/breaking in the same way as #2790 ?

[MatthewDaggitt]

See my comment #2790. That was a mistake, and therefore, no, I don't consider this breaking 👍