Foo.hs

-- tweaking `CLaSH.Sized.Vector.vfold` so that an initial vector can be provided/built upon


-- reusing the `Append` motive from the main `dfold` example
data Append (m :: Nat) (a :: *) (f :: TyFun Nat *) :: *
type instance Apply (Append m a) l = Vec (l + m) a

vifold :: forall k j a b . (KnownNat k, KnownNat j)
       => (forall l . SNat l -> a -> Vec (j + l) b -> Vec (j + l + 1) b)
       -> Vec j b
       -> Vec k a
       -> Vec (j + k) b
vifold f init xs = dfold (Proxy @(Append j b)) f init xs
{-# INLINE vifold #-}

{-
this works, though I'm getting complained at if I index into the accumulated
vector in my `f`:

    No instance for (KnownNat l) arising from a use of `wfun'
    Possible fix:
      add (KnownNat l) to the context of
        a type expected by the context:
          SNat l
          -> Unsigned 8 -> Vec (16 + l) Word32 -> Vec ((16 + l) + 1) Word32
-}