diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Revision history for vec
 
+## 0.4.1
+
+- Add `boring` instances
+- Add `dfoldr`, `dfoldl` and `dfoldl'`
+- Implement `Lazy.reverse` using `dfoldl`
+
 ## 0.4
 
 - Support `fin-0.2`
diff --git a/src/Data/Vec/DataFamily/SpineStrict.hs b/src/Data/Vec/DataFamily/SpineStrict.hs
--- a/src/Data/Vec/DataFamily/SpineStrict.hs
+++ b/src/Data/Vec/DataFamily/SpineStrict.hs
@@ -582,11 +582,11 @@
 last xs = getLast (N.induction1 start step) xs where
     start :: Last 'Z a
     start = Last $ \(x:::VNil) -> x
-    
+
     step :: Last m a -> Last ('S m) a
     step (Last rec) = Last $ \(_ ::: ys) -> rec ys
-    
 
+
 newtype Last n a = Last { getLast :: Vec ('S n) a -> a }
 
 -- | The elements before the 'last' of a 'Vec'.
@@ -596,7 +596,7 @@
 init xs = getInit (N.induction1 start step) xs where
     start :: Init 'Z a
     start = Init (const VNil)
-    
+
     step :: Init m a -> Init ('S m) a
     step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys
 
diff --git a/src/Data/Vec/Lazy.hs b/src/Data/Vec/Lazy.hs
--- a/src/Data/Vec/Lazy.hs
+++ b/src/Data/Vec/Lazy.hs
@@ -38,6 +38,10 @@
     init,
     -- * Reverse
     reverse,
+    -- * Dependent folds
+    dfoldr,
+    dfoldl,
+    dfoldl',
     -- * Concatenation and splitting
     (++),
     split,
@@ -84,11 +88,13 @@
 
 import Prelude
        (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
-       Ord (..), Show (..), id, seq, showParen, showString, uncurry, ($), (.), (&&), Ordering (..))
+       Ord (..), Ordering (..), Show (..), flip, id, seq, showParen, showString,
+       uncurry, ($), (&&), (.))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Control.DeepSeq     (NFData (..))
 import Control.Lens.Yocto  ((<&>))
+import Data.Boring         (Boring (..))
 import Data.Fin            (Fin (..))
 import Data.Hashable       (Hashable (..))
 import Data.List.NonEmpty  (NonEmpty (..))
@@ -97,6 +103,8 @@
 import Data.Semigroup      (Semigroup (..))
 import Data.Typeable       (Typeable)
 
+import SafeCompat (coerce)
+
 --- Instances
 import qualified Data.Foldable    as I (Foldable (..))
 import qualified Data.Traversable as I (Traversable (..))
@@ -261,6 +269,10 @@
     join  = join
 #endif
 
+-- | @since 0.4.1
+instance n ~ 'N.Z => Boring (Vec n a) where
+    boring = empty
+
 -------------------------------------------------------------------------------
 -- Data.Functor.Classes
 -------------------------------------------------------------------------------
@@ -367,7 +379,7 @@
 toList VNil       = []
 toList (x ::: xs) = x : toList xs
 
--- |  
+-- |
 --
 -- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
 -- 1 :| [2,3]
@@ -499,8 +511,52 @@
 -- @since 0.2.1
 --
 reverse :: Vec n a -> Vec n a
-reverse VNil       = VNil
-reverse (x ::: xs) = snoc (reverse xs) x
+reverse xs = unflipVec (dfoldl c (FlipVec VNil) xs)
+  where
+    c :: forall a m. FlippedVec a m -> a -> FlippedVec a ('S m)
+    c = coerce (flip (:::) :: Vec m a -> a -> Vec ('S m) a)
+
+newtype FlippedVec a n = FlipVec { unflipVec :: Vec n a }
+
+-------------------------------------------------------------------------------
+-- Indexed folds
+-------------------------------------------------------------------------------
+
+-- | Dependent right fold.
+--
+-- This could been called an indexed fold, but that name is already used.
+--
+-- @since 0.4.1
+--
+dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
+dfoldr c n = go where
+    go :: Vec m a -> f m
+    go VNil       = n
+    go (x ::: xs) = c x (go xs)
+
+-- | Dependent left fold.
+--
+-- @since 0.4.1
+--
+dfoldl :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
+dfoldl _ n VNil       = n
+dfoldl c n (x ::: xs) = unwrapSucc (dfoldl c' (WrapSucc (c n x)) xs)
+  where
+    c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
+    c' = coerce (c :: f ('S m) -> a -> f ('S ('S m)))
+
+-- | Dependent strict left fold.
+--
+-- @since 0.4.1
+--
+dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
+dfoldl' _ !n VNil       = n
+dfoldl' c !n (x ::: xs) = unwrapSucc (dfoldl' c' (WrapSucc (c n x)) xs)
+  where
+    c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
+    c' = coerce (c :: f ('S m) -> a -> f ('S ('S m)))
+
+newtype WrappedSucc f n = WrapSucc { unwrapSucc :: f ('S n) }
 
 -------------------------------------------------------------------------------
 -- Concatenation
diff --git a/src/Data/Vec/Lazy/Inline.hs b/src/Data/Vec/Lazy/Inline.hs
--- a/src/Data/Vec/Lazy/Inline.hs
+++ b/src/Data/Vec/Lazy/Inline.hs
@@ -260,11 +260,11 @@
 last xs = getLast (N.induction1 start step) xs where
     start :: Last 'Z a
     start = Last $ \(x:::VNil) -> x
-    
+
     step :: Last m a -> Last ('S m) a
     step (Last rec) = Last $ \(_ ::: ys) -> rec ys
-    
 
+
 newtype Last n a = Last { getLast :: Vec ('S n) a -> a }
 
 -- | The elements before the 'last' of a 'Vec'.
@@ -274,7 +274,7 @@
 init xs = getInit (N.induction1 start step) xs where
     start :: Init 'Z a
     start = Init (const VNil)
-    
+
     step :: Init m a -> Init ('S m) a
     step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys
 
diff --git a/src/Data/Vec/Pull.hs b/src/Data/Vec/Pull.hs
--- a/src/Data/Vec/Pull.hs
+++ b/src/Data/Vec/Pull.hs
@@ -67,6 +67,7 @@
        all, const, id, maxBound, maybe, ($), (.))
 
 import Control.Applicative (Applicative (..), (<$>))
+import Data.Boring         (Boring (..))
 import Data.Fin            (Fin (..))
 import Data.List.NonEmpty  (NonEmpty (..))
 import Data.Monoid         (Monoid (..))
@@ -114,7 +115,7 @@
 
 -- | Easily fuseable 'Vec'.
 --
--- It unpurpose don't have /bad/ (fusion-wise) instances, like 'Traversable'.
+-- It on purpose doesn't have /bad/ (fusion-wise) instances, like 'Traversable'.
 -- Generally, there aren't functions which would be __bad consumers__ or __bad producers__.
 newtype Vec n a = Vec { unVec :: Fin n -> a }
   deriving (Typeable)
@@ -187,6 +188,10 @@
     join  = join
 #endif
 
+-- | @since 0.4.1
+instance n ~ 'N.Z => Boring (Vec n a) where
+    boring = empty
+
 -------------------------------------------------------------------------------
 -- Construction
 -------------------------------------------------------------------------------
@@ -301,7 +306,7 @@
 
 -- | The last element of a 'Vec'.
 last :: forall n a. N.SNatI n => Vec ('S n) a -> a
-last (Vec v) = v maxBound 
+last (Vec v) = v maxBound
 
 -- | The elements after the 'head' of a 'Vec'.
 tail :: Vec ('S n) a -> Vec n a
diff --git a/src/SafeCompat.hs b/src/SafeCompat.hs
new file mode 100644
--- /dev/null
+++ b/src/SafeCompat.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE Trustworthy #-}
+module SafeCompat (
+    coerce,
+) where
+
+import Data.Coerce (coerce)
diff --git a/vec.cabal b/vec.cabal
--- a/vec.cabal
+++ b/vec.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               vec
-version:            0.4
+version:            0.4.1
 synopsis:           Vec: length-indexed (sized) list
 category:           Data, Dependent Types
 description:
@@ -79,6 +79,7 @@
    || ==8.8.4
    || ==8.10.4
    || ==9.0.1
+   || ==9.2.1
 
 source-repository head
   type:     git
@@ -118,28 +119,31 @@
   other-modules:
     Control.Lens.Yocto
     Data.Functor.Confusing
+    SafeCompat
 
   -- GHC boot libs
   build-depends:
-    , base          >=4.7     && <4.16
+    , base          >=4.7     && <4.17
     , deepseq       >=1.3.0.1 && <1.5
-    , transformers  >=0.3.0.0 && <0.6
+    , transformers  >=0.3.0.0 && <0.7
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.4 && <0.20
+    build-depends: semigroups >=0.18.4 && <0.21
 
   -- Ensure Data.Functor.Classes is always available
-  if impl(ghc >= 7.10)
-    build-depends: transformers >= 0.4.2.0
+  if impl(ghc >=7.10)
+    build-depends: transformers >=0.4.2.0
+
   else
-    build-depends: transformers-compat ^>=0.6.5
+    build-depends: transformers-compat ^>=0.6.5 || ^>=0.7.1
 
   -- siblings
-  build-depends:            fin ^>=0.2
+  build-depends:            fin ^>=0.2.1
 
   -- other dependencies
   build-depends:
-    , hashable             >=1.2.7.0 && <1.4
+    , boring               ^>=0.2
+    , hashable             >=1.2.7.0 && <1.5
     , indexed-traversable  ^>=0.1.1
     , QuickCheck           ^>=2.14.2
 
@@ -150,7 +154,7 @@
       build-depends: adjunctions ^>=4.4
 
   if flag(semigroupoids)
-    build-depends: semigroupoids >=5.3.5 && <5.4
+    build-depends: semigroupoids ^>=5.3.5
 
   other-extensions:
     CPP