diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -544,10 +544,18 @@
     Conversion to vectors
 --------------------------------------------------------------------}
 
-class ToVec c n a | c -> n a where
+class ToVec c n a where
   toVec :: c -> Vec n a
 
 instance ToVec (Vec n a) n a where toVec = id
+
+instance IsNat n => ToVec [a] n a where
+  toVec = toVecL nat
+
+toVecL :: Nat n -> [a] -> Vec n a
+toVecL Zero [] = ZVec
+toVecL (Succ m) (a:as) = a :< toVecL m as
+toVecL _ _ = error "toVecL: length mismatch"
 
 {--------------------------------------------------------------------
     Misc
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.1.5
+Version:             0.1.6
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, vectors, inequality proofs