Given a standard natural-indexed vector (Vec n) provide an Applicative instance for it with n left polymorphic.
The issue is that we don't have a way of pattern matching on n, therefore we cannot implement pure/<*>. The way I addressed situations like this before was to have two Applicative instances, one for Vec Zero and one for Vec (Succ n), however I think there is a way to decouple this way of "pattern matching on types" by introducing a GADT:

data WNat n where

  WZero :: WNat Zero

  WSucc :: WNat n -> WNat (Succ n)

and a class

class WNatClass n where

  witness :: WNat n

instance WNatClass Zero where

  witness = WZero

instance (WNatClass n) => WNatClass (Succ n) where

  witness = WSucc witness

Now whenever we need to pattern match on a natural index we can just put a WNatClass restriction on it and pattern match on the automatically constructed witness.

For the Vec example:

instance (WNatClass n) => Applicative (Vec n) where
    pure = pure' witness
      where
        pure' :: WNat n -> a -> Vec n a
        pure' WZero _ = VecNil
        pure' (WSucc w) a = a ::: pure' w a
    (<*>) = app' witness
      where
        app' :: WNat n -> Vec n (a -> b) -> Vec n a -> Vec n b
        app' WZero _ _ = VecNil
        app' (WSucc w) (f ::: fs) (a ::: as) = f a ::: app' w fs as

We can also generalise this concept to any index type with PolyKinds, although I'm not 100% sure why it works in general:

class Construct (a :: k) where

  data Wit a :: *

class (Construct a) => Witness a where

  witness :: Wit a

The idea is that each instance of Construct will leave the type 'a' polymorphic and will only bind the kind 'k' and provide an indexed witness:

instance Construct (n :: Nat) where

  data Wit n where

    WZero :: Wit Zero

    WSucc :: Wit n -> Wit (Succ n)