diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 561cf1b..5d274e6 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -175,7 +175,8 @@ intercalate xs xss = concat (intersperse xs xss)
 --
 transpose ∷ SingI n ⇒ Vec (Vec a n) m → Vec (Vec a m) n
 transpose Nil = replicate Nil
-transpose (xs :- xss) = zipWith (:-) xs (transpose xss)
+transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
+  where proof = min_self (sLength xs)
 
 
 -- | 'foldl' applied to a binary operator, a starting value