idris - 这是 Idris 完整性检查器的限制，还是我遗漏了什么？

Question

Idris 声称以下代码并不完整:

data Foo = Bar (Maybe Foo)

foos : Foo -> List Foo
foos (Bar (Just foo)) = foo :: (foos foo)
foos (Bar Nothing) = Nil

我可以做

foos t@(Bar (Just foo)) = foo :: foos (assert_smaller t foo)

但这似乎是不必要的。显然，我创建的第一个 Foo 必须构造为 Bar Nothing，后续构造只能以相同的方式或从现有项构造，因此这应该始终终止。

是否有一些类似的情况无法确定整体性，或者 Idris 还不能处理这种情况？

Answer 1

你是对的。 Idris 还不能处理这种情况。