typechecking - 为什么 Agda 类型检查器会在这个程序上崩溃

Question

考虑以下(无效的)Agda 代码

data Example : Example ex → Set where
  ex : Example ex

这种类型可以通过以下方式在 Agda 中有效写入，利用 Agda 的特性，允许先给值类型，然后再定义

exampleex : Set
ex' : exampleex

data Example : exampleex → Set where
  ex : Example ex'

exampleex = Example ex'
ex' = ex

这一切都编译通过，Agda 正确地知道 ex : Example ex
但是，尝试使用模式匹配在 Example 之外定义函数会导致编译器崩溃

test : (e : Example ex) → Example e → ℕ
test ex x = 0

当我将此函数添加到文件中并运行“agda main.agda”时，agda 说“正在检查 main”但从未完成运行。 Agda 中的类型检查不应该是可判定的吗？

另外，有没有办法解决这个问题并使测试功能可以定义？

Answer 1

这是 Agda 中的一个已知问题。您可以在 Agda 的 github 上 https://github.com/agda/agda/issues/1556 上找到相应的问题。 .