Possibility of build Length index vector without having length information at compile time

Question

So this is length index vector:

data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One
type Three = S Two

data Vec :: Nat -> * -> * where
  Nil  :: Vec Z a
  (:>) :: a -> Vec n a -> Vec (S n) a 

I am thinking how can I construct value of this vector from list

t :: [a] -> Vec n a -- but I don't know n at compile time, does it Z or S Z or so on..

So I can add extra param which have info about length of a vector:

fromList' :: SNat n -> [a] -> Maybe (Vec n a)
fromList' (SS n) (x:xs) = (x :>) <$> fromList' n xs
fromList' SZ [] = return Nil
fromList' _ _ = Nothing

data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

class KNat (n :: Nat) where kNat :: SNat n
instance KNat Z where kNat = SZ
instance KNat n => KNat (S n) where kNat = SS kNat

Now I can run in repl explicitly providing desired length:

fromList' (SS (SS (SZ))) [1,2]

Just 1:>2:>Nil

I can do so:

fromList :: KNat n => [a] -> Maybe (Vec n a)
fromList = fromList' kNat

But now to run this I must provide length info explicitly again in type signature:

fromList [1,2] :: Maybe (Vec Two Int)

Is it true that I can't rid from this extra param (or fixed type signature) carrying type length info in the source file, or another words this length info should be anyway some how fixed statically in my source file, and there is no way to extract this information from list itself (just with t :: [a] -> Vec n a) ? (because there is no types constructed at runtime and Vec type must be fixed statically before runtime starts)

Is my understanding of this situation correct?

So for example if I get lists data from user input (IO) and I expect that length of this lists must be for example only 1,2,3,4,5, the Vec type dictate to me do 5 case brunches for every length:

case (length l)
 of 1 -> dosomething1 $ fromList' (SS (SZ)) l 
 of 2 -> dosomething2 $ fromList' (SS (SS (SZ))) l
 of 3 -> dosomething3 $ fromList' (SS (SS (SS (SZ)))) l
 of 4 -> dosomething4 $ fromList' (SS (SS (SS (SS (SZ))))) l
 of 5 -> dosomething5 $ fromList' (SS (SS (SS (SS (SS (SZ)))))) l
 _ -> showError "Ops"

-- After a lot of python programming my intuition leads me to just :)
-- dosomething $ fromList l  

So I guess then I lift more info (as length in this example) to type level, type system will dictate to me pay more explicit specific static info providing?