为什么Agda typechecker在该程序上崩溃

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

但是，尝试通过示例匹配定义示例之外的函数会导致编译器崩溃

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

当我将此功能添加到文件中并运行“ agda main.agda”时，agda说“ Checking main”，但从未完成运行。 Agda中的类型检查不是应该可以接受吗？

还有，有什么办法可以解决这个问题，并使测试功能可以定义？

Answer 1

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