I’m trying to write code where I transform a curried representation of a function to a function taking a Vect argument. With the function structures I’ve tried, I got stuck, because I’d need to know the Vect length or the head of the Vect before the point where I got it available. Which recursion structure can I use to make freeToVectReader compile? With my current code I get

Mismatch between: _ (implicitly bound at Program:35:7–35:48) and len (implicitly bound at Program:35:7–35:48).

module Main

import Data.Vect

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

data Reader r a = MkReader (r -> a)

runReader : Reader r a -> r -> a
runReader (MkReader f) = f

Functor (Reader r) where
    map f (MkReader g) = MkReader (f . g)

Applicative (Reader r) where
    pure x = MkReader (_ => x)
    MkReader f <*> MkReader g = MkReader (r => (f r) (g r))

Monad (Reader r) where
    MkReader f >>= g = MkReader (r => runReader (g (f r)) r)

ask : Reader r r
ask = MkReader id

local : (r -> r) -> Reader r a -> Reader r a
local f (MkReader g) = MkReader (g . f)

freeToVectReader : Free (Reader r) a -> (m : Nat ** Reader (Vect m r) a)
freeToVectReader (Pure x) = (0 ** MkReader (_ => x))
freeToVectReader (Bind f) = (_ ** do
  r :: rs <- ask
  let nextFree = runReader f r
  let (_ ** reader) = freeToVectReader nextFree
  local (const rs) reader)