如何使freeToVectReader编译？依赖对递归适配问题

我尝试编写代码，将基于Free (Reader ())实现的curried函数转换为接收Vect参数的Reader函数，但当前函数结构遇到阻碍——我需要在获取Vect长度或头部之前就得知这些信息。应使用哪种递归结构才能让freeToVectReader编译？当前代码出现如下错误：

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 ()) a -> (m : Nat ** Reader (Vect m ()) 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)

我成功编写了以下简化函数，可作为参考：

-- Nat 表示参数数量
IntFun : Nat -> Type
IntFun 0 = Int
IntFun (S n) = Int -> IntFun n

funToVectReader : {n : Nat} -> IntFun n -> Reader (Vect n Int) Int
funToVectReader f = case n of
   0 => MkReader (\[] => f)
   S k => MkReader $ \(x :: xs) : Vect (S k) Int => runReader (funToVectReader (f x)) xs

问题出在Bind分支的类型推断上：原代码中忽略了递归调用返回的Nat长度，导致类型系统无法关联外层Vect的长度（S k）和递归后内层Vect的长度（k）。需要显式跟踪长度关系，让递归调用的长度与外层长度形成明确的依赖。

修改后的freeToVectReader代码如下：

freeToVectReader : Free (Reader ()) a -> (m : Nat ** Reader (Vect m ()) a)
freeToVectReader (Pure x) = (0 ** MkReader (\[] => x))
freeToVectReader (Bind f) = 
  let nextFree = runReader f ()
      (k ** reader) = freeToVectReader nextFree
  in (S k ** MkReader $ \( () :: rs ) => runReader reader rs)

关键修改点： #

1. 显式绑定递归长度：将递归调用返回的长度绑定为k，外层直接使用S k作为Vect的长度，让类型系统明确长度的递增关系。
2. 直接构造Reader：避免使用do语法带来的模糊性，直接用MkReader构造函数处理Vect的模式匹配——外层Vect是() :: rs（对应长度S k），内层将rs（长度k）传递给递归得到的reader。

这样修改后，类型系统能够准确跟踪Vect的长度，解决了原有的类型不匹配问题。

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