Agda项目中关于构造子重写引发内部错误的技术分析

在Agda类型检查器的开发过程中，我们发现了一个与重写规则（rewriting）相关的内部错误问题。这个问题涉及到当开发者尝试直接使用构造子（constructor）作为重写规则时，类型检查器会触发一个__IMPOSSIBLE__错误。

问题背景

Agda的rewriting扩展允许用户通过REWRITE编译指令定义自定义的等式重写规则。通常情况下，开发者会先定义一个等式证明，然后将该证明声明为重写规则。然而在某些情况下，开发者可能希望直接将数据类型构造子声明为重写规则。

问题复现

通过以下最小化测试用例可以复现该问题：

{-# OPTIONS --rewriting #-}

data One : Set where
  ⊤ : One

data P : One → One → Set where
  m : P ⊤ ⊤

{-# BUILTIN REWRITE P #-}

p = m

{-# REWRITE p #-} -- 正常工作
{-# REWRITE m #-} -- 触发内部错误

从代码中可以看到，当通过中间定义p来声明重写规则时工作正常，但直接使用构造子m作为重写规则时会导致类型检查器抛出内部错误。

技术分析

这个问题源于Agda类型检查器的重写规则处理逻辑。在源码的Agda/TypeChecking/Rewriting.hs文件中，相关代码位于处理重写规则的部分。具体来说，类型检查器在处理构造子直接作为重写规则时，未能正确识别和处理这种情况。

该问题可能是由于提交e653bcedbf3a41a2dd20e529a50b35086e9b8023引入的回归错误。这个提交修改了重写规则的处理逻辑，但可能没有完全考虑到构造子直接作为重写规则的情况。

影响范围

这个问题不仅影响简单的自定义重写规则，还会影响Agda内置的一些重写规则。例如，以下使用内置primForceLemma的代码也会触发同样的错误：

{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Strict

{-# REWRITE primForceLemma #-}

这表明该问题具有相当的普遍性，会影响所有尝试直接使用构造子作为重写规则的情况。

解决方案

目前推荐的解决方案是避免直接使用构造子作为重写规则，而是先将其绑定到一个标识符上，然后使用该标识符作为重写规则，如示例中的p = m后使用p作为重写规则。

对于长期解决方案，Agda开发团队需要修改重写规则的处理逻辑，使其能够正确处理构造子直接作为重写规则的情况。这可能需要：

1. 在类型检查阶段增加对构造子作为重写规则的特殊处理
2. 确保重写规则的处理逻辑能够正确识别和展开构造子
3. 添加相应的测试用例以防止回归

总结

这个问题揭示了Agda重写规则实现中的一个边界情况处理不足。虽然通过间接方式可以绕过这个问题，但从语言设计的角度来看，直接使用构造子作为重写规则应该是一个合法的使用场景。这个问题的修复将提高Agda重写系统的健壮性和用户体验。

对于Agda用户来说，在当前版本中应当注意避免直接使用构造子作为重写规则，等待官方修复此问题。