[ fix ] issue #2905

Author: jamesmckinna

CHANGELOG.md

@@ -32,6 +32,11 @@ Minor improvements
   properties (and their proofs). In particular, `truncate-irrelevant` is now
   deprecated, because definitionally trivial.
 
+* The function `Data.Vec.Functional.map` have marked with the `INLINE` pragma.
+  This is consistent with the inlining of `Function.Base._∘_` for which it is
+  an alias, and should be backwards compatible, but does improve the behaviour
+  of the termination checker for `Vector`-defined operations.
+
 * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.

src/Data/Vec/Functional.agda

@@ -100,6 +100,7 @@ updateAt {n = suc n} xs (suc i) f (suc j) = updateAt (tail xs) i f j
 
 map : (A → B) → ∀ {n} → Vector A n → Vector B n
 map f xs = f ∘ xs
+{-# INLINE map #-}
 
 _++_ : Vector A m → Vector A n → Vector A (m ℕ.+ n)
 _++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)