idris - 没有居住参数的函数的未解决元变量

Question

我foo在下面的代码中得到了一个未解决的元变量：

namespace Funs
  data Funs : Type -> Type where
    Nil : Funs a
    (::) : {b : Type} -> (a -> List b) -> Funs (List a) -> Funs (List a)

  data FunPtr : Funs a -> Type -> Type where
    here : FunPtr ((::) {b} _ bs) b
    there : FunPtr bs b -> FunPtr (_ :: bs) b

total foo : FunPtr [] b -> Void

如何说服foo没有有效模式可匹配的 Idris？

我试过添加

foo f = ?foo

然后在 Emacs 上进行案例拆分f（只是为了看看可能会出现什么），但这只是删除了这条线，留下foo了一个未解决的元数据。

Answer 1

事实证明，我需要做的就是列举foo' 参数的所有可能模式，然后 Idris 能够一一找出它们与foo' 类型不可统一：

foo : FunPtr [] b -> Void
foo here impossible
foo (there _) impossible