Is it possible to append two vectors using Typenats?

You've got a bigger problem. Even this (incomplete) definition won't compile:

append :: Vec m a -> Vec n a -> Vec (m + n) a
append End a = a

because the type End a doesn't look like Vec m a, and Haskell isn't going to "invert" the type family to prove m ~ 0 would "solve" this type-level equation.

You need to have append pattern match on a GADT to drive inference about m within each case. That's why pretty much any typed-length vector implementation starts with a GADT:

infixr 5 :.
data Vec n a where
  Nil :: Vec 0 a
  (:.) :: a -> Vec n a -> Vec (n+1) a

Now, when you pattern match on GADT constructors like Nil and/or :., you learn some useful information about m:

append :: Vec m a -> Vec n a -> Vec (m + n) a
append Nil v = v
append (a :. u) v = a :. append u v

Without the last line, this works fine. Pattern matching on Nil allows Haskell to infer that m ~ 0, and even Haskell can infer 0 + n ~ n without further guidance.

With the last line, Haskell chokes. The pattern match on :. allows Haskell to infer that for the typing u :: Vec n1 a, we must have m ~ n1 + 1, but it can't quite make the leap to conclude that m + n ~ (n1 + n) + 1.

You can use a plug-in to teach it. For example, the ghc-typelits-natnormalise package can do it. (I think... I didn't actually test it.)

Alternatively, you define an axiom to help Haskell along:

{-# LANGUAGE ScopedTypeVariables #-}
appendaxiom :: forall m n1 n. (m ~ n1 + 1) => m + n :~: (n1 + n) + 1
appendaxiom = unsafeCoerce Refl

and use this axiom in your definition of append. Even here, it is the pattern matching on a GADT constructor (the Refl returned by appendaxiom) that allows the required inference to take place.

append :: forall m n a. Vec m a -> Vec n a -> Vec (m + n) a
append Nil v = v
append (a :. (u :: Vec n1 a)) v =
  case appendaxiom @m @n1 @n of Refl -> a :. append u v

A complete example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
import GHC.TypeLits
import Type.Reflection
import Unsafe.Coerce
infixr 5 :.
data Vec n a where
  Nil :: Vec 0 a
  (:.) :: a -> Vec n a -> Vec (n+1) a
deriving instance (Show a) => Show (Vec n a)
appendaxiom :: forall m n1 n. (m ~ n1 + 1) => m + n :~: (n1 + n) + 1
appendaxiom = unsafeCoerce Refl
append :: forall m n a. Vec m a -> Vec n a -> Vec (m + n) a
append Nil v = v
append (a :. (u :: Vec n1 a)) v =
  case append_axiom @m @n1 @n of Refl -> a :. append u v
main :: IO ()
main = do
  print $ append ((1 :: Int) :. 2 :. 3 :. Nil) (4 :. 5 :. Nil)