What if you use a vector whole length is indexed by a Natural in the type signature? It would still allow permutations and such (like reverse), but not tail.

Using a dependent type system, it would actually be possible to statically ensure that map can only map, and do nothing else whatsoever, but it does become rather unwieldy.