{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}



import GHC.TypeNats

data Vec (n :: Nat) a where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n+1) a

data DVec (n :: Nat) a where
  DNil  :: DVec n a
  DCons :: a -> DVec n a -> DVec (n+1) a
  
deriving instance Show a => Show (DVec n a)

fromVec :: forall n m a. Vec n a -> DVec (n+m) a
fromVec Nil         = DNil
fromVec (Cons x xs) = DCons x (fromVec @(n-1) @m xs)

main = do
  print (DCons 1 (DCons 2 DNil)        :: DVec 3 Int)
  print (fromVec (Cons 1 (Cons 2 Nil)) :: DVec 5 Int)