能否基于依赖右折叠实现依赖左折叠？

我们先给出基础类型定义：

data Nat = Z | S Nat

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

infixr 4 :::

deriving instance Foldable (Vec n)

非依赖（严格）左折叠可以通过常规方式用非依赖右折叠定义：

foldlv' :: forall n a b. (b -> a -> b) -> b -> Vec n a -> b
foldlv' f b as = foldr go id as b
  where
    go :: a -> (b -> b) -> b -> b
    go a r !b = r (f b a)

但依赖左折叠呢？能否基于依赖右折叠来定义它？

先给出依赖右折叠的定义：

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 Nil = n
  go (x ::: xs) = c x (go xs)

我们需要的依赖左折叠目标实现（取自vec包）如下：

dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl' _ !n Nil       = 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) }

我目前尚未找到合适的实现方法，想请教是否存在可行方案？我隐约记得曾有人展示过相关实现，但无法复现。

内容的提问来源于stack exchange，提问作者dfeuer