Haskell中从列表创建定长Vec的相关技术疑问

1. 能否向withVec传入类id函数提取中间向量？ #

某博客实现了依赖类型向量Vec n a，并定义函数：

withVec :: [a] -> (forall n. Sing n -> Vec n a -> r) -> r

该函数可从列表生成中间向量并应用指定函数。目前发现，像sum :: Sing n -> Vec n Int -> Int这类返回普通类型的函数可以正常实现并传入，但尝试实现返回Vec n a类型的函数（类似id函数，用于提取中间向量）却始终失败，想知道是否可行。

2. 为何type-combinators包无编译时检查长度的fromList？ #

type-combinators包的Vec类型未提供从列表创建Vec n a的fromList函数。想确认是否根本无法实现编译时检查长度、从n长列表生成对应Vec n a的fromList？目前已实现运行时检查长度的版本，但希望获得编译时检查的实现。

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