Agda中无关投影的DISPLAY形式参数丢失问题分析

在Agda 2.6.2.2版本中引入了一个关于无关投影(irrelevant projections)与DISPLAY编译指示交互的回归问题。这个问题会影响开发者在使用记录类型和显示规则时的预期行为。

问题背景

Agda支持通过DISPLAY编译指示来自定义特定函数的显示方式。当与记录类型的投影函数结合使用时，这个功能特别有用，因为它允许开发者控制这些投影在交互式开发环境中的显示形式。

在Agda 2.6.2.2中，引入了对无关投影的支持（通过--irrelevant-projections选项启用）。无关投影是指那些返回值被标记为"无关"（使用点号前缀）的投影函数，这意味着这些值在类型检查过程中不会影响相等性判断。

问题表现

考虑以下示例代码：

{-# OPTIONS --irrelevant-projections #-}
{-# OPTIONS --show-irrelevant #-}

record Wrap (A : Set) : Set where
  field theWrapped : A

record Squash (A : Set) : Set where
  field .theSquashed : A

{-# DISPLAY Wrap.theWrapped _ = RELEVANT #-}
{-# DISPLAY Squash.theSquashed _ = IRRELEVANT #-}

postulate
  P : {A : Set} → .A → Set

当使用这些定义时，普通投影(Wrap.theWrapped)的DISPLAY规则能正确应用，显示为P (λ r → RELEVANT)。然而，无关投影(Squash.theSquashed)的DISPLAY规则却错误地显示为P IRRELEVANT，而实际上它应该显示为P (λ r → IRRELEVANT)。

技术原因

这个问题源于Agda内部处理DISPLAY规则时的参数计数逻辑。在实现中，pappToTerm函数使用手工编码的逻辑来计算参数数量，这部分代码在引入无关投影支持后没有相应更新。

具体来说，对于普通记录投影，Agda正确地识别需要添加一个参数(记录值本身)，从而生成λ抽象。但对于无关投影，相同的逻辑错误地省略了这个参数，直接使用了显示规则的右侧，而没有创建应有的函数抽象。

解决方案

修复这个问题需要更新参数计数逻辑，使其能够正确处理无关投影的情况。解决方案是确保无论投影是否标记为无关，DISPLAY规则应用时都保持一致的参数处理方式。

在修复后，无关投影的DISPLAY规则将像普通投影一样，正确地生成包含λ抽象的显示形式，保持语言特性之间的一致性。

影响范围

这个问题主要影响以下使用场景的开发者：

1. 使用--irrelevant-projections选项的项目
2. 对无关投影使用DISPLAY编译指示
3. 依赖这些显示结果进行开发或教学

对于不使用无关投影或DISPLAY编译指示的项目，这个问题不会产生任何影响。

最佳实践

开发者在使用这些高级特性时应当：

1. 明确测试DISPLAY规则是否按预期工作
2. 注意Agda版本变更可能带来的行为变化
3. 对于关键项目，考虑锁定Agda版本以避免意外行为变化

这个问题的修复确保了Agda中显示规则与语言其他特性的一致性和可预测性，为开发者提供了更可靠的开发体验。