Destructuring result of applying a linear function

Question

Apropos this SO answer I tried writing the following Idris 2 function:

import Data.Vect
import Data.Fin

swap : (1 i : Fin (S n)) -> (1 xs : Vect (S n) a) -> Vect (S n) a
swap FZ     (x0 :: xs) = (x0 :: xs)
swap (FS i) (x0 :: xs) = go i xs
  where
    go : Fin k -> Vect k a -> Vect (S k) a
    go FZ     (x :: xs) = x :: x0 :: xs
    go (FS i) (x :: xs) =
      let (x' :: xs') = go i xs in
      x' :: x :: xs'

data Swaps : Nat -> Type where
  Nil  : Swaps 0
  Cons : Fin (S n) -> Swaps n -> Swaps (S n)

permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
permute [] xs = xs
permute (Cons i ss) xs =
  case swap i xs of
    x' :: xs' => x' :: permute ss xs'

This definition of permute doesn't typecheck:

     While processing right hand side of permute. Sorry, I can't find any elaboration which works. All errors:
     If Main.swap: Trying to use linear name xs in non-linear context.
     
     Shuffle:29:15--29:17
      25 | 
      26 | permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
      27 | permute [] xs = xs
      28 | permute (Cons i ss) xs =
      29 |   case swap i xs of

Same when using a let-binding instead of case, and same when using a with rule.

However, if I pattern match on the xs in the second permute clause and then re-construct it in the call to swap, then it typechecks:

permute : (1 ss : Swaps n) -> (1 xs : Vect n a) -> Vect n a
permute [] xs = xs
permute (Cons i ss) (x :: xs) =
  let (x' :: xs') = swap i (x :: xs) in x' :: permute ss xs'

Is there a "deep" reason for this, or is this just an implementation limitation of (the version I have laying around of) Idris 2?