Would it be possible for this type to be inferred?

ghci.lhs

> :set -XGADTs -XDataKinds
> data Nat = Z | S Nat
> data Vect n a where { Nil :: Vect 'Z a; (:-) :: a -> Vect n a -> Vect ('S n) a }
> :t () :- Nil
() :- Nil :: Vect ('S 'Z) ()
> :t \(a :- Nil) -> a

<interactive>:1:16:
    Couldn't match expected type `r' with actual type `t1'
      `r' is untouchable
        inside the constraints (n ~ 'Z)
        bound by a pattern with constructor
                   Nil :: forall a. Vect 'Z a,
                 in a lambda abstraction
        at <interactive>:1:8-10
      `r' is a rigid type variable bound by
          the inferred type of it :: Vect t t1 -> r at <interactive>:1:1
      `t1' is a rigid type variable bound by
           the inferred type of it :: Vect t t1 -> r at <interactive>:1:1
    Possible fix: add a type signature for `it'
    Relevant bindings include a :: t1 (bound at <interactive>:1:3)
    In the expression: a
    In the expression: \ (a :- Nil) -> a
> :t (\(a :- Nil) -> a) :: Vect ('S 'Z) a -> a
(\(a :- Nil) -> a) :: Vect ('S 'Z) a -> a :: Vect ('S 'Z) a -> a