如何对GADT实现的长度索引列表（Vec）进行过滤操作？

假设我们有一个基于GADT实现的长度索引列表，定义如下：

{-# LANGUAGE GADTs, DataKinds, KindSignatures  #-}

data Vec a (n :: Nat) where
  Nil :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Succ n)

-- 配套的Nat定义
data Nat where
  Zero :: Nat
  Succ :: Nat → Nat

我知道这种长度索引的设计能带来类型安全的head操作，也能通过相加长度索引来安全地拼接两个列表。但我现在搞不懂怎么实现它的过滤操作——我想要的是这样一个函数：

filterVec :: (a -> Bool) -> Vec a n -> Vec a m

问题在于，我没法提前知道m的具体值，因为过滤后的列表长度完全取决于原列表里的具体值，而不是它的类型。我想过先把Vec转成普通列表，用标准的filter处理后再转回去，但不知道怎么把过滤后的普通列表重新转换成带长度索引的Vec。

我试过给filterVec的调用处手动加类型注解（得自己先算出结果的长度），这样确实能跑起来，但这显然太麻烦了。

（我挺惊讶这个问题好像还没在Stackoverflow上被问过，如果我漏看了先道歉。我问了几个AI工具，它们都只是含糊地说“需要额外的类型机制”，没给出具体的方案。）

备注：内容来源于stack exchange，提问作者AntC