Agda 的类型检查器爆炸了

Question

以下代码旨在描述 C/C++ 类枚举，它可以占用 4 个字节，尽管它们应该包含的只是几个不同的替代方案。

open import Prelude.Bool
open import Prelude.Nat
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Numeric.Nat.Pow renaming (_^′_ to _^_)

data Enum : Set where
  makeEnum : (size : Nat) → (variants : Nat) → 
             .{{ _ : (variants < size) ≡ true }} → Enum

five : Enum
five = makeEnum (2 ^ 32) 5

data Expr : (t : Enum) → Set where
  constant : (x : Nat) → Expr five

到目前为止一切顺利。一切类型检查都很好。但是添加以下行

func : ∀ {t} → Expr t → Bool
func (constant x) = false

似乎没有做任何事情，导致类型检查器未终止并耗尽所有系统资源。

除了实例参数之外，我没有看到任何可能导致这种情况的东西，但这似乎不符合 Agda 能够解决和类型检查以下内容的事实

5<2³² : (5 < 2 ^ 32) ≡ true
5<2³² = refl

很快。那么这是怎么回事？

Answer 1

Jesper Cockx answered 提出了这个问题。事实证明这是一个编译器错误，将在下一版本的 Agda 中修复。

更新: bug已经在master分支修复。

Agda 的类型检查器爆炸了

Agda's type checker explodes

agda